ax-1ne0 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ax-1ne0		Structured version Visualization version GIF version

Axiom ax-1ne0 11201

Description: 1 and 0 are distinct. Axiom 13 of 22 for real and complex numbers, justified by Theorem ax1ne0 11177. (Contributed by NM, 29-Jan-1995.)

**Assertion**
Ref	Expression
ax-1ne0	⊢ 1 ≠ 0

**Detailed syntax breakdown of Axiom ax-1ne0**
Step	Hyp	Ref	Expression
1		c1 11133	. 2 class 1
2		cc0 11132	. 2 class 0
3	1, 2	wne 2935	1 wff 1 ≠ 0

Colors of variables: wff setvar class

This axiom is referenced by: elimne0 11228 1re 11238 mul02lem2 11415 addrid 11418 ine0 11673 0lt1 11760 recne0 11909 div1 11927 recdiv 11944 divdiv1 11949 divdiv2 11950 recgt0ii 12144 nnne0 12270 0ne1 12307 neg1ne0 12352 expcl2lem 14064 expclzlem 14074 m1expcl2 14076 1exp 14082 hashrabsn1 14359 relexp1g 14999 geo2sum2 15846 geoihalfsum 15854 fprodntriv 15912 prod0 15913 prod1 15914 fprodn0 15949 fprodn0f 15961 efne0 16067 tan0 16121 m1exp1 16346 divalg 16373 gcd1 16496 rpdvds 16624 m1dvdsndvds 16760 pcpre1 16804 pc1 16817 pcrec 16820 pcid 16835 m1expaddsub 19446 cndrng 21319 cndrngOLD 21320 cnmgpid 21355 gzrngunitlem 21358 gzrngunit 21359 zringnzr 21379 zringunit 21385 cnmsgnsubg 21502 cnmsgngrp 21504 psgninv 21507 mvrf1 21921 pmatcollpw3fi1lem1 22681 dscmet 24474 xrhmeo 24864 clmopfne 25016 itg11 25613 ply1remlem 26092 dgrid 26192 plyrem 26233 facth 26234 fta1lem 26235 vieta1lem1 26238 vieta1lem2 26239 vieta1 26240 qaa 26251 iaa 26253 coseq00topi 26430 logneg2 26542 logtayl2 26589 1cxp 26599 cxpeq0 26605 logb1 26694 logbmpt 26713 ang180lem4 26737 ang180lem5 26738 isosctrlem2 26744 isosctrlem3 26745 angpined 26755 dcubic2 26769 dcubic 26771 dquartlem1 26776 atandmtan 26845 efrlim 26894 efrlimOLD 26895 mumullem2 27105 1sgm2ppw 27126 dchrn0 27176 lgsne0 27261 1lgs 27266 gausslemma2dlem0i 27290 lgseisenlem1 27301 lgseisenlem2 27302 lgsquadlem1 27306 lgsquad2lem2 27311 2lgs 27333 2sqlem7 27350 2sqlem8a 27351 2sqlem8 27352 chebbnd2 27403 chto1lb 27404 pnt2 27539 pnt 27540 qabvle 27551 qabvexp 27552 ostthlem2 27554 ostth3 27564 ostth 27565 axlowdimlem6 28751 axlowdimlem13 28758 axlowdimlem14 28759 axlowdim1 28763 usgrexmpldifpr 29064 pthdadjvtx 29537 upgr4cycl4dv4e 29988 konigsberglem1 30055 frgrreggt1 30196 norm1exi 31053 kbpj 31759 largei 32070 ccfldextdgrr 33346 xrge0iif1 33529 ind1a 33628 cntnevol 33837 ballotlemii 34113 sgn0bi 34157 plymulx0 34169 signswch 34183 signstfvcl 34195 indispconn 34834 poimirlem23 37105 efne0d 41880 remulinvcom 41959 sn-0lt1 41989 0dioph 42170 pell1234qrne0 42245 expgrowth 43744 binomcxplemradcnv 43761 xrralrecnnge 44744 iooiinioc 44913 stoweidlem13 45373 wallispi2lem1 45431 dirkertrigeq 45461 fourierdlem30 45497 fourierdlem62 45528 dfodd5 46972 itcoval1 47708 line2ylem 47796 sec0 48163

W3C validator

	
		OSZAR »