![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > subne0d | Structured version Visualization version GIF version |
Description: Two unequal numbers have nonzero difference. (Contributed by Mario Carneiro, 1-Jan-2017.) |
Ref | Expression |
---|---|
negidd.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
pncand.2 | ⊢ (𝜑 → 𝐵 ∈ ℂ) |
subne0d.3 | ⊢ (𝜑 → 𝐴 ≠ 𝐵) |
Ref | Expression |
---|---|
subne0d | ⊢ (𝜑 → (𝐴 − 𝐵) ≠ 0) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | subne0d.3 | . 2 ⊢ (𝜑 → 𝐴 ≠ 𝐵) | |
2 | negidd.1 | . . . 4 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
3 | pncand.2 | . . . 4 ⊢ (𝜑 → 𝐵 ∈ ℂ) | |
4 | subeq0 10510 | . . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵)) | |
5 | 2, 3, 4 | syl2anc 567 | . . 3 ⊢ (𝜑 → ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵)) |
6 | 5 | necon3bid 2987 | . 2 ⊢ (𝜑 → ((𝐴 − 𝐵) ≠ 0 ↔ 𝐴 ≠ 𝐵)) |
7 | 1, 6 | mpbird 247 | 1 ⊢ (𝜑 → (𝐴 − 𝐵) ≠ 0) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 = wceq 1631 ∈ wcel 2145 ≠ wne 2943 (class class class)co 6794 ℂcc 10137 0cc0 10139 − cmin 10469 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-sep 4916 ax-nul 4924 ax-pow 4975 ax-pr 5035 ax-un 7097 ax-resscn 10196 ax-1cn 10197 ax-icn 10198 ax-addcl 10199 ax-addrcl 10200 ax-mulcl 10201 ax-mulrcl 10202 ax-mulcom 10203 ax-addass 10204 ax-mulass 10205 ax-distr 10206 ax-i2m1 10207 ax-1ne0 10208 ax-1rid 10209 ax-rnegex 10210 ax-rrecex 10211 ax-cnre 10212 ax-pre-lttri 10213 ax-pre-lttrn 10214 ax-pre-ltadd 10215 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 829 df-3or 1072 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-nel 3047 df-ral 3066 df-rex 3067 df-reu 3068 df-rab 3070 df-v 3353 df-sbc 3589 df-csb 3684 df-dif 3727 df-un 3729 df-in 3731 df-ss 3738 df-nul 4065 df-if 4227 df-pw 4300 df-sn 4318 df-pr 4320 df-op 4324 df-uni 4576 df-br 4788 df-opab 4848 df-mpt 4865 df-id 5158 df-po 5171 df-so 5172 df-xp 5256 df-rel 5257 df-cnv 5258 df-co 5259 df-dm 5260 df-rn 5261 df-res 5262 df-ima 5263 df-iota 5995 df-fun 6034 df-fn 6035 df-f 6036 df-f1 6037 df-fo 6038 df-f1o 6039 df-fv 6040 df-riota 6755 df-ov 6797 df-oprab 6798 df-mpt2 6799 df-er 7897 df-en 8111 df-dom 8112 df-sdom 8113 df-pnf 10279 df-mnf 10280 df-ltxr 10282 df-sub 10471 |
This theorem is referenced by: modsumfzodifsn 12952 abssubne0 14265 rlimuni 14490 climuni 14492 pwm1geoser 14808 evth 22979 dvlem 23881 dvconst 23901 dvid 23902 dvcnp2 23904 dvaddbr 23922 dvmulbr 23923 dvcobr 23930 dvcjbr 23933 dvrec 23939 dvcnvlem 23960 dvferm2lem 23970 taylthlem2 24349 ulmdvlem1 24375 ang180lem4 24764 ang180lem5 24765 ang180 24766 isosctrlem3 24772 isosctr 24773 ssscongptld 24774 angpieqvdlem 24777 angpieqvdlem2 24778 angpined 24779 angpieqvd 24780 chordthmlem 24781 chordthmlem2 24782 heron 24787 asinlem 24817 lgamgulmlem2 24978 lgamgulmlem3 24979 ttgcontlem1 25987 brbtwn2 26007 axcontlem8 26073 2sqmod 29989 signsvtn0 30988 unbdqndv2lem2 32839 bj-bary1lem 33498 bj-bary1lem1 33499 bj-bary1 33500 pellexlem6 37925 jm2.26lem3 38095 areaquad 38329 bcc0 39066 bccm1k 39068 abssubrp 40006 lptre2pt 40391 limclner 40402 climxrre 40501 cnrefiisplem 40574 fperdvper 40652 stoweidlem23 40758 wallispilem4 40803 wallispi 40805 wallispi2lem1 40806 wallispi2lem2 40807 wallispi2 40808 stirlinglem5 40813 fourierdlem4 40846 fourierdlem42 40884 fourierdlem74 40915 fourierdlem75 40916 fouriersw 40966 sigardiv 41571 sigarcol 41574 sharhght 41575 |
Copyright terms: Public domain | W3C validator |