Step | Hyp | Ref
| Expression |
1 | | icccmp.13 |
. . . . . . 7
|
2 | | icccmp.4 |
. . . . . . . . . 10
|
3 | | ssrab2 3687 |
. . . . . . . . . 10
|
4 | 2, 3 | eqsstri 3635 |
. . . . . . . . 9
|
5 | | icccmp.5 |
. . . . . . . . . 10
|
6 | | icccmp.6 |
. . . . . . . . . 10
|
7 | | iccssre 12255 |
. . . . . . . . . 10
|
8 | 5, 6, 7 | syl2anc 693 |
. . . . . . . . 9
|
9 | 4, 8 | syl5ss 3614 |
. . . . . . . 8
|
10 | | icccmp.1 |
. . . . . . . . . . 11
|
11 | | icccmp.2 |
. . . . . . . . . . 11
↾t |
12 | | icccmp.3 |
. . . . . . . . . . 11
|
13 | | icccmp.7 |
. . . . . . . . . . 11
|
14 | | icccmp.8 |
. . . . . . . . . . 11
|
15 | | icccmp.9 |
. . . . . . . . . . 11
|
16 | 10, 11, 12, 2, 5, 6,
13, 14, 15 | icccmplem1 22625 |
. . . . . . . . . 10
|
17 | 16 | simpld 475 |
. . . . . . . . 9
|
18 | | ne0i 3921 |
. . . . . . . . 9
|
19 | 17, 18 | syl 17 |
. . . . . . . 8
|
20 | 16 | simprd 479 |
. . . . . . . . 9
|
21 | | breq2 4657 |
. . . . . . . . . . 11
|
22 | 21 | ralbidv 2986 |
. . . . . . . . . 10
|
23 | 22 | rspcev 3309 |
. . . . . . . . 9
|
24 | 6, 20, 23 | syl2anc 693 |
. . . . . . . 8
|
25 | | suprcl 10983 |
. . . . . . . 8
|
26 | 9, 19, 24, 25 | syl3anc 1326 |
. . . . . . 7
|
27 | 1, 26 | syl5eqel 2705 |
. . . . . 6
|
28 | | icccmp.11 |
. . . . . . 7
|
29 | 28 | rphalfcld 11884 |
. . . . . 6
|
30 | 27, 29 | ltaddrpd 11905 |
. . . . 5
|
31 | 29 | rpred 11872 |
. . . . . . 7
|
32 | 27, 31 | readdcld 10069 |
. . . . . 6
|
33 | 27, 32 | ltnled 10184 |
. . . . 5
|
34 | 30, 33 | mpbid 222 |
. . . 4
|
35 | | icccmp.14 |
. . . . . . . . . 10
|
36 | 32, 6 | ifcld 4131 |
. . . . . . . . . 10
|
37 | 35, 36 | syl5eqel 2705 |
. . . . . . . . 9
|
38 | | suprub 10984 |
. . . . . . . . . . . . . 14
|
39 | 9, 19, 24, 17, 38 | syl31anc 1329 |
. . . . . . . . . . . . 13
|
40 | 39, 1 | syl6breqr 4695 |
. . . . . . . . . . . 12
|
41 | 27, 32, 30 | ltled 10185 |
. . . . . . . . . . . 12
|
42 | 5, 27, 32, 40, 41 | letrd 10194 |
. . . . . . . . . . 11
|
43 | | breq2 4657 |
. . . . . . . . . . . 12
|
44 | | breq2 4657 |
. . . . . . . . . . . 12
|
45 | 43, 44 | ifboth 4124 |
. . . . . . . . . . 11
|
46 | 42, 13, 45 | syl2anc 693 |
. . . . . . . . . 10
|
47 | 46, 35 | syl6breqr 4695 |
. . . . . . . . 9
|
48 | | min2 12021 |
. . . . . . . . . . 11
|
49 | 32, 6, 48 | syl2anc 693 |
. . . . . . . . . 10
|
50 | 35, 49 | syl5eqbr 4688 |
. . . . . . . . 9
|
51 | | elicc2 12238 |
. . . . . . . . . 10
|
52 | 5, 6, 51 | syl2anc 693 |
. . . . . . . . 9
|
53 | 37, 47, 50, 52 | mpbir3and 1245 |
. . . . . . . 8
|
54 | 27, 28 | ltsubrpd 11904 |
. . . . . . . . . . 11
|
55 | 54, 1 | syl6breq 4694 |
. . . . . . . . . 10
|
56 | 28 | rpred 11872 |
. . . . . . . . . . . 12
|
57 | 27, 56 | resubcld 10458 |
. . . . . . . . . . 11
|
58 | | suprlub 10987 |
. . . . . . . . . . 11
|
59 | 9, 19, 24, 57, 58 | syl31anc 1329 |
. . . . . . . . . 10
|
60 | 55, 59 | mpbid 222 |
. . . . . . . . 9
|
61 | | oveq2 6658 |
. . . . . . . . . . . . . 14
|
62 | 61 | sseq1d 3632 |
. . . . . . . . . . . . 13
|
63 | 62 | rexbidv 3052 |
. . . . . . . . . . . 12
|
64 | 63, 2 | elrab2 3366 |
. . . . . . . . . . 11
|
65 | | unieq 4444 |
. . . . . . . . . . . . . . 15
|
66 | 65 | sseq2d 3633 |
. . . . . . . . . . . . . 14
|
67 | 66 | cbvrexv 3172 |
. . . . . . . . . . . . 13
|
68 | | simpr1 1067 |
. . . . . . . . . . . . . . . . . . . . . 22
|
69 | | elin 3796 |
. . . . . . . . . . . . . . . . . . . . . 22
|
70 | 68, 69 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . 21
|
71 | 70 | simpld 475 |
. . . . . . . . . . . . . . . . . . . 20
|
72 | 71 | elpwid 4170 |
. . . . . . . . . . . . . . . . . . 19
|
73 | | simpll 790 |
. . . . . . . . . . . . . . . . . . . . 21
|
74 | | icccmp.10 |
. . . . . . . . . . . . . . . . . . . . 21
|
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
76 | 75 | snssd 4340 |
. . . . . . . . . . . . . . . . . . 19
|
77 | 72, 76 | unssd 3789 |
. . . . . . . . . . . . . . . . . 18
|
78 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . 20
|
79 | | snex 4908 |
. . . . . . . . . . . . . . . . . . . 20
|
80 | 78, 79 | unex 6956 |
. . . . . . . . . . . . . . . . . . 19
|
81 | 80 | elpw 4164 |
. . . . . . . . . . . . . . . . . 18
|
82 | 77, 81 | sylibr 224 |
. . . . . . . . . . . . . . . . 17
|
83 | 70 | simprd 479 |
. . . . . . . . . . . . . . . . . 18
|
84 | | snfi 8038 |
. . . . . . . . . . . . . . . . . 18
|
85 | | unfi 8227 |
. . . . . . . . . . . . . . . . . 18
|
86 | 83, 84, 85 | sylancl 694 |
. . . . . . . . . . . . . . . . 17
|
87 | 82, 86 | elind 3798 |
. . . . . . . . . . . . . . . 16
|
88 | | simplr2 1104 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
89 | | ssun1 3776 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
90 | 88, 89 | syl6ss 3615 |
. . . . . . . . . . . . . . . . . . . . . 22
|
91 | 73, 5 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
92 | 73, 37 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
93 | | elicc2 12238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
94 | 91, 92, 93 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
95 | 94 | biimpa 501 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
96 | 95 | simp1d 1073 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
97 | 96 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
98 | 95 | simp2d 1074 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
99 | 98 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
100 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
101 | 73, 8 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
102 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
103 | 101, 102 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
104 | | elicc2 12238 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
105 | 91, 103, 104 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
106 | 105 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
107 | 97, 99, 100, 106 | mpbir3and 1245 |
. . . . . . . . . . . . . . . . . . . . . 22
|
108 | 90, 107 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . 21
|
109 | 108 | expr 643 |
. . . . . . . . . . . . . . . . . . . 20
|
110 | 73 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
111 | | icccmp.12 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
112 | 110, 111 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
113 | 96 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
114 | 110, 57 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
115 | 103 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
116 | | simplr3 1105 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
117 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
118 | 114, 115,
113, 116, 117 | lttrd 10198 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
119 | 110, 37 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
120 | 27, 56 | readdcld 10069 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
121 | 110, 120 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
122 | 95 | simp3d 1075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
123 | 122 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
124 | | min1 12020 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
125 | 32, 6, 124 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
126 | 35, 125 | syl5eqbr 4688 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
127 | | rphalflt 11860 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
128 | 28, 127 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
129 | 31, 56, 27, 128 | ltadd2dd 10196 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
130 | 37, 32, 120, 126, 129 | lelttrd 10195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
131 | 110, 130 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
132 | 113, 119,
121, 123, 131 | lelttrd 10195 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
133 | | rexr 10085 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
134 | | rexr 10085 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
135 | | elioo2 12216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
136 | 133, 134,
135 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
137 | 114, 121,
136 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
138 | 113, 118,
132, 137 | mpbir3and 1245 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
139 | 110, 27 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
140 | 110, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
141 | 140 | rpred 11872 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
142 | 12 | bl2ioo 22595 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
143 | 139, 141,
142 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
144 | 138, 143 | eleqtrrd 2704 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
145 | 112, 144 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . . 22
|
146 | | elun2 3781 |
. . . . . . . . . . . . . . . . . . . . . 22
|
147 | 145, 146 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
148 | 147 | expr 643 |
. . . . . . . . . . . . . . . . . . . 20
|
149 | 103 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
150 | | lelttric 10144 |
. . . . . . . . . . . . . . . . . . . . 21
|
151 | 96, 149, 150 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
|
152 | 109, 148,
151 | mpjaod 396 |
. . . . . . . . . . . . . . . . . . 19
|
153 | 152 | ex 450 |
. . . . . . . . . . . . . . . . . 18
|
154 | 153 | ssrdv 3609 |
. . . . . . . . . . . . . . . . 17
|
155 | | uniun 4456 |
. . . . . . . . . . . . . . . . . 18
|
156 | | unisng 4452 |
. . . . . . . . . . . . . . . . . . . 20
|
157 | 75, 156 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
158 | 157 | uneq2d 3767 |
. . . . . . . . . . . . . . . . . 18
|
159 | 155, 158 | syl5eq 2668 |
. . . . . . . . . . . . . . . . 17
|
160 | 154, 159 | sseqtr4d 3642 |
. . . . . . . . . . . . . . . 16
|
161 | | unieq 4444 |
. . . . . . . . . . . . . . . . . 18
|
162 | 161 | sseq2d 3633 |
. . . . . . . . . . . . . . . . 17
|
163 | 162 | rspcev 3309 |
. . . . . . . . . . . . . . . 16
|
164 | 87, 160, 163 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
165 | 164 | 3exp2 1285 |
. . . . . . . . . . . . . 14
|
166 | 165 | rexlimdv 3030 |
. . . . . . . . . . . . 13
|
167 | 67, 166 | syl5bi 232 |
. . . . . . . . . . . 12
|
168 | 167 | expimpd 629 |
. . . . . . . . . . 11
|
169 | 64, 168 | syl5bi 232 |
. . . . . . . . . 10
|
170 | 169 | rexlimdv 3030 |
. . . . . . . . 9
|
171 | 60, 170 | mpd 15 |
. . . . . . . 8
|
172 | | oveq2 6658 |
. . . . . . . . . . 11
|
173 | 172 | sseq1d 3632 |
. . . . . . . . . 10
|
174 | 173 | rexbidv 3052 |
. . . . . . . . 9
|
175 | | unieq 4444 |
. . . . . . . . . . . . . 14
|
176 | 175 | sseq2d 3633 |
. . . . . . . . . . . . 13
|
177 | 176 | cbvrexv 3172 |
. . . . . . . . . . . 12
|
178 | 63, 177 | syl6bb 276 |
. . . . . . . . . . 11
|
179 | 178 | cbvrabv 3199 |
. . . . . . . . . 10
|
180 | 2, 179 | eqtri 2644 |
. . . . . . . . 9
|
181 | 174, 180 | elrab2 3366 |
. . . . . . . 8
|
182 | 53, 171, 181 | sylanbrc 698 |
. . . . . . 7
|
183 | | suprub 10984 |
. . . . . . 7
|
184 | 9, 19, 24, 182, 183 | syl31anc 1329 |
. . . . . 6
|
185 | 184, 1 | syl6breqr 4695 |
. . . . 5
|
186 | | iftrue 4092 |
. . . . . . 7
|
187 | 35, 186 | syl5eq 2668 |
. . . . . 6
|
188 | 187 | breq1d 4663 |
. . . . 5
|
189 | 185, 188 | syl5ibcom 235 |
. . . 4
|
190 | 34, 189 | mtod 189 |
. . 3
|
191 | | iffalse 4095 |
. . . 4
|
192 | 35, 191 | syl5eq 2668 |
. . 3
|
193 | 190, 192 | syl 17 |
. 2
|
194 | 193, 182 | eqeltrrd 2702 |
1
|