Step | Hyp | Ref
| Expression |
1 | | rlimcl 14234 |
. . . 4
|
2 | 1 | a1i 11 |
. . 3
|
3 | | rlimcl 14234 |
. . . 4
|
4 | 3 | a1i 11 |
. . 3
|
5 | | rlimresb.2 |
. . . . . . . . . . . . . . . . . . 19
|
6 | 5 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
7 | | simprrl 804 |
. . . . . . . . . . . . . . . . . 18
|
8 | 6, 7 | sseldd 3604 |
. . . . . . . . . . . . . . . . 17
|
9 | | rlimresb.3 |
. . . . . . . . . . . . . . . . . . 19
|
10 | 9 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
11 | | elicopnf 12269 |
. . . . . . . . . . . . . . . . . . . . . 22
|
12 | 9, 11 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
13 | 12 | biimpa 501 |
. . . . . . . . . . . . . . . . . . . 20
|
14 | 13 | adantrr 753 |
. . . . . . . . . . . . . . . . . . 19
|
15 | 14 | simpld 475 |
. . . . . . . . . . . . . . . . . 18
|
16 | 14 | simprd 479 |
. . . . . . . . . . . . . . . . . 18
|
17 | | simprrr 805 |
. . . . . . . . . . . . . . . . . 18
|
18 | 10, 15, 8, 16, 17 | letrd 10194 |
. . . . . . . . . . . . . . . . 17
|
19 | | elicopnf 12269 |
. . . . . . . . . . . . . . . . . 18
|
20 | 10, 19 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
21 | 8, 18, 20 | mpbir2and 957 |
. . . . . . . . . . . . . . . 16
|
22 | 21 | anassrs 680 |
. . . . . . . . . . . . . . 15
|
23 | 22 | anassrs 680 |
. . . . . . . . . . . . . 14
|
24 | | biimt 350 |
. . . . . . . . . . . . . 14
|
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . 13
|
26 | 25 | pm5.74da 723 |
. . . . . . . . . . . 12
|
27 | | bi2.04 376 |
. . . . . . . . . . . 12
|
28 | 26, 27 | syl6bb 276 |
. . . . . . . . . . 11
|
29 | 28 | pm5.74da 723 |
. . . . . . . . . 10
|
30 | | elin 3796 |
. . . . . . . . . . . 12
|
31 | 30 | imbi1i 339 |
. . . . . . . . . . 11
|
32 | | impexp 462 |
. . . . . . . . . . 11
|
33 | 31, 32 | bitri 264 |
. . . . . . . . . 10
|
34 | 29, 33 | syl6bbr 278 |
. . . . . . . . 9
|
35 | 34 | ralbidv2 2984 |
. . . . . . . 8
|
36 | 35 | rexbidva 3049 |
. . . . . . 7
|
37 | 36 | ralbidv 2986 |
. . . . . 6
|
38 | 37 | adantr 481 |
. . . . 5
|
39 | | rlimresb.1 |
. . . . . . . . 9
|
40 | 39 | ffvelrnda 6359 |
. . . . . . . 8
|
41 | 40 | ralrimiva 2966 |
. . . . . . 7
|
42 | 41 | adantr 481 |
. . . . . 6
|
43 | 5 | adantr 481 |
. . . . . 6
|
44 | | simpr 477 |
. . . . . 6
|
45 | 9 | adantr 481 |
. . . . . 6
|
46 | 42, 43, 44, 45 | rlim3 14229 |
. . . . 5
|
47 | | inss1 3833 |
. . . . . . . . . 10
|
48 | 47 | sseli 3599 |
. . . . . . . . 9
|
49 | 48, 40 | sylan2 491 |
. . . . . . . 8
|
50 | 49 | ralrimiva 2966 |
. . . . . . 7
|
51 | 50 | adantr 481 |
. . . . . 6
|
52 | 47, 5 | syl5ss 3614 |
. . . . . . 7
|
53 | 52 | adantr 481 |
. . . . . 6
|
54 | 51, 53, 44, 45 | rlim3 14229 |
. . . . 5
|
55 | 38, 46, 54 | 3bitr4d 300 |
. . . 4
|
56 | 55 | ex 450 |
. . 3
|
57 | 2, 4, 56 | pm5.21ndd 369 |
. 2
|
58 | 39 | feqmptd 6249 |
. . 3
|
59 | 58 | breq1d 4663 |
. 2
|
60 | | resres 5409 |
. . . 4
|
61 | | ffn 6045 |
. . . . . 6
|
62 | | fnresdm 6000 |
. . . . . 6
|
63 | 39, 61, 62 | 3syl 18 |
. . . . 5
|
64 | 63 | reseq1d 5395 |
. . . 4
|
65 | 58 | reseq1d 5395 |
. . . . 5
|
66 | | resmpt 5449 |
. . . . . 6
|
67 | 47, 66 | ax-mp 5 |
. . . . 5
|
68 | 65, 67 | syl6eq 2672 |
. . . 4
|
69 | 60, 64, 68 | 3eqtr3a 2680 |
. . 3
|
70 | 69 | breq1d 4663 |
. 2
|
71 | 57, 59, 70 | 3bitr4d 300 |
1
|