Step | Hyp | Ref
| Expression |
1 | | xrltso 11974 |
. . . 4
|
2 | 1 | supex 8369 |
. . 3
|
3 | 2 | a1i 11 |
. 2
|
4 | | limsupval.1 |
. . 3
|
5 | 4 | a1i 11 |
. 2
|
6 | 4 | limsupgval 14207 |
. . . 4
|
7 | 6 | adantl 482 |
. . 3
|
8 | | simpl3 1066 |
. . . . . . 7
|
9 | | limsupgre.z |
. . . . . . . . . . 11
|
10 | | uzssz 11707 |
. . . . . . . . . . 11
|
11 | 9, 10 | eqsstri 3635 |
. . . . . . . . . 10
|
12 | | zssre 11384 |
. . . . . . . . . 10
|
13 | 11, 12 | sstri 3612 |
. . . . . . . . 9
|
14 | 13 | a1i 11 |
. . . . . . . 8
|
15 | | simpl2 1065 |
. . . . . . . . 9
|
16 | | ressxr 10083 |
. . . . . . . . 9
|
17 | | fss 6056 |
. . . . . . . . 9
|
18 | 15, 16, 17 | sylancl 694 |
. . . . . . . 8
|
19 | | pnfxr 10092 |
. . . . . . . . 9
|
20 | 19 | a1i 11 |
. . . . . . . 8
|
21 | 4 | limsuplt 14210 |
. . . . . . . 8
|
22 | 14, 18, 20, 21 | syl3anc 1326 |
. . . . . . 7
|
23 | 8, 22 | mpbid 222 |
. . . . . 6
|
24 | | fzfi 12771 |
. . . . . . . 8
|
25 | 15 | adantr 481 |
. . . . . . . . . 10
|
26 | | elfzuz 12338 |
. . . . . . . . . . 11
|
27 | 26, 9 | syl6eleqr 2712 |
. . . . . . . . . 10
|
28 | | ffvelrn 6357 |
. . . . . . . . . 10
|
29 | 25, 27, 28 | syl2an 494 |
. . . . . . . . 9
|
30 | 29 | ralrimiva 2966 |
. . . . . . . 8
|
31 | | fimaxre3 10970 |
. . . . . . . 8
|
32 | 24, 30, 31 | sylancr 695 |
. . . . . . 7
|
33 | | simpr 477 |
. . . . . . . . . 10
|
34 | 33 | ad2antrr 762 |
. . . . . . . . 9
|
35 | 4 | limsupgf 14206 |
. . . . . . . . . 10
|
36 | 35 | ffvelrni 6358 |
. . . . . . . . 9
|
37 | 34, 36 | syl 17 |
. . . . . . . 8
|
38 | | simprl 794 |
. . . . . . . . . 10
|
39 | 16, 38 | sseldi 3601 |
. . . . . . . . 9
|
40 | | simprl 794 |
. . . . . . . . . . 11
|
41 | 40 | adantr 481 |
. . . . . . . . . 10
|
42 | 35 | ffvelrni 6358 |
. . . . . . . . . 10
|
43 | 41, 42 | syl 17 |
. . . . . . . . 9
|
44 | 39, 43 | ifcld 4131 |
. . . . . . . 8
|
45 | 19 | a1i 11 |
. . . . . . . 8
|
46 | 40 | ad2antrr 762 |
. . . . . . . . . . . 12
|
47 | 13 | a1i 11 |
. . . . . . . . . . . . 13
|
48 | 47 | sselda 3603 |
. . . . . . . . . . . 12
|
49 | | xrleid 11983 |
. . . . . . . . . . . . . . . . 17
|
50 | 43, 49 | syl 17 |
. . . . . . . . . . . . . . . 16
|
51 | 18 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
52 | 4 | limsupgle 14208 |
. . . . . . . . . . . . . . . . 17
|
53 | 47, 51, 41, 43, 52 | syl211anc 1332 |
. . . . . . . . . . . . . . . 16
|
54 | 50, 53 | mpbid 222 |
. . . . . . . . . . . . . . 15
|
55 | 54 | r19.21bi 2932 |
. . . . . . . . . . . . . 14
|
56 | 55 | imp 445 |
. . . . . . . . . . . . 13
|
57 | 46, 42 | syl 17 |
. . . . . . . . . . . . . . . 16
|
58 | 39 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
59 | | xrmax1 12006 |
. . . . . . . . . . . . . . . 16
|
60 | 57, 58, 59 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
61 | 51 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . 16
|
62 | 44 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
63 | | xrletr 11989 |
. . . . . . . . . . . . . . . 16
|
64 | 61, 57, 62, 63 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
|
65 | 60, 64 | mpan2d 710 |
. . . . . . . . . . . . . 14
|
66 | 65 | adantr 481 |
. . . . . . . . . . . . 13
|
67 | 56, 66 | mpd 15 |
. . . . . . . . . . . 12
|
68 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
|
69 | 68, 9 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . 17
|
70 | 41 | flcld 12599 |
. . . . . . . . . . . . . . . . . 18
|
71 | 70 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
72 | | elfz5 12334 |
. . . . . . . . . . . . . . . . 17
|
73 | 69, 71, 72 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
74 | 11, 68 | sseldi 3601 |
. . . . . . . . . . . . . . . . 17
|
75 | | flge 12606 |
. . . . . . . . . . . . . . . . 17
|
76 | 46, 74, 75 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
77 | 73, 76 | bitr4d 271 |
. . . . . . . . . . . . . . 15
|
78 | 77 | biimpar 502 |
. . . . . . . . . . . . . 14
|
79 | | simprr 796 |
. . . . . . . . . . . . . . 15
|
80 | 79 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
81 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
82 | 81 | breq1d 4663 |
. . . . . . . . . . . . . . 15
|
83 | 82 | rspcv 3305 |
. . . . . . . . . . . . . 14
|
84 | 78, 80, 83 | sylc 65 |
. . . . . . . . . . . . 13
|
85 | | xrmax2 12007 |
. . . . . . . . . . . . . . . . 17
|
86 | 43, 39, 85 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
87 | 86 | adantr 481 |
. . . . . . . . . . . . . . 15
|
88 | | xrletr 11989 |
. . . . . . . . . . . . . . . 16
|
89 | 61, 58, 62, 88 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
|
90 | 87, 89 | mpan2d 710 |
. . . . . . . . . . . . . 14
|
91 | 90 | adantr 481 |
. . . . . . . . . . . . 13
|
92 | 84, 91 | mpd 15 |
. . . . . . . . . . . 12
|
93 | 46, 48, 67, 92 | lecasei 10143 |
. . . . . . . . . . 11
|
94 | 93 | a1d 25 |
. . . . . . . . . 10
|
95 | 94 | ralrimiva 2966 |
. . . . . . . . 9
|
96 | 4 | limsupgle 14208 |
. . . . . . . . . 10
|
97 | 47, 51, 34, 44, 96 | syl211anc 1332 |
. . . . . . . . 9
|
98 | 95, 97 | mpbird 247 |
. . . . . . . 8
|
99 | 38 | ltpnfd 11955 |
. . . . . . . . 9
|
100 | | simplrr 801 |
. . . . . . . . 9
|
101 | | breq1 4656 |
. . . . . . . . . 10
|
102 | | breq1 4656 |
. . . . . . . . . 10
|
103 | 101, 102 | ifboth 4124 |
. . . . . . . . 9
|
104 | 99, 100, 103 | syl2anc 693 |
. . . . . . . 8
|
105 | 37, 44, 45, 98, 104 | xrlelttrd 11991 |
. . . . . . 7
|
106 | 32, 105 | rexlimddv 3035 |
. . . . . 6
|
107 | 23, 106 | rexlimddv 3035 |
. . . . 5
|
108 | 7, 107 | eqbrtrrd 4677 |
. . . 4
|
109 | | imassrn 5477 |
. . . . . . . . 9
|
110 | | frn 6053 |
. . . . . . . . . 10
|
111 | 15, 110 | syl 17 |
. . . . . . . . 9
|
112 | 109, 111 | syl5ss 3614 |
. . . . . . . 8
|
113 | 112, 16 | syl6ss 3615 |
. . . . . . 7
|
114 | | df-ss 3588 |
. . . . . . 7
|
115 | 113, 114 | sylib 208 |
. . . . . 6
|
116 | 115, 112 | eqsstrd 3639 |
. . . . 5
|
117 | | simpl1 1064 |
. . . . . . . . . . 11
|
118 | | flcl 12596 |
. . . . . . . . . . . . . 14
|
119 | 118 | adantl 482 |
. . . . . . . . . . . . 13
|
120 | 119 | peano2zd 11485 |
. . . . . . . . . . . 12
|
121 | 120, 117 | ifcld 4131 |
. . . . . . . . . . 11
|
122 | 117 | zred 11482 |
. . . . . . . . . . . 12
|
123 | 120 | zred 11482 |
. . . . . . . . . . . 12
|
124 | | max1 12016 |
. . . . . . . . . . . 12
|
125 | 122, 123,
124 | syl2anc 693 |
. . . . . . . . . . 11
|
126 | | eluz2 11693 |
. . . . . . . . . . 11
|
127 | 117, 121,
125, 126 | syl3anbrc 1246 |
. . . . . . . . . 10
|
128 | 127, 9 | syl6eleqr 2712 |
. . . . . . . . 9
|
129 | | fdm 6051 |
. . . . . . . . . 10
|
130 | 15, 129 | syl 17 |
. . . . . . . . 9
|
131 | 128, 130 | eleqtrrd 2704 |
. . . . . . . 8
|
132 | 121 | zred 11482 |
. . . . . . . . 9
|
133 | | fllep1 12602 |
. . . . . . . . . . 11
|
134 | 133 | adantl 482 |
. . . . . . . . . 10
|
135 | | max2 12018 |
. . . . . . . . . . 11
|
136 | 122, 123,
135 | syl2anc 693 |
. . . . . . . . . 10
|
137 | 33, 123, 132, 134, 136 | letrd 10194 |
. . . . . . . . 9
|
138 | | elicopnf 12269 |
. . . . . . . . . 10
|
139 | 138 | adantl 482 |
. . . . . . . . 9
|
140 | 132, 137,
139 | mpbir2and 957 |
. . . . . . . 8
|
141 | | inelcm 4032 |
. . . . . . . 8
|
142 | 131, 140,
141 | syl2anc 693 |
. . . . . . 7
|
143 | | imadisj 5484 |
. . . . . . . 8
|
144 | 143 | necon3bii 2846 |
. . . . . . 7
|
145 | 142, 144 | sylibr 224 |
. . . . . 6
|
146 | 115, 145 | eqnetrd 2861 |
. . . . 5
|
147 | | supxrre1 12160 |
. . . . 5
|
148 | 116, 146,
147 | syl2anc 693 |
. . . 4
|
149 | 108, 148 | mpbird 247 |
. . 3
|
150 | 7, 149 | eqeltrd 2701 |
. 2
|
151 | 3, 5, 150 | fmpt2d 6393 |
1
|