Step | Hyp | Ref
| Expression |
1 | | lgseisen.1 |
. . 3
|
2 | | lgseisen.2 |
. . 3
|
3 | | lgseisen.3 |
. . 3
|
4 | 1, 2, 3 | lgseisen 25104 |
. 2
|
5 | | lgsquad.4 |
. . . . . 6
|
6 | 5 | oveq2i 6661 |
. . . . 5
|
7 | 6 | sumeq1i 14428 |
. . . 4
|
8 | | oddprm 15515 |
. . . . . . . . . . . . 13
|
9 | 1, 8 | syl 17 |
. . . . . . . . . . . 12
|
10 | 5, 9 | syl5eqel 2705 |
. . . . . . . . . . 11
|
11 | 10 | nnred 11035 |
. . . . . . . . . 10
|
12 | 11 | rehalfcld 11279 |
. . . . . . . . 9
|
13 | 12 | flcld 12599 |
. . . . . . . 8
|
14 | 13 | zred 11482 |
. . . . . . 7
|
15 | 14 | ltp1d 10954 |
. . . . . 6
|
16 | | fzdisj 12368 |
. . . . . 6
|
17 | 15, 16 | syl 17 |
. . . . 5
|
18 | 10 | nnrpd 11870 |
. . . . . . . . . . 11
|
19 | 18 | rphalfcld 11884 |
. . . . . . . . . 10
|
20 | 19 | rpge0d 11876 |
. . . . . . . . 9
|
21 | | flge0nn0 12621 |
. . . . . . . . 9
|
22 | 12, 20, 21 | syl2anc 693 |
. . . . . . . 8
|
23 | 10 | nnnn0d 11351 |
. . . . . . . 8
|
24 | | rphalflt 11860 |
. . . . . . . . . . 11
|
25 | 18, 24 | syl 17 |
. . . . . . . . . 10
|
26 | 10 | nnzd 11481 |
. . . . . . . . . . 11
|
27 | | fllt 12607 |
. . . . . . . . . . 11
|
28 | 12, 26, 27 | syl2anc 693 |
. . . . . . . . . 10
|
29 | 25, 28 | mpbid 222 |
. . . . . . . . 9
|
30 | 14, 11, 29 | ltled 10185 |
. . . . . . . 8
|
31 | | elfz2nn0 12431 |
. . . . . . . 8
|
32 | 22, 23, 30, 31 | syl3anbrc 1246 |
. . . . . . 7
|
33 | | nn0uz 11722 |
. . . . . . . . 9
|
34 | 23, 33 | syl6eleq 2711 |
. . . . . . . 8
|
35 | | elfzp12 12419 |
. . . . . . . 8
|
36 | 34, 35 | syl 17 |
. . . . . . 7
|
37 | 32, 36 | mpbid 222 |
. . . . . 6
|
38 | | oveq2 6658 |
. . . . . . . . . 10
|
39 | | fz10 12362 |
. . . . . . . . . 10
|
40 | 38, 39 | syl6eq 2672 |
. . . . . . . . 9
|
41 | | oveq1 6657 |
. . . . . . . . . . 11
|
42 | | 0p1e1 11132 |
. . . . . . . . . . 11
|
43 | 41, 42 | syl6eq 2672 |
. . . . . . . . . 10
|
44 | 43 | oveq1d 6665 |
. . . . . . . . 9
|
45 | 40, 44 | uneq12d 3768 |
. . . . . . . 8
|
46 | | un0 3967 |
. . . . . . . . 9
|
47 | | uncom 3757 |
. . . . . . . . 9
|
48 | 46, 47 | eqtr3i 2646 |
. . . . . . . 8
|
49 | 45, 48 | syl6reqr 2675 |
. . . . . . 7
|
50 | | fzsplit 12367 |
. . . . . . . 8
|
51 | 42 | oveq1i 6660 |
. . . . . . . 8
|
52 | 50, 51 | eleq2s 2719 |
. . . . . . 7
|
53 | 49, 52 | jaoi 394 |
. . . . . 6
|
54 | 37, 53 | syl 17 |
. . . . 5
|
55 | | fzfid 12772 |
. . . . 5
|
56 | 2 | eldifad 3586 |
. . . . . . . . . . . 12
|
57 | | prmnn 15388 |
. . . . . . . . . . . 12
|
58 | 56, 57 | syl 17 |
. . . . . . . . . . 11
|
59 | 58 | nnred 11035 |
. . . . . . . . . 10
|
60 | 1 | eldifad 3586 |
. . . . . . . . . . 11
|
61 | | prmnn 15388 |
. . . . . . . . . . 11
|
62 | 60, 61 | syl 17 |
. . . . . . . . . 10
|
63 | 59, 62 | nndivred 11069 |
. . . . . . . . 9
|
64 | 63 | adantr 481 |
. . . . . . . 8
|
65 | | 2nn 11185 |
. . . . . . . . . 10
|
66 | | elfznn 12370 |
. . . . . . . . . . 11
|
67 | 66 | adantl 482 |
. . . . . . . . . 10
|
68 | | nnmulcl 11043 |
. . . . . . . . . 10
|
69 | 65, 67, 68 | sylancr 695 |
. . . . . . . . 9
|
70 | 69 | nnred 11035 |
. . . . . . . 8
|
71 | 64, 70 | remulcld 10070 |
. . . . . . 7
|
72 | 58 | nnrpd 11870 |
. . . . . . . . . . 11
|
73 | 62 | nnrpd 11870 |
. . . . . . . . . . 11
|
74 | 72, 73 | rpdivcld 11889 |
. . . . . . . . . 10
|
75 | 74 | adantr 481 |
. . . . . . . . 9
|
76 | 69 | nnrpd 11870 |
. . . . . . . . 9
|
77 | 75, 76 | rpmulcld 11888 |
. . . . . . . 8
|
78 | 77 | rpge0d 11876 |
. . . . . . 7
|
79 | | flge0nn0 12621 |
. . . . . . 7
|
80 | 71, 78, 79 | syl2anc 693 |
. . . . . 6
|
81 | 80 | nn0cnd 11353 |
. . . . 5
|
82 | 17, 54, 55, 81 | fsumsplit 14471 |
. . . 4
|
83 | 7, 82 | syl5eqr 2670 |
. . 3
|
84 | 83 | oveq2d 6666 |
. 2
|
85 | | neg1cn 11124 |
. . . . 5
|
86 | 85 | a1i 11 |
. . . 4
|
87 | | fzfid 12772 |
. . . . 5
|
88 | | ssun2 3777 |
. . . . . . . 8
|
89 | 88, 54 | syl5sseqr 3654 |
. . . . . . 7
|
90 | 89 | sselda 3603 |
. . . . . 6
|
91 | 90, 80 | syldan 487 |
. . . . 5
|
92 | 87, 91 | fsumnn0cl 14467 |
. . . 4
|
93 | | fzfid 12772 |
. . . . 5
|
94 | | ssun1 3776 |
. . . . . . . 8
|
95 | 94, 54 | syl5sseqr 3654 |
. . . . . . 7
|
96 | 95 | sselda 3603 |
. . . . . 6
|
97 | 96, 80 | syldan 487 |
. . . . 5
|
98 | 93, 97 | fsumnn0cl 14467 |
. . . 4
|
99 | 86, 92, 98 | expaddd 13010 |
. . 3
|
100 | | fzfid 12772 |
. . . . . . . . 9
|
101 | | xpfi 8231 |
. . . . . . . . 9
|
102 | 55, 100, 101 | syl2anc 693 |
. . . . . . . 8
|
103 | | lgsquad.6 |
. . . . . . . . 9
|
104 | | opabssxp 5193 |
. . . . . . . . 9
|
105 | 103, 104 | eqsstri 3635 |
. . . . . . . 8
|
106 | | ssfi 8180 |
. . . . . . . 8
|
107 | 102, 105,
106 | sylancl 694 |
. . . . . . 7
|
108 | | ssrab2 3687 |
. . . . . . 7
|
109 | | ssfi 8180 |
. . . . . . 7
|
110 | 107, 108,
109 | sylancl 694 |
. . . . . 6
|
111 | | hashcl 13147 |
. . . . . 6
|
112 | 110, 111 | syl 17 |
. . . . 5
|
113 | | ssrab2 3687 |
. . . . . . 7
|
114 | | ssfi 8180 |
. . . . . . 7
|
115 | 107, 113,
114 | sylancl 694 |
. . . . . 6
|
116 | | hashcl 13147 |
. . . . . 6
|
117 | 115, 116 | syl 17 |
. . . . 5
|
118 | 86, 112, 117 | expaddd 13010 |
. . . 4
|
119 | 96, 69 | syldan 487 |
. . . . . . . . . . 11
|
120 | | fzfid 12772 |
. . . . . . . . . . 11
|
121 | | xpsnen2g 8053 |
. . . . . . . . . . 11
|
122 | 119, 120,
121 | syl2anc 693 |
. . . . . . . . . 10
|
123 | | hasheni 13136 |
. . . . . . . . . 10
|
124 | 122, 123 | syl 17 |
. . . . . . . . 9
|
125 | | ssrab2 3687 |
. . . . . . . . . . . . 13
|
126 | 103 | relopabi 5245 |
. . . . . . . . . . . . 13
|
127 | | relss 5206 |
. . . . . . . . . . . . 13
|
128 | 125, 126,
127 | mp2 9 |
. . . . . . . . . . . 12
|
129 | | relxp 5227 |
. . . . . . . . . . . 12
|
130 | 103 | eleq2i 2693 |
. . . . . . . . . . . . . . . 16
|
131 | | opabid 4982 |
. . . . . . . . . . . . . . . 16
|
132 | 130, 131 | bitri 264 |
. . . . . . . . . . . . . . 15
|
133 | | anass 681 |
. . . . . . . . . . . . . . . . . 18
|
134 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
135 | 62 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
136 | 134, 135 | nnmulcld 11068 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
137 | 136 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
138 | 58 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
139 | 138, 119 | nnmulcld 11068 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
140 | 139 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
141 | 140 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
142 | 137, 141 | ltlend 10182 |
. . . . . . . . . . . . . . . . . . . . . 22
|
143 | 119 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
144 | 143 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
145 | 135 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
146 | 145 | rehalfcld 11279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
147 | 11 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
148 | 147 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
149 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
150 | 149 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
151 | 147 | rehalfcld 11279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
152 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
153 | 152 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
154 | | flge 12606 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
155 | 151, 153,
154 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
156 | 150, 155 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
157 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
158 | 157 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
159 | 158 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
160 | | 2re 11090 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
161 | 160 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
162 | | 2pos 11112 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
163 | 162 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
164 | | lemuldiv2 10904 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
165 | 159, 147,
161, 163, 164 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
166 | 156, 165 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
167 | 166 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
168 | 145 | ltm1d 10956 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
169 | | peano2rem 10348 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
170 | 145, 169 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
171 | 160 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
172 | 162 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
173 | | ltdiv1 10887 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
174 | 170, 145,
171, 172, 173 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
175 | 168, 174 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
176 | 5, 175 | syl5eqbr 4688 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
177 | 144, 148,
146, 167, 176 | lelttrd 10195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
178 | 135 | nnrpd 11870 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
179 | | rphalflt 11860 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
180 | 178, 179 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
181 | 144, 146,
145, 177, 180 | lttrd 10198 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
182 | 144, 145 | ltnled 10184 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
183 | 181, 182 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
184 | 60 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
185 | | prmz 15389 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
186 | 184, 185 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
187 | | dvdsle 15032 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
188 | 186, 143,
187 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
189 | 183, 188 | mtod 189 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
190 | | prmrp 15424 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
191 | 60, 56, 190 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
192 | 3, 191 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
193 | 192 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
194 | 56 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
195 | | prmz 15389 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
196 | 194, 195 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
197 | 143 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
198 | | coprmdvds 15366 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
199 | 186, 196,
197, 198 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
200 | 193, 199 | mpan2d 710 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
201 | 189, 200 | mtod 189 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
202 | | nnz 11399 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
203 | 202 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
204 | | dvdsmul2 15004 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
205 | 203, 186,
204 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
206 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
207 | 205, 206 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
208 | 207 | necon3bd 2808 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
209 | 201, 208 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
210 | 209 | biantrud 528 |
. . . . . . . . . . . . . . . . . . . . . 22
|
211 | 142, 210 | bitr4d 271 |
. . . . . . . . . . . . . . . . . . . . 21
|
212 | | nnre 11027 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
213 | 212 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
|
214 | 135 | nngt0d 11064 |
. . . . . . . . . . . . . . . . . . . . . 22
|
215 | | lemuldiv 10903 |
. . . . . . . . . . . . . . . . . . . . . 22
|
216 | 213, 141,
145, 214, 215 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . . 21
|
217 | 138 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
218 | 217 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
219 | 143 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
220 | 135 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
221 | 135 | nnne0d 11065 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
222 | 218, 219,
220, 221 | div23d 10838 |
. . . . . . . . . . . . . . . . . . . . . 22
|
223 | 222 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . 21
|
224 | 211, 216,
223 | 3bitrd 294 |
. . . . . . . . . . . . . . . . . . . 20
|
225 | 217 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
226 | 217 | nngt0d 11064 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
227 | | ltmul2 10874 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
228 | 144, 146,
225, 226, 227 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
229 | 177, 228 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
230 | | 2cnd 11093 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
231 | | 2ne0 11113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
232 | 231 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
233 | | divass 10703 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
234 | | div23 10704 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
235 | 233, 234 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
236 | 218, 220,
230, 232, 235 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
237 | 229, 236 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
238 | 225 | rehalfcld 11279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
239 | 238, 145 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
240 | | lttr 10114 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
241 | 137, 141,
239, 240 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
242 | 237, 241 | mpan2d 710 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
243 | | ltmul1 10873 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
244 | 213, 238,
145, 214, 243 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
245 | 242, 244 | sylibrd 249 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
246 | | peano2rem 10348 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
247 | 225, 246 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
248 | 247 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
249 | 218, 248,
230, 232 | divsubdird 10840 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
250 | | lgsquad.5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
251 | 250 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
252 | 249, 251 | syl6eqr 2674 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
253 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
254 | | nncan 10310 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
255 | 218, 253,
254 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
256 | 255 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
257 | | halflt1 11250 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
258 | 256, 257 | syl6eqbr 4692 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
259 | 252, 258 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
260 | | oddprm 15515 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
261 | 2, 260 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
262 | 250, 261 | syl5eqel 2705 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
263 | 262 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
264 | 263 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
265 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
266 | 238, 264,
265 | ltsubadd2d 10625 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
267 | 259, 266 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
268 | | peano2re 10209 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
269 | 264, 268 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
270 | | lttr 10114 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
271 | 213, 238,
269, 270 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
272 | 267, 271 | mpan2d 710 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
273 | 245, 272 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . 22
|
274 | | nnleltp1 11432 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
275 | 134, 263,
274 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
|
276 | 273, 275 | sylibrd 249 |
. . . . . . . . . . . . . . . . . . . . 21
|
277 | 276 | pm4.71rd 667 |
. . . . . . . . . . . . . . . . . . . 20
|
278 | 96, 71 | syldan 487 |
. . . . . . . . . . . . . . . . . . . . 21
|
279 | | flge 12606 |
. . . . . . . . . . . . . . . . . . . . 21
|
280 | 278, 202,
279 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . 20
|
281 | 224, 277,
280 | 3bitr3d 298 |
. . . . . . . . . . . . . . . . . . 19
|
282 | 281 | pm5.32da 673 |
. . . . . . . . . . . . . . . . . 18
|
283 | 133, 282 | syl5bb 272 |
. . . . . . . . . . . . . . . . 17
|
284 | 283 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
285 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
|
286 | | nnuz 11723 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
287 | 119, 286 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
288 | 26 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
289 | | elfz5 12334 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
290 | 287, 288,
289 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
|
291 | 166, 290 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . 21
|
292 | 291 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
293 | 285, 292 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . 19
|
294 | 293 | biantrurd 529 |
. . . . . . . . . . . . . . . . . 18
|
295 | 262 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . 20
|
296 | 295 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
|
297 | | fznn 12408 |
. . . . . . . . . . . . . . . . . . 19
|
298 | 296, 297 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
299 | 294, 298 | bitr3d 270 |
. . . . . . . . . . . . . . . . 17
|
300 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . 19
|
301 | 119 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . 20
|
302 | 138 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . 20
|
303 | 301, 302 | mulcomd 10061 |
. . . . . . . . . . . . . . . . . . 19
|
304 | 300, 303 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . . . 18
|
305 | 304 | breq2d 4665 |
. . . . . . . . . . . . . . . . 17
|
306 | 299, 305 | anbi12d 747 |
. . . . . . . . . . . . . . . 16
|
307 | 278 | flcld 12599 |
. . . . . . . . . . . . . . . . . 18
|
308 | | fznn 12408 |
. . . . . . . . . . . . . . . . . 18
|
309 | 307, 308 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
310 | 309 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
311 | 284, 306,
310 | 3bitr4d 300 |
. . . . . . . . . . . . . . 15
|
312 | 132, 311 | syl5bb 272 |
. . . . . . . . . . . . . 14
|
313 | 312 | pm5.32da 673 |
. . . . . . . . . . . . 13
|
314 | | vex 3203 |
. . . . . . . . . . . . . . . . . 18
|
315 | | vex 3203 |
. . . . . . . . . . . . . . . . . 18
|
316 | 314, 315 | op1std 7178 |
. . . . . . . . . . . . . . . . 17
|
317 | 316 | eqeq2d 2632 |
. . . . . . . . . . . . . . . 16
|
318 | | eqcom 2629 |
. . . . . . . . . . . . . . . 16
|
319 | 317, 318 | syl6bb 276 |
. . . . . . . . . . . . . . 15
|
320 | 319 | elrab 3363 |
. . . . . . . . . . . . . 14
|
321 | | ancom 466 |
. . . . . . . . . . . . . 14
|
322 | 320, 321 | bitri 264 |
. . . . . . . . . . . . 13
|
323 | | opelxp 5146 |
. . . . . . . . . . . . . 14
|
324 | | velsn 4193 |
. . . . . . . . . . . . . . 15
|
325 | 324 | anbi1i 731 |
. . . . . . . . . . . . . 14
|
326 | 323, 325 | bitri 264 |
. . . . . . . . . . . . 13
|
327 | 313, 322,
326 | 3bitr4g 303 |
. . . . . . . . . . . 12
|
328 | 128, 129,
327 | eqrelrdv 5216 |
. . . . . . . . . . 11
|
329 | 328 | eqcomd 2628 |
. . . . . . . . . 10
|
330 | 329 | fveq2d 6195 |
. . . . . . . . 9
|
331 | | hashfz1 13134 |
. . . . . . . . . 10
|
332 | 97, 331 | syl 17 |
. . . . . . . . 9
|
333 | 124, 330,
332 | 3eqtr3rd 2665 |
. . . . . . . 8
|
334 | 333 | sumeq2dv 14433 |
. . . . . . 7
|
335 | 107 | adantr 481 |
. . . . . . . . 9
|
336 | | ssfi 8180 |
. . . . . . . . 9
|
337 | 335, 125,
336 | sylancl 694 |
. . . . . . . 8
|
338 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
339 | 338 | eqeq2d 2632 |
. . . . . . . . . . . . . . 15
|
340 | 339 | elrab 3363 |
. . . . . . . . . . . . . 14
|
341 | 340 | simprbi 480 |
. . . . . . . . . . . . 13
|
342 | 341 | ad2antll 765 |
. . . . . . . . . . . 12
|
343 | 342 | oveq1d 6665 |
. . . . . . . . . . 11
|
344 | 158 | nncnd 11036 |
. . . . . . . . . . . . 13
|
345 | 344 | adantrr 753 |
. . . . . . . . . . . 12
|
346 | | 2cnd 11093 |
. . . . . . . . . . . 12
|
347 | 231 | a1i 11 |
. . . . . . . . . . . 12
|
348 | 345, 346,
347 | divcan3d 10806 |
. . . . . . . . . . 11
|
349 | 343, 348 | eqtr3d 2658 |
. . . . . . . . . 10
|
350 | 349 | ralrimivva 2971 |
. . . . . . . . 9
|
351 | | invdisj 4638 |
. . . . . . . . 9
Disj |
352 | 350, 351 | syl 17 |
. . . . . . . 8
Disj
|
353 | 93, 337, 352 | hashiun 14554 |
. . . . . . 7
|
354 | | iunrab 4567 |
. . . . . . . . 9
|
355 | | 2cn 11091 |
. . . . . . . . . . . . . 14
|
356 | | zcn 11382 |
. . . . . . . . . . . . . . 15
|
357 | 356 | adantl 482 |
. . . . . . . . . . . . . 14
|
358 | | mulcom 10022 |
. . . . . . . . . . . . . 14
|
359 | 355, 357,
358 | sylancr 695 |
. . . . . . . . . . . . 13
|
360 | 359 | eqeq1d 2624 |
. . . . . . . . . . . 12
|
361 | 360 | rexbidva 3049 |
. . . . . . . . . . 11
|
362 | 152 | anim1i 592 |
. . . . . . . . . . . . 13
|
363 | 362 | reximi2 3010 |
. . . . . . . . . . . 12
|
364 | | simprr 796 |
. . . . . . . . . . . . . . . . . . 19
|
365 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
366 | 105, 365 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . . . 22
|
367 | | xp1st 7198 |
. . . . . . . . . . . . . . . . . . . . . 22
|
368 | 366, 367 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
369 | 368 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
370 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . . . . 20
|
371 | 369, 370 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
372 | 364, 371 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . 18
|
373 | | zre 11381 |
. . . . . . . . . . . . . . . . . . . 20
|
374 | 373 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . 19
|
375 | 11 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
|
376 | 160 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
377 | 162 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
378 | 374, 375,
376, 377, 164 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . 18
|
379 | 372, 378 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
|
380 | 12 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
|
381 | | simprl 794 |
. . . . . . . . . . . . . . . . . 18
|
382 | 380, 381,
154 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
383 | 379, 382 | mpbid 222 |
. . . . . . . . . . . . . . . 16
|
384 | | 2t0e0 11183 |
. . . . . . . . . . . . . . . . . . . . 21
|
385 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
386 | 369, 385 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
387 | 364, 386 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . . 22
|
388 | 387 | nngt0d 11064 |
. . . . . . . . . . . . . . . . . . . . 21
|
389 | 384, 388 | syl5eqbr 4688 |
. . . . . . . . . . . . . . . . . . . 20
|
390 | | 0red 10041 |
. . . . . . . . . . . . . . . . . . . . 21
|
391 | | ltmul2 10874 |
. . . . . . . . . . . . . . . . . . . . 21
|
392 | 390, 374,
376, 377, 391 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . 20
|
393 | 389, 392 | mpbird 247 |
. . . . . . . . . . . . . . . . . . 19
|
394 | | elnnz 11387 |
. . . . . . . . . . . . . . . . . . 19
|
395 | 381, 393,
394 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . 18
|
396 | 395, 286 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . 17
|
397 | 13 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
398 | | elfz5 12334 |
. . . . . . . . . . . . . . . . 17
|
399 | 396, 397,
398 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
400 | 383, 399 | mpbird 247 |
. . . . . . . . . . . . . . 15
|
401 | 400, 364 | jca 554 |
. . . . . . . . . . . . . 14
|
402 | 401 | ex 450 |
. . . . . . . . . . . . 13
|
403 | 402 | reximdv2 3014 |
. . . . . . . . . . . 12
|
404 | 363, 403 | impbid2 216 |
. . . . . . . . . . 11
|
405 | | 2z 11409 |
. . . . . . . . . . . 12
|
406 | | elfzelz 12342 |
. . . . . . . . . . . . 13
|
407 | 368, 406 | syl 17 |
. . . . . . . . . . . 12
|
408 | | divides 14985 |
. . . . . . . . . . . 12
|
409 | 405, 407,
408 | sylancr 695 |
. . . . . . . . . . 11
|
410 | 361, 404,
409 | 3bitr4d 300 |
. . . . . . . . . 10
|
411 | 410 | rabbidva 3188 |
. . . . . . . . 9
|
412 | 354, 411 | syl5eq 2668 |
. . . . . . . 8
|
413 | 412 | fveq2d 6195 |
. . . . . . 7
|
414 | 334, 353,
413 | 3eqtr2d 2662 |
. . . . . 6
|
415 | 414 | oveq2d 6666 |
. . . . 5
|
416 | 1, 2, 3, 5, 250, 103 | lgsquadlem1 25105 |
. . . . 5
|
417 | 415, 416 | oveq12d 6668 |
. . . 4
|
418 | 118, 417 | eqtr4d 2659 |
. . 3
|
419 | | unrab 3898 |
. . . . . . 7
|
420 | | exmid 431 |
. . . . . . . . 9
|
421 | 420 | rgenw 2924 |
. . . . . . . 8
|
422 | | rabid2 3118 |
. . . . . . . 8
|
423 | 421, 422 | mpbir 221 |
. . . . . . 7
|
424 | 419, 423 | eqtr4i 2647 |
. . . . . 6
|
425 | 424 | fveq2i 6194 |
. . . . 5
|
426 | | inrab 3899 |
. . . . . . 7
|
427 | | pm3.24 926 |
. . . . . . . . . 10
|
428 | 427 | a1i 11 |
. . . . . . . . 9
|
429 | 428 | ralrimivw 2967 |
. . . . . . . 8
|
430 | | rabeq0 3957 |
. . . . . . . 8
|
431 | 429, 430 | sylibr 224 |
. . . . . . 7
|
432 | 426, 431 | syl5eq 2668 |
. . . . . 6
|
433 | | hashun 13171 |
. . . . . 6
|
434 | 115, 110,
432, 433 | syl3anc 1326 |
. . . . 5
|
435 | 425, 434 | syl5reqr 2671 |
. . . 4
|
436 | 435 | oveq2d 6666 |
. . 3
|
437 | 99, 418, 436 | 3eqtr2d 2662 |
. 2
|
438 | 4, 84, 437 | 3eqtrd 2660 |
1
|