Step Hyp Ref
Expression
1 xrltso 11376
. . . 4
2 1 supex 7943
. . 3
3 2 a1i 11
. 2
4 limsupval.1
. . 3
5 4 a1i 11
. 2
6 4 limsupgval 13299
. . . 4
7 6 adantl 466
. . 3
8 simpl3 1001
. . . . . . 7
9 limsupgre.z
. . . . . . . . . . 11
10 uzssz 11129
. . . . . . . . . . 11
11 9 , 10 eqsstri 3533
. . . . . . . . . 10
12 zssre 10896
. . . . . . . . . 10
13 11 , 12 sstri 3512
. . . . . . . . 9
14 13 a1i 11
. . . . . . . 8
15 simpl2 1000
. . . . . . . . 9
16 ressxr 9658
. . . . . . . . 9
17 fss 5744
. . . . . . . . 9
18 15 , 16 , 17 sylancl 662
. . . . . . . 8
19 pnfxr 11350
. . . . . . . . 9
20 19 a1i 11
. . . . . . . 8
21 4 limsuplt 13302
. . . . . . . 8
22 14 , 18 , 20 , 21 syl3anc 1228
. . . . . . 7
23 8 , 22 mpbid 210
. . . . . 6
24 fzfi 12082
. . . . . . . 8
25 15 adantr 465
. . . . . . . . . 10
26 elfzuz 11713
. . . . . . . . . . 11
27 26 , 9 syl6eleqr 2556
. . . . . . . . . 10
28 ffvelrn 6029
. . . . . . . . . 10
29 25 , 27 , 28 syl2an 477
. . . . . . . . 9
30 29 ralrimiva 2871
. . . . . . . 8
31 fimaxre3 10517
. . . . . . . 8
32 24 , 30 , 31 sylancr 663
. . . . . . 7
33 simpr 461
. . . . . . . . . 10
34 33 ad2antrr 725
. . . . . . . . 9
35 4 limsupgf 13298
. . . . . . . . . 10
36 35 ffvelrni 6030
. . . . . . . . 9
37 34 , 36 syl 16
. . . . . . . 8
38 simprl 756
. . . . . . . . . 10
39 16 , 38 sseldi 3501
. . . . . . . . 9
40 simprl 756
. . . . . . . . . . 11
41 40 adantr 465
. . . . . . . . . 10
42 35 ffvelrni 6030
. . . . . . . . . 10
43 41 , 42 syl 16
. . . . . . . . 9
44 39 , 43 ifcld 3984
. . . . . . . 8
45 19 a1i 11
. . . . . . . 8
46 40 ad2antrr 725
. . . . . . . . . . . 12
47 13 a1i 11
. . . . . . . . . . . . 13
48 47 sselda 3503
. . . . . . . . . . . 12
49 xrleid 11385
. . . . . . . . . . . . . . . . 17
50 43 , 49 syl 16
. . . . . . . . . . . . . . . 16
51 18 ad2antrr 725
. . . . . . . . . . . . . . . . 17
52 4 limsupgle 13300
. . . . . . . . . . . . . . . . 17
53 47 , 51 , 41 , 43 , 52 syl211anc 1234
. . . . . . . . . . . . . . . 16
54 50 , 53 mpbid 210
. . . . . . . . . . . . . . 15
55 54 r19.21bi 2826
. . . . . . . . . . . . . 14
56 55 imp 429
. . . . . . . . . . . . 13
57 46 , 42 syl 16
. . . . . . . . . . . . . . . 16
58 39 adantr 465
. . . . . . . . . . . . . . . 16
59 xrmax1 11405
. . . . . . . . . . . . . . . 16
60 57 , 58 , 59 syl2anc 661
. . . . . . . . . . . . . . 15
61 51 ffvelrnda 6031
. . . . . . . . . . . . . . . 16
62 44 adantr 465
. . . . . . . . . . . . . . . 16
63 xrletr 11390
. . . . . . . . . . . . . . . 16
64 61 , 57 , 62 , 63 syl3anc 1228
. . . . . . . . . . . . . . 15
65 60 , 64 mpan2d 674
. . . . . . . . . . . . . 14
66 65 adantr 465
. . . . . . . . . . . . 13
67 56 , 66 mpd 15
. . . . . . . . . . . 12
68 simpr 461
. . . . . . . . . . . . . . . . . 18
69 68 , 9 syl6eleq 2555
. . . . . . . . . . . . . . . . 17
70 41 flcld 11935
. . . . . . . . . . . . . . . . . 18
71 70 adantr 465
. . . . . . . . . . . . . . . . 17
72 elfz5 11709
. . . . . . . . . . . . . . . . 17
73 69 , 71 , 72 syl2anc 661
. . . . . . . . . . . . . . . 16
74 11 , 68 sseldi 3501
. . . . . . . . . . . . . . . . 17
75 flge 11942
. . . . . . . . . . . . . . . . 17
76 46 , 74 , 75 syl2anc 661
. . . . . . . . . . . . . . . 16
77 73 , 76 bitr4d 256
. . . . . . . . . . . . . . 15
78 77 biimpar 485
. . . . . . . . . . . . . 14
79 simprr 757
. . . . . . . . . . . . . . 15
80 79 ad2antrr 725
. . . . . . . . . . . . . 14
81 fveq2 5871
. . . . . . . . . . . . . . . 16
82 81 breq1d 4462
. . . . . . . . . . . . . . 15
83 82 rspcv 3206
. . . . . . . . . . . . . 14
84 78 , 80 , 83 sylc 60
. . . . . . . . . . . . 13
85 xrmax2 11406
. . . . . . . . . . . . . . . . 17
86 43 , 39 , 85 syl2anc 661
. . . . . . . . . . . . . . . 16
87 86 adantr 465
. . . . . . . . . . . . . . 15
88 xrletr 11390
. . . . . . . . . . . . . . . 16
89 61 , 58 , 62 , 88 syl3anc 1228
. . . . . . . . . . . . . . 15
90 87 , 89 mpan2d 674
. . . . . . . . . . . . . 14
91 90 adantr 465
. . . . . . . . . . . . 13
92 84 , 91 mpd 15
. . . . . . . . . . . 12
93 46 , 48 , 67 , 92 lecasei 9711
. . . . . . . . . . 11
94 93 a1d 25
. . . . . . . . . 10
95 94 ralrimiva 2871
. . . . . . . . 9
96 4 limsupgle 13300
. . . . . . . . . 10
97 47 , 51 , 34 , 44 , 96 syl211anc 1234
. . . . . . . . 9
98 95 , 97 mpbird 232
. . . . . . . 8
99 ltpnf 11360
. . . . . . . . . 10
100 38 , 99 syl 16
. . . . . . . . 9
101 simplrr 762
. . . . . . . . 9
102 breq1 4455
. . . . . . . . . 10
103 breq1 4455
. . . . . . . . . 10
104 102 , 103 ifboth 3977
. . . . . . . . 9
105 100 , 101 ,
104 syl2anc 661
. . . . . . . 8
106 37 , 44 , 45 , 98 , 105 xrlelttrd 11392
. . . . . . 7
107 32 , 106 rexlimddv 2953
. . . . . 6
108 23 , 107 rexlimddv 2953
. . . . 5
109 7 , 108 eqbrtrrd 4474
. . . 4
110 imassrn 5353
. . . . . . . . 9
111 frn 5742
. . . . . . . . . 10
112 15 , 111 syl 16
. . . . . . . . 9
113 110 , 112 syl5ss 3514
. . . . . . . 8
114 113 , 16 syl6ss 3515
. . . . . . 7
115 df-ss 3489
. . . . . . 7
116 114 , 115 sylib 196
. . . . . 6
117 116 , 113 eqsstrd 3537
. . . . 5