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 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-addid2 ( ( 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 readdid2 ( 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 readdid1 ( 𝑎 ∈ ℝ → ( 𝑎 + 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 readdid1 ( 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 readdid2 ( 𝑏 ∈ ℝ → ( 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 syl5eq ( ( ( 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 syl5eq ( ( ( 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 syl5eq ( ( ( 0 · i ) = ( 1 + i ) ∧ ( 0 · i ) = ( ( ( i · i ) · i ) + 1 ) ) → ( ( 0 · i ) · ( 1 + 1 ) ) = ( ( 1 + i ) + ( ( ( i · i ) · i ) + 1 ) ) )
239 remulid2 ( ( 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