Step Hyp Ref
Expression 1 limsupbnd2.5 . . 3
2 limsupbnd2.4 . . . . . . . . 9
3 limsupbnd.1 . . . . . . . . . . 11
4 ressxr 9658 . . . . . . . . . . 11
5 3 , 4 syl6ss 3515 . . . . . . . . . 10
6 supxrunb1 11540 . . . . . . . . . 10
7 5 , 6 syl 16 . . . . . . . . 9
8 2 , 7 mpbird 232 . . . . . . . 8
9 ifcl 3983 . . . . . . . 8
10 breq1 4455 . . . . . . . . . 10
11 10 rexbidv 2968 . . . . . . . . 9
12 11 rspccva 3209 . . . . . . . 8
13 8 , 9 , 12 syl2an 477 . . . . . . 7
14 r19.29 2992 . . . . . . . 8
15 simplrr 762 . . . . . . . . . . . . . . 15
16 simprl 756 . . . . . . . . . . . . . . . 16
17 16 adantr 465 . . . . . . . . . . . . . . 15
18 max1 11415 . . . . . . . . . . . . . . 15
19 15 , 17 , 18 syl2anc 661 . . . . . . . . . . . . . 14
20 17 , 15 , 9 syl2anc 661 . . . . . . . . . . . . . . 15
21 3 adantr 465 . . . . . . . . . . . . . . . 16
22 21 sselda 3503 . . . . . . . . . . . . . . 15
23 letr 9699 . . . . . . . . . . . . . . 15
24 15 , 20 , 22 , 23 syl3anc 1228 . . . . . . . . . . . . . 14
25 19 , 24 mpand 675 . . . . . . . . . . . . 13
26 25 imim1d 75 . . . . . . . . . . . 12
27 26 impd 431 . . . . . . . . . . 11
28 max2 11417 . . . . . . . . . . . . . . 15
29 15 , 17 , 28 syl2anc 661 . . . . . . . . . . . . . 14
30 letr 9699 . . . . . . . . . . . . . . 15
31 17 , 20 , 22 , 30 syl3anc 1228 . . . . . . . . . . . . . 14
32 29 , 31 mpand 675 . . . . . . . . . . . . 13
33 32 adantld 467 . . . . . . . . . . . 12
34 eqid 2457 . . . . . . . . . . . . . . . . . . 19
35 34 limsupgf 13298 . . . . . . . . . . . . . . . . . 18
36 35 ffvelrni 6030 . . . . . . . . . . . . . . . . 17
37 36 adantl 466 . . . . . . . . . . . . . . . 16
38 xrleid 11385 . . . . . . . . . . . . . . . 16
39 37 , 38 syl 16 . . . . . . . . . . . . . . 15
40 39 adantrr 716 . . . . . . . . . . . . . 14
41 limsupbnd.2 . . . . . . . . . . . . . . . 16
42 41 adantr 465 . . . . . . . . . . . . . . 15
43 16 , 36 syl 16 . . . . . . . . . . . . . . 15
44 34 limsupgle 13300 . . . . . . . . . . . . . . 15
45 21 , 42 , 16 , 43 , 44 syl211anc 1234 . . . . . . . . . . . . . 14
46 40 , 45 mpbid 210 . . . . . . . . . . . . 13
47 46 r19.21bi 2826 . . . . . . . . . . . 12
48 33 , 47 syld 44 . . . . . . . . . . 11
49 27 , 48 jcad 533 . . . . . . . . . 10
50 limsupbnd.3 . . . . . . . . . . . 12
51 50 ad2antrr 725 . . . . . . . . . . 11
52 42 ffvelrnda 6031 . . . . . . . . . . 11
53 43 adantr 465 . . . . . . . . . . 11
54 xrletr 11390 . . . . . . . . . . 11
55 51 , 52 , 53 , 54 syl3anc 1228 . . . . . . . . . 10
56 49 , 55 syld 44 . . . . . . . . 9
57 56 rexlimdva 2949 . . . . . . . 8
58 14 , 57 syl5 32 . . . . . . 7
59 13 , 58 mpan2d 674 . . . . . 6
60 59 anassrs 648 . . . . 5
61 60 rexlimdva 2949 . . . 4
62 61 ralrimdva 2875 . . 3
63 1 , 62 mpd 15 . 2
64 34 limsuple 13301 . . 3
65 3 , 41 , 50 , 64 syl3anc 1228 . 2
66 63 , 65 mpbird 232 1
