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	⊢ ( i · 0 ) = 0

Proof

Step	Hyp	Ref	Expression
1		0cn	⊢ 0 ∈ ℂ
2		cnre	⊢ ( 0 ∈ ℂ → ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ 0 = ( 𝑎 + ( i · 𝑏 ) ) )
3		oveq2	⊢ ( 0 = ( 𝑎 + ( i · 𝑏 ) ) → ( ( 0 −ℝ 𝑎 ) + 0 ) = ( ( 0 −ℝ 𝑎 ) + ( 𝑎 + ( i · 𝑏 ) ) ) )
4		ax-icn	⊢ i ∈ ℂ
5	4	a1i	⊢ ( 𝑏 ∈ ℝ → i ∈ ℂ )
6		recn	⊢ ( 𝑏 ∈ ℝ → 𝑏 ∈ ℂ )
7		0cnd	⊢ ( 𝑏 ∈ ℝ → 0 ∈ ℂ )
8	5 6 7	mulassd	⊢ ( 𝑏 ∈ ℝ → ( ( i · 𝑏 ) · 0 ) = ( i · ( 𝑏 · 0 ) ) )
9		remul01	⊢ ( 𝑏 ∈ ℝ → ( 𝑏 · 0 ) = 0 )
10	9	oveq2d	⊢ ( 𝑏 ∈ ℝ → ( i · ( 𝑏 · 0 ) ) = ( i · 0 ) )
11	8 10	eqtrd	⊢ ( 𝑏 ∈ ℝ → ( ( i · 𝑏 ) · 0 ) = ( i · 0 ) )
12	11	ad2antlr	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( ( 0 −ℝ 𝑎 ) + 0 ) = ( ( 0 −ℝ 𝑎 ) + ( 𝑎 + ( i · 𝑏 ) ) ) ) → ( ( i · 𝑏 ) · 0 ) = ( i · 0 ) )
13		rernegcl	⊢ ( 𝑎 ∈ ℝ → ( 0 −ℝ 𝑎 ) ∈ ℝ )
14	13	recnd	⊢ ( 𝑎 ∈ ℝ → ( 0 −ℝ 𝑎 ) ∈ ℂ )
15	14	adantr	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( 0 −ℝ 𝑎 ) ∈ ℂ )
16		recn	⊢ ( 𝑎 ∈ ℝ → 𝑎 ∈ ℂ )
17	16	adantr	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → 𝑎 ∈ ℂ )
18	5 6	mulcld	⊢ ( 𝑏 ∈ ℝ → ( i · 𝑏 ) ∈ ℂ )
19	18	adantl	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( i · 𝑏 ) ∈ ℂ )
20	15 17 19	addassd	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( ( ( 0 −ℝ 𝑎 ) + 𝑎 ) + ( i · 𝑏 ) ) = ( ( 0 −ℝ 𝑎 ) + ( 𝑎 + ( i · 𝑏 ) ) ) )
21		renegid2	⊢ ( 𝑎 ∈ ℝ → ( ( 0 −ℝ 𝑎 ) + 𝑎 ) = 0 )
22	21	oveq1d	⊢ ( 𝑎 ∈ ℝ → ( ( ( 0 −ℝ 𝑎 ) + 𝑎 ) + ( i · 𝑏 ) ) = ( 0 + ( i · 𝑏 ) ) )
23		sn-addlid	⊢ ( ( i · 𝑏 ) ∈ ℂ → ( 0 + ( i · 𝑏 ) ) = ( i · 𝑏 ) )
24	18 23	syl	⊢ ( 𝑏 ∈ ℝ → ( 0 + ( i · 𝑏 ) ) = ( i · 𝑏 ) )
25	22 24	sylan9eq	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( ( ( 0 −ℝ 𝑎 ) + 𝑎 ) + ( i · 𝑏 ) ) = ( i · 𝑏 ) )
26	20 25	eqtr3d	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( ( 0 −ℝ 𝑎 ) + ( 𝑎 + ( i · 𝑏 ) ) ) = ( i · 𝑏 ) )
27	26	eqeq2d	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( ( ( 0 −ℝ 𝑎 ) + 0 ) = ( ( 0 −ℝ 𝑎 ) + ( 𝑎 + ( i · 𝑏 ) ) ) ↔ ( ( 0 −ℝ 𝑎 ) + 0 ) = ( i · 𝑏 ) ) )
28	27	biimpa	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( ( 0 −ℝ 𝑎 ) + 0 ) = ( ( 0 −ℝ 𝑎 ) + ( 𝑎 + ( i · 𝑏 ) ) ) ) → ( ( 0 −ℝ 𝑎 ) + 0 ) = ( i · 𝑏 ) )
29	28	oveq1d	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( ( 0 −ℝ 𝑎 ) + 0 ) = ( ( 0 −ℝ 𝑎 ) + ( 𝑎 + ( i · 𝑏 ) ) ) ) → ( ( ( 0 −ℝ 𝑎 ) + 0 ) · 0 ) = ( ( i · 𝑏 ) · 0 ) )
30		elre0re	⊢ ( 𝑎 ∈ ℝ → 0 ∈ ℝ )
31	13 30	readdcld	⊢ ( 𝑎 ∈ ℝ → ( ( 0 −ℝ 𝑎 ) + 0 ) ∈ ℝ )
32	31	ad2antrr	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( ( 0 −ℝ 𝑎 ) + 0 ) = ( ( 0 −ℝ 𝑎 ) + ( 𝑎 + ( i · 𝑏 ) ) ) ) → ( ( 0 −ℝ 𝑎 ) + 0 ) ∈ ℝ )
33		remul01	⊢ ( ( ( 0 −ℝ 𝑎 ) + 0 ) ∈ ℝ → ( ( ( 0 −ℝ 𝑎 ) + 0 ) · 0 ) = 0 )
34	32 33	syl	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( ( 0 −ℝ 𝑎 ) + 0 ) = ( ( 0 −ℝ 𝑎 ) + ( 𝑎 + ( i · 𝑏 ) ) ) ) → ( ( ( 0 −ℝ 𝑎 ) + 0 ) · 0 ) = 0 )
35	29 34	eqtr3d	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( ( 0 −ℝ 𝑎 ) + 0 ) = ( ( 0 −ℝ 𝑎 ) + ( 𝑎 + ( i · 𝑏 ) ) ) ) → ( ( i · 𝑏 ) · 0 ) = 0 )
36	12 35	eqtr3d	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( ( 0 −ℝ 𝑎 ) + 0 ) = ( ( 0 −ℝ 𝑎 ) + ( 𝑎 + ( i · 𝑏 ) ) ) ) → ( i · 0 ) = 0 )
37	36	ex	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( ( ( 0 −ℝ 𝑎 ) + 0 ) = ( ( 0 −ℝ 𝑎 ) + ( 𝑎 + ( i · 𝑏 ) ) ) → ( i · 0 ) = 0 ) )
38	3 37	syl5	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( 0 = ( 𝑎 + ( i · 𝑏 ) ) → ( i · 0 ) = 0 ) )
39	38	rexlimivv	⊢ ( ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ 0 = ( 𝑎 + ( i · 𝑏 ) ) → ( i · 0 ) = 0 )
40	1 2 39	mp2b	⊢ ( i · 0 ) = 0