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

Theorem addid1 11335
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 11155 . 2 1 ∈ ℝ
2 ax-rnegex 11122 . 2 (1 ∈ ℝ → ∃𝑐 ∈ ℝ (1 + 𝑐) = 0)
3 ax-1ne0 11120 . . . . . 6 1 ≠ 0
4 oveq2 7365 . . . . . . . . . 10 (𝑐 = 0 → (1 + 𝑐) = (1 + 0))
54eqeq1d 2738 . . . . . . . . 9 (𝑐 = 0 → ((1 + 𝑐) = 0 ↔ (1 + 0) = 0))
65biimpcd 248 . . . . . . . 8 ((1 + 𝑐) = 0 → (𝑐 = 0 → (1 + 0) = 0))
7 oveq2 7365 . . . . . . . . 9 ((1 + 0) = 0 → (((i · i) · (i · i)) · (1 + 0)) = (((i · i) · (i · i)) · 0))
8 ax-icn 11110 . . . . . . . . . . . . . . 15 i ∈ ℂ
98, 8mulcli 11162 . . . . . . . . . . . . . 14 (i · i) ∈ ℂ
109, 9mulcli 11162 . . . . . . . . . . . . 13 ((i · i) · (i · i)) ∈ ℂ
11 ax-1cn 11109 . . . . . . . . . . . . 13 1 ∈ ℂ
12 0cn 11147 . . . . . . . . . . . . 13 0 ∈ ℂ
1310, 11, 12adddii 11167 . . . . . . . . . . . 12 (((i · i) · (i · i)) · (1 + 0)) = ((((i · i) · (i · i)) · 1) + (((i · i) · (i · i)) · 0))
1410mulid1i 11159 . . . . . . . . . . . . 13 (((i · i) · (i · i)) · 1) = ((i · i) · (i · i))
15 mul01 11334 . . . . . . . . . . . . . . 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 11119 . . . . . . . . . . . . . 14 ((i · i) + 1) = 0
1816, 17eqtr4i 2767 . . . . . . . . . . . . 13 (((i · i) · (i · i)) · 0) = ((i · i) + 1)
1914, 18oveq12i 7369 . . . . . . . . . . . 12 ((((i · i) · (i · i)) · 1) + (((i · i) · (i · i)) · 0)) = (((i · i) · (i · i)) + ((i · i) + 1))
2013, 19eqtri 2764 . . . . . . . . . . 11 (((i · i) · (i · i)) · (1 + 0)) = (((i · i) · (i · i)) + ((i · i) + 1))
2120, 16eqeq12i 2754 . . . . . . . . . 10 ((((i · i) · (i · i)) · (1 + 0)) = (((i · i) · (i · i)) · 0) ↔ (((i · i) · (i · i)) + ((i · i) + 1)) = 0)
2210, 9, 11addassi 11165 . . . . . . . . . . . 12 ((((i · i) · (i · i)) + (i · i)) + 1) = (((i · i) · (i · i)) + ((i · i) + 1))
239mulid1i 11159 . . . . . . . . . . . . . . 15 ((i · i) · 1) = (i · i)
2423oveq2i 7368 . . . . . . . . . . . . . 14 (((i · i) · (i · i)) + ((i · i) · 1)) = (((i · i) · (i · i)) + (i · i))
259, 9, 11adddii 11167 . . . . . . . . . . . . . . 15 ((i · i) · ((i · i) + 1)) = (((i · i) · (i · i)) + ((i · i) · 1))
2617oveq2i 7368 . . . . . . . . . . . . . . . 16 ((i · i) · ((i · i) + 1)) = ((i · i) · 0)
27 mul01 11334 . . . . . . . . . . . . . . . . 17 ((i · i) ∈ ℂ → ((i · i) · 0) = 0)
289, 27ax-mp 5 . . . . . . . . . . . . . . . 16 ((i · i) · 0) = 0
2926, 28eqtri 2764 . . . . . . . . . . . . . . 15 ((i · i) · ((i · i) + 1)) = 0
3025, 29eqtr3i 2766 . . . . . . . . . . . . . 14 (((i · i) · (i · i)) + ((i · i) · 1)) = 0
3124, 30eqtr3i 2766 . . . . . . . . . . . . 13 (((i · i) · (i · i)) + (i · i)) = 0
3231oveq1i 7367 . . . . . . . . . . . 12 ((((i · i) · (i · i)) + (i · i)) + 1) = (0 + 1)
3322, 32eqtr3i 2766 . . . . . . . . . . 11 (((i · i) · (i · i)) + ((i · i) + 1)) = (0 + 1)
34 00id 11330 . . . . . . . . . . . 12 (0 + 0) = 0
3534eqcomi 2745 . . . . . . . . . . 11 0 = (0 + 0)
3633, 35eqeq12i 2754 . . . . . . . . . 10 ((((i · i) · (i · i)) + ((i · i) + 1)) = 0 ↔ (0 + 1) = (0 + 0))
37 0re 11157 . . . . . . . . . . 11 0 ∈ ℝ
38 readdcan 11329 . . . . . . . . . . 11 ((1 ∈ ℝ ∧ 0 ∈ ℝ ∧ 0 ∈ ℝ) → ((0 + 1) = (0 + 0) ↔ 1 = 0))
391, 37, 37, 38mp3an 1461 . . . . . . . . . 10 ((0 + 1) = (0 + 0) ↔ 1 = 0)
4021, 36, 393bitri 296 . . . . . . . . 9 ((((i · i) · (i · i)) · (1 + 0)) = (((i · i) · (i · i)) · 0) ↔ 1 = 0)
417, 40sylib 217 . . . . . . . 8 ((1 + 0) = 0 → 1 = 0)
426, 41syl6 35 . . . . . . 7 ((1 + 𝑐) = 0 → (𝑐 = 0 → 1 = 0))
4342necon3d 2964 . . . . . 6 ((1 + 𝑐) = 0 → (1 ≠ 0 → 𝑐 ≠ 0))
443, 43mpi 20 . . . . 5 ((1 + 𝑐) = 0 → 𝑐 ≠ 0)
45 ax-rrecex 11123 . . . . 5 ((𝑐 ∈ ℝ ∧ 𝑐 ≠ 0) → ∃𝑥 ∈ ℝ (𝑐 · 𝑥) = 1)
4644, 45sylan2 593 . . . 4 ((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) → ∃𝑥 ∈ ℝ (𝑐 · 𝑥) = 1)
47 simpr 485 . . . . . . . . . 10 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 𝐴 ∈ ℂ)
48 simplrl 775 . . . . . . . . . . 11 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 𝑥 ∈ ℝ)
4948recnd 11183 . . . . . . . . . 10 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 𝑥 ∈ ℂ)
5047, 49mulcld 11175 . . . . . . . . 9 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (𝐴 · 𝑥) ∈ ℂ)
51 simplll 773 . . . . . . . . . 10 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 𝑐 ∈ ℝ)
5251recnd 11183 . . . . . . . . 9 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 𝑐 ∈ ℂ)
5312a1i 11 . . . . . . . . 9 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 0 ∈ ℂ)
5450, 52, 53adddid 11179 . . . . . . . 8 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝐴 · 𝑥) · (𝑐 + 0)) = (((𝐴 · 𝑥) · 𝑐) + ((𝐴 · 𝑥) · 0)))
5511a1i 11 . . . . . . . . . . . . 13 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 1 ∈ ℂ)
5655, 52, 53addassd 11177 . . . . . . . . . . . 12 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((1 + 𝑐) + 0) = (1 + (𝑐 + 0)))
57 simpllr 774 . . . . . . . . . . . . 13 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (1 + 𝑐) = 0)
5857oveq1d 7372 . . . . . . . . . . . 12 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((1 + 𝑐) + 0) = (0 + 0))
5956, 58eqtr3d 2778 . . . . . . . . . . 11 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (1 + (𝑐 + 0)) = (0 + 0))
6034, 59, 573eqtr4a 2802 . . . . . . . . . 10 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (1 + (𝑐 + 0)) = (1 + 𝑐))
6137a1i 11 . . . . . . . . . . . 12 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 0 ∈ ℝ)
6251, 61readdcld 11184 . . . . . . . . . . 11 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (𝑐 + 0) ∈ ℝ)
631a1i 11 . . . . . . . . . . 11 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → 1 ∈ ℝ)
64 readdcan 11329 . . . . . . . . . . 11 (((𝑐 + 0) ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 1 ∈ ℝ) → ((1 + (𝑐 + 0)) = (1 + 𝑐) ↔ (𝑐 + 0) = 𝑐))
6562, 51, 63, 64syl3anc 1371 . . . . . . . . . 10 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((1 + (𝑐 + 0)) = (1 + 𝑐) ↔ (𝑐 + 0) = 𝑐))
6660, 65mpbid 231 . . . . . . . . 9 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (𝑐 + 0) = 𝑐)
6766oveq2d 7373 . . . . . . . 8 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝐴 · 𝑥) · (𝑐 + 0)) = ((𝐴 · 𝑥) · 𝑐))
6854, 67eqtr3d 2778 . . . . . . 7 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (((𝐴 · 𝑥) · 𝑐) + ((𝐴 · 𝑥) · 0)) = ((𝐴 · 𝑥) · 𝑐))
69 mul31 11322 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑐 ∈ ℂ) → ((𝐴 · 𝑥) · 𝑐) = ((𝑐 · 𝑥) · 𝐴))
7047, 49, 52, 69syl3anc 1371 . . . . . . . . 9 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝐴 · 𝑥) · 𝑐) = ((𝑐 · 𝑥) · 𝐴))
71 simplrr 776 . . . . . . . . . 10 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (𝑐 · 𝑥) = 1)
7271oveq1d 7372 . . . . . . . . 9 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝑐 · 𝑥) · 𝐴) = (1 · 𝐴))
7347mulid2d 11173 . . . . . . . . 9 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (1 · 𝐴) = 𝐴)
7470, 72, 733eqtrd 2780 . . . . . . . 8 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝐴 · 𝑥) · 𝑐) = 𝐴)
75 mul01 11334 . . . . . . . . 9 ((𝐴 · 𝑥) ∈ ℂ → ((𝐴 · 𝑥) · 0) = 0)
7650, 75syl 17 . . . . . . . 8 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → ((𝐴 · 𝑥) · 0) = 0)
7774, 76oveq12d 7375 . . . . . . 7 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (((𝐴 · 𝑥) · 𝑐) + ((𝐴 · 𝑥) · 0)) = (𝐴 + 0))
7868, 77, 743eqtr3d 2784 . . . . . 6 ((((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) ∧ (𝑥 ∈ ℝ ∧ (𝑐 · 𝑥) = 1)) ∧ 𝐴 ∈ ℂ) → (𝐴 + 0) = 𝐴)
7978exp42 436 . . . . 5 ((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) → (𝑥 ∈ ℝ → ((𝑐 · 𝑥) = 1 → (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴))))
8079rexlimdv 3150 . . . 4 ((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) → (∃𝑥 ∈ ℝ (𝑐 · 𝑥) = 1 → (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)))
8146, 80mpd 15 . . 3 ((𝑐 ∈ ℝ ∧ (1 + 𝑐) = 0) → (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴))
8281rexlimiva 3144 . 2 (∃𝑐 ∈ ℝ (1 + 𝑐) = 0 → (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴))
831, 2, 82mp2b 10 1 (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wne 2943  wrex 3073  (class class class)co 7357  cc 11049  cr 11050  0cc0 11051  1c1 11052  ici 11053   + caddc 11054   · cmul 11056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-po 5545  df-so 5546  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11191  df-mnf 11192  df-ltxr 11194
This theorem is referenced by:  cnegex  11336  addid2  11338  addcan2  11340  addid1i  11342  addid1d  11355  subid  11420  subid1  11421  addid0  11574  swrdccat3blem  14627  shftval3  14961  reim0  15003  isercolllem3  15551  fsumcvg  15597  summolem2a  15600  risefac1  15916  cnaddid  19648  ovolicc1  24880  addsqnreup  26791  brbtwn2  27854  axsegconlem1  27866  ax5seglem4  27881  axeuclid  27912  axcontlem2  27914  axcontlem4  27916  2xp3dxp2ge1d  40614  factwoffsmonot  40615  stoweidlem26  44257  2zrngamnd  46229  aacllem  47238
  Copyright terms: Public domain W3C validator