Proof of Theorem mul4sqlem
Step | Hyp | Ref
| Expression |
1 | | mul4sq.1 |
. . . . . . . . . . 11
|
2 | | gzcn 12311 |
. . . . . . . . . . 11
|
3 | 1, 2 | syl 14 |
. . . . . . . . . 10
|
4 | | mul4sq.3 |
. . . . . . . . . . 11
|
5 | | gzcn 12311 |
. . . . . . . . . . 11
|
6 | 4, 5 | syl 14 |
. . . . . . . . . 10
|
7 | 3, 6 | mulcld 7927 |
. . . . . . . . 9
|
8 | 7 | absvalsqd 11133 |
. . . . . . . 8
|
9 | 7 | cjcld 10891 |
. . . . . . . . 9
|
10 | 7, 9 | mulcld 7927 |
. . . . . . . 8
|
11 | 8, 10 | eqeltrd 2247 |
. . . . . . 7
|
12 | | mul4sq.2 |
. . . . . . . . . . 11
|
13 | | gzcn 12311 |
. . . . . . . . . . 11
|
14 | 12, 13 | syl 14 |
. . . . . . . . . 10
|
15 | | mul4sq.4 |
. . . . . . . . . . 11
|
16 | | gzcn 12311 |
. . . . . . . . . . 11
|
17 | 15, 16 | syl 14 |
. . . . . . . . . 10
|
18 | 14, 17 | mulcld 7927 |
. . . . . . . . 9
|
19 | 18 | absvalsqd 11133 |
. . . . . . . 8
|
20 | 18 | cjcld 10891 |
. . . . . . . . 9
|
21 | 18, 20 | mulcld 7927 |
. . . . . . . 8
|
22 | 19, 21 | eqeltrd 2247 |
. . . . . . 7
|
23 | 11, 22 | addcld 7926 |
. . . . . 6
|
24 | 3 | cjcld 10891 |
. . . . . . . . 9
|
25 | 24, 6 | mulcld 7927 |
. . . . . . . 8
|
26 | 14 | cjcld 10891 |
. . . . . . . . 9
|
27 | 26, 17 | mulcld 7927 |
. . . . . . . 8
|
28 | 25, 27 | mulcld 7927 |
. . . . . . 7
|
29 | 6 | cjcld 10891 |
. . . . . . . . 9
|
30 | 14, 29 | mulcld 7927 |
. . . . . . . 8
|
31 | 17 | cjcld 10891 |
. . . . . . . . 9
|
32 | 3, 31 | mulcld 7927 |
. . . . . . . 8
|
33 | 30, 32 | mulcld 7927 |
. . . . . . 7
|
34 | 28, 33 | addcld 7926 |
. . . . . 6
|
35 | 3, 17 | mulcld 7927 |
. . . . . . . . 9
|
36 | 35 | absvalsqd 11133 |
. . . . . . . 8
|
37 | 35 | cjcld 10891 |
. . . . . . . . 9
|
38 | 35, 37 | mulcld 7927 |
. . . . . . . 8
|
39 | 36, 38 | eqeltrd 2247 |
. . . . . . 7
|
40 | 14, 6 | mulcld 7927 |
. . . . . . . . 9
|
41 | 40 | absvalsqd 11133 |
. . . . . . . 8
|
42 | 40 | cjcld 10891 |
. . . . . . . . 9
|
43 | 40, 42 | mulcld 7927 |
. . . . . . . 8
|
44 | 41, 43 | eqeltrd 2247 |
. . . . . . 7
|
45 | 39, 44 | addcld 7926 |
. . . . . 6
|
46 | 23, 34, 45 | ppncand 8257 |
. . . . 5
|
47 | 14, 31 | mulcld 7927 |
. . . . . . . . 9
|
48 | 25, 47 | addcld 7926 |
. . . . . . . 8
|
49 | 48 | absvalsqd 11133 |
. . . . . . 7
|
50 | 25, 47 | cjaddd 10916 |
. . . . . . . . 9
|
51 | 24, 6 | cjmuld 10917 |
. . . . . . . . . . 11
|
52 | 3 | cjcjd 10894 |
. . . . . . . . . . . 12
|
53 | 52 | oveq1d 5865 |
. . . . . . . . . . 11
|
54 | 51, 53 | eqtrd 2203 |
. . . . . . . . . 10
|
55 | 14, 31 | cjmuld 10917 |
. . . . . . . . . . 11
|
56 | 17 | cjcjd 10894 |
. . . . . . . . . . . 12
|
57 | 56 | oveq2d 5866 |
. . . . . . . . . . 11
|
58 | 55, 57 | eqtrd 2203 |
. . . . . . . . . 10
|
59 | 54, 58 | oveq12d 5868 |
. . . . . . . . 9
|
60 | 50, 59 | eqtrd 2203 |
. . . . . . . 8
|
61 | 60 | oveq2d 5866 |
. . . . . . 7
|
62 | 3, 29 | mulcld 7927 |
. . . . . . . . . . 11
|
63 | 25, 62, 27 | adddid 7931 |
. . . . . . . . . 10
|
64 | 6, 24, 3, 29 | mul4d 8061 |
. . . . . . . . . . . . 13
|
65 | 24, 6 | mulcomd 7928 |
. . . . . . . . . . . . . 14
|
66 | 65 | oveq1d 5865 |
. . . . . . . . . . . . 13
|
67 | 3, 6 | mulcomd 7928 |
. . . . . . . . . . . . . 14
|
68 | 3, 6 | cjmuld 10917 |
. . . . . . . . . . . . . 14
|
69 | 67, 68 | oveq12d 5868 |
. . . . . . . . . . . . 13
|
70 | 64, 66, 69 | 3eqtr4d 2213 |
. . . . . . . . . . . 12
|
71 | 70, 8 | eqtr4d 2206 |
. . . . . . . . . . 11
|
72 | 71 | oveq1d 5865 |
. . . . . . . . . 10
|
73 | 63, 72 | eqtrd 2203 |
. . . . . . . . 9
|
74 | 47, 62, 27 | adddid 7931 |
. . . . . . . . . 10
|
75 | 3, 29 | mulcomd 7928 |
. . . . . . . . . . . . 13
|
76 | 75 | oveq2d 5866 |
. . . . . . . . . . . 12
|
77 | 14, 31, 29, 3 | mul4d 8061 |
. . . . . . . . . . . 12
|
78 | 31, 3 | mulcomd 7928 |
. . . . . . . . . . . . 13
|
79 | 78 | oveq2d 5866 |
. . . . . . . . . . . 12
|
80 | 76, 77, 79 | 3eqtrd 2207 |
. . . . . . . . . . 11
|
81 | 14, 31, 17, 26 | mul4d 8061 |
. . . . . . . . . . . . 13
|
82 | 26, 17 | mulcomd 7928 |
. . . . . . . . . . . . . 14
|
83 | 82 | oveq2d 5866 |
. . . . . . . . . . . . 13
|
84 | 14, 17 | cjmuld 10917 |
. . . . . . . . . . . . . . 15
|
85 | 26, 31 | mulcomd 7928 |
. . . . . . . . . . . . . . 15
|
86 | 84, 85 | eqtrd 2203 |
. . . . . . . . . . . . . 14
|
87 | 86 | oveq2d 5866 |
. . . . . . . . . . . . 13
|
88 | 81, 83, 87 | 3eqtr4d 2213 |
. . . . . . . . . . . 12
|
89 | 88, 19 | eqtr4d 2206 |
. . . . . . . . . . 11
|
90 | 80, 89 | oveq12d 5868 |
. . . . . . . . . 10
|
91 | 74, 90 | eqtrd 2203 |
. . . . . . . . 9
|
92 | 73, 91 | oveq12d 5868 |
. . . . . . . 8
|
93 | 62, 27 | addcld 7926 |
. . . . . . . . 9
|
94 | 25, 47, 93 | adddird 7932 |
. . . . . . . 8
|
95 | 11, 22, 28, 33 | add42d 8076 |
. . . . . . . 8
|
96 | 92, 94, 95 | 3eqtr4d 2213 |
. . . . . . 7
|
97 | 49, 61, 96 | 3eqtrd 2207 |
. . . . . 6
|
98 | 24, 17 | mulcld 7927 |
. . . . . . . . 9
|
99 | 98, 30 | subcld 8217 |
. . . . . . . 8
|
100 | 99 | absvalsqd 11133 |
. . . . . . 7
|
101 | | cjsub 10843 |
. . . . . . . . . 10
|
102 | 98, 30, 101 | syl2anc 409 |
. . . . . . . . 9
|
103 | 24, 17 | cjmuld 10917 |
. . . . . . . . . . 11
|
104 | 52 | oveq1d 5865 |
. . . . . . . . . . 11
|
105 | 103, 104 | eqtrd 2203 |
. . . . . . . . . 10
|
106 | 14, 29 | cjmuld 10917 |
. . . . . . . . . . 11
|
107 | 6 | cjcjd 10894 |
. . . . . . . . . . . 12
|
108 | 107 | oveq2d 5866 |
. . . . . . . . . . 11
|
109 | 106, 108 | eqtrd 2203 |
. . . . . . . . . 10
|
110 | 105, 109 | oveq12d 5868 |
. . . . . . . . 9
|
111 | 102, 110 | eqtrd 2203 |
. . . . . . . 8
|
112 | 111 | oveq2d 5866 |
. . . . . . 7
|
113 | 26, 6 | mulcld 7927 |
. . . . . . . . . 10
|
114 | 32, 113 | subcld 8217 |
. . . . . . . . 9
|
115 | 98, 30, 114 | subdird 8321 |
. . . . . . . 8
|
116 | 98, 32, 113 | subdid 8320 |
. . . . . . . . . 10
|
117 | 17, 24, 3, 31 | mul4d 8061 |
. . . . . . . . . . . . 13
|
118 | 24, 17 | mulcomd 7928 |
. . . . . . . . . . . . . 14
|
119 | 118 | oveq1d 5865 |
. . . . . . . . . . . . 13
|
120 | 3, 17 | mulcomd 7928 |
. . . . . . . . . . . . . 14
|
121 | 3, 17 | cjmuld 10917 |
. . . . . . . . . . . . . 14
|
122 | 120, 121 | oveq12d 5868 |
. . . . . . . . . . . . 13
|
123 | 117, 119,
122 | 3eqtr4d 2213 |
. . . . . . . . . . . 12
|
124 | 123, 36 | eqtr4d 2206 |
. . . . . . . . . . 11
|
125 | 26, 6 | mulcomd 7928 |
. . . . . . . . . . . . 13
|
126 | 125 | oveq2d 5866 |
. . . . . . . . . . . 12
|
127 | 24, 17, 6, 26 | mul4d 8061 |
. . . . . . . . . . . 12
|
128 | 17, 26 | mulcomd 7928 |
. . . . . . . . . . . . 13
|
129 | 128 | oveq2d 5866 |
. . . . . . . . . . . 12
|
130 | 126, 127,
129 | 3eqtrd 2207 |
. . . . . . . . . . 11
|
131 | 124, 130 | oveq12d 5868 |
. . . . . . . . . 10
|
132 | 116, 131 | eqtrd 2203 |
. . . . . . . . 9
|
133 | 30, 32, 113 | subdid 8320 |
. . . . . . . . . 10
|
134 | 125 | oveq2d 5866 |
. . . . . . . . . . . . 13
|
135 | 14, 29, 6, 26 | mul4d 8061 |
. . . . . . . . . . . . 13
|
136 | 29, 26 | mulcomd 7928 |
. . . . . . . . . . . . . . 15
|
137 | 14, 6 | cjmuld 10917 |
. . . . . . . . . . . . . . 15
|
138 | 136, 137 | eqtr4d 2206 |
. . . . . . . . . . . . . 14
|
139 | 138 | oveq2d 5866 |
. . . . . . . . . . . . 13
|
140 | 134, 135,
139 | 3eqtrd 2207 |
. . . . . . . . . . . 12
|
141 | 140, 41 | eqtr4d 2206 |
. . . . . . . . . . 11
|
142 | 141 | oveq2d 5866 |
. . . . . . . . . 10
|
143 | 133, 142 | eqtrd 2203 |
. . . . . . . . 9
|
144 | 132, 143 | oveq12d 5868 |
. . . . . . . 8
|
145 | 39, 28, 33, 44 | subadd4d 8265 |
. . . . . . . 8
|
146 | 115, 144,
145 | 3eqtrd 2207 |
. . . . . . 7
|
147 | 100, 112,
146 | 3eqtrd 2207 |
. . . . . 6
|
148 | 97, 147 | oveq12d 5868 |
. . . . 5
|
149 | 3, 24 | mulcld 7927 |
. . . . . . . 8
|
150 | 14, 26 | mulcld 7927 |
. . . . . . . 8
|
151 | 6, 29 | mulcld 7927 |
. . . . . . . . 9
|
152 | 17, 31 | mulcld 7927 |
. . . . . . . . 9
|
153 | 151, 152 | addcld 7926 |
. . . . . . . 8
|
154 | 149, 150,
153 | adddird 7932 |
. . . . . . 7
|
155 | 68 | oveq2d 5866 |
. . . . . . . . . . 11
|
156 | 3, 6, 24, 29 | mul4d 8061 |
. . . . . . . . . . 11
|
157 | 8, 155, 156 | 3eqtrd 2207 |
. . . . . . . . . 10
|
158 | 121 | oveq2d 5866 |
. . . . . . . . . . 11
|
159 | 3, 17, 24, 31 | mul4d 8061 |
. . . . . . . . . . 11
|
160 | 36, 158, 159 | 3eqtrd 2207 |
. . . . . . . . . 10
|
161 | 157, 160 | oveq12d 5868 |
. . . . . . . . 9
|
162 | 149, 151,
152 | adddid 7931 |
. . . . . . . . 9
|
163 | 161, 162 | eqtr4d 2206 |
. . . . . . . 8
|
164 | 137 | oveq2d 5866 |
. . . . . . . . . . 11
|
165 | 14, 6, 26, 29 | mul4d 8061 |
. . . . . . . . . . 11
|
166 | 41, 164, 165 | 3eqtrd 2207 |
. . . . . . . . . 10
|
167 | 84 | oveq2d 5866 |
. . . . . . . . . . 11
|
168 | 14, 17, 26, 31 | mul4d 8061 |
. . . . . . . . . . 11
|
169 | 19, 167, 168 | 3eqtrd 2207 |
. . . . . . . . . 10
|
170 | 166, 169 | oveq12d 5868 |
. . . . . . . . 9
|
171 | 150, 151,
152 | adddid 7931 |
. . . . . . . . 9
|
172 | 170, 171 | eqtr4d 2206 |
. . . . . . . 8
|
173 | 163, 172 | oveq12d 5868 |
. . . . . . 7
|
174 | 154, 173 | eqtr4d 2206 |
. . . . . 6
|
175 | | mul4sq.5 |
. . . . . . . 8
|
176 | 3 | absvalsqd 11133 |
. . . . . . . . 9
|
177 | 14 | absvalsqd 11133 |
. . . . . . . . 9
|
178 | 176, 177 | oveq12d 5868 |
. . . . . . . 8
|
179 | 175, 178 | eqtrid 2215 |
. . . . . . 7
|
180 | | mul4sq.6 |
. . . . . . . 8
|
181 | 6 | absvalsqd 11133 |
. . . . . . . . 9
|
182 | 17 | absvalsqd 11133 |
. . . . . . . . 9
|
183 | 181, 182 | oveq12d 5868 |
. . . . . . . 8
|
184 | 180, 183 | eqtrid 2215 |
. . . . . . 7
|
185 | 179, 184 | oveq12d 5868 |
. . . . . 6
|
186 | 11, 22, 39, 44 | add42d 8076 |
. . . . . 6
|
187 | 174, 185,
186 | 3eqtr4d 2213 |
. . . . 5
|
188 | 46, 148, 187 | 3eqtr4d 2213 |
. . . 4
|
189 | 188 | oveq1d 5865 |
. . 3
|
190 | | mul4sq.7 |
. . . . . . . . . 10
|
191 | 190 | nncnd 8879 |
. . . . . . . . 9
|
192 | 190 | nnap0d 8911 |
. . . . . . . . 9
# |
193 | 48, 191, 192 | absdivapd 11146 |
. . . . . . . 8
|
194 | 190 | nnred 8878 |
. . . . . . . . . 10
|
195 | 190 | nnnn0d 9175 |
. . . . . . . . . . 11
|
196 | 195 | nn0ge0d 9178 |
. . . . . . . . . 10
|
197 | 194, 196 | absidd 11118 |
. . . . . . . . 9
|
198 | 197 | oveq2d 5866 |
. . . . . . . 8
|
199 | 193, 198 | eqtrd 2203 |
. . . . . . 7
|
200 | 199 | oveq1d 5865 |
. . . . . 6
|
201 | 48 | abscld 11132 |
. . . . . . . 8
|
202 | 201 | recnd 7935 |
. . . . . . 7
|
203 | 202, 191,
192 | sqdivapd 10609 |
. . . . . 6
|
204 | 200, 203 | eqtrd 2203 |
. . . . 5
|
205 | 99, 191, 192 | absdivapd 11146 |
. . . . . . . 8
|
206 | 197 | oveq2d 5866 |
. . . . . . . 8
|
207 | 205, 206 | eqtrd 2203 |
. . . . . . 7
|
208 | 207 | oveq1d 5865 |
. . . . . 6
|
209 | 99 | abscld 11132 |
. . . . . . . 8
|
210 | 209 | recnd 7935 |
. . . . . . 7
|
211 | 210, 191,
192 | sqdivapd 10609 |
. . . . . 6
|
212 | 208, 211 | eqtrd 2203 |
. . . . 5
|
213 | 204, 212 | oveq12d 5868 |
. . . 4
|
214 | 23, 34 | addcld 7926 |
. . . . . 6
|
215 | 97, 214 | eqeltrd 2247 |
. . . . 5
|
216 | 45, 34 | subcld 8217 |
. . . . . 6
|
217 | 147, 216 | eqeltrd 2247 |
. . . . 5
|
218 | 190 | nnsqcld 10617 |
. . . . . 6
|
219 | 218 | nncnd 8879 |
. . . . 5
|
220 | 218 | nnap0d 8911 |
. . . . 5
# |
221 | 215, 217,
219, 220 | divdirapd 8733 |
. . . 4
|
222 | 213, 221 | eqtr4d 2206 |
. . 3
|
223 | 176, 149 | eqeltrd 2247 |
. . . . . . 7
|
224 | 177, 150 | eqeltrd 2247 |
. . . . . . 7
|
225 | 223, 224 | addcld 7926 |
. . . . . 6
|
226 | 175, 225 | eqeltrid 2257 |
. . . . 5
|
227 | 184, 153 | eqeltrd 2247 |
. . . . 5
|
228 | 226, 191,
227, 191, 192, 192 | divmuldivapd 8736 |
. . . 4
|
229 | 191 | sqvald 10593 |
. . . . 5
|
230 | 229 | oveq2d 5866 |
. . . 4
|
231 | 228, 230 | eqtr4d 2206 |
. . 3
|
232 | 189, 222,
231 | 3eqtr4d 2213 |
. 2
|
233 | 226, 48 | nncand 8222 |
. . . . . . 7
|
234 | 149, 150,
25, 47 | addsub4d 8264 |
. . . . . . . . 9
|
235 | 179 | oveq1d 5865 |
. . . . . . . . 9
|
236 | 24, 3, 6 | subdid 8320 |
. . . . . . . . . . 11
|
237 | 24, 3 | mulcomd 7928 |
. . . . . . . . . . . 12
|
238 | 237 | oveq1d 5865 |
. . . . . . . . . . 11
|
239 | 236, 238 | eqtrd 2203 |
. . . . . . . . . 10
|
240 | | cjsub 10843 |
. . . . . . . . . . . . 13
|
241 | 14, 17, 240 | syl2anc 409 |
. . . . . . . . . . . 12
|
242 | 241 | oveq2d 5866 |
. . . . . . . . . . 11
|
243 | 14, 26, 31 | subdid 8320 |
. . . . . . . . . . 11
|
244 | 242, 243 | eqtrd 2203 |
. . . . . . . . . 10
|
245 | 239, 244 | oveq12d 5868 |
. . . . . . . . 9
|
246 | 234, 235,
245 | 3eqtr4d 2213 |
. . . . . . . 8
|
247 | 246 | oveq2d 5866 |
. . . . . . 7
|
248 | 233, 247 | eqtr3d 2205 |
. . . . . 6
|
249 | 248 | oveq1d 5865 |
. . . . 5
|
250 | 3, 6 | subcld 8217 |
. . . . . . . 8
|
251 | 24, 250 | mulcld 7927 |
. . . . . . 7
|
252 | 14, 17 | subcld 8217 |
. . . . . . . . 9
|
253 | 252 | cjcld 10891 |
. . . . . . . 8
|
254 | 14, 253 | mulcld 7927 |
. . . . . . 7
|
255 | 251, 254 | addcld 7926 |
. . . . . 6
|
256 | 226, 255,
191, 192 | divsubdirapd 8734 |
. . . . 5
|
257 | 251, 254,
191, 192 | divdirapd 8733 |
. . . . . . 7
|
258 | 24, 250, 191, 192 | divassapd 8730 |
. . . . . . . 8
|
259 | 14, 253, 191, 192 | divassapd 8730 |
. . . . . . . . 9
|
260 | 252, 191,
192 | cjdivapd 10919 |
. . . . . . . . . . 11
|
261 | 194 | cjred 10922 |
. . . . . . . . . . . 12
|
262 | 261 | oveq2d 5866 |
. . . . . . . . . . 11
|
263 | 260, 262 | eqtrd 2203 |
. . . . . . . . . 10
|
264 | 263 | oveq2d 5866 |
. . . . . . . . 9
|
265 | 259, 264 | eqtr4d 2206 |
. . . . . . . 8
|
266 | 258, 265 | oveq12d 5868 |
. . . . . . 7
|
267 | 257, 266 | eqtrd 2203 |
. . . . . 6
|
268 | 267 | oveq2d 5866 |
. . . . 5
|
269 | 249, 256,
268 | 3eqtrd 2207 |
. . . 4
|
270 | | mul4sq.10 |
. . . . . . 7
|
271 | 270 | nn0zd 9319 |
. . . . . 6
|
272 | | zgz 12312 |
. . . . . 6
|
273 | 271, 272 | syl 14 |
. . . . 5
|
274 | | gzcjcl 12315 |
. . . . . . . 8
|
275 | 1, 274 | syl 14 |
. . . . . . 7
|
276 | | mul4sq.8 |
. . . . . . 7
|
277 | | gzmulcl 12317 |
. . . . . . 7
|
278 | 275, 276,
277 | syl2anc 409 |
. . . . . 6
|
279 | | mul4sq.9 |
. . . . . . . 8
|
280 | | gzcjcl 12315 |
. . . . . . . 8
|
281 | 279, 280 | syl 14 |
. . . . . . 7
|
282 | | gzmulcl 12317 |
. . . . . . 7
|
283 | 12, 281, 282 | syl2anc 409 |
. . . . . 6
|
284 | | gzaddcl 12316 |
. . . . . 6
|
285 | 278, 283,
284 | syl2anc 409 |
. . . . 5
|
286 | | gzsubcl 12319 |
. . . . 5
|
287 | 273, 285,
286 | syl2anc 409 |
. . . 4
|
288 | 269, 287 | eqeltrd 2247 |
. . 3
|
289 | 250 | cjcld 10891 |
. . . . . . . 8
|
290 | 14, 289 | mulcld 7927 |
. . . . . . 7
|
291 | 24, 252 | mulcld 7927 |
. . . . . . 7
|
292 | 290, 291,
191, 192 | divsubdirapd 8734 |
. . . . . 6
|
293 | | cjsub 10843 |
. . . . . . . . . . . 12
|
294 | 3, 6, 293 | syl2anc 409 |
. . . . . . . . . . 11
|
295 | 294 | oveq2d 5866 |
. . . . . . . . . 10
|
296 | 14, 24, 29 | subdid 8320 |
. . . . . . . . . 10
|
297 | 295, 296 | eqtrd 2203 |
. . . . . . . . 9
|
298 | 24, 14, 17 | subdid 8320 |
. . . . . . . . . 10
|
299 | 24, 14 | mulcomd 7928 |
. . . . . . . . . . 11
|
300 | 299 | oveq1d 5865 |
. . . . . . . . . 10
|
301 | 298, 300 | eqtrd 2203 |
. . . . . . . . 9
|
302 | 297, 301 | oveq12d 5868 |
. . . . . . . 8
|
303 | 14, 24 | mulcld 7927 |
. . . . . . . . 9
|
304 | 303, 30, 98 | nnncan1d 8251 |
. . . . . . . 8
|
305 | 302, 304 | eqtrd 2203 |
. . . . . . 7
|
306 | 305 | oveq1d 5865 |
. . . . . 6
|
307 | 292, 306 | eqtr3d 2205 |
. . . . 5
|
308 | 14, 289, 191, 192 | divassapd 8730 |
. . . . . . 7
|
309 | 250, 191,
192 | cjdivapd 10919 |
. . . . . . . . 9
|
310 | 261 | oveq2d 5866 |
. . . . . . . . 9
|
311 | 309, 310 | eqtrd 2203 |
. . . . . . . 8
|
312 | 311 | oveq2d 5866 |
. . . . . . 7
|
313 | 308, 312 | eqtr4d 2206 |
. . . . . 6
|
314 | 24, 252, 191, 192 | divassapd 8730 |
. . . . . 6
|
315 | 313, 314 | oveq12d 5868 |
. . . . 5
|
316 | 307, 315 | eqtr3d 2205 |
. . . 4
|
317 | | gzcjcl 12315 |
. . . . . . 7
|
318 | 276, 317 | syl 14 |
. . . . . 6
|
319 | | gzmulcl 12317 |
. . . . . 6
|
320 | 12, 318, 319 | syl2anc 409 |
. . . . 5
|
321 | | gzmulcl 12317 |
. . . . . 6
|
322 | 275, 279,
321 | syl2anc 409 |
. . . . 5
|
323 | | gzsubcl 12319 |
. . . . 5
|
324 | 320, 322,
323 | syl2anc 409 |
. . . 4
|
325 | 316, 324 | eqeltrd 2247 |
. . 3
|
326 | | 4sq.1 |
. . . 4
|
327 | 326 | 4sqlem4a 12330 |
. . 3
|
328 | 288, 325,
327 | syl2anc 409 |
. 2
|
329 | 232, 328 | eqeltrrd 2248 |
1
|