Step | Hyp | Ref
| Expression |
1 | | mbfpos.1 |
. . 3
|
2 | | eqid 2622 |
. . 3
|
3 | 1, 2 | fmptd 6385 |
. 2
|
4 | | mbfposr.2 |
. . 3
MblFn |
5 | | 0re 10040 |
. . . 4
|
6 | | ifcl 4130 |
. . . 4
|
7 | 1, 5, 6 | sylancl 694 |
. . 3
|
8 | 4, 7 | mbfdm2 23405 |
. 2
|
9 | | simplr 792 |
. . . . . . . . . . . . . 14
|
10 | | simpllr 799 |
. . . . . . . . . . . . . . 15
|
11 | 10 | lt0neg1d 10597 |
. . . . . . . . . . . . . 14
|
12 | 9, 11 | mpbid 222 |
. . . . . . . . . . . . 13
|
13 | 12 | biantrurd 529 |
. . . . . . . . . . . 12
|
14 | | simpll 790 |
. . . . . . . . . . . . . 14
|
15 | 14, 1 | sylan 488 |
. . . . . . . . . . . . 13
|
16 | 10, 15 | ltnegd 10605 |
. . . . . . . . . . . 12
|
17 | | 0red 10041 |
. . . . . . . . . . . . 13
|
18 | 15 | renegcld 10457 |
. . . . . . . . . . . . 13
|
19 | 10 | renegcld 10457 |
. . . . . . . . . . . . 13
|
20 | | maxlt 12024 |
. . . . . . . . . . . . 13
|
21 | 17, 18, 19, 20 | syl3anc 1326 |
. . . . . . . . . . . 12
|
22 | 13, 16, 21 | 3bitr4rd 301 |
. . . . . . . . . . 11
|
23 | 1 | renegcld 10457 |
. . . . . . . . . . . . . 14
|
24 | | ifcl 4130 |
. . . . . . . . . . . . . 14
|
25 | 23, 5, 24 | sylancl 694 |
. . . . . . . . . . . . 13
|
26 | 14, 25 | sylan 488 |
. . . . . . . . . . . 12
|
27 | 26 | biantrurd 529 |
. . . . . . . . . . 11
|
28 | 15 | biantrurd 529 |
. . . . . . . . . . 11
|
29 | 22, 27, 28 | 3bitr3d 298 |
. . . . . . . . . 10
|
30 | 19 | rexrd 10089 |
. . . . . . . . . . 11
|
31 | | elioomnf 12268 |
. . . . . . . . . . 11
|
32 | 30, 31 | syl 17 |
. . . . . . . . . 10
|
33 | 10 | rexrd 10089 |
. . . . . . . . . . 11
|
34 | | elioopnf 12267 |
. . . . . . . . . . 11
|
35 | 33, 34 | syl 17 |
. . . . . . . . . 10
|
36 | 29, 32, 35 | 3bitr4d 300 |
. . . . . . . . 9
|
37 | | simpr 477 |
. . . . . . . . . . . 12
|
38 | | eqid 2622 |
. . . . . . . . . . . . 13
|
39 | 38 | fvmpt2 6291 |
. . . . . . . . . . . 12
|
40 | 37, 25, 39 | syl2anc 693 |
. . . . . . . . . . 11
|
41 | 40 | eleq1d 2686 |
. . . . . . . . . 10
|
42 | 14, 41 | sylan 488 |
. . . . . . . . 9
|
43 | 2 | fvmpt2 6291 |
. . . . . . . . . . . 12
|
44 | 37, 1, 43 | syl2anc 693 |
. . . . . . . . . . 11
|
45 | 44 | eleq1d 2686 |
. . . . . . . . . 10
|
46 | 14, 45 | sylan 488 |
. . . . . . . . 9
|
47 | 36, 42, 46 | 3bitr4d 300 |
. . . . . . . 8
|
48 | 47 | pm5.32da 673 |
. . . . . . 7
|
49 | 25, 38 | fmptd 6385 |
. . . . . . . . 9
|
50 | | ffn 6045 |
. . . . . . . . 9
|
51 | | elpreima 6337 |
. . . . . . . . 9
|
52 | 49, 50, 51 | 3syl 18 |
. . . . . . . 8
|
53 | 52 | ad2antrr 762 |
. . . . . . 7
|
54 | | ffn 6045 |
. . . . . . . . 9
|
55 | | elpreima 6337 |
. . . . . . . . 9
|
56 | 3, 54, 55 | 3syl 18 |
. . . . . . . 8
|
57 | 56 | ad2antrr 762 |
. . . . . . 7
|
58 | 48, 53, 57 | 3bitr4d 300 |
. . . . . 6
|
59 | 58 | alrimiv 1855 |
. . . . 5
|
60 | | nfmpt1 4747 |
. . . . . . . 8
|
61 | 60 | nfcnv 5301 |
. . . . . . 7
|
62 | | nfcv 2764 |
. . . . . . 7
|
63 | 61, 62 | nfima 5474 |
. . . . . 6
|
64 | | nfmpt1 4747 |
. . . . . . . 8
|
65 | 64 | nfcnv 5301 |
. . . . . . 7
|
66 | | nfcv 2764 |
. . . . . . 7
|
67 | 65, 66 | nfima 5474 |
. . . . . 6
|
68 | 63, 67 | cleqf 2790 |
. . . . 5
|
69 | 59, 68 | sylibr 224 |
. . . 4
|
70 | | mbfposr.3 |
. . . . . 6
MblFn |
71 | | mbfima 23399 |
. . . . . 6
MblFn
|
72 | 70, 49, 71 | syl2anc 693 |
. . . . 5
|
73 | 72 | ad2antrr 762 |
. . . 4
|
74 | 69, 73 | eqeltrrd 2702 |
. . 3
|
75 | | 0red 10041 |
. . . . . . . . . . . . . . 15
|
76 | | simpll 790 |
. . . . . . . . . . . . . . . 16
|
77 | 76, 1 | sylan 488 |
. . . . . . . . . . . . . . 15
|
78 | | simpllr 799 |
. . . . . . . . . . . . . . 15
|
79 | | maxle 12022 |
. . . . . . . . . . . . . . 15
|
80 | 75, 77, 78, 79 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
81 | | simplr 792 |
. . . . . . . . . . . . . . 15
|
82 | 81 | biantrurd 529 |
. . . . . . . . . . . . . 14
|
83 | 80, 82 | bitr4d 271 |
. . . . . . . . . . . . 13
|
84 | 83 | notbid 308 |
. . . . . . . . . . . 12
|
85 | 77, 5, 6 | sylancl 694 |
. . . . . . . . . . . . 13
|
86 | 78, 85 | ltnled 10184 |
. . . . . . . . . . . 12
|
87 | 78, 77 | ltnled 10184 |
. . . . . . . . . . . 12
|
88 | 84, 86, 87 | 3bitr4d 300 |
. . . . . . . . . . 11
|
89 | 85 | biantrurd 529 |
. . . . . . . . . . 11
|
90 | 77 | biantrurd 529 |
. . . . . . . . . . 11
|
91 | 88, 89, 90 | 3bitr3d 298 |
. . . . . . . . . 10
|
92 | 78 | rexrd 10089 |
. . . . . . . . . . 11
|
93 | | elioopnf 12267 |
. . . . . . . . . . 11
|
94 | 92, 93 | syl 17 |
. . . . . . . . . 10
|
95 | 92, 34 | syl 17 |
. . . . . . . . . 10
|
96 | 91, 94, 95 | 3bitr4d 300 |
. . . . . . . . 9
|
97 | | eqid 2622 |
. . . . . . . . . . . . 13
|
98 | 97 | fvmpt2 6291 |
. . . . . . . . . . . 12
|
99 | 37, 7, 98 | syl2anc 693 |
. . . . . . . . . . 11
|
100 | 99 | eleq1d 2686 |
. . . . . . . . . 10
|
101 | 76, 100 | sylan 488 |
. . . . . . . . 9
|
102 | 76, 45 | sylan 488 |
. . . . . . . . 9
|
103 | 96, 101, 102 | 3bitr4d 300 |
. . . . . . . 8
|
104 | 103 | pm5.32da 673 |
. . . . . . 7
|
105 | 7, 97 | fmptd 6385 |
. . . . . . . . 9
|
106 | | ffn 6045 |
. . . . . . . . 9
|
107 | | elpreima 6337 |
. . . . . . . . 9
|
108 | 105, 106,
107 | 3syl 18 |
. . . . . . . 8
|
109 | 108 | ad2antrr 762 |
. . . . . . 7
|
110 | 56 | ad2antrr 762 |
. . . . . . 7
|
111 | 104, 109,
110 | 3bitr4d 300 |
. . . . . 6
|
112 | 111 | alrimiv 1855 |
. . . . 5
|
113 | | nfmpt1 4747 |
. . . . . . . 8
|
114 | 113 | nfcnv 5301 |
. . . . . . 7
|
115 | 114, 66 | nfima 5474 |
. . . . . 6
|
116 | 115, 67 | cleqf 2790 |
. . . . 5
|
117 | 112, 116 | sylibr 224 |
. . . 4
|
118 | | mbfima 23399 |
. . . . . 6
MblFn
|
119 | 4, 105, 118 | syl2anc 693 |
. . . . 5
|
120 | 119 | ad2antrr 762 |
. . . 4
|
121 | 117, 120 | eqeltrrd 2702 |
. . 3
|
122 | | simpr 477 |
. . 3
|
123 | | 0red 10041 |
. . 3
|
124 | 74, 121, 122, 123 | ltlecasei 10145 |
. 2
|
125 | | 0red 10041 |
. . . . . . . . . . . . 13
|
126 | | simpll 790 |
. . . . . . . . . . . . . 14
|
127 | 126, 1 | sylan 488 |
. . . . . . . . . . . . 13
|
128 | | simpllr 799 |
. . . . . . . . . . . . 13
|
129 | | maxlt 12024 |
. . . . . . . . . . . . 13
|
130 | 125, 127,
128, 129 | syl3anc 1326 |
. . . . . . . . . . . 12
|
131 | | simplr 792 |
. . . . . . . . . . . . 13
|
132 | 131 | biantrurd 529 |
. . . . . . . . . . . 12
|
133 | 130, 132 | bitr4d 271 |
. . . . . . . . . . 11
|
134 | 126, 7 | sylan 488 |
. . . . . . . . . . . 12
|
135 | 134 | biantrurd 529 |
. . . . . . . . . . 11
|
136 | 127 | biantrurd 529 |
. . . . . . . . . . 11
|
137 | 133, 135,
136 | 3bitr3d 298 |
. . . . . . . . . 10
|
138 | 128 | rexrd 10089 |
. . . . . . . . . . 11
|
139 | | elioomnf 12268 |
. . . . . . . . . . 11
|
140 | 138, 139 | syl 17 |
. . . . . . . . . 10
|
141 | | elioomnf 12268 |
. . . . . . . . . . 11
|
142 | 138, 141 | syl 17 |
. . . . . . . . . 10
|
143 | 137, 140,
142 | 3bitr4d 300 |
. . . . . . . . 9
|
144 | 99 | eleq1d 2686 |
. . . . . . . . . 10
|
145 | 126, 144 | sylan 488 |
. . . . . . . . 9
|
146 | 44 | eleq1d 2686 |
. . . . . . . . . 10
|
147 | 126, 146 | sylan 488 |
. . . . . . . . 9
|
148 | 143, 145,
147 | 3bitr4d 300 |
. . . . . . . 8
|
149 | 148 | pm5.32da 673 |
. . . . . . 7
|
150 | | elpreima 6337 |
. . . . . . . . 9
|
151 | 105, 106,
150 | 3syl 18 |
. . . . . . . 8
|
152 | 151 | ad2antrr 762 |
. . . . . . 7
|
153 | | elpreima 6337 |
. . . . . . . . 9
|
154 | 3, 54, 153 | 3syl 18 |
. . . . . . . 8
|
155 | 154 | ad2antrr 762 |
. . . . . . 7
|
156 | 149, 152,
155 | 3bitr4d 300 |
. . . . . 6
|
157 | 156 | alrimiv 1855 |
. . . . 5
|
158 | | nfcv 2764 |
. . . . . . 7
|
159 | 114, 158 | nfima 5474 |
. . . . . 6
|
160 | 65, 158 | nfima 5474 |
. . . . . 6
|
161 | 159, 160 | cleqf 2790 |
. . . . 5
|
162 | 157, 161 | sylibr 224 |
. . . 4
|
163 | | mbfima 23399 |
. . . . . 6
MblFn
|
164 | 4, 105, 163 | syl2anc 693 |
. . . . 5
|
165 | 164 | ad2antrr 762 |
. . . 4
|
166 | 162, 165 | eqeltrrd 2702 |
. . 3
|
167 | | simplr 792 |
. . . . . . . . . . . . . . . 16
|
168 | | simpllr 799 |
. . . . . . . . . . . . . . . . 17
|
169 | 168 | le0neg1d 10599 |
. . . . . . . . . . . . . . . 16
|
170 | 167, 169 | mpbid 222 |
. . . . . . . . . . . . . . 15
|
171 | 170 | biantrurd 529 |
. . . . . . . . . . . . . 14
|
172 | | simpll 790 |
. . . . . . . . . . . . . . . 16
|
173 | 172, 1 | sylan 488 |
. . . . . . . . . . . . . . 15
|
174 | 168, 173 | lenegd 10606 |
. . . . . . . . . . . . . 14
|
175 | | 0red 10041 |
. . . . . . . . . . . . . . 15
|
176 | 173 | renegcld 10457 |
. . . . . . . . . . . . . . 15
|
177 | 168 | renegcld 10457 |
. . . . . . . . . . . . . . 15
|
178 | | maxle 12022 |
. . . . . . . . . . . . . . 15
|
179 | 175, 176,
177, 178 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
180 | 171, 174,
179 | 3bitr4rd 301 |
. . . . . . . . . . . . 13
|
181 | 180 | notbid 308 |
. . . . . . . . . . . 12
|
182 | 172, 25 | sylan 488 |
. . . . . . . . . . . . 13
|
183 | 177, 182 | ltnled 10184 |
. . . . . . . . . . . 12
|
184 | 173, 168 | ltnled 10184 |
. . . . . . . . . . . 12
|
185 | 181, 183,
184 | 3bitr4d 300 |
. . . . . . . . . . 11
|
186 | 182 | biantrurd 529 |
. . . . . . . . . . 11
|
187 | 173 | biantrurd 529 |
. . . . . . . . . . 11
|
188 | 185, 186,
187 | 3bitr3d 298 |
. . . . . . . . . 10
|
189 | 177 | rexrd 10089 |
. . . . . . . . . . 11
|
190 | | elioopnf 12267 |
. . . . . . . . . . 11
|
191 | 189, 190 | syl 17 |
. . . . . . . . . 10
|
192 | 168 | rexrd 10089 |
. . . . . . . . . . 11
|
193 | 192, 141 | syl 17 |
. . . . . . . . . 10
|
194 | 188, 191,
193 | 3bitr4d 300 |
. . . . . . . . 9
|
195 | 40 | eleq1d 2686 |
. . . . . . . . . 10
|
196 | 172, 195 | sylan 488 |
. . . . . . . . 9
|
197 | 172, 146 | sylan 488 |
. . . . . . . . 9
|
198 | 194, 196,
197 | 3bitr4d 300 |
. . . . . . . 8
|
199 | 198 | pm5.32da 673 |
. . . . . . 7
|
200 | | elpreima 6337 |
. . . . . . . . 9
|
201 | 49, 50, 200 | 3syl 18 |
. . . . . . . 8
|
202 | 201 | ad2antrr 762 |
. . . . . . 7
|
203 | 154 | ad2antrr 762 |
. . . . . . 7
|
204 | 199, 202,
203 | 3bitr4d 300 |
. . . . . 6
|
205 | 204 | alrimiv 1855 |
. . . . 5
|
206 | | nfcv 2764 |
. . . . . . 7
|
207 | 61, 206 | nfima 5474 |
. . . . . 6
|
208 | 207, 160 | cleqf 2790 |
. . . . 5
|
209 | 205, 208 | sylibr 224 |
. . . 4
|
210 | | mbfima 23399 |
. . . . . 6
MblFn
|
211 | 70, 49, 210 | syl2anc 693 |
. . . . 5
|
212 | 211 | ad2antrr 762 |
. . . 4
|
213 | 209, 212 | eqeltrrd 2702 |
. . 3
|
214 | 166, 213,
123, 122 | ltlecasei 10145 |
. 2
|
215 | 3, 8, 124, 214 | ismbf2d 23408 |
1
MblFn |