Theorem sn-addid2

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

	Ref	Expression
Assertion	sn-addid2	⊢ ( 𝐴 ∈ ℂ → ( 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		readdid2	⊢ ( 𝑥 ∈ ℝ → ( 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 + 𝐴 ) = 𝐴 )