Proof of Theorem ioorrnopnlem
Step | Hyp | Ref
| Expression |
1 | | ioorrnopnlem.x |
. . . . 5
|
2 | | ioorrnopnlem.d |
. . . . 5
|
3 | 1, 2 | rrndsxmet 40523 |
. . . 4
|
4 | | nfv 1843 |
. . . . . 6
|
5 | | reex 10027 |
. . . . . . 7
|
6 | 5 | a1i 11 |
. . . . . 6
|
7 | | ioossre 12235 |
. . . . . . 7
|
8 | 7 | a1i 11 |
. . . . . 6
|
9 | 4, 6, 8 | ixpssmapc 39243 |
. . . . 5
|
10 | | ioorrnopnlem.f |
. . . . 5
|
11 | 9, 10 | sseldd 3604 |
. . . 4
|
12 | | ioorrnopnlem.e |
. . . . . 6
inf |
13 | | ioorrnopnlem.h |
. . . . . . . . 9
|
14 | 13 | a1i 11 |
. . . . . . . 8
|
15 | | ioorrnopnlem.b |
. . . . . . . . . . . . . 14
|
16 | 15 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
|
17 | 10 | adantr 481 |
. . . . . . . . . . . . . . 15
|
18 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
19 | | fvixp2 39389 |
. . . . . . . . . . . . . . 15
|
20 | 17, 18, 19 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
21 | 7, 20 | sseldi 3601 |
. . . . . . . . . . . . 13
|
22 | 16, 21 | resubcld 10458 |
. . . . . . . . . . . 12
|
23 | | ioorrnopnlem.a |
. . . . . . . . . . . . . . . 16
|
24 | 23 | ffvelrnda 6359 |
. . . . . . . . . . . . . . 15
|
25 | 24 | rexrd 10089 |
. . . . . . . . . . . . . 14
|
26 | 16 | rexrd 10089 |
. . . . . . . . . . . . . 14
|
27 | | iooltub 39735 |
. . . . . . . . . . . . . 14
|
28 | 25, 26, 20, 27 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
29 | 21, 16 | posdifd 10614 |
. . . . . . . . . . . . 13
|
30 | 28, 29 | mpbid 222 |
. . . . . . . . . . . 12
|
31 | 22, 30 | elrpd 11869 |
. . . . . . . . . . 11
|
32 | 21, 24 | resubcld 10458 |
. . . . . . . . . . . 12
|
33 | | ioogtlb 39717 |
. . . . . . . . . . . . . 14
|
34 | 25, 26, 20, 33 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
35 | 24, 21 | posdifd 10614 |
. . . . . . . . . . . . 13
|
36 | 34, 35 | mpbid 222 |
. . . . . . . . . . . 12
|
37 | 32, 36 | elrpd 11869 |
. . . . . . . . . . 11
|
38 | 31, 37 | ifcld 4131 |
. . . . . . . . . 10
|
39 | 38 | ralrimiva 2966 |
. . . . . . . . 9
|
40 | | eqid 2622 |
. . . . . . . . . 10
|
41 | 40 | rnmptss 6392 |
. . . . . . . . 9
|
42 | 39, 41 | syl 17 |
. . . . . . . 8
|
43 | 14, 42 | eqsstrd 3639 |
. . . . . . 7
|
44 | | ltso 10118 |
. . . . . . . . 9
|
45 | 44 | a1i 11 |
. . . . . . . 8
|
46 | 40 | rnmptfi 39351 |
. . . . . . . . . 10
|
47 | 1, 46 | syl 17 |
. . . . . . . . 9
|
48 | 13, 47 | syl5eqel 2705 |
. . . . . . . 8
|
49 | 38 | elexd 3214 |
. . . . . . . . . 10
|
50 | | ioorrnopnlem.n |
. . . . . . . . . 10
|
51 | 4, 49, 40, 50 | rnmptn0 39413 |
. . . . . . . . 9
|
52 | 14, 51 | eqnetrd 2861 |
. . . . . . . 8
|
53 | | rpssre 11843 |
. . . . . . . . . 10
|
54 | 53 | a1i 11 |
. . . . . . . . 9
|
55 | 43, 54 | sstrd 3613 |
. . . . . . . 8
|
56 | | fiinfcl 8407 |
. . . . . . . 8
inf |
57 | 45, 48, 52, 55, 56 | syl13anc 1328 |
. . . . . . 7
inf |
58 | 43, 57 | sseldd 3604 |
. . . . . 6
inf |
59 | 12, 58 | syl5eqel 2705 |
. . . . 5
|
60 | | rpxr 11840 |
. . . . 5
|
61 | 59, 60 | syl 17 |
. . . 4
|
62 | | eqid 2622 |
. . . . 5
|
63 | 62 | blopn 22305 |
. . . 4
|
64 | 3, 11, 61, 63 | syl3anc 1326 |
. . 3
|
65 | | ioorrnopnlem.v |
. . . . 5
|
66 | 65 | a1i 11 |
. . . 4
|
67 | 1 | rrxtopnfi 40506 |
. . . . 5
ℝ^
|
68 | 2 | eqcomi 2631 |
. . . . . . 7
|
69 | 68 | a1i 11 |
. . . . . 6
|
70 | 69 | fveq2d 6195 |
. . . . 5
|
71 | 67, 70 | eqtrd 2656 |
. . . 4
ℝ^ |
72 | 66, 71 | eleq12d 2695 |
. . 3
ℝ^
|
73 | 64, 72 | mpbird 247 |
. 2
ℝ^ |
74 | | xmetpsmet 22153 |
. . . . . 6
PsMet |
75 | 3, 74 | syl 17 |
. . . . 5
PsMet
|
76 | | blcntrps 22217 |
. . . . 5
PsMet
|
77 | 75, 11, 59, 76 | syl3anc 1326 |
. . . 4
|
78 | 66 | eqcomd 2628 |
. . . 4
|
79 | 77, 78 | eleqtrd 2703 |
. . 3
|
80 | | nfv 1843 |
. . . . 5
|
81 | | elmapfn 7880 |
. . . . . . . 8
|
82 | 81 | 3ad2ant2 1083 |
. . . . . . 7
|
83 | 25 | 3ad2antl1 1223 |
. . . . . . . . 9
|
84 | 26 | 3ad2antl1 1223 |
. . . . . . . . 9
|
85 | | simpl2 1065 |
. . . . . . . . . 10
|
86 | | simpr 477 |
. . . . . . . . . 10
|
87 | | elmapi 7879 |
. . . . . . . . . . . 12
|
88 | 87 | adantr 481 |
. . . . . . . . . . 11
|
89 | | simpr 477 |
. . . . . . . . . . 11
|
90 | 88, 89 | ffvelrnd 6360 |
. . . . . . . . . 10
|
91 | 85, 86, 90 | syl2anc 693 |
. . . . . . . . 9
|
92 | 24 | 3ad2antl1 1223 |
. . . . . . . . . 10
|
93 | 53, 59 | sseldi 3601 |
. . . . . . . . . . . . 13
|
94 | 93 | adantr 481 |
. . . . . . . . . . . 12
|
95 | 21, 94 | resubcld 10458 |
. . . . . . . . . . 11
|
96 | 95 | 3ad2antl1 1223 |
. . . . . . . . . 10
|
97 | 53, 38 | sseldi 3601 |
. . . . . . . . . . . . 13
|
98 | 12 | a1i 11 |
. . . . . . . . . . . . . . . 16
inf |
99 | | infxrrefi 39601 |
. . . . . . . . . . . . . . . . . 18
inf inf |
100 | 55, 48, 52, 99 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
inf inf
|
101 | 100 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
inf inf
|
102 | 98, 101 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
inf |
103 | 102 | adantr 481 |
. . . . . . . . . . . . . 14
inf |
104 | | ressxr 10083 |
. . . . . . . . . . . . . . . . . 18
|
105 | 104 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
106 | 55, 105 | sstrd 3613 |
. . . . . . . . . . . . . . . 16
|
107 | 106 | adantr 481 |
. . . . . . . . . . . . . . 15
|
108 | 40 | elrnmpt1 5374 |
. . . . . . . . . . . . . . . . 17
|
109 | 18, 49, 108 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
110 | 109, 13 | syl6eleqr 2712 |
. . . . . . . . . . . . . . 15
|
111 | | infxrlb 12164 |
. . . . . . . . . . . . . . 15
inf |
112 | 107, 110,
111 | syl2anc 693 |
. . . . . . . . . . . . . 14
inf |
113 | 103, 112 | eqbrtrd 4675 |
. . . . . . . . . . . . 13
|
114 | | min2 12021 |
. . . . . . . . . . . . . 14
|
115 | 22, 32, 114 | syl2anc 693 |
. . . . . . . . . . . . 13
|
116 | 94, 97, 32, 113, 115 | letrd 10194 |
. . . . . . . . . . . 12
|
117 | 94, 21, 24, 116 | lesubd 10631 |
. . . . . . . . . . 11
|
118 | 117 | 3ad2antl1 1223 |
. . . . . . . . . 10
|
119 | 21 | adantlr 751 |
. . . . . . . . . . . . . 14
|
120 | 90 | adantll 750 |
. . . . . . . . . . . . . 14
|
121 | 119, 120 | resubcld 10458 |
. . . . . . . . . . . . 13
|
122 | 121 | 3adantl3 1219 |
. . . . . . . . . . . 12
|
123 | 1, 2 | rrndsmet 40522 |
. . . . . . . . . . . . . . 15
|
124 | 123 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
125 | 11 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
126 | | simplr 792 |
. . . . . . . . . . . . . 14
|
127 | | metcl 22137 |
. . . . . . . . . . . . . 14
|
128 | 124, 125,
126, 127 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
129 | 128 | 3adantl3 1219 |
. . . . . . . . . . . 12
|
130 | 94 | adantlr 751 |
. . . . . . . . . . . . 13
|
131 | 130 | 3adantl3 1219 |
. . . . . . . . . . . 12
|
132 | 121 | recnd 10068 |
. . . . . . . . . . . . . . 15
|
133 | 132 | abscld 14175 |
. . . . . . . . . . . . . 14
|
134 | 121 | leabsd 14153 |
. . . . . . . . . . . . . 14
|
135 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
136 | | ixpf 7930 |
. . . . . . . . . . . . . . . . . . 19
|
137 | 10, 136 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
138 | 8 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . . 19
|
139 | | iunss 4561 |
. . . . . . . . . . . . . . . . . . 19
|
140 | 138, 139 | sylibr 224 |
. . . . . . . . . . . . . . . . . 18
|
141 | 137, 140 | fssd 6057 |
. . . . . . . . . . . . . . . . 17
|
142 | 141 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
143 | 126, 87 | syl 17 |
. . . . . . . . . . . . . . . 16
|
144 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
145 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
ℝ^ ℝ^ |
146 | 135, 142,
143, 144, 145 | rrnprjdstle 40521 |
. . . . . . . . . . . . . . 15
ℝ^ |
147 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
ℝ^ ℝ^ |
148 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
|
149 | 147, 148 | rrxdsfi 40505 |
. . . . . . . . . . . . . . . . . . 19
ℝ^
|
150 | 1, 149 | syl 17 |
. . . . . . . . . . . . . . . . . 18
ℝ^
|
151 | 150, 69 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
ℝ^ |
152 | 151 | oveqd 6667 |
. . . . . . . . . . . . . . . 16
ℝ^ |
153 | 152 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
ℝ^ |
154 | 146, 153 | breqtrd 4679 |
. . . . . . . . . . . . . 14
|
155 | 121, 133,
128, 134, 154 | letrd 10194 |
. . . . . . . . . . . . 13
|
156 | 155 | 3adantl3 1219 |
. . . . . . . . . . . 12
|
157 | | simpl3 1066 |
. . . . . . . . . . . 12
|
158 | 122, 129,
131, 156, 157 | lelttrd 10195 |
. . . . . . . . . . 11
|
159 | | ltsub23 10508 |
. . . . . . . . . . . . 13
|
160 | 119, 120,
130, 159 | syl3anc 1326 |
. . . . . . . . . . . 12
|
161 | 160 | 3adantl3 1219 |
. . . . . . . . . . 11
|
162 | 158, 161 | mpbid 222 |
. . . . . . . . . 10
|
163 | 92, 96, 91, 118, 162 | lelttrd 10195 |
. . . . . . . . 9
|
164 | 21, 94 | readdcld 10069 |
. . . . . . . . . . 11
|
165 | 164 | 3ad2antl1 1223 |
. . . . . . . . . 10
|
166 | 16 | 3ad2antl1 1223 |
. . . . . . . . . 10
|
167 | 120, 119 | resubcld 10458 |
. . . . . . . . . . . . 13
|
168 | 167 | 3adantl3 1219 |
. . . . . . . . . . . 12
|
169 | 167 | leabsd 14153 |
. . . . . . . . . . . . . . 15
|
170 | 120 | recnd 10068 |
. . . . . . . . . . . . . . . 16
|
171 | 119 | recnd 10068 |
. . . . . . . . . . . . . . . 16
|
172 | 170, 171 | abssubd 14192 |
. . . . . . . . . . . . . . 15
|
173 | 169, 172 | breqtrd 4679 |
. . . . . . . . . . . . . 14
|
174 | 167, 133,
128, 173, 154 | letrd 10194 |
. . . . . . . . . . . . 13
|
175 | 174 | 3adantl3 1219 |
. . . . . . . . . . . 12
|
176 | 168, 129,
131, 175, 157 | lelttrd 10195 |
. . . . . . . . . . 11
|
177 | 119 | 3adantl3 1219 |
. . . . . . . . . . . 12
|
178 | 91, 177, 131 | ltsubadd2d 10625 |
. . . . . . . . . . 11
|
179 | 176, 178 | mpbid 222 |
. . . . . . . . . 10
|
180 | | min1 12020 |
. . . . . . . . . . . . . 14
|
181 | 22, 32, 180 | syl2anc 693 |
. . . . . . . . . . . . 13
|
182 | 94, 97, 22, 113, 181 | letrd 10194 |
. . . . . . . . . . . 12
|
183 | 21, 94, 16 | leaddsub2d 10629 |
. . . . . . . . . . . 12
|
184 | 182, 183 | mpbird 247 |
. . . . . . . . . . 11
|
185 | 184 | 3ad2antl1 1223 |
. . . . . . . . . 10
|
186 | 91, 165, 166, 179, 185 | ltletrd 10197 |
. . . . . . . . 9
|
187 | 83, 84, 91, 163, 186 | eliood 39720 |
. . . . . . . 8
|
188 | 187 | ralrimiva 2966 |
. . . . . . 7
|
189 | 82, 188 | jca 554 |
. . . . . 6
|
190 | | vex 3203 |
. . . . . . 7
|
191 | 190 | elixp 7915 |
. . . . . 6
|
192 | 189, 191 | sylibr 224 |
. . . . 5
|
193 | 80, 75, 11, 61, 192 | ballss3 39270 |
. . . 4
|
194 | 66, 193 | eqsstrd 3639 |
. . 3
|
195 | 79, 194 | jca 554 |
. 2
|
196 | | eleq2 2690 |
. . . 4
|
197 | | sseq1 3626 |
. . . 4
|
198 | 196, 197 | anbi12d 747 |
. . 3
|
199 | 198 | rspcev 3309 |
. 2
ℝ^ ℝ^
|
200 | 73, 195, 199 | syl2anc 693 |
1
ℝ^
|