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-addid2 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 readdid2 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 readdid1 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 readdid1 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 readdid2 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 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 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