This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sn-addlid

Description: addlid without ax-mulcom . (Contributed by SN, 23-Jan-2024)

Ref Expression
Assertion sn-addlid ( 𝐴 ∈ ℂ → ( 0 + 𝐴 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 cnre ⊢ ( 𝐴 ∈ ℂ → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) )
2 0cnd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → 0 ∈ ℂ )
3 simp2l ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → 𝑥 ∈ ℝ )
4 3 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → 𝑥 ∈ ℂ )
5 ax-icn ⊢ i ∈ ℂ
6 5 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → i ∈ ℂ )
7 simp2r ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → 𝑦 ∈ ℝ )
8 7 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → 𝑦 ∈ ℂ )
9 6 8 mulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → ( i · 𝑦 ) ∈ ℂ )
10 2 4 9 addassd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → ( ( 0 + 𝑥 ) + ( i · 𝑦 ) ) = ( 0 + ( 𝑥 + ( i · 𝑦 ) ) ) )
11 readdlid ⊢ ( 𝑥 ∈ ℝ → ( 0 + 𝑥 ) = 𝑥 )
12 11 adantr ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 0 + 𝑥 ) = 𝑥 )
13 12 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → ( 0 + 𝑥 ) = 𝑥 )
14 13 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → ( ( 0 + 𝑥 ) + ( i · 𝑦 ) ) = ( 𝑥 + ( i · 𝑦 ) ) )
15 10 14 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → ( 0 + ( 𝑥 + ( i · 𝑦 ) ) ) = ( 𝑥 + ( i · 𝑦 ) ) )
16 simp3 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) )
17 16 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → ( 0 + 𝐴 ) = ( 0 + ( 𝑥 + ( i · 𝑦 ) ) ) )
18 15 17 16 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) ) → ( 0 + 𝐴 ) = 𝐴 )
19 18 3exp ⊢ ( 𝐴 ∈ ℂ → ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( 0 + 𝐴 ) = 𝐴 ) ) )
20 19 rexlimdvv ⊢ ( 𝐴 ∈ ℂ → ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( 0 + 𝐴 ) = 𝐴 ) )
21 1 20 mpd ⊢ ( 𝐴 ∈ ℂ → ( 0 + 𝐴 ) = 𝐴 )