Metamath Proof Explorer

Theorem addid1

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)

Ref Expression
Assertion addid1 ( 𝐴 ∈ ℂ → ( 𝐴 + 0 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 1re ⊢ 1 ∈ ℝ
2 ax-rnegex ⊢ ( 1 ∈ ℝ → ∃ 𝑐 ∈ ℝ ( 1 + 𝑐 ) = 0 )
3 ax-1ne0 ⊢ 1 ≠ 0
4 oveq2 ⊢ ( 𝑐 = 0 → ( 1 + 𝑐 ) = ( 1 + 0 ) )
5 4 eqeq1d ⊢ ( 𝑐 = 0 → ( ( 1 + 𝑐 ) = 0 ↔ ( 1 + 0 ) = 0 ) )
6 5 biimpcd ⊢ ( ( 1 + 𝑐 ) = 0 → ( 𝑐 = 0 → ( 1 + 0 ) = 0 ) )
7 oveq2 ⊢ ( ( 1 + 0 ) = 0 → ( ( ( i · i ) · ( i · i ) ) · ( 1 + 0 ) ) = ( ( ( i · i ) · ( i · i ) ) · 0 ) )
8 ax-icn ⊢ i ∈ ℂ
9 8 8 mulcli ⊢ ( i · i ) ∈ ℂ
10 9 9 mulcli ⊢ ( ( i · i ) · ( i · i ) ) ∈ ℂ
11 ax-1cn ⊢ 1 ∈ ℂ
12 0cn ⊢ 0 ∈ ℂ
13 10 11 12 adddii ⊢ ( ( ( i · i ) · ( i · i ) ) · ( 1 + 0 ) ) = ( ( ( ( i · i ) · ( i · i ) ) · 1 ) + ( ( ( i · i ) · ( i · i ) ) · 0 ) )
14 10 mulid1i ⊢ ( ( ( i · i ) · ( i · i ) ) · 1 ) = ( ( i · i ) · ( i · i ) )
15 mul01 ⊢ ( ( ( i · i ) · ( i · i ) ) ∈ ℂ → ( ( ( i · i ) · ( i · i ) ) · 0 ) = 0 )
16 10 15 ax-mp ⊢ ( ( ( i · i ) · ( i · i ) ) · 0 ) = 0
17 ax-i2m1 ⊢ ( ( i · i ) + 1 ) = 0
18 16 17 eqtr4i ⊢ ( ( ( i · i ) · ( i · i ) ) · 0 ) = ( ( i · i ) + 1 )
19 14 18 oveq12i ⊢ ( ( ( ( i · i ) · ( i · i ) ) · 1 ) + ( ( ( i · i ) · ( i · i ) ) · 0 ) ) = ( ( ( i · i ) · ( i · i ) ) + ( ( i · i ) + 1 ) )
20 13 19 eqtri ⊢ ( ( ( i · i ) · ( i · i ) ) · ( 1 + 0 ) ) = ( ( ( i · i ) · ( i · i ) ) + ( ( i · i ) + 1 ) )
21 20 16 eqeq12i ⊢ ( ( ( ( i · i ) · ( i · i ) ) · ( 1 + 0 ) ) = ( ( ( i · i ) · ( i · i ) ) · 0 ) ↔ ( ( ( i · i ) · ( i · i ) ) + ( ( i · i ) + 1 ) ) = 0 )
22 10 9 11 addassi ⊢ ( ( ( ( i · i ) · ( i · i ) ) + ( i · i ) ) + 1 ) = ( ( ( i · i ) · ( i · i ) ) + ( ( i · i ) + 1 ) )
23 9 mulid1i ⊢ ( ( i · i ) · 1 ) = ( i · i )
24 23 oveq2i ⊢ ( ( ( i · i ) · ( i · i ) ) + ( ( i · i ) · 1 ) ) = ( ( ( i · i ) · ( i · i ) ) + ( i · i ) )
25 9 9 11 adddii ⊢ ( ( i · i ) · ( ( i · i ) + 1 ) ) = ( ( ( i · i ) · ( i · i ) ) + ( ( i · i ) · 1 ) )
26 17 oveq2i ⊢ ( ( i · i ) · ( ( i · i ) + 1 ) ) = ( ( i · i ) · 0 )
27 mul01 ⊢ ( ( i · i ) ∈ ℂ → ( ( i · i ) · 0 ) = 0 )
28 9 27 ax-mp ⊢ ( ( i · i ) · 0 ) = 0
29 26 28 eqtri ⊢ ( ( i · i ) · ( ( i · i ) + 1 ) ) = 0
30 25 29 eqtr3i ⊢ ( ( ( i · i ) · ( i · i ) ) + ( ( i · i ) · 1 ) ) = 0
31 24 30 eqtr3i ⊢ ( ( ( i · i ) · ( i · i ) ) + ( i · i ) ) = 0
32 31 oveq1i ⊢ ( ( ( ( i · i ) · ( i · i ) ) + ( i · i ) ) + 1 ) = ( 0 + 1 )
33 22 32 eqtr3i ⊢ ( ( ( i · i ) · ( i · i ) ) + ( ( i · i ) + 1 ) ) = ( 0 + 1 )
34 00id ⊢ ( 0 + 0 ) = 0
35 34 eqcomi ⊢ 0 = ( 0 + 0 )
36 33 35 eqeq12i ⊢ ( ( ( ( i · i ) · ( i · i ) ) + ( ( i · i ) + 1 ) ) = 0 ↔ ( 0 + 1 ) = ( 0 + 0 ) )
37 0re ⊢ 0 ∈ ℝ
38 readdcan ⊢ ( ( 1 ∈ ℝ ∧ 0 ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( 0 + 1 ) = ( 0 + 0 ) ↔ 1 = 0 ) )
39 1 37 37 38 mp3an ⊢ ( ( 0 + 1 ) = ( 0 + 0 ) ↔ 1 = 0 )
40 21 36 39 3bitri ⊢ ( ( ( ( i · i ) · ( i · i ) ) · ( 1 + 0 ) ) = ( ( ( i · i ) · ( i · i ) ) · 0 ) ↔ 1 = 0 )
41 7 40 sylib ⊢ ( ( 1 + 0 ) = 0 → 1 = 0 )
42 6 41 syl6 ⊢ ( ( 1 + 𝑐 ) = 0 → ( 𝑐 = 0 → 1 = 0 ) )
43 42 necon3d ⊢ ( ( 1 + 𝑐 ) = 0 → ( 1 ≠ 0 → 𝑐 ≠ 0 ) )
44 3 43 mpi ⊢ ( ( 1 + 𝑐 ) = 0 → 𝑐 ≠ 0 )
45 ax-rrecex ⊢ ( ( 𝑐 ∈ ℝ ∧ 𝑐 ≠ 0 ) → ∃ 𝑥 ∈ ℝ ( 𝑐 · 𝑥 ) = 1 )
46 44 45 sylan2 ⊢ ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) → ∃ 𝑥 ∈ ℝ ( 𝑐 · 𝑥 ) = 1 )
47 simpr ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑐 · 𝑥 ) = 1 ) ) ∧ 𝐴 ∈ ℂ ) → 𝐴 ∈ ℂ )
48 simplrl ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑐 · 𝑥 ) = 1 ) ) ∧ 𝐴 ∈ ℂ ) → 𝑥 ∈ ℝ )
49 48 recnd ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑐 · 𝑥 ) = 1 ) ) ∧ 𝐴 ∈ ℂ ) → 𝑥 ∈ ℂ )
50 47 49 mulcld ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑐 · 𝑥 ) = 1 ) ) ∧ 𝐴 ∈ ℂ ) → ( 𝐴 · 𝑥 ) ∈ ℂ )
51 simplll ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑐 · 𝑥 ) = 1 ) ) ∧ 𝐴 ∈ ℂ ) → 𝑐 ∈ ℝ )
52 51 recnd ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑐 · 𝑥 ) = 1 ) ) ∧ 𝐴 ∈ ℂ ) → 𝑐 ∈ ℂ )
53 12 a1i ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑐 · 𝑥 ) = 1 ) ) ∧ 𝐴 ∈ ℂ ) → 0 ∈ ℂ )
54 50 52 53 adddid ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑐 · 𝑥 ) = 1 ) ) ∧ 𝐴 ∈ ℂ ) → ( ( 𝐴 · 𝑥 ) · ( 𝑐 + 0 ) ) = ( ( ( 𝐴 · 𝑥 ) · 𝑐 ) + ( ( 𝐴 · 𝑥 ) · 0 ) ) )
55 11 a1i ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑐 · 𝑥 ) = 1 ) ) ∧ 𝐴 ∈ ℂ ) → 1 ∈ ℂ )
56 55 52 53 addassd ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑐 · 𝑥 ) = 1 ) ) ∧ 𝐴 ∈ ℂ ) → ( ( 1 + 𝑐 ) + 0 ) = ( 1 + ( 𝑐 + 0 ) ) )
57 simpllr ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑐 · 𝑥 ) = 1 ) ) ∧ 𝐴 ∈ ℂ ) → ( 1 + 𝑐 ) = 0 )
58 57 oveq1d ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑐 · 𝑥 ) = 1 ) ) ∧ 𝐴 ∈ ℂ ) → ( ( 1 + 𝑐 ) + 0 ) = ( 0 + 0 ) )
59 56 58 eqtr3d ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑐 · 𝑥 ) = 1 ) ) ∧ 𝐴 ∈ ℂ ) → ( 1 + ( 𝑐 + 0 ) ) = ( 0 + 0 ) )
60 34 59 57 3eqtr4a ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑐 · 𝑥 ) = 1 ) ) ∧ 𝐴 ∈ ℂ ) → ( 1 + ( 𝑐 + 0 ) ) = ( 1 + 𝑐 ) )
61 37 a1i ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑐 · 𝑥 ) = 1 ) ) ∧ 𝐴 ∈ ℂ ) → 0 ∈ ℝ )
62 51 61 readdcld ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑐 · 𝑥 ) = 1 ) ) ∧ 𝐴 ∈ ℂ ) → ( 𝑐 + 0 ) ∈ ℝ )
63 1 a1i ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑐 · 𝑥 ) = 1 ) ) ∧ 𝐴 ∈ ℂ ) → 1 ∈ ℝ )
64 readdcan ⊢ ( ( ( 𝑐 + 0 ) ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 1 + ( 𝑐 + 0 ) ) = ( 1 + 𝑐 ) ↔ ( 𝑐 + 0 ) = 𝑐 ) )
65 62 51 63 64 syl3anc ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑐 · 𝑥 ) = 1 ) ) ∧ 𝐴 ∈ ℂ ) → ( ( 1 + ( 𝑐 + 0 ) ) = ( 1 + 𝑐 ) ↔ ( 𝑐 + 0 ) = 𝑐 ) )
66 60 65 mpbid ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑐 · 𝑥 ) = 1 ) ) ∧ 𝐴 ∈ ℂ ) → ( 𝑐 + 0 ) = 𝑐 )
67 66 oveq2d ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑐 · 𝑥 ) = 1 ) ) ∧ 𝐴 ∈ ℂ ) → ( ( 𝐴 · 𝑥 ) · ( 𝑐 + 0 ) ) = ( ( 𝐴 · 𝑥 ) · 𝑐 ) )
68 54 67 eqtr3d ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑐 · 𝑥 ) = 1 ) ) ∧ 𝐴 ∈ ℂ ) → ( ( ( 𝐴 · 𝑥 ) · 𝑐 ) + ( ( 𝐴 · 𝑥 ) · 0 ) ) = ( ( 𝐴 · 𝑥 ) · 𝑐 ) )
69 mul31 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ( 𝐴 · 𝑥 ) · 𝑐 ) = ( ( 𝑐 · 𝑥 ) · 𝐴 ) )
70 47 49 52 69 syl3anc ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑐 · 𝑥 ) = 1 ) ) ∧ 𝐴 ∈ ℂ ) → ( ( 𝐴 · 𝑥 ) · 𝑐 ) = ( ( 𝑐 · 𝑥 ) · 𝐴 ) )
71 simplrr ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑐 · 𝑥 ) = 1 ) ) ∧ 𝐴 ∈ ℂ ) → ( 𝑐 · 𝑥 ) = 1 )
72 71 oveq1d ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑐 · 𝑥 ) = 1 ) ) ∧ 𝐴 ∈ ℂ ) → ( ( 𝑐 · 𝑥 ) · 𝐴 ) = ( 1 · 𝐴 ) )
73 47 mulid2d ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑐 · 𝑥 ) = 1 ) ) ∧ 𝐴 ∈ ℂ ) → ( 1 · 𝐴 ) = 𝐴 )
74 70 72 73 3eqtrd ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑐 · 𝑥 ) = 1 ) ) ∧ 𝐴 ∈ ℂ ) → ( ( 𝐴 · 𝑥 ) · 𝑐 ) = 𝐴 )
75 mul01 ⊢ ( ( 𝐴 · 𝑥 ) ∈ ℂ → ( ( 𝐴 · 𝑥 ) · 0 ) = 0 )
76 50 75 syl ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑐 · 𝑥 ) = 1 ) ) ∧ 𝐴 ∈ ℂ ) → ( ( 𝐴 · 𝑥 ) · 0 ) = 0 )
77 74 76 oveq12d ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑐 · 𝑥 ) = 1 ) ) ∧ 𝐴 ∈ ℂ ) → ( ( ( 𝐴 · 𝑥 ) · 𝑐 ) + ( ( 𝐴 · 𝑥 ) · 0 ) ) = ( 𝐴 + 0 ) )
78 68 77 74 3eqtr3d ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝑐 · 𝑥 ) = 1 ) ) ∧ 𝐴 ∈ ℂ ) → ( 𝐴 + 0 ) = 𝐴 )
79 78 exp42 ⊢ ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) → ( 𝑥 ∈ ℝ → ( ( 𝑐 · 𝑥 ) = 1 → ( 𝐴 ∈ ℂ → ( 𝐴 + 0 ) = 𝐴 ) ) ) )
80 79 rexlimdv ⊢ ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) → ( ∃ 𝑥 ∈ ℝ ( 𝑐 · 𝑥 ) = 1 → ( 𝐴 ∈ ℂ → ( 𝐴 + 0 ) = 𝐴 ) ) )
81 46 80 mpd ⊢ ( ( 𝑐 ∈ ℝ ∧ ( 1 + 𝑐 ) = 0 ) → ( 𝐴 ∈ ℂ → ( 𝐴 + 0 ) = 𝐴 ) )
82 81 rexlimiva ⊢ ( ∃ 𝑐 ∈ ℝ ( 1 + 𝑐 ) = 0 → ( 𝐴 ∈ ℂ → ( 𝐴 + 0 ) = 𝐴 ) )
83 1 2 82 mp2b ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + 0 ) = 𝐴 )