Step | Hyp | Ref
| Expression |
1 | | inss1 3833 |
. . 3
|
2 | 1 | a1i 11 |
. 2
|
3 | 2 | sselda 3603 |
. . . . . . 7
|
4 | | smflimlem4.6 |
. . . . . . . . . 10
|
5 | 4 | a1i 11 |
. . . . . . . . 9
|
6 | | nfv 1843 |
. . . . . . . . . . 11
|
7 | | nfcv 2764 |
. . . . . . . . . . 11
|
8 | | nfcv 2764 |
. . . . . . . . . . 11
|
9 | | smflimlem4.2 |
. . . . . . . . . . 11
|
10 | | smflimlem4.3 |
. . . . . . . . . . . . . 14
SAlg |
11 | 10 | adantr 481 |
. . . . . . . . . . . . 13
SAlg |
12 | | smflimlem4.4 |
. . . . . . . . . . . . . 14
SMblFn |
13 | 12 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
SMblFn |
14 | | eqid 2622 |
. . . . . . . . . . . . 13
|
15 | 11, 13, 14 | smff 40941 |
. . . . . . . . . . . 12
|
16 | 15 | adantlr 751 |
. . . . . . . . . . 11
|
17 | | smflimlem4.5 |
. . . . . . . . . . . 12
|
18 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
19 | 18 | mpteq2dv 4745 |
. . . . . . . . . . . . . 14
|
20 | 19 | eleq1d 2686 |
. . . . . . . . . . . . 13
|
21 | 20 | cbvrabv 3199 |
. . . . . . . . . . . 12
|
22 | 17, 21 | eqtri 2644 |
. . . . . . . . . . 11
|
23 | | simpr 477 |
. . . . . . . . . . 11
|
24 | 6, 7, 8, 9, 16, 22, 23 | fnlimfvre 39906 |
. . . . . . . . . 10
|
25 | 24 | elexd 3214 |
. . . . . . . . 9
|
26 | 5, 25 | fvmpt2d 6293 |
. . . . . . . 8
|
27 | 26, 24 | eqeltrd 2701 |
. . . . . . 7
|
28 | 3, 27 | syldan 487 |
. . . . . 6
|
29 | 28 | adantr 481 |
. . . . 5
|
30 | | smflimlem4.7 |
. . . . . . . 8
|
31 | 30 | adantr 481 |
. . . . . . 7
|
32 | | rpre 11839 |
. . . . . . . 8
|
33 | 32 | adantl 482 |
. . . . . . 7
|
34 | 31, 33 | readdcld 10069 |
. . . . . 6
|
35 | 34 | adantlr 751 |
. . . . 5
|
36 | | nfv 1843 |
. . . . . . . 8
|
37 | | rphalfcl 11858 |
. . . . . . . . . . 11
|
38 | | rpgtrecnn 39597 |
. . . . . . . . . . 11
|
39 | 37, 38 | syl 17 |
. . . . . . . . . 10
|
40 | 39 | adantl 482 |
. . . . . . . . 9
|
41 | 10 | ad4antr 768 |
. . . . . . . . . . . 12
SAlg |
42 | 13 | adantlr 751 |
. . . . . . . . . . . . 13
SMblFn |
43 | 42 | ad5ant15 1303 |
. . . . . . . . . . . 12
SMblFn |
44 | 30 | adantr 481 |
. . . . . . . . . . . . 13
|
45 | 44 | ad3antrrr 766 |
. . . . . . . . . . . 12
|
46 | | smflimlem4.8 |
. . . . . . . . . . . . 13
|
47 | | nfcv 2764 |
. . . . . . . . . . . . . 14
|
48 | | nfcv 2764 |
. . . . . . . . . . . . . 14
|
49 | | nfcv 2764 |
. . . . . . . . . . . . . 14
|
50 | | nfcv 2764 |
. . . . . . . . . . . . . 14
|
51 | 18 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . 19
|
52 | 51 | cbvrabv 3199 |
. . . . . . . . . . . . . . . . . 18
|
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
54 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . 20
|
55 | 54 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
|
56 | 55 | breq2d 4665 |
. . . . . . . . . . . . . . . . . 18
|
57 | 56 | rabbidv 3189 |
. . . . . . . . . . . . . . . . 17
|
58 | 53, 57 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
|
59 | 58 | eqeq1d 2624 |
. . . . . . . . . . . . . . 15
|
60 | 59 | rabbidv 3189 |
. . . . . . . . . . . . . 14
|
61 | 47, 48, 49, 50, 60 | cbvmpt22 39277 |
. . . . . . . . . . . . 13
|
62 | 46, 61 | eqtri 2644 |
. . . . . . . . . . . 12
|
63 | | smflimlem4.9 |
. . . . . . . . . . . . 13
|
64 | | nfcv 2764 |
. . . . . . . . . . . . . 14
|
65 | | nfcv 2764 |
. . . . . . . . . . . . . 14
|
66 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
|
67 | 66 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
68 | 47, 48, 64, 65, 67 | cbvmpt22 39277 |
. . . . . . . . . . . . 13
|
69 | 63, 68 | eqtri 2644 |
. . . . . . . . . . . 12
|
70 | | smflimlem4.10 |
. . . . . . . . . . . . 13
|
71 | | simpll 790 |
. . . . . . . . . . . . . . . . 17
|
72 | 71 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
|
73 | 72 | iineq2dv 4543 |
. . . . . . . . . . . . . . 15
|
74 | 73 | iuneq2dv 4542 |
. . . . . . . . . . . . . 14
|
75 | 74 | cbviinv 4560 |
. . . . . . . . . . . . 13
|
76 | 70, 75 | eqtri 2644 |
. . . . . . . . . . . 12
|
77 | | smflimlem4.11 |
. . . . . . . . . . . . . 14
|
78 | 77 | adantlr 751 |
. . . . . . . . . . . . 13
|
79 | 78 | ad5ant15 1303 |
. . . . . . . . . . . 12
|
80 | | simp-4r 807 |
. . . . . . . . . . . 12
|
81 | | simplr 792 |
. . . . . . . . . . . 12
|
82 | 37 | ad3antlr 767 |
. . . . . . . . . . . 12
|
83 | | simpr 477 |
. . . . . . . . . . . 12
|
84 | 9, 41, 43, 22, 45, 62, 69, 76, 79, 80, 81, 82, 83 | smflimlem3 40981 |
. . . . . . . . . . 11
|
85 | 84 | exp31 630 |
. . . . . . . . . 10
|
86 | 85 | rexlimdv 3030 |
. . . . . . . . 9
|
87 | 40, 86 | mpd 15 |
. . . . . . . 8
|
88 | | nfv 1843 |
. . . . . . . . . 10
|
89 | | nfcv 2764 |
. . . . . . . . . 10
|
90 | | nfcv 2764 |
. . . . . . . . . 10
|
91 | | smflimlem4.1 |
. . . . . . . . . . 11
|
92 | 91 | ad2antrr 762 |
. . . . . . . . . 10
|
93 | | eleq1 2689 |
. . . . . . . . . . . . . 14
|
94 | 93 | anbi2d 740 |
. . . . . . . . . . . . 13
|
95 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
96 | 95 | dmeqd 5326 |
. . . . . . . . . . . . . 14
|
97 | 95, 96 | feq12d 6033 |
. . . . . . . . . . . . 13
|
98 | 94, 97 | imbi12d 334 |
. . . . . . . . . . . 12
|
99 | 98, 15 | chvarv 2263 |
. . . . . . . . . . 11
|
100 | 99 | ad4ant14 1293 |
. . . . . . . . . 10
|
101 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
102 | 101 | dmeqd 5326 |
. . . . . . . . . . . . . . . 16
|
103 | 102 | cbviinv 4560 |
. . . . . . . . . . . . . . 15
|
104 | 103 | a1i 11 |
. . . . . . . . . . . . . 14
|
105 | 104 | iuneq2i 4539 |
. . . . . . . . . . . . 13
|
106 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
107 | 106 | iineq1d 39267 |
. . . . . . . . . . . . . . 15
|
108 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
109 | 108 | dmeqd 5326 |
. . . . . . . . . . . . . . . . 17
|
110 | 109 | cbviinv 4560 |
. . . . . . . . . . . . . . . 16
|
111 | 110 | a1i 11 |
. . . . . . . . . . . . . . 15
|
112 | 107, 111 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
113 | 112 | cbviunv 4559 |
. . . . . . . . . . . . 13
|
114 | 105, 113 | eqtri 2644 |
. . . . . . . . . . . 12
|
115 | 114 | rabeqi 3193 |
. . . . . . . . . . 11
|
116 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
117 | 116 | fveq1d 6193 |
. . . . . . . . . . . . . . . 16
|
118 | 117 | cbvmptv 4750 |
. . . . . . . . . . . . . . 15
|
119 | 118 | eqcomi 2631 |
. . . . . . . . . . . . . 14
|
120 | 119 | eleq1i 2692 |
. . . . . . . . . . . . 13
|
121 | 120 | a1i 11 |
. . . . . . . . . . . 12
|
122 | 121 | rabbiia 3185 |
. . . . . . . . . . 11
|
123 | 17, 115, 122 | 3eqtri 2648 |
. . . . . . . . . 10
|
124 | 119 | fveq2i 6194 |
. . . . . . . . . . . 12
|
125 | 124 | mpteq2i 4741 |
. . . . . . . . . . 11
|
126 | 4, 125 | eqtri 2644 |
. . . . . . . . . 10
|
127 | 3 | adantr 481 |
. . . . . . . . . 10
|
128 | 37 | adantl 482 |
. . . . . . . . . 10
|
129 | 88, 89, 90, 92, 9, 100, 123, 126, 127, 128 | fnlimabslt 39911 |
. . . . . . . . 9
|
130 | 29 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
131 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
|
132 | 130, 131 | resubcld 10458 |
. . . . . . . . . . . . . . . . 17
|
133 | 132 | adantrr 753 |
. . . . . . . . . . . . . . . 16
|
134 | 132 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
|
135 | 134 | abscld 14175 |
. . . . . . . . . . . . . . . . 17
|
136 | 135 | adantrr 753 |
. . . . . . . . . . . . . . . 16
|
137 | 32 | rehalfcld 11279 |
. . . . . . . . . . . . . . . . 17
|
138 | 137 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
|
139 | 133 | leabsd 14153 |
. . . . . . . . . . . . . . . 16
|
140 | 28 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . 21
|
141 | 140 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
142 | | recn 10026 |
. . . . . . . . . . . . . . . . . . . . 21
|
143 | 142 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
144 | 141, 143 | abssubd 14192 |
. . . . . . . . . . . . . . . . . . 19
|
145 | 144 | adantrr 753 |
. . . . . . . . . . . . . . . . . 18
|
146 | | simprr 796 |
. . . . . . . . . . . . . . . . . 18
|
147 | 145, 146 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . 17
|
148 | 147 | adantlr 751 |
. . . . . . . . . . . . . . . 16
|
149 | 133, 136,
138, 139, 148 | lelttrd 10195 |
. . . . . . . . . . . . . . 15
|
150 | 29 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
151 | | simprl 794 |
. . . . . . . . . . . . . . . 16
|
152 | 150, 151,
138 | ltsubadd2d 10625 |
. . . . . . . . . . . . . . 15
|
153 | 149, 152 | mpbid 222 |
. . . . . . . . . . . . . 14
|
154 | 153 | ex 450 |
. . . . . . . . . . . . 13
|
155 | 154 | ad2antrr 762 |
. . . . . . . . . . . 12
|
156 | 155 | ralimdva 2962 |
. . . . . . . . . . 11
|
157 | 156 | ex 450 |
. . . . . . . . . 10
|
158 | 36, 157 | reximdai 3012 |
. . . . . . . . 9
|
159 | 129, 158 | mpd 15 |
. . . . . . . 8
|
160 | 116 | dmeqd 5326 |
. . . . . . . . . 10
|
161 | 160 | eleq2d 2687 |
. . . . . . . . 9
|
162 | 117 | breq1d 4663 |
. . . . . . . . 9
|
163 | 161, 162 | anbi12d 747 |
. . . . . . . 8
|
164 | 117 | oveq1d 6665 |
. . . . . . . . 9
|
165 | 164 | breq2d 4665 |
. . . . . . . 8
|
166 | 36, 9, 87, 159, 163, 165 | rexanuz3 39275 |
. . . . . . 7
|
167 | | df-3an 1039 |
. . . . . . . . 9
|
168 | | 3ancomb 1047 |
. . . . . . . . 9
|
169 | 167, 168 | bitr3i 266 |
. . . . . . . 8
|
170 | 169 | rexbii 3041 |
. . . . . . 7
|
171 | 166, 170 | sylib 208 |
. . . . . 6
|
172 | 29 | ad2antrr 762 |
. . . . . . . . . 10
|
173 | 15 | 3adant3 1081 |
. . . . . . . . . . . . . . 15
|
174 | | simp3 1063 |
. . . . . . . . . . . . . . 15
|
175 | 173, 174 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
|
176 | 175 | ad4ant134 1296 |
. . . . . . . . . . . . 13
|
177 | | simpllr 799 |
. . . . . . . . . . . . . 14
|
178 | 177, 137 | syl 17 |
. . . . . . . . . . . . 13
|
179 | 176, 178 | readdcld 10069 |
. . . . . . . . . . . 12
|
180 | 179 | adantlllr 39199 |
. . . . . . . . . . 11
|
181 | 180 | 3ad2antr1 1226 |
. . . . . . . . . 10
|
182 | | rehalfcl 11258 |
. . . . . . . . . . . . . . 15
|
183 | 33, 182 | syl 17 |
. . . . . . . . . . . . . 14
|
184 | 31, 183 | jca 554 |
. . . . . . . . . . . . 13
|
185 | | readdcl 10019 |
. . . . . . . . . . . . 13
|
186 | 184, 185 | syl 17 |
. . . . . . . . . . . 12
|
187 | 186, 183 | readdcld 10069 |
. . . . . . . . . . 11
|
188 | 187 | ad5ant13 1301 |
. . . . . . . . . 10
|
189 | | simpr2 1068 |
. . . . . . . . . 10
|
190 | 176 | adantrr 753 |
. . . . . . . . . . . . 13
|
191 | 186 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
192 | 178 | adantrr 753 |
. . . . . . . . . . . . 13
|
193 | | simprr 796 |
. . . . . . . . . . . . 13
|
194 | 190, 191,
192, 193 | ltadd1dd 10638 |
. . . . . . . . . . . 12
|
195 | 194 | adantlllr 39199 |
. . . . . . . . . . 11
|
196 | 195 | 3adantr2 1221 |
. . . . . . . . . 10
|
197 | 172, 181,
188, 189, 196 | lttrd 10198 |
. . . . . . . . 9
|
198 | 31 | recnd 10068 |
. . . . . . . . . . . 12
|
199 | 183 | recnd 10068 |
. . . . . . . . . . . 12
|
200 | 198, 199,
199 | addassd 10062 |
. . . . . . . . . . 11
|
201 | 32 | recnd 10068 |
. . . . . . . . . . . . . 14
|
202 | | 2halves 11260 |
. . . . . . . . . . . . . 14
|
203 | 201, 202 | syl 17 |
. . . . . . . . . . . . 13
|
204 | 203 | oveq2d 6666 |
. . . . . . . . . . . 12
|
205 | 204 | adantl 482 |
. . . . . . . . . . 11
|
206 | 200, 205 | eqtrd 2656 |
. . . . . . . . . 10
|
207 | 206 | ad5ant13 1301 |
. . . . . . . . 9
|
208 | 197, 207 | breqtrd 4679 |
. . . . . . . 8
|
209 | 208 | exp31 630 |
. . . . . . 7
|
210 | 209 | rexlimdv 3030 |
. . . . . 6
|
211 | 171, 210 | mpd 15 |
. . . . 5
|
212 | 29, 35, 211 | ltled 10185 |
. . . 4
|
213 | 212 | ralrimiva 2966 |
. . 3
|
214 | | alrple 12037 |
. . . 4
|
215 | 28, 44, 214 | syl2anc 693 |
. . 3
|
216 | 213, 215 | mpbird 247 |
. 2
|
217 | 2, 216 | ssrabdv 3681 |
1
|