Step | Hyp | Ref
| Expression |
1 | | liminfval2.2 |
. . 3
|
2 | | liminfval2.1 |
. . . . 5
inf
|
3 | | oveq1 6657 |
. . . . . . . . 9
|
4 | 3 | imaeq2d 5466 |
. . . . . . . 8
|
5 | 4 | ineq1d 3813 |
. . . . . . 7
|
6 | 5 | infeq1d 8383 |
. . . . . 6
inf
inf
|
7 | 6 | cbvmptv 4750 |
. . . . 5
inf
inf |
8 | 2, 7 | eqtri 2644 |
. . . 4
inf
|
9 | 8 | liminfval 39991 |
. . 3
liminf |
10 | 1, 9 | syl 17 |
. 2
liminf |
11 | | liminfval2.4 |
. . . . . . 7
|
12 | | liminfval2.3 |
. . . . . . . . 9
|
13 | 12 | ssrexr 39659 |
. . . . . . . 8
|
14 | | supxrunb1 12149 |
. . . . . . . 8
|
15 | 13, 14 | syl 17 |
. . . . . . 7
|
16 | 11, 15 | mpbird 247 |
. . . . . 6
|
17 | 8 | liminfgf 39990 |
. . . . . . . . . . 11
|
18 | 17 | ffvelrni 6358 |
. . . . . . . . . 10
|
19 | 18 | ad2antlr 763 |
. . . . . . . . 9
|
20 | | simpll 790 |
. . . . . . . . . 10
|
21 | | simprl 794 |
. . . . . . . . . 10
|
22 | 12 | sselda 3603 |
. . . . . . . . . . 11
|
23 | 17 | ffvelrni 6358 |
. . . . . . . . . . 11
|
24 | 22, 23 | syl 17 |
. . . . . . . . . 10
|
25 | 20, 21, 24 | syl2anc 693 |
. . . . . . . . 9
|
26 | | imassrn 5477 |
. . . . . . . . . . . 12
|
27 | | frn 6053 |
. . . . . . . . . . . . 13
|
28 | 17, 27 | ax-mp 5 |
. . . . . . . . . . . 12
|
29 | 26, 28 | sstri 3612 |
. . . . . . . . . . 11
|
30 | | supxrcl 12145 |
. . . . . . . . . . 11
|
31 | 29, 30 | ax-mp 5 |
. . . . . . . . . 10
|
32 | 31 | a1i 11 |
. . . . . . . . 9
|
33 | | simplr 792 |
. . . . . . . . . . 11
|
34 | 20, 21, 22 | syl2anc 693 |
. . . . . . . . . . 11
|
35 | | simprr 796 |
. . . . . . . . . . 11
|
36 | | liminfgord 39986 |
. . . . . . . . . . 11
inf
inf
|
37 | 33, 34, 35, 36 | syl3anc 1326 |
. . . . . . . . . 10
inf inf
|
38 | 8 | liminfgval 39994 |
. . . . . . . . . . . . 13
inf
|
39 | 38 | ad2antlr 763 |
. . . . . . . . . . . 12
inf
|
40 | 8 | liminfgval 39994 |
. . . . . . . . . . . . . 14
inf
|
41 | 22, 40 | syl 17 |
. . . . . . . . . . . . 13
inf
|
42 | 41 | adantlr 751 |
. . . . . . . . . . . 12
inf
|
43 | 39, 42 | breq12d 4666 |
. . . . . . . . . . 11
inf
inf
|
44 | 43 | adantrr 753 |
. . . . . . . . . 10
inf
inf |
45 | 37, 44 | mpbird 247 |
. . . . . . . . 9
|
46 | 29 | a1i 11 |
. . . . . . . . . . 11
|
47 | | nfv 1843 |
. . . . . . . . . . . . . 14
|
48 | | inss2 3834 |
. . . . . . . . . . . . . . . 16
|
49 | | infxrcl 12163 |
. . . . . . . . . . . . . . . 16
inf
|
50 | 48, 49 | ax-mp 5 |
. . . . . . . . . . . . . . 15
inf
|
51 | 50 | a1i 11 |
. . . . . . . . . . . . . 14
inf
|
52 | 47, 51, 8 | fnmptd 39434 |
. . . . . . . . . . . . 13
|
53 | 52 | adantr 481 |
. . . . . . . . . . . 12
|
54 | | simpr 477 |
. . . . . . . . . . . 12
|
55 | 53, 22, 54 | fnfvimad 39459 |
. . . . . . . . . . 11
|
56 | | supxrub 12154 |
. . . . . . . . . . 11
|
57 | 46, 55, 56 | syl2anc 693 |
. . . . . . . . . 10
|
58 | 20, 21, 57 | syl2anc 693 |
. . . . . . . . 9
|
59 | 19, 25, 32, 45, 58 | xrletrd 11993 |
. . . . . . . 8
|
60 | 59 | rexlimdvaa 3032 |
. . . . . . 7
|
61 | 60 | ralimdva 2962 |
. . . . . 6
|
62 | 16, 61 | mpd 15 |
. . . . 5
|
63 | | xrltso 11974 |
. . . . . . . . 9
|
64 | 63 | infex 8399 |
. . . . . . . 8
inf
|
65 | 64 | rgenw 2924 |
. . . . . . 7
inf |
66 | 8 | fnmpt 6020 |
. . . . . . 7
inf
|
67 | 65, 66 | ax-mp 5 |
. . . . . 6
|
68 | | breq1 4656 |
. . . . . . 7
|
69 | 68 | ralrn 6362 |
. . . . . 6
|
70 | 67, 69 | ax-mp 5 |
. . . . 5
|
71 | 62, 70 | sylibr 224 |
. . . 4
|
72 | | supxrleub 12156 |
. . . . 5
|
73 | 28, 31, 72 | mp2an 708 |
. . . 4
|
74 | 71, 73 | sylibr 224 |
. . 3
|
75 | 26 | a1i 11 |
. . . 4
|
76 | 28 | a1i 11 |
. . . 4
|
77 | | supxrss 12162 |
. . . 4
|
78 | 75, 76, 77 | syl2anc 693 |
. . 3
|
79 | | supxrcl 12145 |
. . . . 5
|
80 | 28, 79 | ax-mp 5 |
. . . 4
|
81 | | xrletri3 11985 |
. . . 4
|
82 | 80, 31, 81 | mp2an 708 |
. . 3
|
83 | 74, 78, 82 | sylanbrc 698 |
. 2
|
84 | 10, 83 | eqtrd 2656 |
1
liminf
|