This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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