![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > subeq0 | Structured version Visualization version GIF version |
Description: If the difference between two numbers is zero, they are equal. (Contributed by NM, 16-Nov-1999.) |
Ref | Expression |
---|---|
subeq0 | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | subid 10704 | . . . 4 ⊢ (𝐵 ∈ ℂ → (𝐵 − 𝐵) = 0) | |
2 | 1 | adantl 474 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐵 − 𝐵) = 0) |
3 | 2 | eqeq2d 2782 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) = (𝐵 − 𝐵) ↔ (𝐴 − 𝐵) = 0)) |
4 | subcan2 10710 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) = (𝐵 − 𝐵) ↔ 𝐴 = 𝐵)) | |
5 | 4 | 3anidm23 1401 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) = (𝐵 − 𝐵) ↔ 𝐴 = 𝐵)) |
6 | 3, 5 | bitr3d 273 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) = 0 ↔ 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 = wceq 1507 ∈ wcel 2050 (class class class)co 6974 ℂcc 10331 0cc0 10333 − cmin 10668 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2744 ax-sep 5056 ax-nul 5063 ax-pow 5115 ax-pr 5182 ax-un 7277 ax-resscn 10390 ax-1cn 10391 ax-icn 10392 ax-addcl 10393 ax-addrcl 10394 ax-mulcl 10395 ax-mulrcl 10396 ax-mulcom 10397 ax-addass 10398 ax-mulass 10399 ax-distr 10400 ax-i2m1 10401 ax-1ne0 10402 ax-1rid 10403 ax-rnegex 10404 ax-rrecex 10405 ax-cnre 10406 ax-pre-lttri 10407 ax-pre-lttrn 10408 ax-pre-ltadd 10409 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-nel 3068 df-ral 3087 df-rex 3088 df-reu 3089 df-rab 3091 df-v 3411 df-sbc 3676 df-csb 3781 df-dif 3826 df-un 3828 df-in 3830 df-ss 3837 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4709 df-br 4926 df-opab 4988 df-mpt 5005 df-id 5308 df-po 5322 df-so 5323 df-xp 5409 df-rel 5410 df-cnv 5411 df-co 5412 df-dm 5413 df-rn 5414 df-res 5415 df-ima 5416 df-iota 6149 df-fun 6187 df-fn 6188 df-f 6189 df-f1 6190 df-fo 6191 df-f1o 6192 df-fv 6193 df-riota 6935 df-ov 6977 df-oprab 6978 df-mpo 6979 df-er 8087 df-en 8305 df-dom 8306 df-sdom 8307 df-pnf 10474 df-mnf 10475 df-ltxr 10477 df-sub 10670 |
This theorem is referenced by: subeq0i 10765 subeq0d 10804 subne0d 10805 subeq0ad 10806 mulcan1g 11092 div2sub 11264 cju 11433 nn0sub 11757 addmodlteq 13127 geoserg 15079 geolim 15084 geolim2 15085 georeclim 15086 geoisum1c 15094 tanadd 15378 fzocongeq 15532 divalglem8 15609 mndodcongi 18445 odf1 18462 odf1o1 18470 cnmet 23095 iccpnfhmeo 23264 plyremlem 24608 geolim3 24643 abelthlem2 24735 abelthlem7 24741 efeq1 24826 tanregt0 24836 logtayl 24956 ang180lem1 25100 ang180lem2 25101 ang180lem3 25102 lawcos 25107 isosctrlem1 25109 isosctrlem2 25110 atandm2 25168 atandm4 25170 2efiatan 25209 tanatan 25210 dvatan 25226 mumullem2 25471 mersenne 25517 dchrsum2 25558 sumdchr2 25560 addsq2reu 25730 axcgrid 26417 axcontlem2 26466 hvmulcan2 28641 poimirlem13 34375 rencldnfilem 38842 qirropth 38930 dvconstbi 40111 isosctrlem1ALT 40716 rrx2pnedifcoorneor 44096 rrx2pnedifcoorneorr 44097 |
Copyright terms: Public domain | W3C validator |