MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  addid1 Structured version   Visualization version   GIF version

Theorem addid1 10379
Description: 0 is an additive identity. This used to be one of our complex number axioms, until it was found to be dependent on the others. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.)
Assertion
Ref Expression
addid1 (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)

Proof of Theorem addid1
Dummy variables 𝑐 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1re 10202 . 2 1 ∈ ℝ
2 ax-rnegex 10170 . 2 (1 ∈ ℝ → ∃𝑐 ∈ ℝ (1 + 𝑐) = 0)
3 ax-1ne0 10168 . . . . . 6 1 ≠ 0
4 oveq2 6809 . . . . . . . . . 10 (𝑐 = 0 → (1 + 𝑐) = (1 + 0))
54eqeq1d 2750 . . . . . . . . 9 (𝑐 = 0 → ((1 + 𝑐) = 0 ↔ (1 + 0) = 0))
65biimpcd 239 . . . . . . . 8 ((1 + 𝑐) = 0 → (𝑐 = 0 → (1 + 0) = 0))
7 oveq2 6809 . . . . . . . . 9 ((1 + 0) = 0 → (((i · i) · (i · i)) · (1 + 0)) = (((i · i) · (i · i)) · 0))
8 ax-icn 10158 . . . . . . . . . . . . . . 15 i ∈ ℂ
98, 8mulcli 10208 . . . . . . . . . . . . . 14 (i · i) ∈ ℂ
109, 9mulcli 10208 . . . . . . . . . . . . 13 ((i · i) · (i · i)) ∈ ℂ
11 ax-1cn 10157 . . . . . . . . . . . . 13 1 ∈ ℂ
12 0cn 10195 . . . . . . . . . . . . 13 0 ∈ ℂ
1310, 11, 12adddii 10213 . . . . . . . . . . . 12 (((i · i) · (i · i)) · (1 + 0)) = ((((i · i) · (i · i)) · 1) + (((i · i) · (i · i)) · 0))
1410mulid1i 10205 . . . . . . . . . . . . 13 (((i · i) · (i · i)) · 1) = ((i · i) · (i · i))
15 mul01 10378 . . . . . . . . . . . . . . 15 (((i · i) · (i · i)) ∈ ℂ → (((i · i) · (i · i)) · 0) = 0)
1610, 15ax-mp 5 . . . . . . . . . . . . . 14 (((i · i) · (i · i)) · 0) = 0
17 ax-i2m1 10167 . . . . . . . . . . . . . 14 ((i · i) + 1) = 0
1816, 17eqtr4i 2773 . . . . . . . . . . . . 13 (((i · i) · (i · i)) · 0) = ((i · i) + 1)
1914, 18oveq12i 6813 . . . . . . . . . . . 12 ((((i · i) · (i · i)) · 1) + (((i · i) · (i · i)) · 0)) = (((i · i) · (i · i)) + ((i · i) + 1))
2013, 19eqtri 2770 . . . . . . . . . . 11 (((i · i) · (i · i)) · (1 + 0)) = (((i · i) · (i · i)) + ((i · i) + 1))
2120, 16eqeq12i 2762 . . . . . . . . . 10 ((((i · i) · (i · i)) · (1 + 0)) = (((i · i) · (i · i)) · 0) ↔ (((i · i) · (i · i)) + ((i · i) + 1)) = 0)
2210, 9, 11addassi 10211 . . . . . . . . . . . 12 ((((i · i) · (i · i)) + (i · i)) + 1) = (((i · i) · (i · i)) + ((i · i) + 1))
239mulid1i 10205 . . . . . . . . . . . . . . 15 ((i · i) · 1) = (i · i)
2423oveq2i 6812 . . . . . . . . . . . . . 14 (((i · i) · (i · i)) + ((i · i) · 1)) = (((i · i) · (i · i)) + (i · i))
259, 9, 11adddii 10213 . . . . . . . . . . . . . . 15 ((i · i) · ((i · i) + 1)) = (((i · i) · (i · i)) + ((i · i) · 1))
2617oveq2i 6812 . . . . . . . . . . . . . . . 16 ((i · i) · ((i · i) + 1)) = ((i · i) · 0)
27 mul01 10378 . . . . . . . . . . . . . . . . 17 ((i · i) ∈ ℂ → ((i · i) · 0) = 0)
289, 27ax-mp 5 . . . . . . . . . . . . . . . 16 ((i · i) · 0) = 0
2926, 28eqtri 2770 . . . . . . . . . . . . . . 15 ((i · i) · ((i · i) + 1)) = 0
3025, 29eqtr3i 2772 . . . . . . . . . . . . . 14 (((i · i) · (i · i)) + ((i · i) · 1)) = 0
3124, 30eqtr3i 2772 . . . . . . . . . . . . 13 (((i · i) · (i · i)) + (i · i)) = 0
3231oveq1i 6811 . . . . . . . . . . . 12 ((((i · i) · (i · i)) + (i · i)) + 1) = (0 + 1)
3322, 32eqtr3i 2772 . . . . . . . . . . 11 (((i · i) · (i · i)) + ((i · i) + 1)) = (0 + 1)
34 00id 10374 . . . . . . . . . . . 12 (0 + 0) = 0
3534eqcomi 2757 . . . . . . . . . . 11 0 = (0 + 0)
3633, 35eqeq12i 2762 . . . . . . . . . 10 ((((i · i) · (i · i)) + ((i · i) + 1)) = 0 ↔ (0 + 1) = (0 + 0))
37 0re 10203 . . . . . . . . . . 11 0 ∈ ℝ
38 readdcan 10373 . . . . . . . . . . 11 ((1 ∈ ℝ ∧ 0 ∈ ℝ ∧ 0 ∈ ℝ) → ((0 + 1) = (0 + 0) ↔ 1 = 0))
391, 37, 37, 38mp3an 1561 . . . . . . . . . 10 ((0 + 1) = (0 + 0) ↔ 1 = 0)
4021, 36, 393bitri 286 . . . . . . . . 9 ((((i · i) · (i · i)) · (1 + 0)) = (((i · i) · (i · i)) · 0) ↔ 1 = 0)
417, 40sylib 208 . . . . . . . 8 ((1 + 0) = 0 → 1 = 0)
426, 41syl6 35 . . . . . . 7 ((1 + 𝑐) = 0 → (𝑐 = 0 → 1 = 0))
4342necon3d 2941 . . . . . 6 ((1 + 𝑐) = 0 → (1 ≠ 0 → 𝑐 ≠ 0))
443, 43mpi 20 . . . . 5 ((1 + 𝑐) = 0 → 𝑐 ≠ 0)
45 ax-rrecex 10171 . . . . 5 ((𝑐 ∈ ℝ ∧ 𝑐 ≠ 0) → ∃𝑥 ∈ ℝ (𝑐 · 𝑥) = 1)
4644, 45sylan2 492 . . . 4 ((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) → ∃𝑥 ∈ ℝ (𝑐 · 𝑥) = 1)
47 simpr 479 . . . . . . . . . 10 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 𝐴 ∈ ℂ)
48 simplrl 819 . . . . . . . . . . 11 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 𝑥 ∈ ℝ)
4948recnd 10231 . . . . . . . . . 10 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 𝑥 ∈ ℂ)
5047, 49mulcld 10223 . . . . . . . . 9 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (𝐴 · 𝑥) ∈ ℂ)
51 simplll 815 . . . . . . . . . 10 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 𝑐 ∈ ℝ)
5251recnd 10231 . . . . . . . . 9 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 𝑐 ∈ ℂ)
5312a1i 11 . . . . . . . . 9 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 0 ∈ ℂ)
5450, 52, 53adddid 10227 . . . . . . . 8 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝐴 · 𝑥) · (𝑐 + 0)) = (((𝐴 · 𝑥) · 𝑐) + ((𝐴 · 𝑥) · 0)))
5511a1i 11 . . . . . . . . . . . . 13 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 1 ∈ ℂ)
5655, 52, 53addassd 10225 . . . . . . . . . . . 12 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((1 + 𝑐) + 0) = (1 + (𝑐 + 0)))
57 simpllr 817 . . . . . . . . . . . . 13 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (1 + 𝑐) = 0)
5857oveq1d 6816 . . . . . . . . . . . 12 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((1 + 𝑐) + 0) = (0 + 0))
5956, 58eqtr3d 2784 . . . . . . . . . . 11 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (1 + (𝑐 + 0)) = (0 + 0))
6034, 59, 573eqtr4a 2808 . . . . . . . . . 10 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (1 + (𝑐 + 0)) = (1 + 𝑐))
6137a1i 11 . . . . . . . . . . . 12 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 0 ∈ ℝ)
6251, 61readdcld 10232 . . . . . . . . . . 11 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (𝑐 + 0) ∈ ℝ)
631a1i 11 . . . . . . . . . . 11 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 1 ∈ ℝ)
64 readdcan 10373 . . . . . . . . . . 11 (((𝑐 + 0) ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 1 ∈ ℝ) → ((1 + (𝑐 + 0)) = (1 + 𝑐) ↔ (𝑐 + 0) = 𝑐))
6562, 51, 63, 64syl3anc 1463 . . . . . . . . . 10 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((1 + (𝑐 + 0)) = (1 + 𝑐) ↔ (𝑐 + 0) = 𝑐))
6660, 65mpbid 222 . . . . . . . . 9 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (𝑐 + 0) = 𝑐)
6766oveq2d 6817 . . . . . . . 8 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝐴 · 𝑥) · (𝑐 + 0)) = ((𝐴 · 𝑥) · 𝑐))
6854, 67eqtr3d 2784 . . . . . . 7 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (((𝐴 · 𝑥) · 𝑐) + ((𝐴 · 𝑥) · 0)) = ((𝐴 · 𝑥) · 𝑐))
69 mul31 10367 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑐 ∈ ℂ) → ((𝐴 · 𝑥) · 𝑐) = ((𝑐 · 𝑥) · 𝐴))
7047, 49, 52, 69syl3anc 1463 . . . . . . . . 9 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝐴 · 𝑥) · 𝑐) = ((𝑐 · 𝑥) · 𝐴))
71 simplrr 820 . . . . . . . . . 10 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (𝑐 · 𝑥) = 1)
7271oveq1d 6816 . . . . . . . . 9 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝑐 · 𝑥) · 𝐴) = (1 · 𝐴))
7347mulid2d 10221 . . . . . . . . 9 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (1 · 𝐴) = 𝐴)
7470, 72, 733eqtrd 2786 . . . . . . . 8 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝐴 · 𝑥) · 𝑐) = 𝐴)
75 mul01 10378 . . . . . . . . 9 ((𝐴 · 𝑥) ∈ ℂ → ((𝐴 · 𝑥) · 0) = 0)
7650, 75syl 17 . . . . . . . 8 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝐴 · 𝑥) · 0) = 0)
7774, 76oveq12d 6819 . . . . . . 7 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (((𝐴 · 𝑥) · 𝑐) + ((𝐴 · 𝑥) · 0)) = (𝐴 + 0))
7868, 77, 743eqtr3d 2790 . . . . . 6 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (𝐴 + 0) = 𝐴)
7978exp42 640 . . . . 5 ((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) → (𝑥 ∈ ℝ → ((𝑐 · 𝑥) = 1 → (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴))))
8079rexlimdv 3156 . . . 4 ((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) → (∃𝑥 ∈ ℝ (𝑐 · 𝑥) = 1 → (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)))
8146, 80mpd 15 . . 3 ((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) → (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴))
8281rexlimiva 3154 . 2 (∃𝑐 ∈ ℝ (1 + 𝑐) = 0 → (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴))
831, 2, 82mp2b 10 1 (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1620  wcel 2127  wne 2920  wrex 3039  (class class class)co 6801  cc 10097  cr 10098  0cc0 10099  1c1 10100  ici 10101   + caddc 10102   · cmul 10104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-8 2129  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-sep 4921  ax-nul 4929  ax-pow 4980  ax-pr 5043  ax-un 7102  ax-resscn 10156  ax-1cn 10157  ax-icn 10158  ax-addcl 10159  ax-addrcl 10160  ax-mulcl 10161  ax-mulrcl 10162  ax-mulcom 10163  ax-addass 10164  ax-mulass 10165  ax-distr 10166  ax-i2m1 10167  ax-1ne0 10168  ax-1rid 10169  ax-rnegex 10170  ax-rrecex 10171  ax-cnre 10172  ax-pre-lttri 10173  ax-pre-lttrn 10174  ax-pre-ltadd 10175
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-nel 3024  df-ral 3043  df-rex 3044  df-rab 3047  df-v 3330  df-sbc 3565  df-csb 3663  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-pw 4292  df-sn 4310  df-pr 4312  df-op 4316  df-uni 4577  df-br 4793  df-opab 4853  df-mpt 4870  df-id 5162  df-po 5175  df-so 5176  df-xp 5260  df-rel 5261  df-cnv 5262  df-co 5263  df-dm 5264  df-rn 5265  df-res 5266  df-ima 5267  df-iota 6000  df-fun 6039  df-fn 6040  df-f 6041  df-f1 6042  df-fo 6043  df-f1o 6044  df-fv 6045  df-ov 6804  df-er 7899  df-en 8110  df-dom 8111  df-sdom 8112  df-pnf 10239  df-mnf 10240  df-ltxr 10242
This theorem is referenced by:  cnegex  10380  addid2  10382  addcan2  10384  addid1i  10386  addid1d  10399  subid  10463  subid1  10464  addid0  10613  swrdccat3blem  13666  shftval3  13986  reim0  14028  isercolllem3  14567  fsumcvg  14613  summolem2a  14616  risefac1  14934  cnaddid  18444  ovolicc1  23455  brbtwn2  25955  axsegconlem1  25967  ax5seglem4  25982  axeuclid  26013  axcontlem2  26015  axcontlem4  26017  stoweidlem26  40715  2zrngamnd  42420  aacllem  43029
  Copyright terms: Public domain W3C validator