Theorem sn-it0e0

Description: Proof of it0e0 without ax-mulcom . Informally, a real number times 0 is 0, and E. r e. RR r = _i x. s by ax-cnre and renegid2 . (Contributed by SN, 30-Apr-2024)

	Ref	Expression
Assertion	sn-it0e0	$$⊢\mathrm{i}\cdot 0=0$$

Proof

Step	Hyp	Ref	Expression
1		0cn	$$⊢0\in ℂ$$
2		cnre	$$⊢0\in ℂ\to \exists a\in ℝ\exists b\in ℝ0=a+\mathrm{i}b$$
3		oveq2	$$⊢0=a+\mathrm{i}b\to \left(0{-}_{ℝ}a\right)+0=\left(0{-}_{ℝ}a\right)+a+\mathrm{i}b$$
4		ax-icn	$$⊢\mathrm{i}\in ℂ$$
5	4	a1i	$$⊢b\in ℝ\to \mathrm{i}\in ℂ$$
6		recn	$$⊢b\in ℝ\to b\in ℂ$$
7		0cnd	$$⊢b\in ℝ\to 0\in ℂ$$
8	5 6 7	mulassd	$$⊢b\in ℝ\to \mathrm{i}b\cdot 0=\mathrm{i}b\cdot 0$$
9		remul01	$$⊢b\in ℝ\to b\cdot 0=0$$
10	9	oveq2d	$$⊢b\in ℝ\to \mathrm{i}b\cdot 0=\mathrm{i}\cdot 0$$
11	8 10	eqtrd	$$⊢b\in ℝ\to \mathrm{i}b\cdot 0=\mathrm{i}\cdot 0$$
12	11	ad2antlr	$$⊢\left(\left(a\in ℝ\wedge b\in ℝ\right)\wedge \left(0{-}_{ℝ}a\right)+0=\left(0{-}_{ℝ}a\right)+a+\mathrm{i}b\right)\to \mathrm{i}b\cdot 0=\mathrm{i}\cdot 0$$
13		rernegcl	$$⊢a\in ℝ\to 0{-}_{ℝ}a\in ℝ$$
14	13	recnd	$$⊢a\in ℝ\to 0{-}_{ℝ}a\in ℂ$$
15	14	adantr	$$⊢\left(a\in ℝ\wedge b\in ℝ\right)\to 0{-}_{ℝ}a\in ℂ$$
16		recn	$$⊢a\in ℝ\to a\in ℂ$$
17	16	adantr	$$⊢\left(a\in ℝ\wedge b\in ℝ\right)\to a\in ℂ$$
18	5 6	mulcld	$$⊢b\in ℝ\to \mathrm{i}b\in ℂ$$
19	18	adantl	$$⊢\left(a\in ℝ\wedge b\in ℝ\right)\to \mathrm{i}b\in ℂ$$
20	15 17 19	addassd	$$⊢\left(a\in ℝ\wedge b\in ℝ\right)\to \left(0{-}_{ℝ}a\right)+a+\mathrm{i}b=\left(0{-}_{ℝ}a\right)+a+\mathrm{i}b$$
21		renegid2	$$⊢a\in ℝ\to \left(0{-}_{ℝ}a\right)+a=0$$
22	21	oveq1d	$$⊢a\in ℝ\to \left(0{-}_{ℝ}a\right)+a+\mathrm{i}b=0+\mathrm{i}b$$
23		sn-addid2	$$⊢\mathrm{i}b\in ℂ\to 0+\mathrm{i}b=\mathrm{i}b$$
24	18 23	syl	$$⊢b\in ℝ\to 0+\mathrm{i}b=\mathrm{i}b$$
25	22 24	sylan9eq	$$⊢\left(a\in ℝ\wedge b\in ℝ\right)\to \left(0{-}_{ℝ}a\right)+a+\mathrm{i}b=\mathrm{i}b$$
26	20 25	eqtr3d	$$⊢\left(a\in ℝ\wedge b\in ℝ\right)\to \left(0{-}_{ℝ}a\right)+a+\mathrm{i}b=\mathrm{i}b$$
27	26	eqeq2d	$$⊢\left(a\in ℝ\wedge b\in ℝ\right)\to \left(\left(0{-}_{ℝ}a\right)+0=\left(0{-}_{ℝ}a\right)+a+\mathrm{i}b\leftrightarrow \left(0{-}_{ℝ}a\right)+0=\mathrm{i}b\right)$$
28	27	biimpa	$$⊢\left(\left(a\in ℝ\wedge b\in ℝ\right)\wedge \left(0{-}_{ℝ}a\right)+0=\left(0{-}_{ℝ}a\right)+a+\mathrm{i}b\right)\to \left(0{-}_{ℝ}a\right)+0=\mathrm{i}b$$
29	28	oveq1d	$$⊢\left(\left(a\in ℝ\wedge b\in ℝ\right)\wedge \left(0{-}_{ℝ}a\right)+0=\left(0{-}_{ℝ}a\right)+a+\mathrm{i}b\right)\to \left(\left(0{-}_{ℝ}a\right)+0\right)\cdot 0=\mathrm{i}b\cdot 0$$
30		elre0re	$$⊢a\in ℝ\to 0\in ℝ$$
31	13 30	readdcld	$$⊢a\in ℝ\to \left(0{-}_{ℝ}a\right)+0\in ℝ$$
32	31	ad2antrr	$$⊢\left(\left(a\in ℝ\wedge b\in ℝ\right)\wedge \left(0{-}_{ℝ}a\right)+0=\left(0{-}_{ℝ}a\right)+a+\mathrm{i}b\right)\to \left(0{-}_{ℝ}a\right)+0\in ℝ$$
33		remul01	$$⊢\left(0{-}_{ℝ}a\right)+0\in ℝ\to \left(\left(0{-}_{ℝ}a\right)+0\right)\cdot 0=0$$
34	32 33	syl	$$⊢\left(\left(a\in ℝ\wedge b\in ℝ\right)\wedge \left(0{-}_{ℝ}a\right)+0=\left(0{-}_{ℝ}a\right)+a+\mathrm{i}b\right)\to \left(\left(0{-}_{ℝ}a\right)+0\right)\cdot 0=0$$
35	29 34	eqtr3d	$$⊢\left(\left(a\in ℝ\wedge b\in ℝ\right)\wedge \left(0{-}_{ℝ}a\right)+0=\left(0{-}_{ℝ}a\right)+a+\mathrm{i}b\right)\to \mathrm{i}b\cdot 0=0$$
36	12 35	eqtr3d	$$⊢\left(\left(a\in ℝ\wedge b\in ℝ\right)\wedge \left(0{-}_{ℝ}a\right)+0=\left(0{-}_{ℝ}a\right)+a+\mathrm{i}b\right)\to \mathrm{i}\cdot 0=0$$
37	36	ex	$$⊢\left(a\in ℝ\wedge b\in ℝ\right)\to \left(\left(0{-}_{ℝ}a\right)+0=\left(0{-}_{ℝ}a\right)+a+\mathrm{i}b\to \mathrm{i}\cdot 0=0\right)$$
38	3 37	syl5	$$⊢\left(a\in ℝ\wedge b\in ℝ\right)\to \left(0=a+\mathrm{i}b\to \mathrm{i}\cdot 0=0\right)$$
39	38	rexlimivv	$$⊢\exists a\in ℝ\exists b\in ℝ0=a+\mathrm{i}b\to \mathrm{i}\cdot 0=0$$
40	1 2 39	mp2b	$$⊢\mathrm{i}\cdot 0=0$$