Metamath Proof Explorer

Theorem addid2

Description: 0 is a left identity for addition. This used to be one of our complex number axioms, until it was discovered that it was dependent on the others. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013)

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

Proof

Step Hyp Ref Expression
1 cnegex ⊢ ( 𝐴 ∈ ℂ → ∃ 𝑥 ∈ ℂ ( 𝐴 + 𝑥 ) = 0 )
2 cnegex ⊢ ( 𝑥 ∈ ℂ → ∃ 𝑦 ∈ ℂ ( 𝑥 + 𝑦 ) = 0 )
3 2 ad2antrl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ) → ∃ 𝑦 ∈ ℂ ( 𝑥 + 𝑦 ) = 0 )
4 0cn ⊢ 0 ∈ ℂ
5 addass ⊢ ( ( 0 ∈ ℂ ∧ 0 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 0 + 0 ) + 𝑦 ) = ( 0 + ( 0 + 𝑦 ) ) )
6 4 4 5 mp3an12 ⊢ ( 𝑦 ∈ ℂ → ( ( 0 + 0 ) + 𝑦 ) = ( 0 + ( 0 + 𝑦 ) ) )
7 6 adantr ⊢ ( ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) → ( ( 0 + 0 ) + 𝑦 ) = ( 0 + ( 0 + 𝑦 ) ) )
8 7 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → ( ( 0 + 0 ) + 𝑦 ) = ( 0 + ( 0 + 𝑦 ) ) )
9 00id ⊢ ( 0 + 0 ) = 0
10 9 oveq1i ⊢ ( ( 0 + 0 ) + 𝑦 ) = ( 0 + 𝑦 )
11 simp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → 𝐴 ∈ ℂ )
12 simp2l ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → 𝑥 ∈ ℂ )
13 simp3l ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → 𝑦 ∈ ℂ )
14 11 12 13 addassd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → ( ( 𝐴 + 𝑥 ) + 𝑦 ) = ( 𝐴 + ( 𝑥 + 𝑦 ) ) )
15 simp2r ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → ( 𝐴 + 𝑥 ) = 0 )
16 15 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → ( ( 𝐴 + 𝑥 ) + 𝑦 ) = ( 0 + 𝑦 ) )
17 simp3r ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → ( 𝑥 + 𝑦 ) = 0 )
18 17 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → ( 𝐴 + ( 𝑥 + 𝑦 ) ) = ( 𝐴 + 0 ) )
19 14 16 18 3eqtr3rd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → ( 𝐴 + 0 ) = ( 0 + 𝑦 ) )
20 addid1 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + 0 ) = 𝐴 )
21 20 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → ( 𝐴 + 0 ) = 𝐴 )
22 19 21 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → ( 0 + 𝑦 ) = 𝐴 )
23 10 22 eqtrid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → ( ( 0 + 0 ) + 𝑦 ) = 𝐴 )
24 22 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → ( 0 + ( 0 + 𝑦 ) ) = ( 0 + 𝐴 ) )
25 8 23 24 3eqtr3rd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → ( 0 + 𝐴 ) = 𝐴 )
26 25 3expia ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ) → ( ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) → ( 0 + 𝐴 ) = 𝐴 ) )
27 26 expd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ) → ( 𝑦 ∈ ℂ → ( ( 𝑥 + 𝑦 ) = 0 → ( 0 + 𝐴 ) = 𝐴 ) ) )
28 27 rexlimdv ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ) → ( ∃ 𝑦 ∈ ℂ ( 𝑥 + 𝑦 ) = 0 → ( 0 + 𝐴 ) = 𝐴 ) )
29 3 28 mpd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ) → ( 0 + 𝐴 ) = 𝐴 )
30 1 29 rexlimddv ⊢ ( 𝐴 ∈ ℂ → ( 0 + 𝐴 ) = 𝐴 )