Step | Hyp | Ref
| Expression |
1 | | suplocicc.3 |
. . 3
|
2 | | suplocicc.1 |
. . . 4
|
3 | | suplocicc.2 |
. . . 4
|
4 | | iccssre 9899 |
. . . 4
|
5 | 2, 3, 4 | syl2anc 409 |
. . 3
|
6 | 1, 5 | sstrd 3157 |
. 2
|
7 | | suplocicc.m |
. 2
|
8 | | peano2re 8042 |
. . . 4
|
9 | 3, 8 | syl 14 |
. . 3
|
10 | 6 | sselda 3147 |
. . . . 5
|
11 | 3 | adantr 274 |
. . . . 5
|
12 | 9 | adantr 274 |
. . . . 5
|
13 | 2 | rexrd 7956 |
. . . . . . 7
|
14 | 13 | adantr 274 |
. . . . . 6
|
15 | 3 | rexrd 7956 |
. . . . . . 7
|
16 | 15 | adantr 274 |
. . . . . 6
|
17 | 1 | sselda 3147 |
. . . . . 6
|
18 | | iccleub 9875 |
. . . . . 6
|
19 | 14, 16, 17, 18 | syl3anc 1233 |
. . . . 5
|
20 | 11 | ltp1d 8833 |
. . . . 5
|
21 | 10, 11, 12, 19, 20 | lelttrd 8031 |
. . . 4
|
22 | 21 | ralrimiva 2543 |
. . 3
|
23 | | brralrspcev 4045 |
. . 3
|
24 | 9, 22, 23 | syl2anc 409 |
. 2
|
25 | 7 | ad5antr 493 |
. . . . . . . . . 10
|
26 | | simpr 109 |
. . . . . . . . . . . 12
|
27 | | simp-4r 537 |
. . . . . . . . . . . . . 14
|
28 | 27 | ad2antrr 485 |
. . . . . . . . . . . . 13
|
29 | 2 | ad4antr 491 |
. . . . . . . . . . . . . 14
|
30 | 29 | ad2antrr 485 |
. . . . . . . . . . . . 13
|
31 | 6 | ad6antr 495 |
. . . . . . . . . . . . . 14
|
32 | 31, 26 | sseldd 3148 |
. . . . . . . . . . . . 13
|
33 | | simplr 525 |
. . . . . . . . . . . . 13
|
34 | 13 | ad6antr 495 |
. . . . . . . . . . . . . 14
|
35 | 15 | ad6antr 495 |
. . . . . . . . . . . . . 14
|
36 | 1 | ad6antr 495 |
. . . . . . . . . . . . . . 15
|
37 | 36, 26 | sseldd 3148 |
. . . . . . . . . . . . . 14
|
38 | | iccgelb 9876 |
. . . . . . . . . . . . . 14
|
39 | 34, 35, 37, 38 | syl3anc 1233 |
. . . . . . . . . . . . 13
|
40 | 28, 30, 32, 33, 39 | ltletrd 8329 |
. . . . . . . . . . . 12
|
41 | | breq2 3991 |
. . . . . . . . . . . . 13
|
42 | 41 | rspcev 2834 |
. . . . . . . . . . . 12
|
43 | 26, 40, 42 | syl2anc 409 |
. . . . . . . . . . 11
|
44 | 43 | orcd 728 |
. . . . . . . . . 10
|
45 | 25, 44 | exlimddv 1891 |
. . . . . . . . 9
|
46 | | simpllr 529 |
. . . . . . . . . . . . 13
|
47 | | simplr 525 |
. . . . . . . . . . . . 13
|
48 | | simp-5r 539 |
. . . . . . . . . . . . . 14
|
49 | | simp-4r 537 |
. . . . . . . . . . . . . 14
|
50 | 3 | ad5antr 493 |
. . . . . . . . . . . . . 14
|
51 | | ltmininf 11185 |
. . . . . . . . . . . . . 14
inf |
52 | 48, 49, 50, 51 | syl3anc 1233 |
. . . . . . . . . . . . 13
inf |
53 | 46, 47, 52 | mpbir2and 939 |
. . . . . . . . . . . 12
inf |
54 | | simpr 109 |
. . . . . . . . . . . . 13
|
55 | | suplocicc.bc |
. . . . . . . . . . . . . 14
|
56 | 55 | ad5antr 493 |
. . . . . . . . . . . . 13
|
57 | 2 | ad5antr 493 |
. . . . . . . . . . . . . 14
|
58 | | ltmininf 11185 |
. . . . . . . . . . . . . 14
inf
|
59 | 57, 49, 50, 58 | syl3anc 1233 |
. . . . . . . . . . . . 13
inf
|
60 | 54, 56, 59 | mpbir2and 939 |
. . . . . . . . . . . 12
inf |
61 | | mincl 11181 |
. . . . . . . . . . . . . 14
inf |
62 | 49, 50, 61 | syl2anc 409 |
. . . . . . . . . . . . 13
inf |
63 | | maxltsup 11169 |
. . . . . . . . . . . . 13
inf
inf
inf
inf |
64 | 48, 57, 62, 63 | syl3anc 1233 |
. . . . . . . . . . . 12
inf
inf
inf
|
65 | 53, 60, 64 | mpbir2and 939 |
. . . . . . . . . . 11
inf |
66 | | breq2 3991 |
. . . . . . . . . . . . 13
inf
inf
|
67 | | breq2 3991 |
. . . . . . . . . . . . . . 15
inf
inf
|
68 | 67 | ralbidv 2470 |
. . . . . . . . . . . . . 14
inf
inf
|
69 | 68 | orbi2d 785 |
. . . . . . . . . . . . 13
inf
inf
|
70 | 66, 69 | imbi12d 233 |
. . . . . . . . . . . 12
inf
inf
inf
|
71 | | breq1 3990 |
. . . . . . . . . . . . . . 15
|
72 | | breq1 3990 |
. . . . . . . . . . . . . . . . 17
|
73 | 72 | rexbidv 2471 |
. . . . . . . . . . . . . . . 16
|
74 | 73 | orbi1d 786 |
. . . . . . . . . . . . . . 15
|
75 | 71, 74 | imbi12d 233 |
. . . . . . . . . . . . . 14
|
76 | 75 | ralbidv 2470 |
. . . . . . . . . . . . 13
|
77 | | suplocicc.l |
. . . . . . . . . . . . . 14
|
78 | 77 | ad5antr 493 |
. . . . . . . . . . . . 13
|
79 | | maxcl 11161 |
. . . . . . . . . . . . . . 15
|
80 | 48, 57, 79 | syl2anc 409 |
. . . . . . . . . . . . . 14
|
81 | | maxle2 11163 |
. . . . . . . . . . . . . . 15
|
82 | 48, 57, 81 | syl2anc 409 |
. . . . . . . . . . . . . 14
|
83 | | maxltsup 11169 |
. . . . . . . . . . . . . . . . 17
|
84 | 48, 57, 50, 83 | syl3anc 1233 |
. . . . . . . . . . . . . . . 16
|
85 | 47, 56, 84 | mpbir2and 939 |
. . . . . . . . . . . . . . 15
|
86 | 80, 50, 85 | ltled 8025 |
. . . . . . . . . . . . . 14
|
87 | | elicc2 9882 |
. . . . . . . . . . . . . . 15
|
88 | 57, 50, 87 | syl2anc 409 |
. . . . . . . . . . . . . 14
|
89 | 80, 82, 86, 88 | mpbir3and 1175 |
. . . . . . . . . . . . 13
|
90 | 76, 78, 89 | rspcdva 2839 |
. . . . . . . . . . . 12
|
91 | 57, 62, 60 | ltled 8025 |
. . . . . . . . . . . . 13
inf |
92 | | min2inf 11183 |
. . . . . . . . . . . . . 14
inf |
93 | 49, 50, 92 | syl2anc 409 |
. . . . . . . . . . . . 13
inf |
94 | | elicc2 9882 |
. . . . . . . . . . . . . 14
inf
inf
inf
inf |
95 | 57, 50, 94 | syl2anc 409 |
. . . . . . . . . . . . 13
inf
inf
inf
inf
|
96 | 62, 91, 93, 95 | mpbir3and 1175 |
. . . . . . . . . . . 12
inf |
97 | 70, 90, 96 | rspcdva 2839 |
. . . . . . . . . . 11
inf
inf
|
98 | 65, 97 | mpd 13 |
. . . . . . . . . 10
inf
|
99 | 48 | ad2antrr 485 |
. . . . . . . . . . . . . 14
|
100 | | simplr 525 |
. . . . . . . . . . . . . . . 16
|
101 | 2 | ad2antrr 485 |
. . . . . . . . . . . . . . . 16
|
102 | 100, 101,
79 | syl2anc 409 |
. . . . . . . . . . . . . . 15
|
103 | 102 | ad5antr 493 |
. . . . . . . . . . . . . 14
|
104 | 6 | ad6antr 495 |
. . . . . . . . . . . . . . . 16
|
105 | | simpr 109 |
. . . . . . . . . . . . . . . 16
|
106 | 104, 105 | sseldd 3148 |
. . . . . . . . . . . . . . 15
|
107 | 106 | adantr 274 |
. . . . . . . . . . . . . 14
|
108 | 57 | ad2antrr 485 |
. . . . . . . . . . . . . . 15
|
109 | | maxle1 11162 |
. . . . . . . . . . . . . . 15
|
110 | 99, 108, 109 | syl2anc 409 |
. . . . . . . . . . . . . 14
|
111 | | simpr 109 |
. . . . . . . . . . . . . 14
|
112 | 99, 103, 107, 110, 111 | lelttrd 8031 |
. . . . . . . . . . . . 13
|
113 | 112 | ex 114 |
. . . . . . . . . . . 12
|
114 | 113 | reximdva 2572 |
. . . . . . . . . . 11
|
115 | 106 | adantr 274 |
. . . . . . . . . . . . . 14
inf |
116 | 62 | ad2antrr 485 |
. . . . . . . . . . . . . 14
inf inf
|
117 | 49 | ad2antrr 485 |
. . . . . . . . . . . . . 14
inf |
118 | | simpr 109 |
. . . . . . . . . . . . . 14
inf
inf |
119 | | simpr 109 |
. . . . . . . . . . . . . . . 16
|
120 | 3 | ad2antrr 485 |
. . . . . . . . . . . . . . . 16
|
121 | | min1inf 11182 |
. . . . . . . . . . . . . . . 16
inf |
122 | 119, 120,
121 | syl2anc 409 |
. . . . . . . . . . . . . . 15
inf |
123 | 122 | ad5antr 493 |
. . . . . . . . . . . . . 14
inf inf
|
124 | 115, 116,
117, 118, 123 | ltletrd 8329 |
. . . . . . . . . . . . 13
inf
|
125 | 124 | ex 114 |
. . . . . . . . . . . 12
inf |
126 | 125 | ralimdva 2537 |
. . . . . . . . . . 11
inf
|
127 | 114, 126 | orim12d 781 |
. . . . . . . . . 10
inf
|
128 | 98, 127 | mpd 13 |
. . . . . . . . 9
|
129 | | simplr 525 |
. . . . . . . . . 10
|
130 | | simpllr 529 |
. . . . . . . . . . 11
|
131 | | axltwlin 7974 |
. . . . . . . . . . 11
|
132 | 27, 130, 29, 131 | syl3anc 1233 |
. . . . . . . . . 10
|
133 | 129, 132 | mpd 13 |
. . . . . . . . 9
|
134 | 45, 128, 133 | mpjaodan 793 |
. . . . . . . 8
|
135 | 6 | ad5antr 493 |
. . . . . . . . . . . 12
|
136 | | simpr 109 |
. . . . . . . . . . . 12
|
137 | 135, 136 | sseldd 3148 |
. . . . . . . . . . 11
|
138 | 3 | ad5antr 493 |
. . . . . . . . . . 11
|
139 | | simp-4r 537 |
. . . . . . . . . . 11
|
140 | 13 | ad5antr 493 |
. . . . . . . . . . . 12
|
141 | 15 | ad5antr 493 |
. . . . . . . . . . . 12
|
142 | 1 | ad5antr 493 |
. . . . . . . . . . . . 13
|
143 | 142, 136 | sseldd 3148 |
. . . . . . . . . . . 12
|
144 | | iccleub 9875 |
. . . . . . . . . . . 12
|
145 | 140, 141,
143, 144 | syl3anc 1233 |
. . . . . . . . . . 11
|
146 | | simplr 525 |
. . . . . . . . . . 11
|
147 | 137, 138,
139, 145, 146 | lelttrd 8031 |
. . . . . . . . . 10
|
148 | 147 | ralrimiva 2543 |
. . . . . . . . 9
|
149 | 148 | olcd 729 |
. . . . . . . 8
|
150 | | axltwlin 7974 |
. . . . . . . . . 10
|
151 | 100, 119,
120, 150 | syl3anc 1233 |
. . . . . . . . 9
|
152 | 151 | imp 123 |
. . . . . . . 8
|
153 | 134, 149,
152 | mpjaodan 793 |
. . . . . . 7
|
154 | 153 | ex 114 |
. . . . . 6
|
155 | 154 | ralrimiva 2543 |
. . . . 5
|
156 | 155 | ralrimiva 2543 |
. . . 4
|
157 | | breq2 3991 |
. . . . . . 7
|
158 | | breq2 3991 |
. . . . . . . . 9
|
159 | 158 | ralbidv 2470 |
. . . . . . . 8
|
160 | 159 | orbi2d 785 |
. . . . . . 7
|
161 | 157, 160 | imbi12d 233 |
. . . . . 6
|
162 | 161 | cbvralv 2696 |
. . . . 5
|
163 | 162 | ralbii 2476 |
. . . 4
|
164 | 156, 163 | sylib 121 |
. . 3
|
165 | | breq1 3990 |
. . . . . 6
|
166 | | breq1 3990 |
. . . . . . . 8
|
167 | 166 | rexbidv 2471 |
. . . . . . 7
|
168 | 167 | orbi1d 786 |
. . . . . 6
|
169 | 165, 168 | imbi12d 233 |
. . . . 5
|
170 | 169 | ralbidv 2470 |
. . . 4
|
171 | 170 | cbvralv 2696 |
. . 3
|
172 | 164, 171 | sylib 121 |
. 2
|
173 | | axsuploc 7979 |
. 2
|
174 | 6, 7, 24, 172, 173 | syl22anc 1234 |
1
|