HomeRelated theorems
GIF version
| Home |
Metamath Proof Explorer |
< Previous
Next >
Related theorems GIF version |
| Description: 1 and 0 are distinct. Axiom 14 of 25 for real and complex numbers, derived from ZF set theory. |
| Ref | Expression |
|---|---|
| ax1ne0 | ⊢ 1 ≠ 0 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 1ne0sr 5197 | . . . 4 ⊢ ¬ 1R = 0R | |
| 2 | 1r 5182 | . . . . . 6 ⊢ 1R ∈ R | |
| 3 | 2 | elisseti 1814 | . . . . 5 ⊢ 1R ∈ V |
| 4 | 3 | eqresr 5247 | . . . 4 ⊢ (⟨1R, 0R⟩ = ⟨0R, 0R⟩ ↔ 1R = 0R) |
| 5 | 1, 4 | mtbir 192 | . . 3 ⊢ ¬ ⟨1R, 0R⟩ = ⟨0R, 0R⟩ |
| 6 | df-1 5234 | . . . 4 ⊢ 1 = ⟨1R, 0R⟩ | |
| 7 | df-0 5233 | . . . 4 ⊢ 0 = ⟨0R, 0R⟩ | |
| 8 | 6, 7 | eqeq12i 1485 | . . 3 ⊢ (1 = 0 ↔ ⟨1R, 0R⟩ = ⟨0R, 0R⟩) |
| 9 | 5, 8 | mtbir 192 | . 2 ⊢ ¬ 1 = 0 |
| 10 | df-ne 1584 | . 2 ⊢ (1 ≠ 0 ↔ ¬ 1 = 0) | |
| 11 | 9, 10 | mpbir 190 | 1 ⊢ 1 ≠ 0 |
| Colors of variables: wff set class |
| Syntax hints: ¬ wn 2 = wceq 954 ≠ wne 1582 ⟨cop 2407 Rcnr 4985 0Rc0r 4986 1Rc1r 4987 0cc0 5226 1c1 5227 |
| This theorem is referenced by: elimne0 5308 ine0 5426 lt01 5673 mulcant2 5680 recne0z 5714 div11t 5741 recrec 5745 div1 5748 recrect 5752 recdivt 5766 divdivmult 5771 recgt0i 5790 expne0it 6539 efseq1ex 7268 erelem2 7282 efne0t 7331 dscmet 7882 ablmul 8096 mulid 8097 vcoprne 8164 efif1lem5 8684 pilog 8725 hvsubcant 8915 hvsubcan2t 8916 norm1ex 9096 kbpjt 9854 large 10167 superpos 10252 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 960 ax-gen 961 ax-8 962 ax-9 963 ax-10 964 ax-11 965 ax-12 966 ax-13 967 ax-14 968 ax-17 969 ax-4 971 ax-5o 973 ax-6o 976 ax-9o 1121 ax-10o 1138 ax-16 1208 ax-11o 1216 ax-ext 1457 ax-rep 2689 ax-sep 2699 ax-nul 2706 ax-pow 2738 ax-pr 2775 ax-un 2865 ax-inf2 4617 |
| This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 775 df-3an 776 df-ex 979 df-sb 1170 df-eu 1380 df-mo 1381 df-clab 1462 df-cleq 1467 df-clel 1470 df-ne 1584 df-ral 1646 df-rex 1647 df-reu 1648 df-rab 1649 df-v 1808 df-sbc 1938 df-csb 1998 df-dif 2045 df-un 2046 df-in 2047 df-ss 2049 df-pss 2051 df-nul 2277 df-if 2358 df-pw 2398 df-sn 2408 df-pr 2409 df-tp 2411 df-op 2412 df-uni 2500 df-int 2530 df-iun 2564 df-br 2616 df-opab 2663 df-tr 2677 df-eprel 2829 df-id 2832 df-po 2839 df-so 2849 df-fr 2916 df-we 2933 df-ord 2950 df-on 2951 df-lim 2952 df-suc 2953 df-om 3132 df-xp 3184 df-rel 3185 df-cnv 3186 df-co 3187 df-dm 3188 df-rn 3189 df-res 3190 df-ima 3191 df-fun 3192 df-fn 3193 df-f 3194 df-fv 3198 df-rdg 3934 df-opr 3967 df-oprab 3968 df-1st 4080 df-2nd 4081 df-1o 4134 df-oadd 4136 df-omul 4137 df-er 4262 df-ec 4264 df-qs 4267 df-ni 4992 df-pli 4993 df-mi 4994 df-lti 4995 df-plpq 5027 df-mpq 5028 df-enq 5029 df-nq 5030 df-plq 5031 df-mq 5032 df-rq 5033 df-ltq 5034 df-1q 5035 df-np 5078 df-1p 5079 df-plp 5080 df-ltp 5082 df-enr 5158 df-nr 5159 df-ltr 5162 df-0r 5163 df-1r 5164 df-0 5233 df-1 5234 |