Theorem sn-mul02

Description: mul02 without ax-mulcom . See https://github.com/icecream17/Stuff/blob/main/math/0A%3D0.md for an outline. (Contributed by SN, 30-Jun-2024)

	Ref	Expression
Assertion	sn-mul02	$$⊢A\in ℂ\to 0\cdot A=0$$

Proof

Step	Hyp	Ref	Expression
1		cnre	$$⊢A\in ℂ\to \exists x\in ℝ\exists y\in ℝA=x+\mathrm{i}y$$
2		0cnd	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to 0\in ℂ$$
3		recn	$$⊢x\in ℝ\to x\in ℂ$$
4	3	adantr	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to x\in ℂ$$
5		ax-icn	$$⊢\mathrm{i}\in ℂ$$
6	5	a1i	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \mathrm{i}\in ℂ$$
7		recn	$$⊢y\in ℝ\to y\in ℂ$$
8	7	adantl	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to y\in ℂ$$
9	6 8	mulcld	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \mathrm{i}y\in ℂ$$
10	2 4 9	adddid	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to 0\cdot \left(x+\mathrm{i}y\right)=0\cdot x+0\cdot \mathrm{i}y$$
11		remul02	$$⊢x\in ℝ\to 0\cdot x=0$$
12	11	adantr	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to 0\cdot x=0$$
13		sn-0tie0	$$⊢0\cdot \mathrm{i}=0$$
14	13	oveq1i	$$⊢0\cdot \mathrm{i}y=0\cdot y$$
15	2 6 8	mulassd	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to 0\cdot \mathrm{i}y=0\cdot \mathrm{i}y$$
16		remul02	$$⊢y\in ℝ\to 0\cdot y=0$$
17	16	adantl	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to 0\cdot y=0$$
18	14 15 17	3eqtr3a	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to 0\cdot \mathrm{i}y=0$$
19	12 18	oveq12d	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to 0\cdot x+0\cdot \mathrm{i}y=0+0$$
20		sn-00id	$$⊢0+0=0$$
21	19 20	eqtrdi	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to 0\cdot x+0\cdot \mathrm{i}y=0$$
22	10 21	eqtrd	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to 0\cdot \left(x+\mathrm{i}y\right)=0$$
23		oveq2	$$⊢A=x+\mathrm{i}y\to 0\cdot A=0\cdot \left(x+\mathrm{i}y\right)$$
24	23	eqeq1d	$$⊢A=x+\mathrm{i}y\to \left(0\cdot A=0\leftrightarrow 0\cdot \left(x+\mathrm{i}y\right)=0\right)$$
25	22 24	syl5ibrcom	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \left(A=x+\mathrm{i}y\to 0\cdot A=0\right)$$
26	25	rexlimivv	$$⊢\exists x\in ℝ\exists y\in ℝA=x+\mathrm{i}y\to 0\cdot A=0$$
27	1 26	syl	$$⊢A\in ℂ\to 0\cdot A=0$$