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∈ℂ→∃a∈ℝ∃b∈ℝ0⋅i=a+i⁢b
5 simplr ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i=a+i⁢b
6 neqne ⊢¬0⋅i=0→0⋅i≠0
7 6 adantl ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i≠0
8 simplll ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→a∈ℝ
9 rernegcl ⊢a∈ℝ→0-ℝa∈ℝ
10 8 9 syl ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0-ℝa∈ℝ
11 1red ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→1∈ℝ
12 10 11 readdcld ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0-ℝa+1∈ℝ
13 ax-rrecex ⊢0-ℝa+1∈ℝ∧0-ℝa+1≠0→∃x∈ℝ0-ℝa+1⁢x=1
14 12 13 sylan ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧0-ℝa+1≠0→∃x∈ℝ0-ℝa+1⁢x=1
15 2 a1i ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→i∈ℂ
16 10 recnd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0-ℝa∈ℂ
17 1cnd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→1∈ℂ
18 15 16 17 adddid ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→i⁢0-ℝa+1=i⁢0-ℝa+i⋅1
19 it1ei ⊢i⋅1=i
20 19 oveq2i ⊢i⁢0-ℝa+i⋅1=i⁢0-ℝa+i
21 18 20 eqtrdi ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→i⁢0-ℝa+1=i⁢0-ℝa+i
22 21 oveq2d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i⁢0-ℝa+1=0⋅i⁢0-ℝa+i
23 0cnd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0∈ℂ
24 15 16 mulcld ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→i⁢0-ℝa∈ℂ
25 23 24 15 adddid ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i⁢0-ℝa+i=0⋅i⁢0-ℝa+0⋅i
26 22 25 eqtrd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i⁢0-ℝa+1=0⋅i⁢0-ℝa+0⋅i
27 5 oveq2d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0-ℝa+0⋅i=0-ℝa+a+i⁢b
28 renegid2 ⊢a∈ℝ→0-ℝa+a=0
29 28 ad3antrrr ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0-ℝa+a=0
30 29 oveq1d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0-ℝa+a+i⁢b=0+i⁢b
31 8 recnd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→a∈ℂ
32 simpllr ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→b∈ℝ
33 32 recnd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→b∈ℂ
34 15 33 mulcld ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→i⁢b∈ℂ
35 16 31 34 addassd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0-ℝa+a+i⁢b=0-ℝa+a+i⁢b
36 sn-addlid ⊢i⁢b∈ℂ→0+i⁢b=i⁢b
37 34 36 syl ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0+i⁢b=i⁢b
38 30 35 37 3eqtr3d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0-ℝa+a+i⁢b=i⁢b
39 27 38 eqtrd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0-ℝa+0⋅i=i⁢b
40 39 oveq2d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i⁢0-ℝa+0⋅i=0⋅i⁢i⁢b
41 3 a1i ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i∈ℂ
42 41 16 41 adddid ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i⁢0-ℝa+0⋅i=0⋅i⁢0-ℝa+0⋅i⁢0⋅i
43 23 15 16 mulassd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i⁢0-ℝa=0⋅i⁢0-ℝa
44 41 23 15 mulassd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i⋅0⁢i=0⋅i⁢0⋅i
45 sn-mul01 ⊢0⋅i∈ℂ→0⋅i⋅0=0
46 41 45 syl ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i⋅0=0
47 46 oveq1d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i⋅0⁢i=0⋅i
48 44 47 eqtr3d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i⁢0⋅i=0⋅i
49 43 48 oveq12d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i⁢0-ℝa+0⋅i⁢0⋅i=0⋅i⁢0-ℝa+0⋅i
50 42 49 eqtrd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i⁢0-ℝa+0⋅i=0⋅i⁢0-ℝa+0⋅i
51 23 15 34 mulassd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i⁢i⁢b=0⋅i⁢i⁢b
52 15 15 33 mulassd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→i⁢i⁢b=i⁢i⁢b
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 ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→i⁢i∈ℝ
59 58 32 remulcld ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→i⁢i⁢b∈ℝ
60 52 59 eqeltrrd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→i⁢i⁢b∈ℝ
61 remul02 ⊢i⁢i⁢b∈ℝ→0⋅i⁢i⁢b=0
62 60 61 syl ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i⁢i⁢b=0
63 51 62 eqtrd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i⁢i⁢b=0
64 40 50 63 3eqtr3d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i⁢0-ℝa+0⋅i=0
65 26 64 eqtrd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i⁢0-ℝa+1=0
66 65 ad2antrr ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧0-ℝa+1≠0∧x∈ℝ∧0-ℝa+1⁢x=1→0⋅i⁢0-ℝa+1=0
67 66 oveq1d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧0-ℝa+1≠0∧x∈ℝ∧0-ℝa+1⁢x=1→0⋅i⁢0-ℝa+1⁢x=0⋅x
68 0cnd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧0-ℝa+1≠0∧x∈ℝ∧0-ℝa+1⁢x=1→0∈ℂ
69 2 a1i ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧0-ℝa+1≠0∧x∈ℝ∧0-ℝa+1⁢x=1→i∈ℂ
70 10 ad2antrr ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧0-ℝa+1≠0∧x∈ℝ∧0-ℝa+1⁢x=1→0-ℝa∈ℝ
71 70 recnd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧0-ℝa+1≠0∧x∈ℝ∧0-ℝa+1⁢x=1→0-ℝa∈ℂ
72 1cnd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧0-ℝa+1≠0∧x∈ℝ∧0-ℝa+1⁢x=1→1∈ℂ
73 71 72 addcld ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧0-ℝa+1≠0∧x∈ℝ∧0-ℝa+1⁢x=1→0-ℝa+1∈ℂ
74 69 73 mulcld ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧0-ℝa+1≠0∧x∈ℝ∧0-ℝa+1⁢x=1→i⁢0-ℝa+1∈ℂ
75 simprl ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧0-ℝa+1≠0∧x∈ℝ∧0-ℝa+1⁢x=1→x∈ℝ
76 75 recnd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧0-ℝa+1≠0∧x∈ℝ∧0-ℝa+1⁢x=1→x∈ℂ
77 68 74 76 mulassd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧0-ℝa+1≠0∧x∈ℝ∧0-ℝa+1⁢x=1→0⋅i⁢0-ℝa+1⁢x=0⋅i⁢0-ℝa+1⁢x
78 69 73 76 mulassd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧0-ℝa+1≠0∧x∈ℝ∧0-ℝa+1⁢x=1→i⁢0-ℝa+1⁢x=i⁢0-ℝa+1⁢x
79 simprr ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧0-ℝa+1≠0∧x∈ℝ∧0-ℝa+1⁢x=1→0-ℝa+1⁢x=1
80 79 oveq2d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧0-ℝa+1≠0∧x∈ℝ∧0-ℝa+1⁢x=1→i⁢0-ℝa+1⁢x=i⋅1
81 80 19 eqtrdi ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧0-ℝa+1≠0∧x∈ℝ∧0-ℝa+1⁢x=1→i⁢0-ℝa+1⁢x=i
82 78 81 eqtrd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧0-ℝa+1≠0∧x∈ℝ∧0-ℝa+1⁢x=1→i⁢0-ℝa+1⁢x=i
83 82 oveq2d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧0-ℝa+1≠0∧x∈ℝ∧0-ℝa+1⁢x=1→0⋅i⁢0-ℝa+1⁢x=0⋅i
84 77 83 eqtrd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧0-ℝa+1≠0∧x∈ℝ∧0-ℝa+1⁢x=1→0⋅i⁢0-ℝa+1⁢x=0⋅i
85 remul02 ⊢x∈ℝ→0⋅x=0
86 75 85 syl ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧0-ℝa+1≠0∧x∈ℝ∧0-ℝa+1⁢x=1→0⋅x=0
87 67 84 86 3eqtr3d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧0-ℝa+1≠0∧x∈ℝ∧0-ℝa+1⁢x=1→0⋅i=0
88 14 87 rexlimddv ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧0-ℝa+1≠0→0⋅i=0
89 88 ex ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0-ℝa+1≠0→0⋅i=0
90 89 necon1d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i≠0→0-ℝa+1=0
91 7 90 mpd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0-ℝa+1=0
92 91 oveq2d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→a+0-ℝa+1=a+0
93 31 16 17 addassd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→a+0-ℝa+1=a+0-ℝa+1
94 renegid ⊢a∈ℝ→a+0-ℝa=0
95 8 94 syl ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→a+0-ℝa=0
96 95 oveq1d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→a+0-ℝa+1=0+1
97 readdlid ⊢1∈ℝ→0+1=1
98 54 97 ax-mp ⊢0+1=1
99 96 98 eqtrdi ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→a+0-ℝa+1=1
100 93 99 eqtr3d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→a+0-ℝa+1=1
101 readdrid ⊢a∈ℝ→a+0=a
102 8 101 syl ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→a+0=a
103 92 100 102 3eqtr3rd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→a=1
104 rernegcl ⊢b∈ℝ→0-ℝb∈ℝ
105 32 104 syl ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0-ℝb∈ℝ
106 11 105 readdcld ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→1+0-ℝb∈ℝ
107 ax-rrecex ⊢1+0-ℝb∈ℝ∧1+0-ℝb≠0→∃y∈ℝ1+0-ℝb⁢y=1
108 106 107 sylan ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧1+0-ℝb≠0→∃y∈ℝ1+0-ℝb⁢y=1
109 105 recnd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0-ℝb∈ℂ
110 15 109 mulcld ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→i⁢0-ℝb∈ℂ
111 23 15 110 adddid ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i+i⁢0-ℝb=0⋅i+0⋅i⁢0-ℝb
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 ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i=0⋅0⋅i
119 118 oveq1d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i+0⋅i⁢0-ℝb=0⋅0⋅i+0⋅i⁢0-ℝb
120 111 119 eqtrd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i+i⁢0-ℝb=0⋅0⋅i+0⋅i⁢0-ℝb
121 15 17 109 adddid ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→i⁢1+0-ℝb=i⋅1+i⁢0-ℝb
122 19 a1i ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→i⋅1=i
123 122 oveq1d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→i⋅1+i⁢0-ℝb=i+i⁢0-ℝb
124 121 123 eqtrd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→i⁢1+0-ℝb=i+i⁢0-ℝb
125 124 oveq2d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i⁢1+0-ℝb=0⋅i+i⁢0-ℝb
126 23 41 110 adddid ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅0⋅i+i⁢0-ℝb=0⋅0⋅i+0⋅i⁢0-ℝb
127 120 125 126 3eqtr4d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i⁢1+0-ℝb=0⋅0⋅i+i⁢0-ℝb
128 103 oveq1d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→a+i⁢b=1+i⁢b
129 5 128 eqtrd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i=1+i⁢b
130 129 oveq1d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i+i⁢0-ℝb=1+i⁢b+i⁢0-ℝb
131 17 34 110 addassd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→1+i⁢b+i⁢0-ℝb=1+i⁢b+i⁢0-ℝb
132 renegid ⊢b∈ℝ→b+0-ℝb=0
133 32 132 syl ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→b+0-ℝb=0
134 133 oveq2d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→i⁢b+0-ℝb=i⋅0
135 15 33 109 adddid ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→i⁢b+0-ℝb=i⁢b+i⁢0-ℝb
136 sn-mul01 ⊢i∈ℂ→i⋅0=0
137 2 136 mp1i ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→i⋅0=0
138 134 135 137 3eqtr3d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→i⁢b+i⁢0-ℝb=0
139 138 oveq2d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→1+i⁢b+i⁢0-ℝb=1+0
140 readdrid ⊢1∈ℝ→1+0=1
141 54 140 ax-mp ⊢1+0=1
142 139 141 eqtrdi ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→1+i⁢b+i⁢0-ℝb=1
143 131 142 eqtrd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→1+i⁢b+i⁢0-ℝb=1
144 130 143 eqtrd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i+i⁢0-ℝb=1
145 144 oveq2d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅0⋅i+i⁢0-ℝb=0⋅1
146 127 145 eqtrd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i⁢1+0-ℝb=0⋅1
147 ax-1rid ⊢0∈ℝ→0⋅1=0
148 112 147 ax-mp ⊢0⋅1=0
149 146 148 eqtrdi ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i⁢1+0-ℝb=0
150 149 ad2antrr ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧1+0-ℝb≠0∧y∈ℝ∧1+0-ℝb⁢y=1→0⋅i⁢1+0-ℝb=0
151 150 oveq1d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧1+0-ℝb≠0∧y∈ℝ∧1+0-ℝb⁢y=1→0⋅i⁢1+0-ℝb⁢y=0⋅y
152 0cnd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧1+0-ℝb≠0∧y∈ℝ∧1+0-ℝb⁢y=1→0∈ℂ
153 2 a1i ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧1+0-ℝb≠0∧y∈ℝ∧1+0-ℝb⁢y=1→i∈ℂ
154 1cnd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧1+0-ℝb≠0∧y∈ℝ∧1+0-ℝb⁢y=1→1∈ℂ
155 109 ad2antrr ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧1+0-ℝb≠0∧y∈ℝ∧1+0-ℝb⁢y=1→0-ℝb∈ℂ
156 154 155 addcld ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧1+0-ℝb≠0∧y∈ℝ∧1+0-ℝb⁢y=1→1+0-ℝb∈ℂ
157 153 156 mulcld ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧1+0-ℝb≠0∧y∈ℝ∧1+0-ℝb⁢y=1→i⁢1+0-ℝb∈ℂ
158 simprl ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧1+0-ℝb≠0∧y∈ℝ∧1+0-ℝb⁢y=1→y∈ℝ
159 158 recnd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧1+0-ℝb≠0∧y∈ℝ∧1+0-ℝb⁢y=1→y∈ℂ
160 152 157 159 mulassd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧1+0-ℝb≠0∧y∈ℝ∧1+0-ℝb⁢y=1→0⋅i⁢1+0-ℝb⁢y=0⋅i⁢1+0-ℝb⁢y
161 153 156 159 mulassd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧1+0-ℝb≠0∧y∈ℝ∧1+0-ℝb⁢y=1→i⁢1+0-ℝb⁢y=i⁢1+0-ℝb⁢y
162 simprr ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧1+0-ℝb≠0∧y∈ℝ∧1+0-ℝb⁢y=1→1+0-ℝb⁢y=1
163 162 oveq2d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧1+0-ℝb≠0∧y∈ℝ∧1+0-ℝb⁢y=1→i⁢1+0-ℝb⁢y=i⋅1
164 163 19 eqtrdi ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧1+0-ℝb≠0∧y∈ℝ∧1+0-ℝb⁢y=1→i⁢1+0-ℝb⁢y=i
165 161 164 eqtrd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧1+0-ℝb≠0∧y∈ℝ∧1+0-ℝb⁢y=1→i⁢1+0-ℝb⁢y=i
166 165 oveq2d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧1+0-ℝb≠0∧y∈ℝ∧1+0-ℝb⁢y=1→0⋅i⁢1+0-ℝb⁢y=0⋅i
167 160 166 eqtrd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧1+0-ℝb≠0∧y∈ℝ∧1+0-ℝb⁢y=1→0⋅i⁢1+0-ℝb⁢y=0⋅i
168 remul02 ⊢y∈ℝ→0⋅y=0
169 158 168 syl ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧1+0-ℝb≠0∧y∈ℝ∧1+0-ℝb⁢y=1→0⋅y=0
170 151 167 169 3eqtr3d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧1+0-ℝb≠0∧y∈ℝ∧1+0-ℝb⁢y=1→0⋅i=0
171 108 170 rexlimddv ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0∧1+0-ℝb≠0→0⋅i=0
172 171 ex ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→1+0-ℝb≠0→0⋅i=0
173 172 necon1d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i≠0→1+0-ℝb=0
174 7 173 mpd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→1+0-ℝb=0
175 174 oveq1d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→1+0-ℝb+b=0+b
176 17 109 33 addassd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→1+0-ℝb+b=1+0-ℝb+b
177 renegid2 ⊢b∈ℝ→0-ℝb+b=0
178 32 177 syl ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0-ℝb+b=0
179 178 oveq2d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→1+0-ℝb+b=1+0
180 179 141 eqtrdi ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→1+0-ℝb+b=1
181 176 180 eqtrd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→1+0-ℝb+b=1
182 readdlid ⊢b∈ℝ→0+b=b
183 32 182 syl ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0+b=b
184 175 181 183 3eqtr3rd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→b=1
185 184 oveq2d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→i⁢b=i⋅1
186 103 185 oveq12d ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→a+i⁢b=1+i⋅1
187 5 186 eqtrd ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬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→∃z∈ℝ1+1⁢z=1
215 209 213 214 mp2an ⊢∃z∈ℝ1+1⁢z=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⁢z=1⁢1+1⁢z
243 242 adantr ⊢0⋅i=1+i∧0⋅i=i⁢i⁢i+1∧z∈ℝ∧1+1⁢z=1→0⋅i⁢1+1⁢z=1⁢1+1⁢z
244 3 a1i ⊢0⋅i=1+i∧0⋅i=i⁢i⁢i+1∧z∈ℝ∧1+1⁢z=1→0⋅i∈ℂ
245 1cnd ⊢0⋅i=1+i∧0⋅i=i⁢i⁢i+1∧z∈ℝ∧1+1⁢z=1→1∈ℂ
246 245 245 addcld ⊢0⋅i=1+i∧0⋅i=i⁢i⁢i+1∧z∈ℝ∧1+1⁢z=1→1+1∈ℂ
247 simprl ⊢0⋅i=1+i∧0⋅i=i⁢i⁢i+1∧z∈ℝ∧1+1⁢z=1→z∈ℝ
248 247 recnd ⊢0⋅i=1+i∧0⋅i=i⁢i⁢i+1∧z∈ℝ∧1+1⁢z=1→z∈ℂ
249 244 246 248 mulassd ⊢0⋅i=1+i∧0⋅i=i⁢i⁢i+1∧z∈ℝ∧1+1⁢z=1→0⋅i⁢1+1⁢z=0⋅i⁢1+1⁢z
250 simprr ⊢0⋅i=1+i∧0⋅i=i⁢i⁢i+1∧z∈ℝ∧1+1⁢z=1→1+1⁢z=1
251 250 oveq2d ⊢0⋅i=1+i∧0⋅i=i⁢i⁢i+1∧z∈ℝ∧1+1⁢z=1→0⋅i⁢1+1⁢z=0⋅i⋅1
252 251 232 eqtrdi ⊢0⋅i=1+i∧0⋅i=i⁢i⁢i+1∧z∈ℝ∧1+1⁢z=1→0⋅i⁢1+1⁢z=0⋅i
253 249 252 eqtrd ⊢0⋅i=1+i∧0⋅i=i⁢i⁢i+1∧z∈ℝ∧1+1⁢z=1→0⋅i⁢1+1⁢z=0⋅i
254 245 246 248 mulassd ⊢0⋅i=1+i∧0⋅i=i⁢i⁢i+1∧z∈ℝ∧1+1⁢z=1→1⁢1+1⁢z=1⁢1+1⁢z
255 250 oveq2d ⊢0⋅i=1+i∧0⋅i=i⁢i⁢i+1∧z∈ℝ∧1+1⁢z=1→1⁢1+1⁢z=1⋅1
256 1t1e1ALT ⊢1⋅1=1
257 255 256 eqtrdi ⊢0⋅i=1+i∧0⋅i=i⁢i⁢i+1∧z∈ℝ∧1+1⁢z=1→1⁢1+1⁢z=1
258 254 257 eqtrd ⊢0⋅i=1+i∧0⋅i=i⁢i⁢i+1∧z∈ℝ∧1+1⁢z=1→1⁢1+1⁢z=1
259 243 253 258 3eqtr3d ⊢0⋅i=1+i∧0⋅i=i⁢i⁢i+1∧z∈ℝ∧1+1⁢z=1→0⋅i=1
260 259 rexlimdvaa ⊢0⋅i=1+i∧0⋅i=i⁢i⁢i+1→∃z∈ℝ1+1⁢z=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 ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b∧¬0⋅i=0→0⋅i=0
269 268 pm2.18da ⊢a∈ℝ∧b∈ℝ∧0⋅i=a+i⁢b→0⋅i=0
270 269 ex ⊢a∈ℝ∧b∈ℝ→0⋅i=a+i⁢b→0⋅i=0
271 270 rexlimivv ⊢∃a∈ℝ∃b∈ℝ0⋅i=a+i⁢b→0⋅i=0
272 3 4 271 mp2b ⊢0⋅i=0