Step Hyp Ref
Expression 1 climrlim2.5 . 2
2 eluzelz 11119 . . . . . . . . . . . . . . . 16
3 climrlim2.1 . . . . . . . . . . . . . . . 16
4 2 , 3 eleq2s 2565 . . . . . . . . . . . . . . 15
5 4 ad2antlr 726 . . . . . . . . . . . . . 14
6 climrlim2.3 . . . . . . . . . . . . . . . . . 18
7 6 sselda 3503 . . . . . . . . . . . . . . . . 17
8 7 flcld 11935 . . . . . . . . . . . . . . . 16
9 8 adantlr 714 . . . . . . . . . . . . . . 15
10 9 ad2ant2r 746 . . . . . . . . . . . . . 14
11 simprr 757 . . . . . . . . . . . . . . 15
12 7 adantlr 714 . . . . . . . . . . . . . . . . 17
13 12 ad2ant2r 746 . . . . . . . . . . . . . . . 16
14 flge 11942 . . . . . . . . . . . . . . . 16
15 13 , 5 , 14 syl2anc 661 . . . . . . . . . . . . . . 15
16 11 , 15 mpbid 210 . . . . . . . . . . . . . 14
17 eluz2 11116 . . . . . . . . . . . . . 14
18 5 , 10 , 16 , 17 syl3anbrc 1180 . . . . . . . . . . . . 13
19 simpr 461 . . . . . . . . . . . . . 14
20 19 ralimi 2850 . . . . . . . . . . . . 13
21 fveq2 5871 . . . . . . . . . . . . . . . . 17
22 21 oveq1d 6311 . . . . . . . . . . . . . . . 16
23 22 fveq2d 5875 . . . . . . . . . . . . . . 15
24 23 breq1d 4462 . . . . . . . . . . . . . 14
25 24 rspcv 3206 . . . . . . . . . . . . 13
26 18 , 20 , 25 syl2im 38 . . . . . . . . . . . 12
27 climrlim2.4 . . . . . . . . . . . . . . . . . . . . 21
28 27 adantr 465 . . . . . . . . . . . . . . . . . . . 20
29 climrlim2.7 . . . . . . . . . . . . . . . . . . . . 21
30 flge 11942 . . . . . . . . . . . . . . . . . . . . . 22
31 7 , 28 , 30 syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21
32 29 , 31 mpbid 210 . . . . . . . . . . . . . . . . . . . 20
33 eluz2 11116 . . . . . . . . . . . . . . . . . . . 20
34 28 , 8 , 32 , 33 syl3anbrc 1180 . . . . . . . . . . . . . . . . . . 19
35 34 , 3 syl6eleqr 2556 . . . . . . . . . . . . . . . . . 18
36 climrlim2.6 . . . . . . . . . . . . . . . . . . . . 21
37 36 ralrimiva 2871 . . . . . . . . . . . . . . . . . . . 20
38 37 adantr 465 . . . . . . . . . . . . . . . . . . 19
39 climrlim2.2 . . . . . . . . . . . . . . . . . . . . 21
40 39 eleq1d 2526 . . . . . . . . . . . . . . . . . . . 20
41 40 rspcv 3206 . . . . . . . . . . . . . . . . . . 19
42 35 , 38 , 41 sylc 60 . . . . . . . . . . . . . . . . . 18
43 eqid 2457 . . . . . . . . . . . . . . . . . . 19
44 39 , 43 fvmptg 5954 . . . . . . . . . . . . . . . . . 18
45 35 , 42 , 44 syl2anc 661 . . . . . . . . . . . . . . . . 17
46 45 adantlr 714 . . . . . . . . . . . . . . . 16
47 46 ad2ant2r 746 . . . . . . . . . . . . . . 15
48 47 oveq1d 6311 . . . . . . . . . . . . . 14
49 48 fveq2d 5875 . . . . . . . . . . . . 13
50 49 breq1d 4462 . . . . . . . . . . . 12
51 26 , 50 sylibd 214 . . . . . . . . . . 11
52 51 expr 615 . . . . . . . . . 10
53 52 com23 78 . . . . . . . . 9
54 53 ralrimdva 2875 . . . . . . . 8
55 eluzelre 11120 . . . . . . . . . 10
56 55 , 3 eleq2s 2565 . . . . . . . . 9
57 56 adantl 466 . . . . . . . 8
58 54 , 57 jctild 543 . . . . . . 7
59 58 expimpd 603 . . . . . 6
60 59 reximdv2 2928 . . . . 5
61 60 ralimdva 2865 . . . 4
62 61 adantld 467 . . 3
63 climrel 13315 . . . . . 6
64 63 brrelexi 5045 . . . . 5
65 1 , 64 syl 16 . . . 4
66 eqidd 2458 . . . 4
67 3 , 27 , 65 , 66 clim2 13327 . . 3
68 42 ralrimiva 2871 . . . 4
69 climcl 13322 . . . . 5
70 1 , 69 syl 16 . . . 4
71 68 , 6 , 70 rlim2 13319 . . 3
72 62 , 67 , 71 3imtr4d 268 . 2
73 1 , 72 mpd 15 1
