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

Metamath Proof Explorer

Theorem sn-0tie0

Description: Lemma for sn-mul02 . Commuted version of sn-it0e0 . (Contributed by SN, 30-Jun-2024)

Ref Expression
Assertion sn-0tie0 ( 0 · i ) = 0

Proof

Step Hyp Ref Expression
1 0cn ⊢ 0 ∈ ℂ
2 ax-icn ⊢ i ∈ ℂ
3 1 2 mulcli ⊢ ( 0 · i ) ∈ ℂ
4 cnre ⊢ ( ( 0 · i ) ∈ ℂ → ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) )
5 simplr ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) )
6 neqne ⊢ ( ¬ ( 0 · i ) = 0 → ( 0 · i ) ≠ 0 )
7 6 adantl ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 0 · i ) ≠ 0 )
8 simplll ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → 𝑎 ∈ ℝ )
9 rernegcl ⊢ ( 𝑎 ∈ ℝ → ( 0 −ℝ 𝑎 ) ∈ ℝ )
10 8 9 syl ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 0 −ℝ 𝑎 ) ∈ ℝ )
11 1red ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → 1 ∈ ℝ )
12 10 11 readdcld ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 0 −ℝ 𝑎 ) + 1 ) ∈ ℝ )
13 ax-rrecex ⊢ ( ( ( ( 0 −ℝ 𝑎 ) + 1 ) ∈ ℝ ∧ ( ( 0 −ℝ 𝑎 ) + 1 ) ≠ 0 ) → ∃ 𝑥 ∈ ℝ ( ( ( 0 −ℝ 𝑎 ) + 1 ) · 𝑥 ) = 1 )
14 12 13 sylan ⊢ ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( ( 0 −ℝ 𝑎 ) + 1 ) ≠ 0 ) → ∃ 𝑥 ∈ ℝ ( ( ( 0 −ℝ 𝑎 ) + 1 ) · 𝑥 ) = 1 )
15 2 a1i ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → i ∈ ℂ )
16 10 recnd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 0 −ℝ 𝑎 ) ∈ ℂ )
17 1cnd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → 1 ∈ ℂ )
18 15 16 17 adddid ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( i · ( ( 0 −ℝ 𝑎 ) + 1 ) ) = ( ( i · ( 0 −ℝ 𝑎 ) ) + ( i · 1 ) ) )
19 sn-it1ei ⊢ ( i · 1 ) = i
20 19 oveq2i ⊢ ( ( i · ( 0 −ℝ 𝑎 ) ) + ( i · 1 ) ) = ( ( i · ( 0 −ℝ 𝑎 ) ) + i )
21 18 20 eqtrdi ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( i · ( ( 0 −ℝ 𝑎 ) + 1 ) ) = ( ( i · ( 0 −ℝ 𝑎 ) ) + i ) )
22 21 oveq2d ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 0 · ( i · ( ( 0 −ℝ 𝑎 ) + 1 ) ) ) = ( 0 · ( ( i · ( 0 −ℝ 𝑎 ) ) + i ) ) )
23 0cnd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → 0 ∈ ℂ )
24 15 16 mulcld ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( i · ( 0 −ℝ 𝑎 ) ) ∈ ℂ )
25 23 24 15 adddid ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 0 · ( ( i · ( 0 −ℝ 𝑎 ) ) + i ) ) = ( ( 0 · ( i · ( 0 −ℝ 𝑎 ) ) ) + ( 0 · i ) ) )
26 22 25 eqtrd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 0 · ( i · ( ( 0 −ℝ 𝑎 ) + 1 ) ) ) = ( ( 0 · ( i · ( 0 −ℝ 𝑎 ) ) ) + ( 0 · i ) ) )
27 5 oveq2d ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 0 −ℝ 𝑎 ) + ( 0 · i ) ) = ( ( 0 −ℝ 𝑎 ) + ( 𝑎 + ( i · 𝑏 ) ) ) )
28 renegid2 ⊢ ( 𝑎 ∈ ℝ → ( ( 0 −ℝ 𝑎 ) + 𝑎 ) = 0 )
29 28 ad3antrrr ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 0 −ℝ 𝑎 ) + 𝑎 ) = 0 )
30 29 oveq1d ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( ( 0 −ℝ 𝑎 ) + 𝑎 ) + ( i · 𝑏 ) ) = ( 0 + ( i · 𝑏 ) ) )
31 8 recnd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → 𝑎 ∈ ℂ )
32 simpllr ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → 𝑏 ∈ ℝ )
33 32 recnd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → 𝑏 ∈ ℂ )
34 15 33 mulcld ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( i · 𝑏 ) ∈ ℂ )
35 16 31 34 addassd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( ( 0 −ℝ 𝑎 ) + 𝑎 ) + ( i · 𝑏 ) ) = ( ( 0 −ℝ 𝑎 ) + ( 𝑎 + ( i · 𝑏 ) ) ) )
36 sn-addlid ⊢ ( ( i · 𝑏 ) ∈ ℂ → ( 0 + ( i · 𝑏 ) ) = ( i · 𝑏 ) )
37 34 36 syl ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 0 + ( i · 𝑏 ) ) = ( i · 𝑏 ) )
38 30 35 37 3eqtr3d ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 0 −ℝ 𝑎 ) + ( 𝑎 + ( i · 𝑏 ) ) ) = ( i · 𝑏 ) )
39 27 38 eqtrd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 0 −ℝ 𝑎 ) + ( 0 · i ) ) = ( i · 𝑏 ) )
40 39 oveq2d ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 0 · i ) · ( ( 0 −ℝ 𝑎 ) + ( 0 · i ) ) ) = ( ( 0 · i ) · ( i · 𝑏 ) ) )
41 3 a1i ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 0 · i ) ∈ ℂ )
42 41 16 41 adddid ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 0 · i ) · ( ( 0 −ℝ 𝑎 ) + ( 0 · i ) ) ) = ( ( ( 0 · i ) · ( 0 −ℝ 𝑎 ) ) + ( ( 0 · i ) · ( 0 · i ) ) ) )
43 23 15 16 mulassd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 0 · i ) · ( 0 −ℝ 𝑎 ) ) = ( 0 · ( i · ( 0 −ℝ 𝑎 ) ) ) )
44 41 23 15 mulassd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( ( 0 · i ) · 0 ) · i ) = ( ( 0 · i ) · ( 0 · i ) ) )
45 sn-mul01 ⊢ ( ( 0 · i ) ∈ ℂ → ( ( 0 · i ) · 0 ) = 0 )
46 41 45 syl ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 0 · i ) · 0 ) = 0 )
47 46 oveq1d ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( ( 0 · i ) · 0 ) · i ) = ( 0 · i ) )
48 44 47 eqtr3d ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 0 · i ) · ( 0 · i ) ) = ( 0 · i ) )
49 43 48 oveq12d ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( ( 0 · i ) · ( 0 −ℝ 𝑎 ) ) + ( ( 0 · i ) · ( 0 · i ) ) ) = ( ( 0 · ( i · ( 0 −ℝ 𝑎 ) ) ) + ( 0 · i ) ) )
50 42 49 eqtrd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 0 · i ) · ( ( 0 −ℝ 𝑎 ) + ( 0 · i ) ) ) = ( ( 0 · ( i · ( 0 −ℝ 𝑎 ) ) ) + ( 0 · i ) ) )
51 23 15 34 mulassd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 0 · i ) · ( i · 𝑏 ) ) = ( 0 · ( i · ( i · 𝑏 ) ) ) )
52 15 15 33 mulassd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( i · i ) · 𝑏 ) = ( i · ( i · 𝑏 ) ) )
53 reixi ⊢ ( i · i ) = ( 0 −ℝ 1 )
54 1re ⊢ 1 ∈ ℝ
55 rernegcl ⊢ ( 1 ∈ ℝ → ( 0 −ℝ 1 ) ∈ ℝ )
56 54 55 ax-mp ⊢ ( 0 −ℝ 1 ) ∈ ℝ
57 53 56 eqeltri ⊢ ( i · i ) ∈ ℝ
58 57 a1i ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( i · i ) ∈ ℝ )
59 58 32 remulcld ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( i · i ) · 𝑏 ) ∈ ℝ )
60 52 59 eqeltrrd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( i · ( i · 𝑏 ) ) ∈ ℝ )
61 remul02 ⊢ ( ( i · ( i · 𝑏 ) ) ∈ ℝ → ( 0 · ( i · ( i · 𝑏 ) ) ) = 0 )
62 60 61 syl ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 0 · ( i · ( i · 𝑏 ) ) ) = 0 )
63 51 62 eqtrd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 0 · i ) · ( i · 𝑏 ) ) = 0 )
64 40 50 63 3eqtr3d ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 0 · ( i · ( 0 −ℝ 𝑎 ) ) ) + ( 0 · i ) ) = 0 )
65 26 64 eqtrd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 0 · ( i · ( ( 0 −ℝ 𝑎 ) + 1 ) ) ) = 0 )
66 65 ad2antrr ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( ( 0 −ℝ 𝑎 ) + 1 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( ( 0 −ℝ 𝑎 ) + 1 ) · 𝑥 ) = 1 ) ) → ( 0 · ( i · ( ( 0 −ℝ 𝑎 ) + 1 ) ) ) = 0 )
67 66 oveq1d ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( ( 0 −ℝ 𝑎 ) + 1 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( ( 0 −ℝ 𝑎 ) + 1 ) · 𝑥 ) = 1 ) ) → ( ( 0 · ( i · ( ( 0 −ℝ 𝑎 ) + 1 ) ) ) · 𝑥 ) = ( 0 · 𝑥 ) )
68 0cnd ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( ( 0 −ℝ 𝑎 ) + 1 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( ( 0 −ℝ 𝑎 ) + 1 ) · 𝑥 ) = 1 ) ) → 0 ∈ ℂ )
69 2 a1i ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( ( 0 −ℝ 𝑎 ) + 1 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( ( 0 −ℝ 𝑎 ) + 1 ) · 𝑥 ) = 1 ) ) → i ∈ ℂ )
70 10 ad2antrr ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( ( 0 −ℝ 𝑎 ) + 1 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( ( 0 −ℝ 𝑎 ) + 1 ) · 𝑥 ) = 1 ) ) → ( 0 −ℝ 𝑎 ) ∈ ℝ )
71 70 recnd ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( ( 0 −ℝ 𝑎 ) + 1 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( ( 0 −ℝ 𝑎 ) + 1 ) · 𝑥 ) = 1 ) ) → ( 0 −ℝ 𝑎 ) ∈ ℂ )
72 1cnd ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( ( 0 −ℝ 𝑎 ) + 1 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( ( 0 −ℝ 𝑎 ) + 1 ) · 𝑥 ) = 1 ) ) → 1 ∈ ℂ )
73 71 72 addcld ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( ( 0 −ℝ 𝑎 ) + 1 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( ( 0 −ℝ 𝑎 ) + 1 ) · 𝑥 ) = 1 ) ) → ( ( 0 −ℝ 𝑎 ) + 1 ) ∈ ℂ )
74 69 73 mulcld ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( ( 0 −ℝ 𝑎 ) + 1 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( ( 0 −ℝ 𝑎 ) + 1 ) · 𝑥 ) = 1 ) ) → ( i · ( ( 0 −ℝ 𝑎 ) + 1 ) ) ∈ ℂ )
75 simprl ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( ( 0 −ℝ 𝑎 ) + 1 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( ( 0 −ℝ 𝑎 ) + 1 ) · 𝑥 ) = 1 ) ) → 𝑥 ∈ ℝ )
76 75 recnd ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( ( 0 −ℝ 𝑎 ) + 1 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( ( 0 −ℝ 𝑎 ) + 1 ) · 𝑥 ) = 1 ) ) → 𝑥 ∈ ℂ )
77 68 74 76 mulassd ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( ( 0 −ℝ 𝑎 ) + 1 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( ( 0 −ℝ 𝑎 ) + 1 ) · 𝑥 ) = 1 ) ) → ( ( 0 · ( i · ( ( 0 −ℝ 𝑎 ) + 1 ) ) ) · 𝑥 ) = ( 0 · ( ( i · ( ( 0 −ℝ 𝑎 ) + 1 ) ) · 𝑥 ) ) )
78 69 73 76 mulassd ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( ( 0 −ℝ 𝑎 ) + 1 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( ( 0 −ℝ 𝑎 ) + 1 ) · 𝑥 ) = 1 ) ) → ( ( i · ( ( 0 −ℝ 𝑎 ) + 1 ) ) · 𝑥 ) = ( i · ( ( ( 0 −ℝ 𝑎 ) + 1 ) · 𝑥 ) ) )
79 simprr ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( ( 0 −ℝ 𝑎 ) + 1 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( ( 0 −ℝ 𝑎 ) + 1 ) · 𝑥 ) = 1 ) ) → ( ( ( 0 −ℝ 𝑎 ) + 1 ) · 𝑥 ) = 1 )
80 79 oveq2d ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( ( 0 −ℝ 𝑎 ) + 1 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( ( 0 −ℝ 𝑎 ) + 1 ) · 𝑥 ) = 1 ) ) → ( i · ( ( ( 0 −ℝ 𝑎 ) + 1 ) · 𝑥 ) ) = ( i · 1 ) )
81 80 19 eqtrdi ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( ( 0 −ℝ 𝑎 ) + 1 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( ( 0 −ℝ 𝑎 ) + 1 ) · 𝑥 ) = 1 ) ) → ( i · ( ( ( 0 −ℝ 𝑎 ) + 1 ) · 𝑥 ) ) = i )
82 78 81 eqtrd ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( ( 0 −ℝ 𝑎 ) + 1 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( ( 0 −ℝ 𝑎 ) + 1 ) · 𝑥 ) = 1 ) ) → ( ( i · ( ( 0 −ℝ 𝑎 ) + 1 ) ) · 𝑥 ) = i )
83 82 oveq2d ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( ( 0 −ℝ 𝑎 ) + 1 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( ( 0 −ℝ 𝑎 ) + 1 ) · 𝑥 ) = 1 ) ) → ( 0 · ( ( i · ( ( 0 −ℝ 𝑎 ) + 1 ) ) · 𝑥 ) ) = ( 0 · i ) )
84 77 83 eqtrd ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( ( 0 −ℝ 𝑎 ) + 1 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( ( 0 −ℝ 𝑎 ) + 1 ) · 𝑥 ) = 1 ) ) → ( ( 0 · ( i · ( ( 0 −ℝ 𝑎 ) + 1 ) ) ) · 𝑥 ) = ( 0 · i ) )
85 remul02 ⊢ ( 𝑥 ∈ ℝ → ( 0 · 𝑥 ) = 0 )
86 75 85 syl ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( ( 0 −ℝ 𝑎 ) + 1 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( ( 0 −ℝ 𝑎 ) + 1 ) · 𝑥 ) = 1 ) ) → ( 0 · 𝑥 ) = 0 )
87 67 84 86 3eqtr3d ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( ( 0 −ℝ 𝑎 ) + 1 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( ( 0 −ℝ 𝑎 ) + 1 ) · 𝑥 ) = 1 ) ) → ( 0 · i ) = 0 )
88 14 87 rexlimddv ⊢ ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( ( 0 −ℝ 𝑎 ) + 1 ) ≠ 0 ) → ( 0 · i ) = 0 )
89 88 ex ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( ( 0 −ℝ 𝑎 ) + 1 ) ≠ 0 → ( 0 · i ) = 0 ) )
90 89 necon1d ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 0 · i ) ≠ 0 → ( ( 0 −ℝ 𝑎 ) + 1 ) = 0 ) )
91 7 90 mpd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 0 −ℝ 𝑎 ) + 1 ) = 0 )
92 91 oveq2d ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 𝑎 + ( ( 0 −ℝ 𝑎 ) + 1 ) ) = ( 𝑎 + 0 ) )
93 31 16 17 addassd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 𝑎 + ( 0 −ℝ 𝑎 ) ) + 1 ) = ( 𝑎 + ( ( 0 −ℝ 𝑎 ) + 1 ) ) )
94 renegid ⊢ ( 𝑎 ∈ ℝ → ( 𝑎 + ( 0 −ℝ 𝑎 ) ) = 0 )
95 8 94 syl ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 𝑎 + ( 0 −ℝ 𝑎 ) ) = 0 )
96 95 oveq1d ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 𝑎 + ( 0 −ℝ 𝑎 ) ) + 1 ) = ( 0 + 1 ) )
97 readdlid ⊢ ( 1 ∈ ℝ → ( 0 + 1 ) = 1 )
98 54 97 ax-mp ⊢ ( 0 + 1 ) = 1
99 96 98 eqtrdi ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 𝑎 + ( 0 −ℝ 𝑎 ) ) + 1 ) = 1 )
100 93 99 eqtr3d ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 𝑎 + ( ( 0 −ℝ 𝑎 ) + 1 ) ) = 1 )
101 readdrid ⊢ ( 𝑎 ∈ ℝ → ( 𝑎 + 0 ) = 𝑎 )
102 8 101 syl ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 𝑎 + 0 ) = 𝑎 )
103 92 100 102 3eqtr3rd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → 𝑎 = 1 )
104 rernegcl ⊢ ( 𝑏 ∈ ℝ → ( 0 −ℝ 𝑏 ) ∈ ℝ )
105 32 104 syl ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 0 −ℝ 𝑏 ) ∈ ℝ )
106 11 105 readdcld ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 1 + ( 0 −ℝ 𝑏 ) ) ∈ ℝ )
107 ax-rrecex ⊢ ( ( ( 1 + ( 0 −ℝ 𝑏 ) ) ∈ ℝ ∧ ( 1 + ( 0 −ℝ 𝑏 ) ) ≠ 0 ) → ∃ 𝑦 ∈ ℝ ( ( 1 + ( 0 −ℝ 𝑏 ) ) · 𝑦 ) = 1 )
108 106 107 sylan ⊢ ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( 1 + ( 0 −ℝ 𝑏 ) ) ≠ 0 ) → ∃ 𝑦 ∈ ℝ ( ( 1 + ( 0 −ℝ 𝑏 ) ) · 𝑦 ) = 1 )
109 105 recnd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 0 −ℝ 𝑏 ) ∈ ℂ )
110 15 109 mulcld ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( i · ( 0 −ℝ 𝑏 ) ) ∈ ℂ )
111 23 15 110 adddid ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 0 · ( i + ( i · ( 0 −ℝ 𝑏 ) ) ) ) = ( ( 0 · i ) + ( 0 · ( i · ( 0 −ℝ 𝑏 ) ) ) ) )
112 0re ⊢ 0 ∈ ℝ
113 remul02 ⊢ ( 0 ∈ ℝ → ( 0 · 0 ) = 0 )
114 112 113 ax-mp ⊢ ( 0 · 0 ) = 0
115 114 oveq1i ⊢ ( ( 0 · 0 ) · i ) = ( 0 · i )
116 1 1 2 mulassi ⊢ ( ( 0 · 0 ) · i ) = ( 0 · ( 0 · i ) )
117 115 116 eqtr3i ⊢ ( 0 · i ) = ( 0 · ( 0 · i ) )
118 117 a1i ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 0 · i ) = ( 0 · ( 0 · i ) ) )
119 118 oveq1d ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 0 · i ) + ( 0 · ( i · ( 0 −ℝ 𝑏 ) ) ) ) = ( ( 0 · ( 0 · i ) ) + ( 0 · ( i · ( 0 −ℝ 𝑏 ) ) ) ) )
120 111 119 eqtrd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 0 · ( i + ( i · ( 0 −ℝ 𝑏 ) ) ) ) = ( ( 0 · ( 0 · i ) ) + ( 0 · ( i · ( 0 −ℝ 𝑏 ) ) ) ) )
121 15 17 109 adddid ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( i · ( 1 + ( 0 −ℝ 𝑏 ) ) ) = ( ( i · 1 ) + ( i · ( 0 −ℝ 𝑏 ) ) ) )
122 19 a1i ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( i · 1 ) = i )
123 122 oveq1d ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( i · 1 ) + ( i · ( 0 −ℝ 𝑏 ) ) ) = ( i + ( i · ( 0 −ℝ 𝑏 ) ) ) )
124 121 123 eqtrd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( i · ( 1 + ( 0 −ℝ 𝑏 ) ) ) = ( i + ( i · ( 0 −ℝ 𝑏 ) ) ) )
125 124 oveq2d ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 0 · ( i · ( 1 + ( 0 −ℝ 𝑏 ) ) ) ) = ( 0 · ( i + ( i · ( 0 −ℝ 𝑏 ) ) ) ) )
126 23 41 110 adddid ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 0 · ( ( 0 · i ) + ( i · ( 0 −ℝ 𝑏 ) ) ) ) = ( ( 0 · ( 0 · i ) ) + ( 0 · ( i · ( 0 −ℝ 𝑏 ) ) ) ) )
127 120 125 126 3eqtr4d ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 0 · ( i · ( 1 + ( 0 −ℝ 𝑏 ) ) ) ) = ( 0 · ( ( 0 · i ) + ( i · ( 0 −ℝ 𝑏 ) ) ) ) )
128 103 oveq1d ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 𝑎 + ( i · 𝑏 ) ) = ( 1 + ( i · 𝑏 ) ) )
129 5 128 eqtrd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 0 · i ) = ( 1 + ( i · 𝑏 ) ) )
130 129 oveq1d ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 0 · i ) + ( i · ( 0 −ℝ 𝑏 ) ) ) = ( ( 1 + ( i · 𝑏 ) ) + ( i · ( 0 −ℝ 𝑏 ) ) ) )
131 17 34 110 addassd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 1 + ( i · 𝑏 ) ) + ( i · ( 0 −ℝ 𝑏 ) ) ) = ( 1 + ( ( i · 𝑏 ) + ( i · ( 0 −ℝ 𝑏 ) ) ) ) )
132 renegid ⊢ ( 𝑏 ∈ ℝ → ( 𝑏 + ( 0 −ℝ 𝑏 ) ) = 0 )
133 32 132 syl ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 𝑏 + ( 0 −ℝ 𝑏 ) ) = 0 )
134 133 oveq2d ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( i · ( 𝑏 + ( 0 −ℝ 𝑏 ) ) ) = ( i · 0 ) )
135 15 33 109 adddid ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( i · ( 𝑏 + ( 0 −ℝ 𝑏 ) ) ) = ( ( i · 𝑏 ) + ( i · ( 0 −ℝ 𝑏 ) ) ) )
136 sn-mul01 ⊢ ( i ∈ ℂ → ( i · 0 ) = 0 )
137 2 136 mp1i ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( i · 0 ) = 0 )
138 134 135 137 3eqtr3d ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( i · 𝑏 ) + ( i · ( 0 −ℝ 𝑏 ) ) ) = 0 )
139 138 oveq2d ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 1 + ( ( i · 𝑏 ) + ( i · ( 0 −ℝ 𝑏 ) ) ) ) = ( 1 + 0 ) )
140 readdrid ⊢ ( 1 ∈ ℝ → ( 1 + 0 ) = 1 )
141 54 140 ax-mp ⊢ ( 1 + 0 ) = 1
142 139 141 eqtrdi ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 1 + ( ( i · 𝑏 ) + ( i · ( 0 −ℝ 𝑏 ) ) ) ) = 1 )
143 131 142 eqtrd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 1 + ( i · 𝑏 ) ) + ( i · ( 0 −ℝ 𝑏 ) ) ) = 1 )
144 130 143 eqtrd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 0 · i ) + ( i · ( 0 −ℝ 𝑏 ) ) ) = 1 )
145 144 oveq2d ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 0 · ( ( 0 · i ) + ( i · ( 0 −ℝ 𝑏 ) ) ) ) = ( 0 · 1 ) )
146 127 145 eqtrd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 0 · ( i · ( 1 + ( 0 −ℝ 𝑏 ) ) ) ) = ( 0 · 1 ) )
147 ax-1rid ⊢ ( 0 ∈ ℝ → ( 0 · 1 ) = 0 )
148 112 147 ax-mp ⊢ ( 0 · 1 ) = 0
149 146 148 eqtrdi ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 0 · ( i · ( 1 + ( 0 −ℝ 𝑏 ) ) ) ) = 0 )
150 149 ad2antrr ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( 1 + ( 0 −ℝ 𝑏 ) ) ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 1 + ( 0 −ℝ 𝑏 ) ) · 𝑦 ) = 1 ) ) → ( 0 · ( i · ( 1 + ( 0 −ℝ 𝑏 ) ) ) ) = 0 )
151 150 oveq1d ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( 1 + ( 0 −ℝ 𝑏 ) ) ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 1 + ( 0 −ℝ 𝑏 ) ) · 𝑦 ) = 1 ) ) → ( ( 0 · ( i · ( 1 + ( 0 −ℝ 𝑏 ) ) ) ) · 𝑦 ) = ( 0 · 𝑦 ) )
152 0cnd ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( 1 + ( 0 −ℝ 𝑏 ) ) ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 1 + ( 0 −ℝ 𝑏 ) ) · 𝑦 ) = 1 ) ) → 0 ∈ ℂ )
153 2 a1i ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( 1 + ( 0 −ℝ 𝑏 ) ) ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 1 + ( 0 −ℝ 𝑏 ) ) · 𝑦 ) = 1 ) ) → i ∈ ℂ )
154 1cnd ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( 1 + ( 0 −ℝ 𝑏 ) ) ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 1 + ( 0 −ℝ 𝑏 ) ) · 𝑦 ) = 1 ) ) → 1 ∈ ℂ )
155 109 ad2antrr ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( 1 + ( 0 −ℝ 𝑏 ) ) ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 1 + ( 0 −ℝ 𝑏 ) ) · 𝑦 ) = 1 ) ) → ( 0 −ℝ 𝑏 ) ∈ ℂ )
156 154 155 addcld ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( 1 + ( 0 −ℝ 𝑏 ) ) ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 1 + ( 0 −ℝ 𝑏 ) ) · 𝑦 ) = 1 ) ) → ( 1 + ( 0 −ℝ 𝑏 ) ) ∈ ℂ )
157 153 156 mulcld ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( 1 + ( 0 −ℝ 𝑏 ) ) ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 1 + ( 0 −ℝ 𝑏 ) ) · 𝑦 ) = 1 ) ) → ( i · ( 1 + ( 0 −ℝ 𝑏 ) ) ) ∈ ℂ )
158 simprl ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( 1 + ( 0 −ℝ 𝑏 ) ) ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 1 + ( 0 −ℝ 𝑏 ) ) · 𝑦 ) = 1 ) ) → 𝑦 ∈ ℝ )
159 158 recnd ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( 1 + ( 0 −ℝ 𝑏 ) ) ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 1 + ( 0 −ℝ 𝑏 ) ) · 𝑦 ) = 1 ) ) → 𝑦 ∈ ℂ )
160 152 157 159 mulassd ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( 1 + ( 0 −ℝ 𝑏 ) ) ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 1 + ( 0 −ℝ 𝑏 ) ) · 𝑦 ) = 1 ) ) → ( ( 0 · ( i · ( 1 + ( 0 −ℝ 𝑏 ) ) ) ) · 𝑦 ) = ( 0 · ( ( i · ( 1 + ( 0 −ℝ 𝑏 ) ) ) · 𝑦 ) ) )
161 153 156 159 mulassd ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( 1 + ( 0 −ℝ 𝑏 ) ) ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 1 + ( 0 −ℝ 𝑏 ) ) · 𝑦 ) = 1 ) ) → ( ( i · ( 1 + ( 0 −ℝ 𝑏 ) ) ) · 𝑦 ) = ( i · ( ( 1 + ( 0 −ℝ 𝑏 ) ) · 𝑦 ) ) )
162 simprr ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( 1 + ( 0 −ℝ 𝑏 ) ) ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 1 + ( 0 −ℝ 𝑏 ) ) · 𝑦 ) = 1 ) ) → ( ( 1 + ( 0 −ℝ 𝑏 ) ) · 𝑦 ) = 1 )
163 162 oveq2d ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( 1 + ( 0 −ℝ 𝑏 ) ) ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 1 + ( 0 −ℝ 𝑏 ) ) · 𝑦 ) = 1 ) ) → ( i · ( ( 1 + ( 0 −ℝ 𝑏 ) ) · 𝑦 ) ) = ( i · 1 ) )
164 163 19 eqtrdi ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( 1 + ( 0 −ℝ 𝑏 ) ) ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 1 + ( 0 −ℝ 𝑏 ) ) · 𝑦 ) = 1 ) ) → ( i · ( ( 1 + ( 0 −ℝ 𝑏 ) ) · 𝑦 ) ) = i )
165 161 164 eqtrd ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( 1 + ( 0 −ℝ 𝑏 ) ) ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 1 + ( 0 −ℝ 𝑏 ) ) · 𝑦 ) = 1 ) ) → ( ( i · ( 1 + ( 0 −ℝ 𝑏 ) ) ) · 𝑦 ) = i )
166 165 oveq2d ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( 1 + ( 0 −ℝ 𝑏 ) ) ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 1 + ( 0 −ℝ 𝑏 ) ) · 𝑦 ) = 1 ) ) → ( 0 · ( ( i · ( 1 + ( 0 −ℝ 𝑏 ) ) ) · 𝑦 ) ) = ( 0 · i ) )
167 160 166 eqtrd ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( 1 + ( 0 −ℝ 𝑏 ) ) ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 1 + ( 0 −ℝ 𝑏 ) ) · 𝑦 ) = 1 ) ) → ( ( 0 · ( i · ( 1 + ( 0 −ℝ 𝑏 ) ) ) ) · 𝑦 ) = ( 0 · i ) )
168 remul02 ⊢ ( 𝑦 ∈ ℝ → ( 0 · 𝑦 ) = 0 )
169 158 168 syl ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( 1 + ( 0 −ℝ 𝑏 ) ) ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 1 + ( 0 −ℝ 𝑏 ) ) · 𝑦 ) = 1 ) ) → ( 0 · 𝑦 ) = 0 )
170 151 167 169 3eqtr3d ⊢ ( ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( 1 + ( 0 −ℝ 𝑏 ) ) ≠ 0 ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 1 + ( 0 −ℝ 𝑏 ) ) · 𝑦 ) = 1 ) ) → ( 0 · i ) = 0 )
171 108 170 rexlimddv ⊢ ( ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) ∧ ( 1 + ( 0 −ℝ 𝑏 ) ) ≠ 0 ) → ( 0 · i ) = 0 )
172 171 ex ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 1 + ( 0 −ℝ 𝑏 ) ) ≠ 0 → ( 0 · i ) = 0 ) )
173 172 necon1d ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 0 · i ) ≠ 0 → ( 1 + ( 0 −ℝ 𝑏 ) ) = 0 ) )
174 7 173 mpd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 1 + ( 0 −ℝ 𝑏 ) ) = 0 )
175 174 oveq1d ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 1 + ( 0 −ℝ 𝑏 ) ) + 𝑏 ) = ( 0 + 𝑏 ) )
176 17 109 33 addassd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 1 + ( 0 −ℝ 𝑏 ) ) + 𝑏 ) = ( 1 + ( ( 0 −ℝ 𝑏 ) + 𝑏 ) ) )
177 renegid2 ⊢ ( 𝑏 ∈ ℝ → ( ( 0 −ℝ 𝑏 ) + 𝑏 ) = 0 )
178 32 177 syl ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 0 −ℝ 𝑏 ) + 𝑏 ) = 0 )
179 178 oveq2d ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 1 + ( ( 0 −ℝ 𝑏 ) + 𝑏 ) ) = ( 1 + 0 ) )
180 179 141 eqtrdi ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 1 + ( ( 0 −ℝ 𝑏 ) + 𝑏 ) ) = 1 )
181 176 180 eqtrd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( ( 1 + ( 0 −ℝ 𝑏 ) ) + 𝑏 ) = 1 )
182 readdlid ⊢ ( 𝑏 ∈ ℝ → ( 0 + 𝑏 ) = 𝑏 )
183 32 182 syl ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 0 + 𝑏 ) = 𝑏 )
184 175 181 183 3eqtr3rd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → 𝑏 = 1 )
185 184 oveq2d ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( i · 𝑏 ) = ( i · 1 ) )
186 103 185 oveq12d ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 𝑎 + ( i · 𝑏 ) ) = ( 1 + ( i · 1 ) ) )
187 5 186 eqtrd ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 0 · i ) = ( 1 + ( i · 1 ) ) )
188 19 oveq2i ⊢ ( 1 + ( i · 1 ) ) = ( 1 + i )
189 188 eqeq2i ⊢ ( ( 0 · i ) = ( 1 + ( i · 1 ) ) ↔ ( 0 · i ) = ( 1 + i ) )
190 oveq2 ⊢ ( ( 0 · i ) = ( 1 + i ) → ( ( ( i · i ) · i ) · ( 0 · i ) ) = ( ( ( i · i ) · i ) · ( 1 + i ) ) )
191 2 2 mulcli ⊢ ( i · i ) ∈ ℂ
192 191 2 mulcli ⊢ ( ( i · i ) · i ) ∈ ℂ
193 192 1 2 mulassi ⊢ ( ( ( ( i · i ) · i ) · 0 ) · i ) = ( ( ( i · i ) · i ) · ( 0 · i ) )
194 sn-mul01 ⊢ ( ( ( i · i ) · i ) ∈ ℂ → ( ( ( i · i ) · i ) · 0 ) = 0 )
195 192 194 ax-mp ⊢ ( ( ( i · i ) · i ) · 0 ) = 0
196 195 oveq1i ⊢ ( ( ( ( i · i ) · i ) · 0 ) · i ) = ( 0 · i )
197 193 196 eqtr3i ⊢ ( ( ( i · i ) · i ) · ( 0 · i ) ) = ( 0 · i )
198 ax-1cn ⊢ 1 ∈ ℂ
199 192 198 2 adddii ⊢ ( ( ( i · i ) · i ) · ( 1 + i ) ) = ( ( ( ( i · i ) · i ) · 1 ) + ( ( ( i · i ) · i ) · i ) )
200 191 2 198 mulassi ⊢ ( ( ( i · i ) · i ) · 1 ) = ( ( i · i ) · ( i · 1 ) )
201 19 oveq2i ⊢ ( ( i · i ) · ( i · 1 ) ) = ( ( i · i ) · i )
202 200 201 eqtri ⊢ ( ( ( i · i ) · i ) · 1 ) = ( ( i · i ) · i )
203 191 2 2 mulassi ⊢ ( ( ( i · i ) · i ) · i ) = ( ( i · i ) · ( i · i ) )
204 rei4 ⊢ ( ( i · i ) · ( i · i ) ) = 1
205 203 204 eqtri ⊢ ( ( ( i · i ) · i ) · i ) = 1
206 202 205 oveq12i ⊢ ( ( ( ( i · i ) · i ) · 1 ) + ( ( ( i · i ) · i ) · i ) ) = ( ( ( i · i ) · i ) + 1 )
207 199 206 eqtri ⊢ ( ( ( i · i ) · i ) · ( 1 + i ) ) = ( ( ( i · i ) · i ) + 1 )
208 190 197 207 3eqtr3g ⊢ ( ( 0 · i ) = ( 1 + i ) → ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) )
209 54 54 readdcli ⊢ ( 1 + 1 ) ∈ ℝ
210 df-2 ⊢ 2 = ( 1 + 1 )
211 sn-0ne2 ⊢ 0 ≠ 2
212 211 necomi ⊢ 2 ≠ 0
213 210 212 eqnetrri ⊢ ( 1 + 1 ) ≠ 0
214 ax-rrecex ⊢ ( ( ( 1 + 1 ) ∈ ℝ ∧ ( 1 + 1 ) ≠ 0 ) → ∃ 𝑧 ∈ ℝ ( ( 1 + 1 ) · 𝑧 ) = 1 )
215 209 213 214 mp2an ⊢ ∃ 𝑧 ∈ ℝ ( ( 1 + 1 ) · 𝑧 ) = 1
216 192 198 addcli ⊢ ( ( ( i · i ) · i ) + 1 ) ∈ ℂ
217 198 2 216 addassi ⊢ ( ( 1 + i ) + ( ( ( i · i ) · i ) + 1 ) ) = ( 1 + ( i + ( ( ( i · i ) · i ) + 1 ) ) )
218 2 192 198 addassi ⊢ ( ( i + ( ( i · i ) · i ) ) + 1 ) = ( i + ( ( ( i · i ) · i ) + 1 ) )
219 218 oveq2i ⊢ ( 1 + ( ( i + ( ( i · i ) · i ) ) + 1 ) ) = ( 1 + ( i + ( ( ( i · i ) · i ) + 1 ) ) )
220 2 2 2 mulassi ⊢ ( ( i · i ) · i ) = ( i · ( i · i ) )
221 220 oveq2i ⊢ ( i + ( ( i · i ) · i ) ) = ( i + ( i · ( i · i ) ) )
222 ipiiie0 ⊢ ( i + ( i · ( i · i ) ) ) = 0
223 221 222 eqtri ⊢ ( i + ( ( i · i ) · i ) ) = 0
224 223 oveq1i ⊢ ( ( i + ( ( i · i ) · i ) ) + 1 ) = ( 0 + 1 )
225 224 98 eqtri ⊢ ( ( i + ( ( i · i ) · i ) ) + 1 ) = 1
226 225 oveq2i ⊢ ( 1 + ( ( i + ( ( i · i ) · i ) ) + 1 ) ) = ( 1 + 1 )
227 217 219 226 3eqtr2i ⊢ ( ( 1 + i ) + ( ( ( i · i ) · i ) + 1 ) ) = ( 1 + 1 )
228 227 a1i ⊢ ( ( ( 0 · i ) = ( 1 + i ) ∧ ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) ) → ( ( 1 + i ) + ( ( ( i · i ) · i ) + 1 ) ) = ( 1 + 1 ) )
229 3 198 198 adddii ⊢ ( ( 0 · i ) · ( 1 + 1 ) ) = ( ( ( 0 · i ) · 1 ) + ( ( 0 · i ) · 1 ) )
230 1 2 198 mulassi ⊢ ( ( 0 · i ) · 1 ) = ( 0 · ( i · 1 ) )
231 19 oveq2i ⊢ ( 0 · ( i · 1 ) ) = ( 0 · i )
232 230 231 eqtri ⊢ ( ( 0 · i ) · 1 ) = ( 0 · i )
233 simpl ⊢ ( ( ( 0 · i ) = ( 1 + i ) ∧ ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) ) → ( 0 · i ) = ( 1 + i ) )
234 232 233 eqtrid ⊢ ( ( ( 0 · i ) = ( 1 + i ) ∧ ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) ) → ( ( 0 · i ) · 1 ) = ( 1 + i ) )
235 simpr ⊢ ( ( ( 0 · i ) = ( 1 + i ) ∧ ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) ) → ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) )
236 232 235 eqtrid ⊢ ( ( ( 0 · i ) = ( 1 + i ) ∧ ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) ) → ( ( 0 · i ) · 1 ) = ( ( ( i · i ) · i ) + 1 ) )
237 234 236 oveq12d ⊢ ( ( ( 0 · i ) = ( 1 + i ) ∧ ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) ) → ( ( ( 0 · i ) · 1 ) + ( ( 0 · i ) · 1 ) ) = ( ( 1 + i ) + ( ( ( i · i ) · i ) + 1 ) ) )
238 229 237 eqtrid ⊢ ( ( ( 0 · i ) = ( 1 + i ) ∧ ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) ) → ( ( 0 · i ) · ( 1 + 1 ) ) = ( ( 1 + i ) + ( ( ( i · i ) · i ) + 1 ) ) )
239 remullid ⊢ ( ( 1 + 1 ) ∈ ℝ → ( 1 · ( 1 + 1 ) ) = ( 1 + 1 ) )
240 209 239 mp1i ⊢ ( ( ( 0 · i ) = ( 1 + i ) ∧ ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) ) → ( 1 · ( 1 + 1 ) ) = ( 1 + 1 ) )
241 228 238 240 3eqtr4d ⊢ ( ( ( 0 · i ) = ( 1 + i ) ∧ ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) ) → ( ( 0 · i ) · ( 1 + 1 ) ) = ( 1 · ( 1 + 1 ) ) )
242 241 oveq1d ⊢ ( ( ( 0 · i ) = ( 1 + i ) ∧ ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) ) → ( ( ( 0 · i ) · ( 1 + 1 ) ) · 𝑧 ) = ( ( 1 · ( 1 + 1 ) ) · 𝑧 ) )
243 242 adantr ⊢ ( ( ( ( 0 · i ) = ( 1 + i ) ∧ ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 1 + 1 ) · 𝑧 ) = 1 ) ) → ( ( ( 0 · i ) · ( 1 + 1 ) ) · 𝑧 ) = ( ( 1 · ( 1 + 1 ) ) · 𝑧 ) )
244 3 a1i ⊢ ( ( ( ( 0 · i ) = ( 1 + i ) ∧ ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 1 + 1 ) · 𝑧 ) = 1 ) ) → ( 0 · i ) ∈ ℂ )
245 1cnd ⊢ ( ( ( ( 0 · i ) = ( 1 + i ) ∧ ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 1 + 1 ) · 𝑧 ) = 1 ) ) → 1 ∈ ℂ )
246 245 245 addcld ⊢ ( ( ( ( 0 · i ) = ( 1 + i ) ∧ ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 1 + 1 ) · 𝑧 ) = 1 ) ) → ( 1 + 1 ) ∈ ℂ )
247 simprl ⊢ ( ( ( ( 0 · i ) = ( 1 + i ) ∧ ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 1 + 1 ) · 𝑧 ) = 1 ) ) → 𝑧 ∈ ℝ )
248 247 recnd ⊢ ( ( ( ( 0 · i ) = ( 1 + i ) ∧ ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 1 + 1 ) · 𝑧 ) = 1 ) ) → 𝑧 ∈ ℂ )
249 244 246 248 mulassd ⊢ ( ( ( ( 0 · i ) = ( 1 + i ) ∧ ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 1 + 1 ) · 𝑧 ) = 1 ) ) → ( ( ( 0 · i ) · ( 1 + 1 ) ) · 𝑧 ) = ( ( 0 · i ) · ( ( 1 + 1 ) · 𝑧 ) ) )
250 simprr ⊢ ( ( ( ( 0 · i ) = ( 1 + i ) ∧ ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 1 + 1 ) · 𝑧 ) = 1 ) ) → ( ( 1 + 1 ) · 𝑧 ) = 1 )
251 250 oveq2d ⊢ ( ( ( ( 0 · i ) = ( 1 + i ) ∧ ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 1 + 1 ) · 𝑧 ) = 1 ) ) → ( ( 0 · i ) · ( ( 1 + 1 ) · 𝑧 ) ) = ( ( 0 · i ) · 1 ) )
252 251 232 eqtrdi ⊢ ( ( ( ( 0 · i ) = ( 1 + i ) ∧ ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 1 + 1 ) · 𝑧 ) = 1 ) ) → ( ( 0 · i ) · ( ( 1 + 1 ) · 𝑧 ) ) = ( 0 · i ) )
253 249 252 eqtrd ⊢ ( ( ( ( 0 · i ) = ( 1 + i ) ∧ ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 1 + 1 ) · 𝑧 ) = 1 ) ) → ( ( ( 0 · i ) · ( 1 + 1 ) ) · 𝑧 ) = ( 0 · i ) )
254 245 246 248 mulassd ⊢ ( ( ( ( 0 · i ) = ( 1 + i ) ∧ ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 1 + 1 ) · 𝑧 ) = 1 ) ) → ( ( 1 · ( 1 + 1 ) ) · 𝑧 ) = ( 1 · ( ( 1 + 1 ) · 𝑧 ) ) )
255 250 oveq2d ⊢ ( ( ( ( 0 · i ) = ( 1 + i ) ∧ ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 1 + 1 ) · 𝑧 ) = 1 ) ) → ( 1 · ( ( 1 + 1 ) · 𝑧 ) ) = ( 1 · 1 ) )
256 1t1e1ALT ⊢ ( 1 · 1 ) = 1
257 255 256 eqtrdi ⊢ ( ( ( ( 0 · i ) = ( 1 + i ) ∧ ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 1 + 1 ) · 𝑧 ) = 1 ) ) → ( 1 · ( ( 1 + 1 ) · 𝑧 ) ) = 1 )
258 254 257 eqtrd ⊢ ( ( ( ( 0 · i ) = ( 1 + i ) ∧ ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 1 + 1 ) · 𝑧 ) = 1 ) ) → ( ( 1 · ( 1 + 1 ) ) · 𝑧 ) = 1 )
259 243 253 258 3eqtr3d ⊢ ( ( ( ( 0 · i ) = ( 1 + i ) ∧ ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 1 + 1 ) · 𝑧 ) = 1 ) ) → ( 0 · i ) = 1 )
260 259 rexlimdvaa ⊢ ( ( ( 0 · i ) = ( 1 + i ) ∧ ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) ) → ( ∃ 𝑧 ∈ ℝ ( ( 1 + 1 ) · 𝑧 ) = 1 → ( 0 · i ) = 1 ) )
261 215 260 mpi ⊢ ( ( ( 0 · i ) = ( 1 + i ) ∧ ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) ) → ( 0 · i ) = 1 )
262 208 261 mpdan ⊢ ( ( 0 · i ) = ( 1 + i ) → ( 0 · i ) = 1 )
263 189 262 sylbi ⊢ ( ( 0 · i ) = ( 1 + ( i · 1 ) ) → ( 0 · i ) = 1 )
264 oveq2 ⊢ ( ( 0 · i ) = 1 → ( 0 · ( 0 · i ) ) = ( 0 · 1 ) )
265 116 115 eqtr3i ⊢ ( 0 · ( 0 · i ) ) = ( 0 · i )
266 264 265 148 3eqtr3g ⊢ ( ( 0 · i ) = 1 → ( 0 · i ) = 0 )
267 263 266 syl ⊢ ( ( 0 · i ) = ( 1 + ( i · 1 ) ) → ( 0 · i ) = 0 )
268 187 267 syl ⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) ∧ ¬ ( 0 · i ) = 0 ) → ( 0 · i ) = 0 )
269 268 pm2.18da ⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) ) → ( 0 · i ) = 0 )
270 269 ex ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) → ( 0 · i ) = 0 ) )
271 270 rexlimivv ⊢ ( ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ ( 0 · i ) = ( 𝑎 + ( i · 𝑏 ) ) → ( 0 · i ) = 0 )
272 3 4 271 mp2b ⊢ ( 0 · i ) = 0