Step | Hyp | Ref
| Expression |
1 | | fourierdlem64.i |
. . 3
..^ |
2 | | ssrab2 3687 |
. . . 4
..^ ..^ |
3 | | fzossfz 12488 |
. . . . . . . 8
..^ |
4 | | fzssz 12343 |
. . . . . . . 8
|
5 | 3, 4 | sstri 3612 |
. . . . . . 7
..^ |
6 | 2, 5 | sstri 3612 |
. . . . . 6
..^ |
7 | 6 | a1i 11 |
. . . . 5
..^
|
8 | | 0zd 11389 |
. . . . . . . 8
|
9 | | fourierdlem64.m |
. . . . . . . . 9
|
10 | 9 | nnzd 11481 |
. . . . . . . 8
|
11 | 9 | nngt0d 11064 |
. . . . . . . 8
|
12 | | fzolb 12476 |
. . . . . . . 8
..^ |
13 | 8, 10, 11, 12 | syl3anbrc 1246 |
. . . . . . 7
..^ |
14 | | fourierdlem64.l |
. . . . . . . . . 10
|
15 | | ssrab2 3687 |
. . . . . . . . . . . 12
|
16 | 15 | a1i 11 |
. . . . . . . . . . 11
|
17 | | fourierdlem64.h |
. . . . . . . . . . . . . . . . . . 19
|
18 | | fourierdlem64.c |
. . . . . . . . . . . . . . . . . . . . 21
|
19 | | fourierdlem64.d |
. . . . . . . . . . . . . . . . . . . . 21
|
20 | | prssi 4353 |
. . . . . . . . . . . . . . . . . . . . 21
|
21 | 18, 19, 20 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
|
22 | | ssrab2 3687 |
. . . . . . . . . . . . . . . . . . . . . 22
|
23 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
|
24 | 18, 19 | iccssred 39727 |
. . . . . . . . . . . . . . . . . . . . 21
|
25 | 23, 24 | sstrd 3613 |
. . . . . . . . . . . . . . . . . . . 20
|
26 | 21, 25 | unssd 3789 |
. . . . . . . . . . . . . . . . . . 19
|
27 | 17, 26 | syl5eqss 3649 |
. . . . . . . . . . . . . . . . . 18
|
28 | | fourierdlem64.t |
. . . . . . . . . . . . . . . . . . . . . 22
|
29 | | fourierdlem64.p |
. . . . . . . . . . . . . . . . . . . . . 22
..^ |
30 | | fourierdlem64.q |
. . . . . . . . . . . . . . . . . . . . . 22
|
31 | | fourierdlem64.cltd |
. . . . . . . . . . . . . . . . . . . . . 22
|
32 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
..^ |
33 | | fourierdlem64.n |
. . . . . . . . . . . . . . . . . . . . . 22
|
34 | | fourierdlem64.v |
. . . . . . . . . . . . . . . . . . . . . 22
|
35 | 28, 29, 9, 30, 18, 19, 31, 32, 17, 33, 34 | fourierdlem54 40377 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
36 | 35 | simprd 479 |
. . . . . . . . . . . . . . . . . . . 20
|
37 | | isof1o 6573 |
. . . . . . . . . . . . . . . . . . . 20
|
38 | | f1of 6137 |
. . . . . . . . . . . . . . . . . . . 20
|
39 | 36, 37, 38 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
|
40 | | fourierdlem64.j |
. . . . . . . . . . . . . . . . . . . 20
..^ |
41 | | elfzofz 12485 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
43 | 39, 42 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . 18
|
44 | 27, 43 | sseldd 3604 |
. . . . . . . . . . . . . . . . 17
|
45 | 29 | fourierdlem2 40326 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ |
46 | 9, 45 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
47 | 30, 46 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
48 | 47 | simpld 475 |
. . . . . . . . . . . . . . . . . . 19
|
49 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . 19
|
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
51 | 9 | nnnn0d 11351 |
. . . . . . . . . . . . . . . . . . . 20
|
52 | | nn0uz 11722 |
. . . . . . . . . . . . . . . . . . . 20
|
53 | 51, 52 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . 19
|
54 | | eluzfz1 12348 |
. . . . . . . . . . . . . . . . . . 19
|
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
56 | 50, 55 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . 17
|
57 | 44, 56 | resubcld 10458 |
. . . . . . . . . . . . . . . 16
|
58 | 29, 9, 30 | fourierdlem11 40335 |
. . . . . . . . . . . . . . . . . . 19
|
59 | 58 | simp2d 1074 |
. . . . . . . . . . . . . . . . . 18
|
60 | 58 | simp1d 1073 |
. . . . . . . . . . . . . . . . . 18
|
61 | 59, 60 | resubcld 10458 |
. . . . . . . . . . . . . . . . 17
|
62 | 28, 61 | syl5eqel 2705 |
. . . . . . . . . . . . . . . 16
|
63 | 58 | simp3d 1075 |
. . . . . . . . . . . . . . . . . . 19
|
64 | 60, 59 | posdifd 10614 |
. . . . . . . . . . . . . . . . . . 19
|
65 | 63, 64 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
|
66 | 65, 28 | syl6breqr 4695 |
. . . . . . . . . . . . . . . . 17
|
67 | 66 | gt0ne0d 10592 |
. . . . . . . . . . . . . . . 16
|
68 | 57, 62, 67 | redivcld 10853 |
. . . . . . . . . . . . . . 15
|
69 | | btwnz 11479 |
. . . . . . . . . . . . . . 15
|
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . 14
|
71 | 70 | simpld 475 |
. . . . . . . . . . . . 13
|
72 | | zre 11381 |
. . . . . . . . . . . . . . 15
|
73 | 56 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
|
74 | | simplr 792 |
. . . . . . . . . . . . . . . . . . 19
|
75 | 62 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
|
76 | 74, 75 | remulcld 10070 |
. . . . . . . . . . . . . . . . . 18
|
77 | 73, 76 | readdcld 10069 |
. . . . . . . . . . . . . . . . 17
|
78 | 44 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
79 | | simpr 477 |
. . . . . . . . . . . . . . . . . . 19
|
80 | 57 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
|
81 | 62, 66 | elrpd 11869 |
. . . . . . . . . . . . . . . . . . . . 21
|
82 | 81 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
|
83 | 74, 80, 82 | ltmuldivd 11919 |
. . . . . . . . . . . . . . . . . . 19
|
84 | 79, 83 | mpbird 247 |
. . . . . . . . . . . . . . . . . 18
|
85 | 56 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
86 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . 21
|
87 | 62 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
88 | 86, 87 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . . 20
|
89 | 44 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
90 | 85, 88, 89 | ltaddsub2d 10628 |
. . . . . . . . . . . . . . . . . . 19
|
91 | 90 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
92 | 84, 91 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
|
93 | 77, 78, 92 | ltled 10185 |
. . . . . . . . . . . . . . . 16
|
94 | 93 | ex 450 |
. . . . . . . . . . . . . . 15
|
95 | 72, 94 | sylan2 491 |
. . . . . . . . . . . . . 14
|
96 | 95 | reximdva 3017 |
. . . . . . . . . . . . 13
|
97 | 71, 96 | mpd 15 |
. . . . . . . . . . . 12
|
98 | | rabn0 3958 |
. . . . . . . . . . . 12
|
99 | 97, 98 | sylibr 224 |
. . . . . . . . . . 11
|
100 | | simpl 473 |
. . . . . . . . . . . . . 14
|
101 | 16 | sselda 3603 |
. . . . . . . . . . . . . 14
|
102 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . 19
|
103 | 102 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
|
104 | 103 | breq1d 4663 |
. . . . . . . . . . . . . . . . 17
|
105 | 104 | elrab 3363 |
. . . . . . . . . . . . . . . 16
|
106 | 105 | simprbi 480 |
. . . . . . . . . . . . . . 15
|
107 | 106 | adantl 482 |
. . . . . . . . . . . . . 14
|
108 | | zre 11381 |
. . . . . . . . . . . . . . 15
|
109 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
110 | 56 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
|
111 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
|
112 | 62 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
113 | 111, 112 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . 19
|
114 | 113 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
115 | 44 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
|
116 | 110, 114,
115 | leaddsub2d 10629 |
. . . . . . . . . . . . . . . . 17
|
117 | 109, 116 | mpbid 222 |
. . . . . . . . . . . . . . . 16
|
118 | | simplr 792 |
. . . . . . . . . . . . . . . . 17
|
119 | 57 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
120 | 81 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
121 | 118, 119,
120 | lemuldivd 11921 |
. . . . . . . . . . . . . . . 16
|
122 | 117, 121 | mpbid 222 |
. . . . . . . . . . . . . . 15
|
123 | 108, 122 | sylanl2 683 |
. . . . . . . . . . . . . 14
|
124 | 100, 101,
107, 123 | syl21anc 1325 |
. . . . . . . . . . . . 13
|
125 | 124 | ralrimiva 2966 |
. . . . . . . . . . . 12
|
126 | | breq2 4657 |
. . . . . . . . . . . . . 14
|
127 | 126 | ralbidv 2986 |
. . . . . . . . . . . . 13
|
128 | 127 | rspcev 3309 |
. . . . . . . . . . . 12
|
129 | 68, 125, 128 | syl2anc 693 |
. . . . . . . . . . 11
|
130 | | suprzcl 11457 |
. . . . . . . . . . 11
|
131 | 16, 99, 129, 130 | syl3anc 1326 |
. . . . . . . . . 10
|
132 | 14, 131 | syl5eqel 2705 |
. . . . . . . . 9
|
133 | | oveq1 6657 |
. . . . . . . . . . . 12
|
134 | 133 | oveq2d 6666 |
. . . . . . . . . . 11
|
135 | 134 | breq1d 4663 |
. . . . . . . . . 10
|
136 | 135 | elrab 3363 |
. . . . . . . . 9
|
137 | 132, 136 | sylib 208 |
. . . . . . . 8
|
138 | 137 | simprd 479 |
. . . . . . 7
|
139 | | fveq2 6191 |
. . . . . . . . . 10
|
140 | 139 | oveq1d 6665 |
. . . . . . . . 9
|
141 | 140 | breq1d 4663 |
. . . . . . . 8
|
142 | 141 | elrab 3363 |
. . . . . . 7
..^ ..^
|
143 | 13, 138, 142 | sylanbrc 698 |
. . . . . 6
..^ |
144 | | ne0i 3921 |
. . . . . 6
..^ ..^ |
145 | 143, 144 | syl 17 |
. . . . 5
..^
|
146 | 9 | nnred 11035 |
. . . . . 6
|
147 | 2 | a1i 11 |
. . . . . . . . 9
..^
..^ |
148 | 147 | sselda 3603 |
. . . . . . . 8
..^ ..^ |
149 | | elfzoelz 12470 |
. . . . . . . . . . 11
..^
|
150 | 149 | zred 11482 |
. . . . . . . . . 10
..^
|
151 | 150 | adantl 482 |
. . . . . . . . 9
..^ |
152 | 146 | adantr 481 |
. . . . . . . . 9
..^ |
153 | | elfzolt2 12479 |
. . . . . . . . . 10
..^
|
154 | 153 | adantl 482 |
. . . . . . . . 9
..^ |
155 | 151, 152,
154 | ltled 10185 |
. . . . . . . 8
..^ |
156 | 148, 155 | syldan 487 |
. . . . . . 7
..^ |
157 | 156 | ralrimiva 2966 |
. . . . . 6
..^ |
158 | | breq2 4657 |
. . . . . . . 8
|
159 | 158 | ralbidv 2986 |
. . . . . . 7
..^ ..^ |
160 | 159 | rspcev 3309 |
. . . . . 6
..^ ..^
|
161 | 146, 157,
160 | syl2anc 693 |
. . . . 5
..^ |
162 | | suprzcl 11457 |
. . . . 5
..^
..^ ..^
..^
..^ |
163 | 7, 145, 161, 162 | syl3anc 1326 |
. . . 4
..^ ..^ |
164 | 2, 163 | sseldi 3601 |
. . 3
..^ ..^ |
165 | 1, 164 | syl5eqel 2705 |
. 2
..^ |
166 | 15, 131 | sseldi 3601 |
. . 3
|
167 | 14, 166 | syl5eqel 2705 |
. 2
|
168 | 3, 165 | sseldi 3601 |
. . . . . . . . . 10
|
169 | 50, 168 | ffvelrnd 6360 |
. . . . . . . . 9
|
170 | 167 | zred 11482 |
. . . . . . . . . 10
|
171 | 170, 62 | remulcld 10070 |
. . . . . . . . 9
|
172 | 169, 171 | readdcld 10069 |
. . . . . . . 8
|
173 | 172 | rexrd 10089 |
. . . . . . 7
|
174 | 173 | adantr 481 |
. . . . . 6
|
175 | | fzofzp1 12565 |
. . . . . . . . . . 11
..^
|
176 | 165, 175 | syl 17 |
. . . . . . . . . 10
|
177 | 50, 176 | ffvelrnd 6360 |
. . . . . . . . 9
|
178 | 177, 171 | readdcld 10069 |
. . . . . . . 8
|
179 | 178 | rexrd 10089 |
. . . . . . 7
|
180 | 179 | adantr 481 |
. . . . . 6
|
181 | | elioore 12205 |
. . . . . . 7
|
182 | 181 | adantl 482 |
. . . . . 6
|
183 | 172 | adantr 481 |
. . . . . . 7
|
184 | 44 | adantr 481 |
. . . . . . 7
|
185 | 1, 163 | syl5eqel 2705 |
. . . . . . . . . 10
..^ |
186 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
187 | 186 | oveq1d 6665 |
. . . . . . . . . . . 12
|
188 | 187 | breq1d 4663 |
. . . . . . . . . . 11
|
189 | 188 | elrab 3363 |
. . . . . . . . . 10
..^ ..^
|
190 | 185, 189 | sylib 208 |
. . . . . . . . 9
..^
|
191 | 190 | simprd 479 |
. . . . . . . 8
|
192 | 191 | adantr 481 |
. . . . . . 7
|
193 | 184 | rexrd 10089 |
. . . . . . . 8
|
194 | | fzofzp1 12565 |
. . . . . . . . . . . . 13
..^
|
195 | 40, 194 | syl 17 |
. . . . . . . . . . . 12
|
196 | 39, 195 | ffvelrnd 6360 |
. . . . . . . . . . 11
|
197 | 27, 196 | sseldd 3604 |
. . . . . . . . . 10
|
198 | 197 | rexrd 10089 |
. . . . . . . . 9
|
199 | 198 | adantr 481 |
. . . . . . . 8
|
200 | | simpr 477 |
. . . . . . . 8
|
201 | | ioogtlb 39717 |
. . . . . . . 8
|
202 | 193, 199,
200, 201 | syl3anc 1326 |
. . . . . . 7
|
203 | 183, 184,
182, 192, 202 | lelttrd 10195 |
. . . . . 6
|
204 | | zssre 11384 |
. . . . . . . . . . . . . . . 16
|
205 | 15, 204 | sstri 3612 |
. . . . . . . . . . . . . . 15
|
206 | 205 | a1i 11 |
. . . . . . . . . . . . . 14
|
207 | 99 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
208 | 129 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
209 | 167 | peano2zd 11485 |
. . . . . . . . . . . . . . . 16
|
210 | 209 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
|
211 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
212 | 146 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
213 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
214 | 212, 213 | npcand 10396 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
215 | 211, 214 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . . . . . . . 22
|
216 | 215 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
|
217 | 47 | simprd 479 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^ |
218 | 217 | simpld 475 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
219 | 218 | simprd 479 |
. . . . . . . . . . . . . . . . . . . . . 22
|
220 | 219 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
221 | 59 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
222 | 60 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
223 | 221, 222 | npcand 10396 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
224 | 223 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
225 | 28 | eqcomi 2631 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
226 | 225 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
227 | 226 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
228 | 218 | simpld 475 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
229 | 228 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
230 | 229 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
231 | 224, 227,
230 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . . . . . 22
|
232 | 231 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
233 | 216, 220,
232 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . . . 20
|
234 | 62 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . 22
|
235 | 228, 222 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . . 22
|
236 | 234, 235 | addcomd 10238 |
. . . . . . . . . . . . . . . . . . . . 21
|
237 | 236 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
238 | 233, 237 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
|
239 | 238 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . 18
|
240 | 171 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . 21
|
241 | 235, 234,
240 | addassd 10062 |
. . . . . . . . . . . . . . . . . . . 20
|
242 | 234 | mulid2d 10058 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
243 | 242, 234 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
244 | 243, 240 | addcomd 10238 |
. . . . . . . . . . . . . . . . . . . . . 22
|
245 | 242 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
246 | 245 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . 22
|
247 | 170 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
248 | 247, 213,
234 | adddird 10065 |
. . . . . . . . . . . . . . . . . . . . . 22
|
249 | 244, 246,
248 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . . . . . . 21
|
250 | 249 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . 20
|
251 | 241, 250 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
|
252 | 251 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
253 | 239, 252 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . 17
|
254 | 253 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
255 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
256 | 254, 255 | eqbrtrd 4675 |
. . . . . . . . . . . . . . 15
|
257 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
|
258 | 257 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
|
259 | 258 | breq1d 4663 |
. . . . . . . . . . . . . . . 16
|
260 | 259 | elrab 3363 |
. . . . . . . . . . . . . . 15
|
261 | 210, 256,
260 | sylanbrc 698 |
. . . . . . . . . . . . . 14
|
262 | | suprub 10984 |
. . . . . . . . . . . . . 14
|
263 | 206, 207,
208, 261, 262 | syl31anc 1329 |
. . . . . . . . . . . . 13
|
264 | 263, 14 | syl6breqr 4695 |
. . . . . . . . . . . 12
|
265 | 170 | ltp1d 10954 |
. . . . . . . . . . . . . 14
|
266 | | peano2re 10209 |
. . . . . . . . . . . . . . . 16
|
267 | 170, 266 | syl 17 |
. . . . . . . . . . . . . . 15
|
268 | 170, 267 | ltnled 10184 |
. . . . . . . . . . . . . 14
|
269 | 265, 268 | mpbid 222 |
. . . . . . . . . . . . 13
|
270 | 269 | ad2antrr 762 |
. . . . . . . . . . . 12
|
271 | 264, 270 | pm2.65da 600 |
. . . . . . . . . . 11
|
272 | 5, 165 | sseldi 3601 |
. . . . . . . . . . . . . . 15
|
273 | 272 | zred 11482 |
. . . . . . . . . . . . . 14
|
274 | 273 | adantr 481 |
. . . . . . . . . . . . 13
|
275 | | peano2rem 10348 |
. . . . . . . . . . . . . . 15
|
276 | 146, 275 | syl 17 |
. . . . . . . . . . . . . 14
|
277 | 276 | adantr 481 |
. . . . . . . . . . . . 13
|
278 | | elfzolt2 12479 |
. . . . . . . . . . . . . . . 16
..^
|
279 | | elfzoelz 12470 |
. . . . . . . . . . . . . . . . 17
..^
|
280 | | elfzoel2 12469 |
. . . . . . . . . . . . . . . . 17
..^
|
281 | | zltlem1 11430 |
. . . . . . . . . . . . . . . . 17
|
282 | 279, 280,
281 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
..^
|
283 | 278, 282 | mpbid 222 |
. . . . . . . . . . . . . . 15
..^
|
284 | 165, 283 | syl 17 |
. . . . . . . . . . . . . 14
|
285 | 284 | adantr 481 |
. . . . . . . . . . . . 13
|
286 | | neqne 2802 |
. . . . . . . . . . . . . . 15
|
287 | 286 | necomd 2849 |
. . . . . . . . . . . . . 14
|
288 | 287 | adantl 482 |
. . . . . . . . . . . . 13
|
289 | 274, 277,
285, 288 | leneltd 10191 |
. . . . . . . . . . . 12
|
290 | 6, 204 | sstri 3612 |
. . . . . . . . . . . . . . . 16
..^ |
291 | 290 | a1i 11 |
. . . . . . . . . . . . . . 15
..^
|
292 | 145 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
..^
|
293 | 161 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
..^ |
294 | 176 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
295 | 273 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
296 | 276 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
297 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . . 20
|
298 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
|
299 | 295, 296,
297, 298 | ltadd1dd 10638 |
. . . . . . . . . . . . . . . . . . 19
|
300 | 214 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
301 | 299, 300 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . 18
|
302 | | elfzfzo 39488 |
. . . . . . . . . . . . . . . . . 18
..^
|
303 | 294, 301,
302 | sylanbrc 698 |
. . . . . . . . . . . . . . . . 17
..^ |
304 | 303 | anim1i 592 |
. . . . . . . . . . . . . . . 16
..^
|
305 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
|
306 | 305 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . 18
|
307 | 306 | breq1d 4663 |
. . . . . . . . . . . . . . . . 17
|
308 | 307 | elrab 3363 |
. . . . . . . . . . . . . . . 16
..^ ..^
|
309 | 304, 308 | sylibr 224 |
. . . . . . . . . . . . . . 15
..^ |
310 | | suprub 10984 |
. . . . . . . . . . . . . . 15
..^ ..^ ..^ ..^ ..^ |
311 | 291, 292,
293, 309, 310 | syl31anc 1329 |
. . . . . . . . . . . . . 14
..^
|
312 | 311, 1 | syl6breqr 4695 |
. . . . . . . . . . . . 13
|
313 | 273 | ltp1d 10954 |
. . . . . . . . . . . . . . 15
|
314 | | peano2re 10209 |
. . . . . . . . . . . . . . . . 17
|
315 | 273, 314 | syl 17 |
. . . . . . . . . . . . . . . 16
|
316 | 273, 315 | ltnled 10184 |
. . . . . . . . . . . . . . 15
|
317 | 313, 316 | mpbid 222 |
. . . . . . . . . . . . . 14
|
318 | 317 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
319 | 312, 318 | pm2.65da 600 |
. . . . . . . . . . . 12
|
320 | 289, 319 | syldan 487 |
. . . . . . . . . . 11
|
321 | 271, 320 | pm2.61dan 832 |
. . . . . . . . . 10
|
322 | 44, 178 | ltnled 10184 |
. . . . . . . . . 10
|
323 | 321, 322 | mpbird 247 |
. . . . . . . . 9
|
324 | 197 | adantr 481 |
. . . . . . . . . . . 12
|
325 | 19 | adantr 481 |
. . . . . . . . . . . 12
|
326 | 178 | adantr 481 |
. . . . . . . . . . . 12
|
327 | 18 | rexrd 10089 |
. . . . . . . . . . . . . 14
|
328 | 19 | rexrd 10089 |
. . . . . . . . . . . . . 14
|
329 | 18, 19, 31 | ltled 10185 |
. . . . . . . . . . . . . . . . . . . 20
|
330 | | lbicc2 12288 |
. . . . . . . . . . . . . . . . . . . 20
|
331 | 327, 328,
329, 330 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
|
332 | | ubicc2 12289 |
. . . . . . . . . . . . . . . . . . . 20
|
333 | 327, 328,
329, 332 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
|
334 | 331, 333 | jca 554 |
. . . . . . . . . . . . . . . . . 18
|
335 | | prssg 4350 |
. . . . . . . . . . . . . . . . . . 19
|
336 | 18, 19, 335 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
|
337 | 334, 336 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
|
338 | 337, 23 | unssd 3789 |
. . . . . . . . . . . . . . . 16
|
339 | 17, 338 | syl5eqss 3649 |
. . . . . . . . . . . . . . 15
|
340 | 339, 196 | sseldd 3604 |
. . . . . . . . . . . . . 14
|
341 | | iccleub 12229 |
. . . . . . . . . . . . . 14
|
342 | 327, 328,
340, 341 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
343 | 342 | adantr 481 |
. . . . . . . . . . . 12
|
344 | | simpr 477 |
. . . . . . . . . . . 12
|
345 | 324, 325,
326, 343, 344 | letrd 10194 |
. . . . . . . . . . 11
|
346 | 345 | adantlr 751 |
. . . . . . . . . 10
|
347 | | simpr 477 |
. . . . . . . . . . . . 13
|
348 | 178 | adantr 481 |
. . . . . . . . . . . . . 14
|
349 | 19 | adantr 481 |
. . . . . . . . . . . . . 14
|
350 | 348, 349 | ltnled 10184 |
. . . . . . . . . . . . 13
|
351 | 347, 350 | mpbird 247 |
. . . . . . . . . . . 12
|
352 | 351 | adantlr 751 |
. . . . . . . . . . 11
|
353 | | simpll 790 |
. . . . . . . . . . . . 13
|
354 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
355 | 178 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
356 | 197 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
357 | 355, 356 | ltnled 10184 |
. . . . . . . . . . . . . . 15
|
358 | 354, 357 | mpbird 247 |
. . . . . . . . . . . . . 14
|
359 | 358 | ad4ant14 1293 |
. . . . . . . . . . . . 13
|
360 | 18 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
|
361 | 19 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
|
362 | 178 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
|
363 | 18 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
364 | 178 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
365 | 44 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
366 | 339, 43 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
367 | | iccgelb 12230 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
368 | 327, 328,
366, 367 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . 22
|
369 | 368 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
370 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . 21
|
371 | 363, 365,
364, 369, 370 | lelttrd 10195 |
. . . . . . . . . . . . . . . . . . . 20
|
372 | 363, 364,
371 | ltled 10185 |
. . . . . . . . . . . . . . . . . . 19
|
373 | 372 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
374 | 178 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
375 | 19 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
376 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
|
377 | 374, 375,
376 | ltled 10185 |
. . . . . . . . . . . . . . . . . . 19
|
378 | 377 | adantlr 751 |
. . . . . . . . . . . . . . . . . 18
|
379 | 360, 361,
362, 373, 378 | eliccd 39726 |
. . . . . . . . . . . . . . . . 17
|
380 | 167 | znegcld 11484 |
. . . . . . . . . . . . . . . . . . 19
|
381 | 247, 234 | mulneg1d 10483 |
. . . . . . . . . . . . . . . . . . . . . 22
|
382 | 381 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . 21
|
383 | 178 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . 22
|
384 | 383, 240 | negsubd 10398 |
. . . . . . . . . . . . . . . . . . . . 21
|
385 | 177 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . 22
|
386 | 385, 240 | pncand 10393 |
. . . . . . . . . . . . . . . . . . . . 21
|
387 | 382, 384,
386 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . . . 20
|
388 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . . 22
|
389 | 50, 388 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
390 | | fnfvelrn 6356 |
. . . . . . . . . . . . . . . . . . . . 21
|
391 | 389, 176,
390 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
|
392 | 387, 391 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . 19
|
393 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . 22
|
394 | 393 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . 21
|
395 | 394 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . 20
|
396 | 395 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . 19
|
397 | 380, 392,
396 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
|
398 | 397 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
399 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . 20
|
400 | 399 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . 19
|
401 | 400 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . 18
|
402 | 401 | elrab 3363 |
. . . . . . . . . . . . . . . . 17
|
403 | 379, 398,
402 | sylanbrc 698 |
. . . . . . . . . . . . . . . 16
|
404 | | elun2 3781 |
. . . . . . . . . . . . . . . 16
|
405 | 403, 404 | syl 17 |
. . . . . . . . . . . . . . 15
|
406 | 17 | eqcomi 2631 |
. . . . . . . . . . . . . . 15
|
407 | 405, 406 | syl6eleq 2711 |
. . . . . . . . . . . . . 14
|
408 | 407 | adantr 481 |
. . . . . . . . . . . . 13
|
409 | | f1ofo 6144 |
. . . . . . . . . . . . . . . . . 18
|
410 | 36, 37, 409 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
|
411 | | foelrn 6378 |
. . . . . . . . . . . . . . . . 17
|
412 | 410, 411 | sylan 488 |
. . . . . . . . . . . . . . . 16
|
413 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
|
414 | 413 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . 18
|
415 | 414 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
416 | 415 | reximdv 3016 |
. . . . . . . . . . . . . . . 16
|
417 | 412, 416 | mpd 15 |
. . . . . . . . . . . . . . 15
|
418 | 417 | ad4ant14 1293 |
. . . . . . . . . . . . . 14
|
419 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
420 | 413 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
421 | 420 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
422 | 419, 421 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . . 22
|
423 | 422 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . 21
|
424 | 423 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . 20
|
425 | 36 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . 21
|
426 | 42 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . 21
|
427 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . 21
|
428 | | isorel 6576 |
. . . . . . . . . . . . . . . . . . . . 21
|
429 | 425, 426,
427, 428 | syl12anc 1324 |
. . . . . . . . . . . . . . . . . . . 20
|
430 | 424, 429 | mpbird 247 |
. . . . . . . . . . . . . . . . . . 19
|
431 | 430 | adantllr 755 |
. . . . . . . . . . . . . . . . . 18
|
432 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
433 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
434 | 432, 433 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . . . 22
|
435 | 434 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . 21
|
436 | 435 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . 20
|
437 | 36 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . 21
|
438 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . 21
|
439 | 195 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . 21
|
440 | | isorel 6576 |
. . . . . . . . . . . . . . . . . . . . 21
|
441 | 437, 438,
439, 440 | syl12anc 1324 |
. . . . . . . . . . . . . . . . . . . 20
|
442 | 436, 441 | mpbird 247 |
. . . . . . . . . . . . . . . . . . 19
|
443 | 442 | adantlllr 39199 |
. . . . . . . . . . . . . . . . . 18
|
444 | 431, 443 | jca 554 |
. . . . . . . . . . . . . . . . 17
|
445 | 444 | ex 450 |
. . . . . . . . . . . . . . . 16
|
446 | 445 | adantlr 751 |
. . . . . . . . . . . . . . 15
|
447 | 446 | reximdva 3017 |
. . . . . . . . . . . . . 14
|
448 | 418, 447 | mpd 15 |
. . . . . . . . . . . . 13
|
449 | 353, 359,
408, 448 | syl21anc 1325 |
. . . . . . . . . . . 12
|
450 | | elfzelz 12342 |
. . . . . . . . . . . . . . . 16
|
451 | 450 | ad2antlr 763 |
. . . . . . . . . . . . . . 15
|
452 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . . 18
|
453 | 42, 452 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
454 | 453 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
455 | | simprl 794 |
. . . . . . . . . . . . . . . 16
|
456 | | simprr 796 |
. . . . . . . . . . . . . . . 16
|
457 | | btwnnz 11453 |
. . . . . . . . . . . . . . . 16
|
458 | 454, 455,
456, 457 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
|
459 | 451, 458 | pm2.65da 600 |
. . . . . . . . . . . . . 14
|
460 | 459 | nrexdv 3001 |
. . . . . . . . . . . . 13
|
461 | 460 | ad3antrrr 766 |
. . . . . . . . . . . 12
|
462 | 449, 461 | condan 835 |
. . . . . . . . . . 11
|
463 | 352, 462 | syldan 487 |
. . . . . . . . . 10
|
464 | 346, 463 | pm2.61dan 832 |
. . . . . . . . 9
|
465 | 323, 464 | mpdan 702 |
. . . . . . . 8
|
466 | 465 | adantr 481 |
. . . . . . 7
|
467 | 182 | adantr 481 |
. . . . . . . 8
|
468 | 197 | ad2antrr 762 |
. . . . . . . 8
|
469 | 178 | ad2antrr 762 |
. . . . . . . 8
|
470 | | iooltub 39735 |
. . . . . . . . . 10
|
471 | 193, 199,
200, 470 | syl3anc 1326 |
. . . . . . . . 9
|
472 | 471 | adantr 481 |
. . . . . . . 8
|
473 | | simpr 477 |
. . . . . . . 8
|
474 | 467, 468,
469, 472, 473 | ltletrd 10197 |
. . . . . . 7
|
475 | 466, 474 | mpdan 702 |
. . . . . 6
|
476 | 174, 180,
182, 203, 475 | eliood 39720 |
. . . . 5
|
477 | 476 | ralrimiva 2966 |
. . . 4
|
478 | | dfss3 3592 |
. . . 4
|
479 | 477, 478 | sylibr 224 |
. . 3
|
480 | | fveq2 6191 |
. . . . . . 7
|
481 | 480 | oveq1d 6665 |
. . . . . 6
|
482 | | oveq1 6657 |
. . . . . . . 8
|
483 | 482 | fveq2d 6195 |
. . . . . . 7
|
484 | 483 | oveq1d 6665 |
. . . . . 6
|
485 | 481, 484 | oveq12d 6668 |
. . . . 5
|
486 | 485 | sseq2d 3633 |
. . . 4
|
487 | | oveq1 6657 |
. . . . . . 7
|
488 | 487 | oveq2d 6666 |
. . . . . 6
|
489 | 487 | oveq2d 6666 |
. . . . . 6
|
490 | 488, 489 | oveq12d 6668 |
. . . . 5
|
491 | 490 | sseq2d 3633 |
. . . 4
|
492 | 486, 491 | rspc2ev 3324 |
. . 3
..^
..^
|
493 | 165, 167,
479, 492 | syl3anc 1326 |
. 2
..^ |
494 | 165, 167,
493 | jca31 557 |
1
..^ ..^
|