Step | Hyp | Ref
| Expression |
1 | | mbff 23394 |
. . . 4
MblFn |
2 | 1 | feqmptd 6249 |
. . 3
MblFn |
3 | 2 | 3ad2ant1 1082 |
. 2
MblFn
|
4 | | rzal 4073 |
. . . . . . . 8
|
5 | | mpteq12 4736 |
. . . . . . . 8
|
6 | 4, 5 | mpdan 702 |
. . . . . . 7
|
7 | | fconstmpt 5163 |
. . . . . . . 8
|
8 | | 0mbl 23307 |
. . . . . . . . 9
|
9 | | ibl0 23553 |
. . . . . . . . 9
|
10 | 8, 9 | ax-mp 5 |
. . . . . . . 8
|
11 | 7, 10 | eqeltrri 2698 |
. . . . . . 7
|
12 | 6, 11 | syl6eqel 2709 |
. . . . . 6
|
13 | 12 | adantl 482 |
. . . . 5
MblFn |
14 | | r19.2z 4060 |
. . . . . . . . . 10
|
15 | 14 | anim1i 592 |
. . . . . . . . 9
|
16 | 15 | an31s 848 |
. . . . . . . 8
|
17 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
MblFn
|
18 | 17 | ffvelrnda 6359 |
. . . . . . . . . . . . . 14
MblFn
|
19 | 18 | absge0d 14183 |
. . . . . . . . . . . . 13
MblFn
|
20 | | 0red 10041 |
. . . . . . . . . . . . . 14
MblFn
|
21 | 18 | abscld 14175 |
. . . . . . . . . . . . . 14
MblFn
|
22 | | simplr 792 |
. . . . . . . . . . . . . 14
MblFn
|
23 | | letr 10131 |
. . . . . . . . . . . . . 14
|
24 | 20, 21, 22, 23 | syl3anc 1326 |
. . . . . . . . . . . . 13
MblFn
|
25 | 19, 24 | mpand 711 |
. . . . . . . . . . . 12
MblFn
|
26 | 25 | rexlimdva 3031 |
. . . . . . . . . . 11
MblFn
|
27 | 26 | ex 450 |
. . . . . . . . . 10
MblFn
|
28 | 27 | com23 86 |
. . . . . . . . 9
MblFn
|
29 | 28 | imp32 449 |
. . . . . . . 8
MblFn
|
30 | 16, 29 | sylan2 491 |
. . . . . . 7
MblFn
|
31 | 30 | anassrs 680 |
. . . . . 6
MblFn |
32 | | an32 839 |
. . . . . . . 8
|
33 | | id 22 |
. . . . . . . . . . 11
MblFn MblFn |
34 | 2, 33 | eqeltrrd 2702 |
. . . . . . . . . 10
MblFn
MblFn |
35 | 34 | ad2antrr 762 |
. . . . . . . . 9
MblFn
MblFn |
36 | 1 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . 18
MblFn
|
37 | 36 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . 17
MblFn
|
38 | 37 | recld 13934 |
. . . . . . . . . . . . . . . 16
MblFn
|
39 | 38 | rexrd 10089 |
. . . . . . . . . . . . . . 15
MblFn
|
40 | 39 | adantrr 753 |
. . . . . . . . . . . . . 14
MblFn
|
41 | | simprr 796 |
. . . . . . . . . . . . . 14
MblFn
|
42 | | elxrge0 12281 |
. . . . . . . . . . . . . 14
|
43 | 40, 41, 42 | sylanbrc 698 |
. . . . . . . . . . . . 13
MblFn
|
44 | | 0e0iccpnf 12283 |
. . . . . . . . . . . . . 14
|
45 | 44 | a1i 11 |
. . . . . . . . . . . . 13
MblFn
|
46 | 43, 45 | ifclda 4120 |
. . . . . . . . . . . 12
MblFn
|
47 | | eqid 2622 |
. . . . . . . . . . . 12
|
48 | 46, 47 | fmptd 6385 |
. . . . . . . . . . 11
MblFn
|
49 | | mbfdm 23395 |
. . . . . . . . . . . . . 14
MblFn
|
50 | 49 | ad2antrr 762 |
. . . . . . . . . . . . 13
MblFn
|
51 | | simplr 792 |
. . . . . . . . . . . . 13
MblFn
|
52 | | elrege0 12278 |
. . . . . . . . . . . . . . 15
|
53 | 52 | biimpri 218 |
. . . . . . . . . . . . . 14
|
54 | 53 | ad2antrl 764 |
. . . . . . . . . . . . 13
MblFn
|
55 | | itg2const 23507 |
. . . . . . . . . . . . 13
|
56 | 50, 51, 54, 55 | syl3anc 1326 |
. . . . . . . . . . . 12
MblFn
|
57 | | simprll 802 |
. . . . . . . . . . . . 13
MblFn
|
58 | 57, 51 | remulcld 10070 |
. . . . . . . . . . . 12
MblFn
|
59 | 56, 58 | eqeltrd 2701 |
. . . . . . . . . . 11
MblFn
|
60 | | rexr 10085 |
. . . . . . . . . . . . . . . . 17
|
61 | | elxrge0 12281 |
. . . . . . . . . . . . . . . . . 18
|
62 | 61 | biimpri 218 |
. . . . . . . . . . . . . . . . 17
|
63 | 60, 62 | sylan 488 |
. . . . . . . . . . . . . . . 16
|
64 | 63 | ad2antrl 764 |
. . . . . . . . . . . . . . 15
MblFn
|
65 | 64 | adantr 481 |
. . . . . . . . . . . . . 14
MblFn
|
66 | | ifcl 4130 |
. . . . . . . . . . . . . 14
|
67 | 65, 44, 66 | sylancl 694 |
. . . . . . . . . . . . 13
MblFn
|
68 | | eqid 2622 |
. . . . . . . . . . . . 13
|
69 | 67, 68 | fmptd 6385 |
. . . . . . . . . . . 12
MblFn
|
70 | | ifan 4134 |
. . . . . . . . . . . . . . 15
|
71 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
MblFn
|
72 | 71 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . 21
MblFn
|
73 | 72 | recld 13934 |
. . . . . . . . . . . . . . . . . . . 20
MblFn
|
74 | 72 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . 20
MblFn
|
75 | 57 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
MblFn
|
76 | 72 | releabsd 14190 |
. . . . . . . . . . . . . . . . . . . 20
MblFn
|
77 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
78 | 77 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
79 | 78 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
80 | 79 | rspccva 3308 |
. . . . . . . . . . . . . . . . . . . . . 22
|
81 | 80 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . 21
|
82 | 81 | adantll 750 |
. . . . . . . . . . . . . . . . . . . 20
MblFn
|
83 | 73, 74, 75, 76, 82 | letrd 10194 |
. . . . . . . . . . . . . . . . . . 19
MblFn
|
84 | | simprlr 803 |
. . . . . . . . . . . . . . . . . . . 20
MblFn
|
85 | 84 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
MblFn
|
86 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . 20
|
87 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . 20
|
88 | 86, 87 | ifboth 4124 |
. . . . . . . . . . . . . . . . . . 19
|
89 | 83, 85, 88 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
MblFn
|
90 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . 19
|
91 | 90 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
MblFn
|
92 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . 19
|
93 | 92 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
MblFn
|
94 | 89, 91, 93 | 3brtr4d 4685 |
. . . . . . . . . . . . . . . . 17
MblFn
|
95 | 94 | ex 450 |
. . . . . . . . . . . . . . . 16
MblFn
|
96 | | 0le0 11110 |
. . . . . . . . . . . . . . . . . 18
|
97 | 96 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
98 | | iffalse 4095 |
. . . . . . . . . . . . . . . . 17
|
99 | | iffalse 4095 |
. . . . . . . . . . . . . . . . 17
|
100 | 97, 98, 99 | 3brtr4d 4685 |
. . . . . . . . . . . . . . . 16
|
101 | 95, 100 | pm2.61d1 171 |
. . . . . . . . . . . . . . 15
MblFn
|
102 | 70, 101 | syl5eqbr 4688 |
. . . . . . . . . . . . . 14
MblFn
|
103 | 102 | ralrimivw 2967 |
. . . . . . . . . . . . 13
MblFn
|
104 | | reex 10027 |
. . . . . . . . . . . . . . 15
|
105 | 104 | a1i 11 |
. . . . . . . . . . . . . 14
MblFn
|
106 | | eqidd 2623 |
. . . . . . . . . . . . . 14
MblFn
|
107 | | eqidd 2623 |
. . . . . . . . . . . . . 14
MblFn
|
108 | 105, 46, 67, 106, 107 | ofrfval2 6915 |
. . . . . . . . . . . . 13
MblFn
|
109 | 103, 108 | mpbird 247 |
. . . . . . . . . . . 12
MblFn
|
110 | | itg2le 23506 |
. . . . . . . . . . . 12
|
111 | 48, 69, 109, 110 | syl3anc 1326 |
. . . . . . . . . . 11
MblFn
|
112 | | itg2lecl 23505 |
. . . . . . . . . . 11
|
113 | 48, 59, 111, 112 | syl3anc 1326 |
. . . . . . . . . 10
MblFn
|
114 | 38 | renegcld 10457 |
. . . . . . . . . . . . . . . 16
MblFn
|
115 | 114 | rexrd 10089 |
. . . . . . . . . . . . . . 15
MblFn
|
116 | 115 | adantrr 753 |
. . . . . . . . . . . . . 14
MblFn
|
117 | | simprr 796 |
. . . . . . . . . . . . . 14
MblFn
|
118 | | elxrge0 12281 |
. . . . . . . . . . . . . 14
|
119 | 116, 117,
118 | sylanbrc 698 |
. . . . . . . . . . . . 13
MblFn
|
120 | 44 | a1i 11 |
. . . . . . . . . . . . 13
MblFn
|
121 | 119, 120 | ifclda 4120 |
. . . . . . . . . . . 12
MblFn
|
122 | | eqid 2622 |
. . . . . . . . . . . 12
|
123 | 121, 122 | fmptd 6385 |
. . . . . . . . . . 11
MblFn
|
124 | | ifan 4134 |
. . . . . . . . . . . . . . 15
|
125 | 73 | renegcld 10457 |
. . . . . . . . . . . . . . . . . . . 20
MblFn
|
126 | 73 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . 22
MblFn
|
127 | 126 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . . 21
MblFn
|
128 | 125 | leabsd 14153 |
. . . . . . . . . . . . . . . . . . . . . 22
MblFn
|
129 | 126 | absnegd 14188 |
. . . . . . . . . . . . . . . . . . . . . 22
MblFn
|
130 | 128, 129 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . 21
MblFn
|
131 | | absrele 14048 |
. . . . . . . . . . . . . . . . . . . . . 22
|
132 | 72, 131 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
MblFn
|
133 | 125, 127,
74, 130, 132 | letrd 10194 |
. . . . . . . . . . . . . . . . . . . 20
MblFn
|
134 | 125, 74, 75, 133, 82 | letrd 10194 |
. . . . . . . . . . . . . . . . . . 19
MblFn
|
135 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . 20
|
136 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . 20
|
137 | 135, 136 | ifboth 4124 |
. . . . . . . . . . . . . . . . . . 19
|
138 | 134, 85, 137 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
MblFn
|
139 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . 19
|
140 | 139 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
MblFn
|
141 | 138, 140,
93 | 3brtr4d 4685 |
. . . . . . . . . . . . . . . . 17
MblFn
|
142 | 141 | ex 450 |
. . . . . . . . . . . . . . . 16
MblFn
|
143 | | iffalse 4095 |
. . . . . . . . . . . . . . . . 17
|
144 | 97, 143, 99 | 3brtr4d 4685 |
. . . . . . . . . . . . . . . 16
|
145 | 142, 144 | pm2.61d1 171 |
. . . . . . . . . . . . . . 15
MblFn
|
146 | 124, 145 | syl5eqbr 4688 |
. . . . . . . . . . . . . 14
MblFn
|
147 | 146 | ralrimivw 2967 |
. . . . . . . . . . . . 13
MblFn
|
148 | | eqidd 2623 |
. . . . . . . . . . . . . 14
MblFn
|
149 | 105, 121,
67, 148, 107 | ofrfval2 6915 |
. . . . . . . . . . . . 13
MblFn
|
150 | 147, 149 | mpbird 247 |
. . . . . . . . . . . 12
MblFn
|
151 | | itg2le 23506 |
. . . . . . . . . . . 12
|
152 | 123, 69, 150, 151 | syl3anc 1326 |
. . . . . . . . . . 11
MblFn
|
153 | | itg2lecl 23505 |
. . . . . . . . . . 11
|
154 | 123, 59, 152, 153 | syl3anc 1326 |
. . . . . . . . . 10
MblFn
|
155 | 113, 154 | jca 554 |
. . . . . . . . 9
MblFn
|
156 | 37 | imcld 13935 |
. . . . . . . . . . . . . . . 16
MblFn
|
157 | 156 | rexrd 10089 |
. . . . . . . . . . . . . . 15
MblFn
|
158 | 157 | adantrr 753 |
. . . . . . . . . . . . . 14
MblFn
|
159 | | simprr 796 |
. . . . . . . . . . . . . 14
MblFn
|
160 | | elxrge0 12281 |
. . . . . . . . . . . . . 14
|
161 | 158, 159,
160 | sylanbrc 698 |
. . . . . . . . . . . . 13
MblFn
|
162 | 44 | a1i 11 |
. . . . . . . . . . . . 13
MblFn
|
163 | 161, 162 | ifclda 4120 |
. . . . . . . . . . . 12
MblFn
|
164 | | eqid 2622 |
. . . . . . . . . . . 12
|
165 | 163, 164 | fmptd 6385 |
. . . . . . . . . . 11
MblFn
|
166 | | ifan 4134 |
. . . . . . . . . . . . . . 15
|
167 | 72 | imcld 13935 |
. . . . . . . . . . . . . . . . . . . 20
MblFn
|
168 | 167 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . 22
MblFn
|
169 | 168 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . . 21
MblFn
|
170 | 167 | leabsd 14153 |
. . . . . . . . . . . . . . . . . . . . 21
MblFn
|
171 | | absimle 14049 |
. . . . . . . . . . . . . . . . . . . . . 22
|
172 | 72, 171 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
MblFn
|
173 | 167, 169,
74, 170, 172 | letrd 10194 |
. . . . . . . . . . . . . . . . . . . 20
MblFn
|
174 | 167, 74, 75, 173, 82 | letrd 10194 |
. . . . . . . . . . . . . . . . . . 19
MblFn
|
175 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . 20
|
176 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . 20
|
177 | 175, 176 | ifboth 4124 |
. . . . . . . . . . . . . . . . . . 19
|
178 | 174, 85, 177 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
MblFn
|
179 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . 19
|
180 | 179 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
MblFn
|
181 | 178, 180,
93 | 3brtr4d 4685 |
. . . . . . . . . . . . . . . . 17
MblFn
|
182 | 181 | ex 450 |
. . . . . . . . . . . . . . . 16
MblFn
|
183 | | iffalse 4095 |
. . . . . . . . . . . . . . . . 17
|
184 | 97, 183, 99 | 3brtr4d 4685 |
. . . . . . . . . . . . . . . 16
|
185 | 182, 184 | pm2.61d1 171 |
. . . . . . . . . . . . . . 15
MblFn
|
186 | 166, 185 | syl5eqbr 4688 |
. . . . . . . . . . . . . 14
MblFn
|
187 | 186 | ralrimivw 2967 |
. . . . . . . . . . . . 13
MblFn
|
188 | | eqidd 2623 |
. . . . . . . . . . . . . 14
MblFn
|
189 | 105, 163,
67, 188, 107 | ofrfval2 6915 |
. . . . . . . . . . . . 13
MblFn
|
190 | 187, 189 | mpbird 247 |
. . . . . . . . . . . 12
MblFn
|
191 | | itg2le 23506 |
. . . . . . . . . . . 12
|
192 | 165, 69, 190, 191 | syl3anc 1326 |
. . . . . . . . . . 11
MblFn
|
193 | | itg2lecl 23505 |
. . . . . . . . . . 11
|
194 | 165, 59, 192, 193 | syl3anc 1326 |
. . . . . . . . . 10
MblFn
|
195 | 156 | renegcld 10457 |
. . . . . . . . . . . . . . . 16
MblFn
|
196 | 195 | rexrd 10089 |
. . . . . . . . . . . . . . 15
MblFn
|
197 | 196 | adantrr 753 |
. . . . . . . . . . . . . 14
MblFn
|
198 | | simprr 796 |
. . . . . . . . . . . . . 14
MblFn
|
199 | | elxrge0 12281 |
. . . . . . . . . . . . . 14
|
200 | 197, 198,
199 | sylanbrc 698 |
. . . . . . . . . . . . 13
MblFn
|
201 | 44 | a1i 11 |
. . . . . . . . . . . . 13
MblFn
|
202 | 200, 201 | ifclda 4120 |
. . . . . . . . . . . 12
MblFn
|
203 | | eqid 2622 |
. . . . . . . . . . . 12
|
204 | 202, 203 | fmptd 6385 |
. . . . . . . . . . 11
MblFn
|
205 | | ifan 4134 |
. . . . . . . . . . . . . . 15
|
206 | 167 | renegcld 10457 |
. . . . . . . . . . . . . . . . . . . 20
MblFn
|
207 | 206 | leabsd 14153 |
. . . . . . . . . . . . . . . . . . . . . 22
MblFn
|
208 | 168 | absnegd 14188 |
. . . . . . . . . . . . . . . . . . . . . 22
MblFn
|
209 | 207, 208 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . 21
MblFn
|
210 | 206, 169,
74, 209, 172 | letrd 10194 |
. . . . . . . . . . . . . . . . . . . 20
MblFn
|
211 | 206, 74, 75, 210, 82 | letrd 10194 |
. . . . . . . . . . . . . . . . . . 19
MblFn
|
212 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . 20
|
213 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . 20
|
214 | 212, 213 | ifboth 4124 |
. . . . . . . . . . . . . . . . . . 19
|
215 | 211, 85, 214 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
MblFn
|
216 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . 19
|
217 | 216 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
MblFn
|
218 | 215, 217,
93 | 3brtr4d 4685 |
. . . . . . . . . . . . . . . . 17
MblFn
|
219 | 218 | ex 450 |
. . . . . . . . . . . . . . . 16
MblFn
|
220 | | iffalse 4095 |
. . . . . . . . . . . . . . . . 17
|
221 | 97, 220, 99 | 3brtr4d 4685 |
. . . . . . . . . . . . . . . 16
|
222 | 219, 221 | pm2.61d1 171 |
. . . . . . . . . . . . . . 15
MblFn
|
223 | 205, 222 | syl5eqbr 4688 |
. . . . . . . . . . . . . 14
MblFn
|
224 | 223 | ralrimivw 2967 |
. . . . . . . . . . . . 13
MblFn
|
225 | | eqidd 2623 |
. . . . . . . . . . . . . 14
MblFn
|
226 | 105, 202,
67, 225, 107 | ofrfval2 6915 |
. . . . . . . . . . . . 13
MblFn
|
227 | 224, 226 | mpbird 247 |
. . . . . . . . . . . 12
MblFn
|
228 | | itg2le 23506 |
. . . . . . . . . . . 12
|
229 | 204, 69, 227, 228 | syl3anc 1326 |
. . . . . . . . . . 11
MblFn
|
230 | | itg2lecl 23505 |
. . . . . . . . . . 11
|
231 | 204, 59, 229, 230 | syl3anc 1326 |
. . . . . . . . . 10
MblFn
|
232 | 194, 231 | jca 554 |
. . . . . . . . 9
MblFn
|
233 | | eqid 2622 |
. . . . . . . . . 10
|
234 | | eqid 2622 |
. . . . . . . . . 10
|
235 | | eqid 2622 |
. . . . . . . . . 10
|
236 | | eqid 2622 |
. . . . . . . . . 10
|
237 | 233, 234,
235, 236, 72 | iblcnlem1 23554 |
. . . . . . . . 9
MblFn
MblFn
|
238 | 35, 155, 232, 237 | mpbir3and 1245 |
. . . . . . . 8
MblFn
|
239 | 32, 238 | sylan2b 492 |
. . . . . . 7
MblFn
|
240 | 239 | anassrs 680 |
. . . . . 6
MblFn |
241 | 31, 240 | syldan 487 |
. . . . 5
MblFn |
242 | 13, 241 | pm2.61dane 2881 |
. . . 4
MblFn
|
243 | 242 | rexlimdvaa 3032 |
. . 3
MblFn
|
244 | 243 | 3impia 1261 |
. 2
MblFn
|
245 | 3, 244 | eqeltrd 2701 |
1
MblFn
|