Theorem ax1ne0 6797

Description: 1 and 0 are distinct. Axiom 13 of 23 for real and complex numbers, derived from ZF set theory.

Assertion

Ref	Expression
ax1ne0	|- 1 =/= 0

Proof of Theorem ax1ne0

Step	Hyp	Ref	Expression
1		1ne0sr 6723	. . . 4 |- -. 1R = 0R
2		1sr 6708	. . . . . 6 |- 1R e. R.
3	2	elisseti 2548	. . . . 5 |- 1R e. _V
4	3	eqresr 6773	. . . 4 |- (<.1R, 0R>. = <.0R, 0R>. <-> 1R = 0R)
5	1, 4	mtbir 314	. . 3 |- -. <.1R, 0R>. = <.0R, 0R>.
6		df-1 6760	. . . 4 |- 1 = <.1R, 0R>.
7		df-0 6759	. . . 4 |- 0 = <.0R, 0R>.
8	6, 7	eqeq12i 2154	. . 3 |- (1 = 0 <-> <.1R, 0R>. = <.0R, 0R>.)
9	5, 8	mtbir 314	. 2 |- -. 1 = 0
10		df-ne 2268	. 2 |- (1 =/= 0 <-> -. 1 = 0)
11	9, 10	mpbir 273	1 |- 1 =/= 0

Syntax hints:  -. wn 2   = wceq 1586   =/= wne 2266  <.cop 3240  R.cnr 6511  0Rc0r 6512  1Rc1r 6513  0cc0 6752  1c1 6753

This theorem is referenced by:  elimne0 6820  1re 6839  mul02lem2 6972  addid1 6977  ine0 7076  lt01 7204  mulcant2i 7211  recne0zi 7245  div11 7272  recreci 7276  div1i 7279  recrec 7283  recdiv 7298  divdiv1 7303  divdiv2 7304  recgt0ii 7323  expne0i 8214  efseq1ex 8966  erelem2 8980  efne0 9029  divalg 9300  dscmet 10062  ablmul 10308  mulid 10309  vcoprne 10399  efif1lem5 10959  pilog 10993  hvsubcan 11411  hvsubcan2 11412  norm1exi 11589  kbpj 12349  largei 12670  superpos 12757  divexp 16603

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929  ax-inf2 5964

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-ral 2359  df-rex 2360  df-reu 2361  df-rab 2362  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-if 3181  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-int 3401  df-iun 3438  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-id 3747  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-lim 3816  df-suc 3817  df-om 4086  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-fv 4147  df-opr 4983  df-oprab 4984  df-1st 5126  df-2nd 5127  df-rdg 5304  df-1o 5344  df-oadd 5346  df-omul 5347  df-er 5479  df-ec 5481  df-qs 5484  df-ni 6518  df-pli 6519  df-mi 6520  df-lti 6521  df-plpq 6553  df-mpq 6554  df-enq 6555  df-nq 6556  df-plq 6557  df-mq 6558  df-rq 6559  df-ltq 6560  df-1q 6561  df-np 6604  df-1p 6605  df-plp 6606  df-ltp 6608  df-enr 6684  df-nr 6685  df-ltr 6688  df-0r 6689  df-1r 6690  df-0 6759  df-1 6760

Copyright terms: Public domain