![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ltneii | Structured version Visualization version GIF version |
Description: 'Greater than' implies not equal. (Contributed by Mario Carneiro, 16-Sep-2015.) |
Ref | Expression |
---|---|
lt.1 | ⊢ 𝐴 ∈ ℝ |
ltneii.2 | ⊢ 𝐴 < 𝐵 |
Ref | Expression |
---|---|
ltneii | ⊢ 𝐴 ≠ 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lt.1 | . . 3 ⊢ 𝐴 ∈ ℝ | |
2 | ltneii.2 | . . 3 ⊢ 𝐴 < 𝐵 | |
3 | 1, 2 | gtneii 10469 | . 2 ⊢ 𝐵 ≠ 𝐴 |
4 | 3 | necomi 3054 | 1 ⊢ 𝐴 ≠ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2166 ≠ wne 3000 class class class wbr 4874 ℝcr 10252 < clt 10392 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-8 2168 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2804 ax-sep 5006 ax-nul 5014 ax-pow 5066 ax-pr 5128 ax-un 7210 ax-resscn 10310 ax-pre-lttri 10327 ax-pre-lttrn 10328 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3or 1114 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2606 df-eu 2641 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-ne 3001 df-nel 3104 df-ral 3123 df-rex 3124 df-rab 3127 df-v 3417 df-sbc 3664 df-csb 3759 df-dif 3802 df-un 3804 df-in 3806 df-ss 3813 df-nul 4146 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4660 df-br 4875 df-opab 4937 df-mpt 4954 df-id 5251 df-po 5264 df-so 5265 df-xp 5349 df-rel 5350 df-cnv 5351 df-co 5352 df-dm 5353 df-rn 5354 df-res 5355 df-ima 5356 df-iota 6087 df-fun 6126 df-fn 6127 df-f 6128 df-f1 6129 df-fo 6130 df-f1o 6131 df-fv 6132 df-er 8010 df-en 8224 df-dom 8225 df-sdom 8226 df-pnf 10394 df-mnf 10395 df-ltxr 10397 |
This theorem is referenced by: 1ne2 11567 f1oun2prg 14039 geo2sum 14979 3dvds 15430 plusgndxnmulrndx 16358 basendxnmulrndx 16359 slotsbhcdif 16434 oppchomfval 16727 oppcbas 16731 rescbas 16842 rescabs 16846 odubas 17487 opprlem 18983 rmodislmod 19288 srasca 19543 sravsca 19544 opsrbaslem 19839 cnfldfun 20119 zlmlem 20226 zlmsca 20230 znbaslem 20247 thlbas 20404 thlle 20405 matbas 20587 matplusg 20588 tuslem 22442 setsmsbas 22651 tnglem 22815 ppiub 25343 2lgslem3 25543 2lgslem4 25545 ttgval 26175 ttglem 26176 slotsbaseefdif 26294 structvtxvallem 26319 usgrexmpldifpr 26556 upgr4cycl4dv4e 27562 konigsbergiedgw 27628 konigsberglem3 27634 konigsberglem5 27636 ex-dif 27839 ex-id 27850 ex-fv 27859 ex-mod 27865 resvbas 30378 resvplusg 30379 resvmulr 30381 hlhilslem 38014 rabren3dioph 38224 xrlexaddrp 40366 fourierdlem102 41220 fourierdlem114 41232 fouriersw 41243 nnsum4primesodd 42515 nnsum4primesoddALTV 42516 zlmodzxznm 43134 2p2ne5 43441 |
Copyright terms: Public domain | W3C validator |