HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem ax1ne0 7150
Description: 1 and 0 are distinct. Axiom 13 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1ne0 7172.
Assertion
Ref Expression
ax1ne0 |- 1 =/= 0

Proof of Theorem ax1ne0
StepHypRef Expression
1 1ne0sr 7087 . . . 4 |- -. 1R = 0R
2 1sr 7072 . . . . . 6 |- 1R e. R.
32elisseti 2509 . . . . 5 |- 1R e. _V
43eqresr 7128 . . . 4 |- (<.1R, 0R>. = <.0R, 0R>. <-> 1R = 0R)
51, 4mtbir 346 . . 3 |- -. <.1R, 0R>. = <.0R, 0R>.
6 df-1 7114 . . . 4 |- 1 = <.1R, 0R>.
7 df-0 7113 . . . 4 |- 0 = <.0R, 0R>.
86, 7eqeq12i 2105 . . 3 |- (1 = 0 <-> <.1R, 0R>. = <.0R, 0R>.)
95, 8mtbir 346 . 2 |- -. 1 = 0
10 df-ne 2220 . 2 |- (1 =/= 0 <-> -. 1 = 0)
119, 10mpbir 238 1 |- 1 =/= 0
Colors of variables: wff set class
Syntax hints:  -. wn 2   = wceq 1592   =/= wne 2218  <.cop 3235  R.cnr 6856  0Rc0r 6857  1Rc1r 6858  0cc0 7106  1c1 7107
This theorem is referenced by:  axlowdimlem13 14423  axlowdimlem14 14424  axlowdim1 14428
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1516  ax-6 1517  ax-7 1518  ax-gen 1519  ax-8 1596  ax-10 1597  ax-11 1598  ax-12 1599  ax-13 1600  ax-14 1601  ax-17 1608  ax-9 1620  ax-4 1626  ax-16 1803  ax-ext 2074  ax-rep 3599  ax-sep 3609  ax-nul 3619  ax-pow 3655  ax-pr 3679  ax-un 3947  ax-inf2 6137
This theorem depends on definitions:  df-bi 210  df-or 419  df-an 420  df-3or 1038  df-3an 1039  df-ex 1521  df-sb 1765  df-eu 1992  df-mo 1993  df-clab 2080  df-cleq 2085  df-clel 2088  df-ne 2220  df-ral 2314  df-rex 2315  df-reu 2316  df-rab 2317  df-v 2501  df-sbc 2671  df-csb 2745  df-dif 2804  df-un 2806  df-in 2808  df-ss 2810  df-pss 2812  df-nul 3066  df-if 3166  df-pw 3222  df-sn 3237  df-pr 3238  df-tp 3240  df-op 3241  df-uni 3365  df-int 3399  df-iun 3437  df-br 3510  df-opab 3568  df-tr 3583  df-eprel 3762  df-id 3765  df-po 3770  df-so 3782  df-fr 3800  df-we 3816  df-ord 3832  df-on 3833  df-lim 3834  df-suc 3835  df-om 4104  df-xp 4151  df-rel 4152  df-cnv 4153  df-co 4154  df-dm 4155  df-rn 4156  df-res 4157  df-ima 4158  df-fun 4159  df-fn 4160  df-f 4161  df-fv 4165  df-opr 5069  df-oprab 5070  df-mpt 5202  df-mpt2 5203  df-1st 5268  df-2nd 5269  df-rdg 5460  df-1o 5500  df-oadd 5504  df-omul 5505  df-er 5637  df-ec 5639  df-qs 5642  df-ni 6863  df-pli 6864  df-mi 6865  df-lti 6866  df-plpq 6899  df-mpq 6900  df-ltpq 6901  df-enq 6902  df-nq 6903  df-erq 6904  df-plq 6905  df-mq 6906  df-rq 6907  df-ltnq 6908  df-1nq 6909  df-np 6973  df-1p 6974  df-plp 6975  df-ltp 6977  df-enr 7049  df-nr 7050  df-ltr 7053  df-0r 7054  df-1r 7055  df-0 7113  df-1 7114
Copyright terms: Public domain