Step | Hyp | Ref
| Expression |
1 | | nnre 11027 |
. . . . . . . . . . . 12
|
2 | 1 | ad2antlr 763 |
. . . . . . . . . . 11
|
3 | | ltpnf 11954 |
. . . . . . . . . . 11
|
4 | 2, 3 | syl 17 |
. . . . . . . . . 10
|
5 | | iftrue 4092 |
. . . . . . . . . . 11
|
6 | 5 | adantl 482 |
. . . . . . . . . 10
|
7 | | simpr 477 |
. . . . . . . . . 10
|
8 | 4, 6, 7 | 3brtr4d 4685 |
. . . . . . . . 9
|
9 | | iffalse 4095 |
. . . . . . . . . . 11
|
10 | 9 | adantl 482 |
. . . . . . . . . 10
|
11 | | itg2cl 23499 |
. . . . . . . . . . . . . . 15
|
12 | | xrrebnd 11999 |
. . . . . . . . . . . . . . 15
|
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . 14
|
14 | | itg2ge0 23502 |
. . . . . . . . . . . . . . . 16
|
15 | | mnflt0 11959 |
. . . . . . . . . . . . . . . . 17
|
16 | | mnfxr 10096 |
. . . . . . . . . . . . . . . . . . 19
|
17 | | 0xr 10086 |
. . . . . . . . . . . . . . . . . . 19
|
18 | | xrltletr 11988 |
. . . . . . . . . . . . . . . . . . 19
|
19 | 16, 17, 18 | mp3an12 1414 |
. . . . . . . . . . . . . . . . . 18
|
20 | 11, 19 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
21 | 15, 20 | mpani 712 |
. . . . . . . . . . . . . . . 16
|
22 | 14, 21 | mpd 15 |
. . . . . . . . . . . . . . 15
|
23 | 22 | biantrurd 529 |
. . . . . . . . . . . . . 14
|
24 | | nltpnft 11995 |
. . . . . . . . . . . . . . . 16
|
25 | 11, 24 | syl 17 |
. . . . . . . . . . . . . . 15
|
26 | 25 | con2bid 344 |
. . . . . . . . . . . . . 14
|
27 | 13, 23, 26 | 3bitr2rd 297 |
. . . . . . . . . . . . 13
|
28 | 27 | biimpa 501 |
. . . . . . . . . . . 12
|
29 | 28 | adantlr 751 |
. . . . . . . . . . 11
|
30 | | nnrp 11842 |
. . . . . . . . . . . . 13
|
31 | 30 | rpreccld 11882 |
. . . . . . . . . . . 12
|
32 | 31 | ad2antlr 763 |
. . . . . . . . . . 11
|
33 | 29, 32 | ltsubrpd 11904 |
. . . . . . . . . 10
|
34 | 10, 33 | eqbrtrd 4675 |
. . . . . . . . 9
|
35 | 8, 34 | pm2.61dan 832 |
. . . . . . . 8
|
36 | | nnrecre 11057 |
. . . . . . . . . . . . 13
|
37 | 36 | ad2antlr 763 |
. . . . . . . . . . . 12
|
38 | 29, 37 | resubcld 10458 |
. . . . . . . . . . 11
|
39 | 2, 38 | ifclda 4120 |
. . . . . . . . . 10
|
40 | 39 | rexrd 10089 |
. . . . . . . . 9
|
41 | 11 | adantr 481 |
. . . . . . . . 9
|
42 | | xrltnle 10105 |
. . . . . . . . 9
|
43 | 40, 41, 42 | syl2anc 693 |
. . . . . . . 8
|
44 | 35, 43 | mpbid 222 |
. . . . . . 7
|
45 | | itg2leub 23501 |
. . . . . . . 8
|
46 | 40, 45 | syldan 487 |
. . . . . . 7
|
47 | 44, 46 | mtbid 314 |
. . . . . 6
|
48 | | rexanali 2998 |
. . . . . 6
|
49 | 47, 48 | sylibr 224 |
. . . . 5
|
50 | | itg1cl 23452 |
. . . . . . . 8
|
51 | | ltnle 10117 |
. . . . . . . 8
|
52 | 39, 50, 51 | syl2an 494 |
. . . . . . 7
|
53 | 52 | anbi2d 740 |
. . . . . 6
|
54 | 53 | rexbidva 3049 |
. . . . 5
|
55 | 49, 54 | mpbird 247 |
. . . 4
|
56 | 55 | ralrimiva 2966 |
. . 3
|
57 | | ovex 6678 |
. . . . 5
|
58 | | i1ff 23443 |
. . . . . . 7
|
59 | | reex 10027 |
. . . . . . . 8
|
60 | 59, 59 | elmap 7886 |
. . . . . . 7
|
61 | 58, 60 | sylibr 224 |
. . . . . 6
|
62 | 61 | ssriv 3607 |
. . . . 5
|
63 | 57, 62 | ssexi 4803 |
. . . 4
|
64 | | nnenom 12779 |
. . . 4
|
65 | | breq1 4656 |
. . . . 5
|
66 | | fveq2 6191 |
. . . . . 6
|
67 | 66 | breq2d 4665 |
. . . . 5
|
68 | 65, 67 | anbi12d 747 |
. . . 4
|
69 | 63, 64, 68 | axcc4 9261 |
. . 3
|
70 | 56, 69 | syl 17 |
. 2
|
71 | | simprl 794 |
. . . . 5
|
72 | | simpl 473 |
. . . . . . 7
|
73 | 72 | ralimi 2952 |
. . . . . 6
|
74 | 73 | ad2antll 765 |
. . . . 5
|
75 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
76 | 75 | fveq2d 6195 |
. . . . . . . . . . . 12
|
77 | 76 | cbvmptv 4750 |
. . . . . . . . . . 11
|
78 | 77 | rneqi 5352 |
. . . . . . . . . 10
|
79 | 78 | supeq1i 8353 |
. . . . . . . . 9
|
80 | | ffvelrn 6357 |
. . . . . . . . . . . . . . 15
|
81 | | itg1cl 23452 |
. . . . . . . . . . . . . . 15
|
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . . 14
|
83 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
84 | 82, 83 | fmptd 6385 |
. . . . . . . . . . . . 13
|
85 | 84 | ad2antrl 764 |
. . . . . . . . . . . 12
|
86 | | frn 6053 |
. . . . . . . . . . . 12
|
87 | 85, 86 | syl 17 |
. . . . . . . . . . 11
|
88 | | ressxr 10083 |
. . . . . . . . . . 11
|
89 | 87, 88 | syl6ss 3615 |
. . . . . . . . . 10
|
90 | | supxrcl 12145 |
. . . . . . . . . 10
|
91 | 89, 90 | syl 17 |
. . . . . . . . 9
|
92 | 79, 91 | syl5eqelr 2706 |
. . . . . . . 8
|
93 | | elxr 11950 |
. . . . . . . . . . 11
|
94 | | simplrl 800 |
. . . . . . . . . . . . . . . . . 18
|
95 | | arch 11289 |
. . . . . . . . . . . . . . . . . 18
|
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
97 | 5 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
98 | 97 | breq2d 4665 |
. . . . . . . . . . . . . . . . . 18
|
99 | 98 | rexbidv 3052 |
. . . . . . . . . . . . . . . . 17
|
100 | 96, 99 | mpbird 247 |
. . . . . . . . . . . . . . . 16
|
101 | 28 | adantlr 751 |
. . . . . . . . . . . . . . . . . . 19
|
102 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . 19
|
103 | 101, 102 | resubcld 10458 |
. . . . . . . . . . . . . . . . . 18
|
104 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . 19
|
105 | 102, 101 | posdifd 10614 |
. . . . . . . . . . . . . . . . . . 19
|
106 | 104, 105 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
|
107 | | nnrecl 11290 |
. . . . . . . . . . . . . . . . . 18
|
108 | 103, 106,
107 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
109 | 36 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
110 | 101 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
111 | 102 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
112 | | ltsub13 10509 |
. . . . . . . . . . . . . . . . . . . 20
|
113 | 109, 110,
111, 112 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
|
114 | 9 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . 20
|
115 | 114 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . 19
|
116 | 113, 115 | bitr4d 271 |
. . . . . . . . . . . . . . . . . 18
|
117 | 116 | rexbidva 3049 |
. . . . . . . . . . . . . . . . 17
|
118 | 108, 117 | mpbid 222 |
. . . . . . . . . . . . . . . 16
|
119 | 100, 118 | pm2.61dan 832 |
. . . . . . . . . . . . . . 15
|
120 | 119 | expr 643 |
. . . . . . . . . . . . . 14
|
121 | | rexr 10085 |
. . . . . . . . . . . . . . 15
|
122 | | xrltnle 10105 |
. . . . . . . . . . . . . . 15
|
123 | 121, 11, 122 | syl2anr 495 |
. . . . . . . . . . . . . 14
|
124 | 121 | ad2antlr 763 |
. . . . . . . . . . . . . . . . 17
|
125 | 40 | adantlr 751 |
. . . . . . . . . . . . . . . . 17
|
126 | | xrltnle 10105 |
. . . . . . . . . . . . . . . . 17
|
127 | 124, 125,
126 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
128 | 127 | rexbidva 3049 |
. . . . . . . . . . . . . . 15
|
129 | | rexnal 2995 |
. . . . . . . . . . . . . . 15
|
130 | 128, 129 | syl6bb 276 |
. . . . . . . . . . . . . 14
|
131 | 120, 123,
130 | 3imtr3d 282 |
. . . . . . . . . . . . 13
|
132 | 131 | con4d 114 |
. . . . . . . . . . . 12
|
133 | 11 | adantr 481 |
. . . . . . . . . . . . . . 15
|
134 | | pnfge 11964 |
. . . . . . . . . . . . . . 15
|
135 | 133, 134 | syl 17 |
. . . . . . . . . . . . . 14
|
136 | | simpr 477 |
. . . . . . . . . . . . . 14
|
137 | 135, 136 | breqtrrd 4681 |
. . . . . . . . . . . . 13
|
138 | 137 | a1d 25 |
. . . . . . . . . . . 12
|
139 | | 1nn 11031 |
. . . . . . . . . . . . . . 15
|
140 | 139 | ne0ii 3923 |
. . . . . . . . . . . . . 14
|
141 | | r19.2z 4060 |
. . . . . . . . . . . . . 14
|
142 | 140, 141 | mpan 706 |
. . . . . . . . . . . . 13
|
143 | 39 | adantlr 751 |
. . . . . . . . . . . . . . . . 17
|
144 | | mnflt 11957 |
. . . . . . . . . . . . . . . . . 18
|
145 | | rexr 10085 |
. . . . . . . . . . . . . . . . . . 19
|
146 | | xrltnle 10105 |
. . . . . . . . . . . . . . . . . . 19
|
147 | 16, 145, 146 | sylancr 695 |
. . . . . . . . . . . . . . . . . 18
|
148 | 144, 147 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
|
149 | 143, 148 | syl 17 |
. . . . . . . . . . . . . . . 16
|
150 | | simplr 792 |
. . . . . . . . . . . . . . . . 17
|
151 | 150 | breq2d 4665 |
. . . . . . . . . . . . . . . 16
|
152 | 149, 151 | mtbird 315 |
. . . . . . . . . . . . . . 15
|
153 | 152 | nrexdv 3001 |
. . . . . . . . . . . . . 14
|
154 | 153 | pm2.21d 118 |
. . . . . . . . . . . . 13
|
155 | 142, 154 | syl5 34 |
. . . . . . . . . . . 12
|
156 | 132, 138,
155 | 3jaodan 1394 |
. . . . . . . . . . 11
|
157 | 93, 156 | sylan2b 492 |
. . . . . . . . . 10
|
158 | 157 | ralrimiva 2966 |
. . . . . . . . 9
|
159 | 158 | adantr 481 |
. . . . . . . 8
|
160 | 40 | adantlr 751 |
. . . . . . . . . . . . 13
|
161 | 82 | adantll 750 |
. . . . . . . . . . . . . 14
|
162 | 161 | rexrd 10089 |
. . . . . . . . . . . . 13
|
163 | | xrltle 11982 |
. . . . . . . . . . . . 13
|
164 | 160, 162,
163 | syl2anc 693 |
. . . . . . . . . . . 12
|
165 | 84 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
166 | 165, 86 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
167 | 166, 88 | syl6ss 3615 |
. . . . . . . . . . . . . . . 16
|
168 | 167 | adantr 481 |
. . . . . . . . . . . . . . 15
|
169 | 78, 168 | syl5eqssr 3650 |
. . . . . . . . . . . . . 14
|
170 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
171 | 170 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
|
172 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
|
173 | | fvex 6201 |
. . . . . . . . . . . . . . . . 17
|
174 | 171, 172,
173 | fvmpt 6282 |
. . . . . . . . . . . . . . . 16
|
175 | | fvex 6201 |
. . . . . . . . . . . . . . . . . 18
|
176 | 175, 172 | fnmpti 6022 |
. . . . . . . . . . . . . . . . 17
|
177 | | fnfvelrn 6356 |
. . . . . . . . . . . . . . . . 17
|
178 | 176, 177 | mpan 706 |
. . . . . . . . . . . . . . . 16
|
179 | 174, 178 | eqeltrrd 2702 |
. . . . . . . . . . . . . . 15
|
180 | 179 | adantl 482 |
. . . . . . . . . . . . . 14
|
181 | | supxrub 12154 |
. . . . . . . . . . . . . 14
|
182 | 169, 180,
181 | syl2anc 693 |
. . . . . . . . . . . . 13
|
183 | 168, 90 | syl 17 |
. . . . . . . . . . . . . . 15
|
184 | 79, 183 | syl5eqelr 2706 |
. . . . . . . . . . . . . 14
|
185 | | xrletr 11989 |
. . . . . . . . . . . . . 14
|
186 | 160, 162,
184, 185 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
187 | 182, 186 | mpan2d 710 |
. . . . . . . . . . . 12
|
188 | 164, 187 | syld 47 |
. . . . . . . . . . 11
|
189 | 188 | adantld 483 |
. . . . . . . . . 10
|
190 | 189 | ralimdva 2962 |
. . . . . . . . 9
|
191 | 190 | impr 649 |
. . . . . . . 8
|
192 | | breq2 4657 |
. . . . . . . . . . 11
|
193 | 192 | ralbidv 2986 |
. . . . . . . . . 10
|
194 | | breq2 4657 |
. . . . . . . . . 10
|
195 | 193, 194 | imbi12d 334 |
. . . . . . . . 9
|
196 | 195 | rspcv 3305 |
. . . . . . . 8
|
197 | 92, 159, 191, 196 | syl3c 66 |
. . . . . . 7
|
198 | 197, 79 | syl6breqr 4695 |
. . . . . 6
|
199 | | itg2ub 23500 |
. . . . . . . . . . . . . . 15
|
200 | 199 | 3expia 1267 |
. . . . . . . . . . . . . 14
|
201 | 80, 200 | sylan2 491 |
. . . . . . . . . . . . 13
|
202 | 201 | anassrs 680 |
. . . . . . . . . . . 12
|
203 | 202 | adantrd 484 |
. . . . . . . . . . 11
|
204 | 203 | ralimdva 2962 |
. . . . . . . . . 10
|
205 | 204 | impr 649 |
. . . . . . . . 9
|
206 | 76, 83, 175 | fvmpt 6282 |
. . . . . . . . . . . 12
|
207 | 206 | breq1d 4663 |
. . . . . . . . . . 11
|
208 | 207 | ralbiia 2979 |
. . . . . . . . . 10
|
209 | 76 | breq1d 4663 |
. . . . . . . . . . 11
|
210 | 209 | cbvralv 3171 |
. . . . . . . . . 10
|
211 | 208, 210 | bitr4i 267 |
. . . . . . . . 9
|
212 | 205, 211 | sylibr 224 |
. . . . . . . 8
|
213 | | ffn 6045 |
. . . . . . . . 9
|
214 | | breq1 4656 |
. . . . . . . . . 10
|
215 | 214 | ralrn 6362 |
. . . . . . . . 9
|
216 | 85, 213, 215 | 3syl 18 |
. . . . . . . 8
|
217 | 212, 216 | mpbird 247 |
. . . . . . 7
|
218 | 11 | adantr 481 |
. . . . . . . 8
|
219 | | supxrleub 12156 |
. . . . . . . 8
|
220 | 89, 218, 219 | syl2anc 693 |
. . . . . . 7
|
221 | 217, 220 | mpbird 247 |
. . . . . 6
|
222 | 11 | adantr 481 |
. . . . . . . 8
|
223 | 167, 90 | syl 17 |
. . . . . . . 8
|
224 | | xrletri3 11985 |
. . . . . . . 8
|
225 | 222, 223,
224 | syl2anc 693 |
. . . . . . 7
|
226 | 225 | adantrr 753 |
. . . . . 6
|
227 | 198, 221,
226 | mpbir2and 957 |
. . . . 5
|
228 | 71, 74, 227 | 3jca 1242 |
. . . 4
|
229 | 228 | ex 450 |
. . 3
|
230 | 229 | eximdv 1846 |
. 2
|
231 | 70, 230 | mpd 15 |
1
|