Step Hyp Ref
Expression 1 climsup.3 . . . . . . . . . 10
2 frn 5742 . . . . . . . . . 10
3 1 , 2 syl 16 . . . . . . . . 9
4 ffn 5736 . . . . . . . . . . . 12
5 1 , 4 syl 16 . . . . . . . . . . 11
6 climsup.2 . . . . . . . . . . . . 13
7 uzid 11124 . . . . . . . . . . . . 13
8 6 , 7 syl 16 . . . . . . . . . . . 12
9 climsup.1 . . . . . . . . . . . 12
10 8 , 9 syl6eleqr 2556 . . . . . . . . . . 11
11 fnfvelrn 6028 . . . . . . . . . . 11
12 5 , 10 , 11 syl2anc 661 . . . . . . . . . 10
13 ne0i 3790 . . . . . . . . . 10
14 12 , 13 syl 16 . . . . . . . . 9
15 climsup.5 . . . . . . . . . 10
16 breq1 4455 . . . . . . . . . . . . 13
17 16 ralrn 6034 . . . . . . . . . . . 12
18 17 rexbidv 2968 . . . . . . . . . . 11
19 5 , 18 syl 16 . . . . . . . . . 10
20 15 , 19 mpbird 232 . . . . . . . . 9
21 3 , 14 , 20 3jca 1176 . . . . . . . 8
22 suprcl 10528 . . . . . . . 8
23 21 , 22 syl 16 . . . . . . 7
24 ltsubrp 11280 . . . . . . 7
25 23 , 24 sylan 471 . . . . . 6
26 21 adantr 465 . . . . . . 7
27 rpre 11255 . . . . . . . 8
28 resubcl 9906 . . . . . . . 8
29 23 , 27 , 28 syl2an 477 . . . . . . 7
30 suprlub 10530 . . . . . . 7
31 26 , 29 , 30 syl2anc 661 . . . . . 6
32 25 , 31 mpbid 210 . . . . 5
33 breq2 4456 . . . . . . . 8
34 33 rexrn 6033 . . . . . . 7
35 5 , 34 syl 16 . . . . . 6
36 35 biimpa 484 . . . . 5
37 32 , 36 syldan 470 . . . 4
38 ffvelrn 6029 . . . . . . . . . . . 12
39 1 , 38 sylan 471 . . . . . . . . . . 11
40 39 ad2ant2r 746 . . . . . . . . . 10
41 1 adantr 465 . . . . . . . . . . 11
42 9 uztrn2 11127 . . . . . . . . . . 11
43 ffvelrn 6029 . . . . . . . . . . 11
44 41 , 42 , 43 syl2an 477 . . . . . . . . . 10
45 23 ad2antrr 725 . . . . . . . . . 10
46 simprr 757 . . . . . . . . . . 11
47 fzssuz 11753 . . . . . . . . . . . . . 14
48 uzss 11130 . . . . . . . . . . . . . . . . 17
49 48 , 9 syl6sseqr 3550 . . . . . . . . . . . . . . . 16
50 49 , 9 eleq2s 2565 . . . . . . . . . . . . . . 15
51 50 ad2antrl 727 . . . . . . . . . . . . . 14
52 47 , 51 syl5ss 3514 . . . . . . . . . . . . 13
53 ffvelrn 6029 . . . . . . . . . . . . . . . 16
54 53 ralrimiva 2871 . . . . . . . . . . . . . . 15
55 1 , 54 syl 16 . . . . . . . . . . . . . 14
56 55 ad2antrr 725 . . . . . . . . . . . . 13
57 ssralv 3563 . . . . . . . . . . . . 13
58 52 , 56 , 57 sylc 60 . . . . . . . . . . . 12
59 58 r19.21bi 2826 . . . . . . . . . . 11
60 fzssuz 11753 . . . . . . . . . . . . . 14
61 60 , 51 syl5ss 3514 . . . . . . . . . . . . 13
62 61 sselda 3503 . . . . . . . . . . . 12
63 climsup.4 . . . . . . . . . . . . . . 15
64 63 ralrimiva 2871 . . . . . . . . . . . . . 14
65 64 ad2antrr 725 . . . . . . . . . . . . 13
66 fveq2 5871 . . . . . . . . . . . . . . 15
67 oveq1 6303 . . . . . . . . . . . . . . . 16
68 67 fveq2d 5875 . . . . . . . . . . . . . . 15
69 66 , 68 breq12d 4465 . . . . . . . . . . . . . 14
70 69 rspccva 3209 . . . . . . . . . . . . 13
71 65 , 70 sylan 471 . . . . . . . . . . . 12
72 62 , 71 syldan 470 . . . . . . . . . . 11
73 46 , 59 , 72 monoord 12137 . . . . . . . . . 10
74 40 , 44 , 45 , 73 lesub2dd 10194 . . . . . . . . 9
75 45 , 44 resubcld 10012 . . . . . . . . . 10
76 45 , 40 resubcld 10012 . . . . . . . . . 10
77 27 ad2antlr 726 . . . . . . . . . 10
78 lelttr 9696 . . . . . . . . . 10
79 75 , 76 , 77 , 78 syl3anc 1228 . . . . . . . . 9
80 74 , 79 mpand 675 . . . . . . . 8
81 ltsub23 10057 . . . . . . . . 9
82 45 , 77 , 40 , 81 syl3anc 1228 . . . . . . . 8
83 21 ad2antrr 725 . . . . . . . . . . 11
84 5 adantr 465 . . . . . . . . . . . 12
85 fnfvelrn 6028 . . . . . . . . . . . 12
86 84 , 42 , 85 syl2an 477 . . . . . . . . . . 11
87 suprub 10529 . . . . . . . . . . 11
88 83 , 86 , 87 syl2anc 661 . . . . . . . . . 10
89 44 , 45 , 88 abssuble0d 13264 . . . . . . . . 9
90 89 breq1d 4462 . . . . . . . 8
91 80 , 82 , 90 3imtr4d 268 . . . . . . 7
92 91 anassrs 648 . . . . . 6
93 92 ralrimdva 2875 . . . . 5
94 93 reximdva 2932 . . . 4
95 37 , 94 mpd 15 . . 3
96 95 ralrimiva 2871 . 2
97 fvex 5881 . . . . 5
98 9 , 97 eqeltri 2541 . . . 4
99 fex 6145 . . . 4
100 1 , 98 , 99 sylancl 662 . . 3
101 eqidd 2458 . . 3
102 23 recnd 9643 . . 3
103 1 , 43 sylan 471 . . . 4
104 103 recnd 9643 . . 3
105 9 , 6 , 100 , 101 , 102 , 104 clim2c 13328 . 2
106 96 , 105 mpbird 232 1
