Proof of Theorem ioorrnopnxrlem
Step | Hyp | Ref
| Expression |
1 | | ioorrnopnxrlem.v |
. . . 4
|
2 | 1 | a1i 11 |
. . 3
|
3 | | ioorrnopnxrlem.x |
. . . 4
|
4 | | iftrue 4092 |
. . . . . . . 8
|
5 | 4 | adantl 482 |
. . . . . . 7
|
6 | | ioorrnopnxrlem.f |
. . . . . . . . . . . 12
|
7 | 6 | adantr 481 |
. . . . . . . . . . 11
|
8 | | simpr 477 |
. . . . . . . . . . 11
|
9 | | fvixp2 39389 |
. . . . . . . . . . 11
|
10 | 7, 8, 9 | syl2anc 693 |
. . . . . . . . . 10
|
11 | 10 | elioored 39776 |
. . . . . . . . 9
|
12 | | 1red 10055 |
. . . . . . . . 9
|
13 | 11, 12 | resubcld 10458 |
. . . . . . . 8
|
14 | 13 | adantr 481 |
. . . . . . 7
|
15 | 5, 14 | eqeltrd 2701 |
. . . . . 6
|
16 | | iffalse 4095 |
. . . . . . . 8
|
17 | 16 | adantl 482 |
. . . . . . 7
|
18 | | neqne 2802 |
. . . . . . . . 9
|
19 | 18 | adantl 482 |
. . . . . . . 8
|
20 | | ioorrnopnxrlem.a |
. . . . . . . . . . 11
|
21 | 20 | ffvelrnda 6359 |
. . . . . . . . . 10
|
22 | 21 | adantr 481 |
. . . . . . . . 9
|
23 | | simpr 477 |
. . . . . . . . 9
|
24 | | pnfxr 10092 |
. . . . . . . . . . . 12
|
25 | 24 | a1i 11 |
. . . . . . . . . . 11
|
26 | 11 | rexrd 10089 |
. . . . . . . . . . . 12
|
27 | | ioorrnopnxrlem.b |
. . . . . . . . . . . . . 14
|
28 | 27 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
|
29 | | ioogtlb 39717 |
. . . . . . . . . . . . 13
|
30 | 21, 28, 10, 29 | syl3anc 1326 |
. . . . . . . . . . . 12
|
31 | 11 | ltpnfd 11955 |
. . . . . . . . . . . 12
|
32 | 21, 26, 25, 30, 31 | xrlttrd 11990 |
. . . . . . . . . . 11
|
33 | 21, 25, 32 | xrltned 39573 |
. . . . . . . . . 10
|
34 | 33 | adantr 481 |
. . . . . . . . 9
|
35 | 22, 23, 34 | xrred 39581 |
. . . . . . . 8
|
36 | 19, 35 | syldan 487 |
. . . . . . 7
|
37 | 17, 36 | eqeltrd 2701 |
. . . . . 6
|
38 | 15, 37 | pm2.61dan 832 |
. . . . 5
|
39 | | ioorrnopnxrlem.l |
. . . . 5
|
40 | 38, 39 | fmptd 6385 |
. . . 4
|
41 | | iftrue 4092 |
. . . . . . . 8
|
42 | 41 | adantl 482 |
. . . . . . 7
|
43 | 11, 12 | readdcld 10069 |
. . . . . . . 8
|
44 | 43 | adantr 481 |
. . . . . . 7
|
45 | 42, 44 | eqeltrd 2701 |
. . . . . 6
|
46 | | iffalse 4095 |
. . . . . . . 8
|
47 | 46 | adantl 482 |
. . . . . . 7
|
48 | | neqne 2802 |
. . . . . . . . 9
|
49 | 48 | adantl 482 |
. . . . . . . 8
|
50 | 28 | adantr 481 |
. . . . . . . . 9
|
51 | | mnfxr 10096 |
. . . . . . . . . . . 12
|
52 | 51 | a1i 11 |
. . . . . . . . . . 11
|
53 | 11 | mnfltd 11958 |
. . . . . . . . . . . 12
|
54 | | iooltub 39735 |
. . . . . . . . . . . . 13
|
55 | 21, 28, 10, 54 | syl3anc 1326 |
. . . . . . . . . . . 12
|
56 | 52, 26, 28, 53, 55 | xrlttrd 11990 |
. . . . . . . . . . 11
|
57 | 52, 28, 56 | xrgtned 39538 |
. . . . . . . . . 10
|
58 | 57 | adantr 481 |
. . . . . . . . 9
|
59 | | simpr 477 |
. . . . . . . . 9
|
60 | 50, 58, 59 | xrred 39581 |
. . . . . . . 8
|
61 | 49, 60 | syldan 487 |
. . . . . . 7
|
62 | 47, 61 | eqeltrd 2701 |
. . . . . 6
|
63 | 45, 62 | pm2.61dan 832 |
. . . . 5
|
64 | | ioorrnopnxrlem.r |
. . . . 5
|
65 | 63, 64 | fmptd 6385 |
. . . 4
|
66 | 3, 40, 65 | ioorrnopn 40525 |
. . 3
ℝ^ |
67 | 2, 66 | eqeltrd 2701 |
. 2
ℝ^ |
68 | 6 | elexd 3214 |
. . . . . 6
|
69 | | ixpfn 7914 |
. . . . . . 7
|
70 | 6, 69 | syl 17 |
. . . . . 6
|
71 | 40 | ffvelrnda 6359 |
. . . . . . . . 9
|
72 | 71 | rexrd 10089 |
. . . . . . . 8
|
73 | 65 | ffvelrnda 6359 |
. . . . . . . . 9
|
74 | 73 | rexrd 10089 |
. . . . . . . 8
|
75 | 39 | a1i 11 |
. . . . . . . . . . . . 13
|
76 | 38 | elexd 3214 |
. . . . . . . . . . . . 13
|
77 | 75, 76 | fvmpt2d 6293 |
. . . . . . . . . . . 12
|
78 | 77 | adantr 481 |
. . . . . . . . . . 11
|
79 | 78, 5 | eqtrd 2656 |
. . . . . . . . . 10
|
80 | 11 | ltm1d 10956 |
. . . . . . . . . . 11
|
81 | 80 | adantr 481 |
. . . . . . . . . 10
|
82 | 79, 81 | eqbrtrd 4675 |
. . . . . . . . 9
|
83 | 77 | adantr 481 |
. . . . . . . . . . 11
|
84 | 83, 17 | eqtrd 2656 |
. . . . . . . . . 10
|
85 | 30 | adantr 481 |
. . . . . . . . . 10
|
86 | 84, 85 | eqbrtrd 4675 |
. . . . . . . . 9
|
87 | 82, 86 | pm2.61dan 832 |
. . . . . . . 8
|
88 | 11 | ltp1d 10954 |
. . . . . . . . . . 11
|
89 | 88 | adantr 481 |
. . . . . . . . . 10
|
90 | 64 | a1i 11 |
. . . . . . . . . . . . . 14
|
91 | 63 | elexd 3214 |
. . . . . . . . . . . . . 14
|
92 | 90, 91 | fvmpt2d 6293 |
. . . . . . . . . . . . 13
|
93 | 92 | adantr 481 |
. . . . . . . . . . . 12
|
94 | 93, 42 | eqtrd 2656 |
. . . . . . . . . . 11
|
95 | 94 | eqcomd 2628 |
. . . . . . . . . 10
|
96 | 89, 95 | breqtrd 4679 |
. . . . . . . . 9
|
97 | 55 | adantr 481 |
. . . . . . . . . 10
|
98 | 92 | adantr 481 |
. . . . . . . . . . . 12
|
99 | 98, 47 | eqtrd 2656 |
. . . . . . . . . . 11
|
100 | 99 | eqcomd 2628 |
. . . . . . . . . 10
|
101 | 97, 100 | breqtrd 4679 |
. . . . . . . . 9
|
102 | 96, 101 | pm2.61dan 832 |
. . . . . . . 8
|
103 | 72, 74, 11, 87, 102 | eliood 39720 |
. . . . . . 7
|
104 | 103 | ralrimiva 2966 |
. . . . . 6
|
105 | 68, 70, 104 | 3jca 1242 |
. . . . 5
|
106 | | elixp2 7912 |
. . . . 5
|
107 | 105, 106 | sylibr 224 |
. . . 4
|
108 | 107, 1 | syl6eleqr 2712 |
. . 3
|
109 | 21 | adantr 481 |
. . . . . . . . 9
|
110 | 72 | adantr 481 |
. . . . . . . . 9
|
111 | 15 | mnfltd 11958 |
. . . . . . . . . . 11
|
112 | 111, 5 | breqtrd 4679 |
. . . . . . . . . 10
|
113 | | simpr 477 |
. . . . . . . . . . 11
|
114 | 113, 79 | breq12d 4666 |
. . . . . . . . . 10
|
115 | 112, 114 | mpbird 247 |
. . . . . . . . 9
|
116 | 109, 110,
115 | xrltled 39486 |
. . . . . . . 8
|
117 | 84 | eqcomd 2628 |
. . . . . . . . 9
|
118 | 36, 117 | eqled 10140 |
. . . . . . . 8
|
119 | 116, 118 | pm2.61dan 832 |
. . . . . . 7
|
120 | 74 | adantr 481 |
. . . . . . . . 9
|
121 | 28 | adantr 481 |
. . . . . . . . 9
|
122 | 44 | ltpnfd 11955 |
. . . . . . . . . 10
|
123 | | simpr 477 |
. . . . . . . . . . 11
|
124 | 94, 123 | breq12d 4666 |
. . . . . . . . . 10
|
125 | 122, 124 | mpbird 247 |
. . . . . . . . 9
|
126 | 120, 121,
125 | xrltled 39486 |
. . . . . . . 8
|
127 | 73 | adantr 481 |
. . . . . . . . 9
|
128 | 127, 99 | eqled 10140 |
. . . . . . . 8
|
129 | 126, 128 | pm2.61dan 832 |
. . . . . . 7
|
130 | | ioossioo 12265 |
. . . . . . 7
|
131 | 21, 28, 119, 129, 130 | syl22anc 1327 |
. . . . . 6
|
132 | 131 | ralrimiva 2966 |
. . . . 5
|
133 | | ss2ixp 7921 |
. . . . 5
|
134 | 132, 133 | syl 17 |
. . . 4
|
135 | 2, 134 | eqsstrd 3639 |
. . 3
|
136 | 108, 135 | jca 554 |
. 2
|
137 | | eleq2 2690 |
. . . 4
|
138 | | sseq1 3626 |
. . . 4
|
139 | 137, 138 | anbi12d 747 |
. . 3
|
140 | 139 | rspcev 3309 |
. 2
ℝ^ ℝ^
|
141 | 67, 136, 140 | syl2anc 693 |
1
ℝ^
|