Theorem sn-mul01

Description: mul01 without ax-mulcom . (Contributed by SN, 5-May-2024)

	Ref	Expression
Assertion	sn-mul01	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 0 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
2		0cnd	⊢ ( 𝐴 ∈ ℂ → 0 ∈ ℂ )
3	1 2	mulcld	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 0 ) ∈ ℂ )
4		sn-00id	⊢ ( 0 + 0 ) = 0
5	4	oveq2i	⊢ ( 𝐴 · ( 0 + 0 ) ) = ( 𝐴 · 0 )
6	1 2 2	adddid	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · ( 0 + 0 ) ) = ( ( 𝐴 · 0 ) + ( 𝐴 · 0 ) ) )
7	5 6	syl5reqr	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 · 0 ) + ( 𝐴 · 0 ) ) = ( 𝐴 · 0 ) )
8	3 7	sn-addid0	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 0 ) = 0 )