Step | Hyp | Ref
| Expression |
1 | | totbndbnd 33588 |
. 2
|
2 | | rpcn 11841 |
. . . . . . . . . 10
|
3 | 2 | adantl 482 |
. . . . . . . . 9
|
4 | | gzcn 15636 |
. . . . . . . . 9
|
5 | | mulcl 10020 |
. . . . . . . . 9
|
6 | 3, 4, 5 | syl2an 494 |
. . . . . . . 8
|
7 | | eqid 2622 |
. . . . . . . 8
|
8 | 6, 7 | fmptd 6385 |
. . . . . . 7
|
9 | | frn 6053 |
. . . . . . 7
|
10 | 8, 9 | syl 17 |
. . . . . 6
|
11 | | cnex 10017 |
. . . . . . 7
|
12 | 11 | elpw2 4828 |
. . . . . 6
|
13 | 10, 12 | sylibr 224 |
. . . . 5
|
14 | | cnmet 22575 |
. . . . . . . . . . . . . . . . 17
|
15 | | cntotbnd.d |
. . . . . . . . . . . . . . . . . 18
|
16 | 15 | bnd2lem 33590 |
. . . . . . . . . . . . . . . . 17
|
17 | 14, 16 | mpan 706 |
. . . . . . . . . . . . . . . 16
|
18 | 17 | sselda 3603 |
. . . . . . . . . . . . . . 15
|
19 | 18 | adantrl 752 |
. . . . . . . . . . . . . 14
|
20 | 19 | recld 13934 |
. . . . . . . . . . . . 13
|
21 | | simprl 794 |
. . . . . . . . . . . . 13
|
22 | 20, 21 | rerpdivcld 11903 |
. . . . . . . . . . . 12
|
23 | | halfre 11246 |
. . . . . . . . . . . 12
|
24 | | readdcl 10019 |
. . . . . . . . . . . 12
|
25 | 22, 23, 24 | sylancl 694 |
. . . . . . . . . . 11
|
26 | 25 | flcld 12599 |
. . . . . . . . . 10
|
27 | 19 | imcld 13935 |
. . . . . . . . . . . . 13
|
28 | 27, 21 | rerpdivcld 11903 |
. . . . . . . . . . . 12
|
29 | | readdcl 10019 |
. . . . . . . . . . . 12
|
30 | 28, 23, 29 | sylancl 694 |
. . . . . . . . . . 11
|
31 | 30 | flcld 12599 |
. . . . . . . . . 10
|
32 | | gzreim 15643 |
. . . . . . . . . 10
|
33 | 26, 31, 32 | syl2anc 693 |
. . . . . . . . 9
|
34 | | gzcn 15636 |
. . . . . . . . . . . . . . 15
|
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . 14
|
36 | 21 | rpcnd 11874 |
. . . . . . . . . . . . . . 15
|
37 | 21 | rpne0d 11877 |
. . . . . . . . . . . . . . 15
|
38 | 19, 36, 37 | divcld 10801 |
. . . . . . . . . . . . . 14
|
39 | 35, 38 | subcld 10392 |
. . . . . . . . . . . . 13
|
40 | 39 | abscld 14175 |
. . . . . . . . . . . 12
|
41 | | 1re 10039 |
. . . . . . . . . . . . 13
|
42 | 41 | a1i 11 |
. . . . . . . . . . . 12
|
43 | 26 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . 20
|
44 | | ax-icn 9995 |
. . . . . . . . . . . . . . . . . . . . 21
|
45 | 31 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . . 21
|
46 | | mulcl 10020 |
. . . . . . . . . . . . . . . . . . . . 21
|
47 | 44, 45, 46 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . 20
|
48 | 22 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
|
49 | 28 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . 21
|
50 | | mulcl 10020 |
. . . . . . . . . . . . . . . . . . . . 21
|
51 | 44, 49, 50 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . 20
|
52 | 43, 47, 48, 51 | addsub4d 10439 |
. . . . . . . . . . . . . . . . . . 19
|
53 | 38 | replimd 13937 |
. . . . . . . . . . . . . . . . . . . . 21
|
54 | 21 | rpred 11872 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
55 | 54, 19, 37 | redivd 13969 |
. . . . . . . . . . . . . . . . . . . . . 22
|
56 | 54, 19, 37 | imdivd 13970 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
57 | 56 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . 22
|
58 | 55, 57 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . 21
|
59 | 53, 58 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . 20
|
60 | 59 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
|
61 | 44 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
|
62 | 61, 45, 49 | subdid 10486 |
. . . . . . . . . . . . . . . . . . . 20
|
63 | 62 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
|
64 | 52, 60, 63 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . . . 18
|
65 | 64 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
|
66 | 65 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
|
67 | 26 | zred 11482 |
. . . . . . . . . . . . . . . . . 18
|
68 | 67, 22 | resubcld 10458 |
. . . . . . . . . . . . . . . . 17
|
69 | 31 | zred 11482 |
. . . . . . . . . . . . . . . . . 18
|
70 | 69, 28 | resubcld 10458 |
. . . . . . . . . . . . . . . . 17
|
71 | | absreimsq 14032 |
. . . . . . . . . . . . . . . . 17
|
72 | 68, 70, 71 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
73 | 66, 72 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
74 | 68 | resqcld 13035 |
. . . . . . . . . . . . . . . 16
|
75 | 70 | resqcld 13035 |
. . . . . . . . . . . . . . . 16
|
76 | 23 | resqcli 12949 |
. . . . . . . . . . . . . . . . . 18
|
77 | 76 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
78 | 23 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
79 | | absresq 14042 |
. . . . . . . . . . . . . . . . . . 19
|
80 | 68, 79 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
81 | | rddif 14080 |
. . . . . . . . . . . . . . . . . . . 20
|
82 | 22, 81 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
83 | 68 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . 21
|
84 | 83 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . 20
|
85 | 83 | absge0d 14183 |
. . . . . . . . . . . . . . . . . . . 20
|
86 | | halfgt0 11248 |
. . . . . . . . . . . . . . . . . . . . . 22
|
87 | 23, 86 | elrpii 11835 |
. . . . . . . . . . . . . . . . . . . . 21
|
88 | | rpge0 11845 |
. . . . . . . . . . . . . . . . . . . . 21
|
89 | 87, 88 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . 20
|
90 | 84, 78, 85, 89 | le2sqd 13044 |
. . . . . . . . . . . . . . . . . . 19
|
91 | 82, 90 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
|
92 | 80, 91 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . . . 17
|
93 | | halfcn 11247 |
. . . . . . . . . . . . . . . . . . . 20
|
94 | 93 | sqvali 12943 |
. . . . . . . . . . . . . . . . . . 19
|
95 | | halflt1 11250 |
. . . . . . . . . . . . . . . . . . . . 21
|
96 | 23, 41, 23, 86 | ltmul1ii 10952 |
. . . . . . . . . . . . . . . . . . . . 21
|
97 | 95, 96 | mpbi 220 |
. . . . . . . . . . . . . . . . . . . 20
|
98 | 93 | mulid2i 10043 |
. . . . . . . . . . . . . . . . . . . 20
|
99 | 97, 98 | breqtri 4678 |
. . . . . . . . . . . . . . . . . . 19
|
100 | 94, 99 | eqbrtri 4674 |
. . . . . . . . . . . . . . . . . 18
|
101 | 100 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
102 | 74, 77, 78, 92, 101 | lelttrd 10195 |
. . . . . . . . . . . . . . . 16
|
103 | | absresq 14042 |
. . . . . . . . . . . . . . . . . . 19
|
104 | 70, 103 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
105 | | rddif 14080 |
. . . . . . . . . . . . . . . . . . . 20
|
106 | 28, 105 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
107 | 70 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . 21
|
108 | 107 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . 20
|
109 | 107 | absge0d 14183 |
. . . . . . . . . . . . . . . . . . . 20
|
110 | 108, 78, 109, 89 | le2sqd 13044 |
. . . . . . . . . . . . . . . . . . 19
|
111 | 106, 110 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
|
112 | 104, 111 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . . . 17
|
113 | 75, 77, 78, 112, 101 | lelttrd 10195 |
. . . . . . . . . . . . . . . 16
|
114 | 74, 75, 42, 102, 113 | lt2halvesd 11280 |
. . . . . . . . . . . . . . 15
|
115 | 73, 114 | eqbrtrd 4675 |
. . . . . . . . . . . . . 14
|
116 | | sq1 12958 |
. . . . . . . . . . . . . 14
|
117 | 115, 116 | syl6breqr 4695 |
. . . . . . . . . . . . 13
|
118 | 39 | absge0d 14183 |
. . . . . . . . . . . . . 14
|
119 | | 0le1 10551 |
. . . . . . . . . . . . . . 15
|
120 | 119 | a1i 11 |
. . . . . . . . . . . . . 14
|
121 | 40, 42, 118, 120 | lt2sqd 13043 |
. . . . . . . . . . . . 13
|
122 | 117, 121 | mpbird 247 |
. . . . . . . . . . . 12
|
123 | 40, 42, 21, 122 | ltmul2dd 11928 |
. . . . . . . . . . 11
|
124 | 36, 35 | mulcld 10060 |
. . . . . . . . . . . . 13
|
125 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
126 | 125 | cnmetdval 22574 |
. . . . . . . . . . . . 13
|
127 | 124, 19, 126 | syl2anc 693 |
. . . . . . . . . . . 12
|
128 | 36, 35, 38 | subdid 10486 |
. . . . . . . . . . . . . . 15
|
129 | 19, 36, 37 | divcan2d 10803 |
. . . . . . . . . . . . . . . 16
|
130 | 129 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
131 | 128, 130 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
132 | 131 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
133 | 36, 39 | absmuld 14193 |
. . . . . . . . . . . . 13
|
134 | 132, 133 | eqtr3d 2658 |
. . . . . . . . . . . 12
|
135 | 21 | rpge0d 11876 |
. . . . . . . . . . . . . 14
|
136 | 54, 135 | absidd 14161 |
. . . . . . . . . . . . 13
|
137 | 136 | oveq1d 6665 |
. . . . . . . . . . . 12
|
138 | 127, 134,
137 | 3eqtrrd 2661 |
. . . . . . . . . . 11
|
139 | 36 | mulid1d 10057 |
. . . . . . . . . . 11
|
140 | 123, 138,
139 | 3brtr3d 4684 |
. . . . . . . . . 10
|
141 | | cnxmet 22576 |
. . . . . . . . . . . 12
|
142 | 141 | a1i 11 |
. . . . . . . . . . 11
|
143 | | rpxr 11840 |
. . . . . . . . . . . 12
|
144 | 143 | ad2antrl 764 |
. . . . . . . . . . 11
|
145 | | elbl2 22195 |
. . . . . . . . . . 11
|
146 | 142, 144,
124, 19, 145 | syl22anc 1327 |
. . . . . . . . . 10
|
147 | 140, 146 | mpbird 247 |
. . . . . . . . 9
|
148 | | oveq2 6658 |
. . . . . . . . . . . 12
|
149 | 148 | oveq1d 6665 |
. . . . . . . . . . 11
|
150 | 149 | eleq2d 2687 |
. . . . . . . . . 10
|
151 | 150 | rspcev 3309 |
. . . . . . . . 9
|
152 | 33, 147, 151 | syl2anc 693 |
. . . . . . . 8
|
153 | 152 | expr 643 |
. . . . . . 7
|
154 | | eliun 4524 |
. . . . . . . 8
|
155 | | ovex 6678 |
. . . . . . . . . 10
|
156 | 155 | rgenw 2924 |
. . . . . . . . 9
|
157 | | oveq1 6657 |
. . . . . . . . . . 11
|
158 | 157 | eleq2d 2687 |
. . . . . . . . . 10
|
159 | 7, 158 | rexrnmpt 6369 |
. . . . . . . . 9
|
160 | 156, 159 | ax-mp 5 |
. . . . . . . 8
|
161 | 154, 160 | bitri 264 |
. . . . . . 7
|
162 | 153, 161 | syl6ibr 242 |
. . . . . 6
|
163 | 162 | ssrdv 3609 |
. . . . 5
|
164 | | simpl 473 |
. . . . . . 7
|
165 | | 0cn 10032 |
. . . . . . . 8
|
166 | 15 | ssbnd 33587 |
. . . . . . . 8
|
167 | 14, 165, 166 | mp2an 708 |
. . . . . . 7
|
168 | 164, 167 | sylib 208 |
. . . . . 6
|
169 | | fzfi 12771 |
. . . . . . . . 9
|
170 | | xpfi 8231 |
. . . . . . . . 9
|
171 | 169, 169,
170 | mp2an 708 |
. . . . . . . 8
|
172 | | eqid 2622 |
. . . . . . . . . 10
|
173 | | ovex 6678 |
. . . . . . . . . 10
|
174 | 172, 173 | fnmpt2i 7239 |
. . . . . . . . 9
|
175 | | dffn4 6121 |
. . . . . . . . 9
|
176 | 174, 175 | mpbi 220 |
. . . . . . . 8
|
177 | | fofi 8252 |
. . . . . . . 8
|
178 | 171, 176,
177 | mp2an 708 |
. . . . . . 7
|
179 | 7, 155 | elrnmpti 5376 |
. . . . . . . . . 10
|
180 | | elgz 15635 |
. . . . . . . . . . . . . . . . . . . . . 22
|
181 | 180 | simp2bi 1077 |
. . . . . . . . . . . . . . . . . . . . 21
|
182 | 181 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . 20
|
183 | 182 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . 19
|
184 | 183 | abscld 14175 |
. . . . . . . . . . . . . . . . . 18
|
185 | 4 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . 19
|
186 | 185 | abscld 14175 |
. . . . . . . . . . . . . . . . . 18
|
187 | | simpllr 799 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
188 | 187 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
189 | 188 | rpred 11872 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
190 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
191 | 190 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
192 | 189, 191 | readdcld 10069 |
. . . . . . . . . . . . . . . . . . . . . 22
|
193 | 192, 188 | rerpdivcld 11903 |
. . . . . . . . . . . . . . . . . . . . 21
|
194 | 193 | flcld 12599 |
. . . . . . . . . . . . . . . . . . . 20
|
195 | 194 | peano2zd 11485 |
. . . . . . . . . . . . . . . . . . 19
|
196 | 195 | zred 11482 |
. . . . . . . . . . . . . . . . . 18
|
197 | | absrele 14048 |
. . . . . . . . . . . . . . . . . . 19
|
198 | 185, 197 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
199 | 188 | rpcnd 11874 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
200 | 199, 185 | absmuld 14193 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
201 | 188 | rpge0d 11876 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
202 | 189, 201 | absidd 14161 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
203 | 202 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
204 | 200, 203 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . 22
|
205 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
206 | | sslin 3839 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
207 | 205, 206 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
208 | 141 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
209 | 6 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
210 | 165 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
211 | 187 | rpxrd 11873 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
212 | 190 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
213 | | bldisj 22203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
214 | 213 | 3exp2 1285 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
215 | 214 | imp32 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
216 | 208, 209,
210, 211, 212, 215 | syl32anc 1334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
217 | | sseq0 3975 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
218 | 207, 216,
217 | syl6an 568 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
219 | 218 | necon3ad 2807 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
220 | 219 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
221 | | rexadd 12063 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
222 | 189, 191,
221 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
223 | 209 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
224 | 125 | cnmetdval 22574 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
225 | 223, 165,
224 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
226 | 223 | subid1d 10381 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
227 | 226 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
228 | 225, 227 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
229 | 222, 228 | breq12d 4666 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
230 | 220, 229 | mtbid 314 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
231 | 223 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
232 | 231, 192 | ltnled 10184 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
233 | 230, 232 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . 22
|
234 | 204, 233 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . . . . . . . 21
|
235 | 186, 192,
188 | ltmuldiv2d 11920 |
. . . . . . . . . . . . . . . . . . . . 21
|
236 | 234, 235 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . 20
|
237 | | flltp1 12601 |
. . . . . . . . . . . . . . . . . . . . 21
|
238 | 193, 237 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
239 | 186, 193,
196, 236, 238 | lttrd 10198 |
. . . . . . . . . . . . . . . . . . 19
|
240 | 186, 196,
239 | ltled 10185 |
. . . . . . . . . . . . . . . . . 18
|
241 | 184, 186,
196, 198, 240 | letrd 10194 |
. . . . . . . . . . . . . . . . 17
|
242 | 182 | zred 11482 |
. . . . . . . . . . . . . . . . . 18
|
243 | 242, 196 | absled 14169 |
. . . . . . . . . . . . . . . . 17
|
244 | 241, 243 | mpbid 222 |
. . . . . . . . . . . . . . . 16
|
245 | 195 | znegcld 11484 |
. . . . . . . . . . . . . . . . 17
|
246 | | elfz 12332 |
. . . . . . . . . . . . . . . . 17
|
247 | 182, 245,
195, 246 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
248 | 244, 247 | mpbird 247 |
. . . . . . . . . . . . . . 15
|
249 | 180 | simp3bi 1078 |
. . . . . . . . . . . . . . . . . . . . 21
|
250 | 249 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . 20
|
251 | 250 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . 19
|
252 | 251 | abscld 14175 |
. . . . . . . . . . . . . . . . . 18
|
253 | | absimle 14049 |
. . . . . . . . . . . . . . . . . . 19
|
254 | 185, 253 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
255 | 252, 186,
196, 254, 240 | letrd 10194 |
. . . . . . . . . . . . . . . . 17
|
256 | 250 | zred 11482 |
. . . . . . . . . . . . . . . . . 18
|
257 | 256, 196 | absled 14169 |
. . . . . . . . . . . . . . . . 17
|
258 | 255, 257 | mpbid 222 |
. . . . . . . . . . . . . . . 16
|
259 | | elfz 12332 |
. . . . . . . . . . . . . . . . 17
|
260 | 250, 245,
195, 259 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
261 | 258, 260 | mpbird 247 |
. . . . . . . . . . . . . . 15
|
262 | 185 | replimd 13937 |
. . . . . . . . . . . . . . . 16
|
263 | 262 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
264 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
|
265 | 264 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
|
266 | 265 | eqeq2d 2632 |
. . . . . . . . . . . . . . . 16
|
267 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
|
268 | 267 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
|
269 | 268 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
|
270 | 269 | eqeq2d 2632 |
. . . . . . . . . . . . . . . 16
|
271 | 266, 270 | rspc2ev 3324 |
. . . . . . . . . . . . . . 15
|
272 | 248, 261,
263, 271 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
273 | 272 | ex 450 |
. . . . . . . . . . . . 13
|
274 | 172, 173 | elrnmpt2 6773 |
. . . . . . . . . . . . 13
|
275 | 273, 274 | syl6ibr 242 |
. . . . . . . . . . . 12
|
276 | 157 | ineq1d 3813 |
. . . . . . . . . . . . . 14
|
277 | 276 | neeq1d 2853 |
. . . . . . . . . . . . 13
|
278 | | eleq1 2689 |
. . . . . . . . . . . . 13
|
279 | 277, 278 | imbi12d 334 |
. . . . . . . . . . . 12
|
280 | 275, 279 | syl5ibrcom 237 |
. . . . . . . . . . 11
|
281 | 280 | rexlimdva 3031 |
. . . . . . . . . 10
|
282 | 179, 281 | syl5bi 232 |
. . . . . . . . 9
|
283 | 282 | 3imp 1256 |
. . . . . . . 8
|
284 | 283 | rabssdv 3682 |
. . . . . . 7
|
285 | | ssfi 8180 |
. . . . . . 7
|
286 | 178, 284,
285 | sylancr 695 |
. . . . . 6
|
287 | 168, 286 | rexlimddv 3035 |
. . . . 5
|
288 | | iuneq1 4534 |
. . . . . . . 8
|
289 | 288 | sseq2d 3633 |
. . . . . . 7
|
290 | | rabeq 3192 |
. . . . . . . 8
|
291 | 290 | eleq1d 2686 |
. . . . . . 7
|
292 | 289, 291 | anbi12d 747 |
. . . . . 6
|
293 | 292 | rspcev 3309 |
. . . . 5
|
294 | 13, 163, 287, 293 | syl12anc 1324 |
. . . 4
|
295 | 294 | ralrimiva 2966 |
. . 3
|
296 | 15 | sstotbnd3 33575 |
. . . 4
|
297 | 14, 17, 296 | sylancr 695 |
. . 3
|
298 | 295, 297 | mpbird 247 |
. 2
|
299 | 1, 298 | impbii 199 |
1
|