This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cxploglim2

Description: Every power of the logarithm grows slower than any positive power. (Contributed by Mario Carneiro, 20-May-2016)

Ref Expression
Assertion cxploglim2 
|- ( ( A e. CC /\ B e. RR+ ) -> ( n e. RR+ |-> ( ( ( log ` n ) ^c A ) / ( n ^c B ) ) ) ~~>r 0 )

Proof

Step Hyp Ref Expression
1 3re 
 |-  3 e. RR
2 1 a1i 
 |-  ( ( A e. CC /\ B e. RR+ ) -> 3 e. RR )
3 0red 
 |-  ( ( A e. CC /\ B e. RR+ ) -> 0 e. RR )
4 3 recnd 
 |-  ( ( A e. CC /\ B e. RR+ ) -> 0 e. CC )
5 ovexd 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ n e. RR+ ) -> ( ( log ` n ) / ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) ) e. _V )
6 simpr 
 |-  ( ( A e. CC /\ B e. RR+ ) -> B e. RR+ )
7 recl 
 |-  ( A e. CC -> ( Re ` A ) e. RR )
8 7 adantr 
 |-  ( ( A e. CC /\ B e. RR+ ) -> ( Re ` A ) e. RR )
9 1re 
 |-  1 e. RR
10 ifcl 
 |-  ( ( ( Re ` A ) e. RR /\ 1 e. RR ) -> if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) e. RR )
11 8 9 10 sylancl 
 |-  ( ( A e. CC /\ B e. RR+ ) -> if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) e. RR )
12 9 a1i 
 |-  ( ( A e. CC /\ B e. RR+ ) -> 1 e. RR )
13 0lt1 
 |-  0 < 1
14 13 a1i 
 |-  ( ( A e. CC /\ B e. RR+ ) -> 0 < 1 )
15 max1 
 |-  ( ( 1 e. RR /\ ( Re ` A ) e. RR ) -> 1 <_ if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) )
16 9 8 15 sylancr 
 |-  ( ( A e. CC /\ B e. RR+ ) -> 1 <_ if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) )
17 3 12 11 14 16 ltletrd 
 |-  ( ( A e. CC /\ B e. RR+ ) -> 0 < if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) )
18 11 17 elrpd 
 |-  ( ( A e. CC /\ B e. RR+ ) -> if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) e. RR+ )
19 6 18 rpdivcld 
 |-  ( ( A e. CC /\ B e. RR+ ) -> ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) e. RR+ )
20 cxploglim 
 |-  ( ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) e. RR+ -> ( n e. RR+ |-> ( ( log ` n ) / ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) ) ) ~~>r 0 )
21 19 20 syl 
 |-  ( ( A e. CC /\ B e. RR+ ) -> ( n e. RR+ |-> ( ( log ` n ) / ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) ) ) ~~>r 0 )
22 5 21 18 rlimcxp 
 |-  ( ( A e. CC /\ B e. RR+ ) -> ( n e. RR+ |-> ( ( ( log ` n ) / ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) ~~>r 0 )
23 5 21 rlimmptrcl 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ n e. RR+ ) -> ( ( log ` n ) / ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) ) e. CC )
24 11 adantr 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ n e. RR+ ) -> if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) e. RR )
25 24 recnd 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ n e. RR+ ) -> if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) e. CC )
26 23 25 cxpcld 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ n e. RR+ ) -> ( ( ( log ` n ) / ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) e. CC )
27 relogcl 
 |-  ( n e. RR+ -> ( log ` n ) e. RR )
28 27 adantl 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ n e. RR+ ) -> ( log ` n ) e. RR )
29 28 recnd 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ n e. RR+ ) -> ( log ` n ) e. CC )
30 simpll 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ n e. RR+ ) -> A e. CC )
31 29 30 cxpcld 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ n e. RR+ ) -> ( ( log ` n ) ^c A ) e. CC )
32 simpr 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ n e. RR+ ) -> n e. RR+ )
33 rpre 
 |-  ( B e. RR+ -> B e. RR )
34 33 ad2antlr 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ n e. RR+ ) -> B e. RR )
35 32 34 rpcxpcld 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ n e. RR+ ) -> ( n ^c B ) e. RR+ )
36 35 rpcnd 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ n e. RR+ ) -> ( n ^c B ) e. CC )
37 35 rpne0d 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ n e. RR+ ) -> ( n ^c B ) =/= 0 )
38 31 36 37 divcld 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ n e. RR+ ) -> ( ( ( log ` n ) ^c A ) / ( n ^c B ) ) e. CC )
39 38 adantrr 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( ( ( log ` n ) ^c A ) / ( n ^c B ) ) e. CC )
40 39 abscld 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( abs ` ( ( ( log ` n ) ^c A ) / ( n ^c B ) ) ) e. RR )
41 rpre 
 |-  ( n e. RR+ -> n e. RR )
42 41 ad2antrl 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> n e. RR )
43 9 a1i 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> 1 e. RR )
44 1 a1i 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> 3 e. RR )
45 1lt3 
 |-  1 < 3
46 45 a1i 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> 1 < 3 )
47 simprr 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> 3 <_ n )
48 43 44 42 46 47 ltletrd 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> 1 < n )
49 42 48 rplogcld 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( log ` n ) e. RR+ )
50 32 adantrr 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> n e. RR+ )
51 33 ad2antlr 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> B e. RR )
52 18 adantr 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) e. RR+ )
53 51 52 rerpdivcld 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) e. RR )
54 50 53 rpcxpcld 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) e. RR+ )
55 49 54 rpdivcld 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( ( log ` n ) / ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) ) e. RR+ )
56 11 adantr 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) e. RR )
57 55 56 rpcxpcld 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( ( ( log ` n ) / ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) e. RR+ )
58 57 rpred 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( ( ( log ` n ) / ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) e. RR )
59 26 adantrr 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( ( ( log ` n ) / ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) e. CC )
60 59 abscld 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( abs ` ( ( ( log ` n ) / ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) e. RR )
61 31 adantrr 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( ( log ` n ) ^c A ) e. CC )
62 61 abscld 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( abs ` ( ( log ` n ) ^c A ) ) e. RR )
63 49 56 rpcxpcld 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( ( log ` n ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) e. RR+ )
64 63 rpred 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( ( log ` n ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) e. RR )
65 35 adantrr 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( n ^c B ) e. RR+ )
66 simpll 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> A e. CC )
67 abscxp 
 |-  ( ( ( log ` n ) e. RR+ /\ A e. CC ) -> ( abs ` ( ( log ` n ) ^c A ) ) = ( ( log ` n ) ^c ( Re ` A ) ) )
68 49 66 67 syl2anc 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( abs ` ( ( log ` n ) ^c A ) ) = ( ( log ` n ) ^c ( Re ` A ) ) )
69 66 recld 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( Re ` A ) e. RR )
70 max2 
 |-  ( ( 1 e. RR /\ ( Re ` A ) e. RR ) -> ( Re ` A ) <_ if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) )
71 9 69 70 sylancr 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( Re ` A ) <_ if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) )
72 27 ad2antrl 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( log ` n ) e. RR )
73 loge 
 |-  ( log ` _e ) = 1
74 ere 
 |-  _e e. RR
75 74 a1i 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> _e e. RR )
76 egt2lt3 
 |-  ( 2 < _e /\ _e < 3 )
77 76 simpri 
 |-  _e < 3
78 77 a1i 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> _e < 3 )
79 75 44 42 78 47 ltletrd 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> _e < n )
80 epr 
 |-  _e e. RR+
81 logltb 
 |-  ( ( _e e. RR+ /\ n e. RR+ ) -> ( _e < n <-> ( log ` _e ) < ( log ` n ) ) )
82 80 50 81 sylancr 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( _e < n <-> ( log ` _e ) < ( log ` n ) ) )
83 79 82 mpbid 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( log ` _e ) < ( log ` n ) )
84 73 83 eqbrtrrid 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> 1 < ( log ` n ) )
85 72 84 69 56 cxpled 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( ( Re ` A ) <_ if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) <-> ( ( log ` n ) ^c ( Re ` A ) ) <_ ( ( log ` n ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) )
86 71 85 mpbid 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( ( log ` n ) ^c ( Re ` A ) ) <_ ( ( log ` n ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) )
87 68 86 eqbrtrd 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( abs ` ( ( log ` n ) ^c A ) ) <_ ( ( log ` n ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) )
88 62 64 65 87 lediv1dd 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( ( abs ` ( ( log ` n ) ^c A ) ) / ( n ^c B ) ) <_ ( ( ( log ` n ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) / ( n ^c B ) ) )
89 31 36 37 absdivd 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ n e. RR+ ) -> ( abs ` ( ( ( log ` n ) ^c A ) / ( n ^c B ) ) ) = ( ( abs ` ( ( log ` n ) ^c A ) ) / ( abs ` ( n ^c B ) ) ) )
90 89 adantrr 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( abs ` ( ( ( log ` n ) ^c A ) / ( n ^c B ) ) ) = ( ( abs ` ( ( log ` n ) ^c A ) ) / ( abs ` ( n ^c B ) ) ) )
91 65 rprege0d 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( ( n ^c B ) e. RR /\ 0 <_ ( n ^c B ) ) )
92 absid 
 |-  ( ( ( n ^c B ) e. RR /\ 0 <_ ( n ^c B ) ) -> ( abs ` ( n ^c B ) ) = ( n ^c B ) )
93 91 92 syl 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( abs ` ( n ^c B ) ) = ( n ^c B ) )
94 93 oveq2d 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( ( abs ` ( ( log ` n ) ^c A ) ) / ( abs ` ( n ^c B ) ) ) = ( ( abs ` ( ( log ` n ) ^c A ) ) / ( n ^c B ) ) )
95 90 94 eqtrd 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( abs ` ( ( ( log ` n ) ^c A ) / ( n ^c B ) ) ) = ( ( abs ` ( ( log ` n ) ^c A ) ) / ( n ^c B ) ) )
96 49 rprege0d 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( ( log ` n ) e. RR /\ 0 <_ ( log ` n ) ) )
97 11 recnd 
 |-  ( ( A e. CC /\ B e. RR+ ) -> if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) e. CC )
98 97 adantr 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) e. CC )
99 divcxp 
 |-  ( ( ( ( log ` n ) e. RR /\ 0 <_ ( log ` n ) ) /\ ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) e. RR+ /\ if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) e. CC ) -> ( ( ( log ` n ) / ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) = ( ( ( log ` n ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) / ( ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) )
100 96 54 98 99 syl3anc 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( ( ( log ` n ) / ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) = ( ( ( log ` n ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) / ( ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) )
101 50 53 98 cxpmuld 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( n ^c ( ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) x. if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) = ( ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) )
102 51 recnd 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> B e. CC )
103 52 rpne0d 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) =/= 0 )
104 102 98 103 divcan1d 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) x. if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) = B )
105 104 oveq2d 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( n ^c ( ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) x. if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) = ( n ^c B ) )
106 101 105 eqtr3d 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) = ( n ^c B ) )
107 106 oveq2d 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( ( ( log ` n ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) / ( ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) = ( ( ( log ` n ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) / ( n ^c B ) ) )
108 100 107 eqtrd 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( ( ( log ` n ) / ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) = ( ( ( log ` n ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) / ( n ^c B ) ) )
109 88 95 108 3brtr4d 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( abs ` ( ( ( log ` n ) ^c A ) / ( n ^c B ) ) ) <_ ( ( ( log ` n ) / ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) )
110 58 leabsd 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( ( ( log ` n ) / ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) <_ ( abs ` ( ( ( log ` n ) / ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) )
111 40 58 60 109 110 letrd 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( abs ` ( ( ( log ` n ) ^c A ) / ( n ^c B ) ) ) <_ ( abs ` ( ( ( log ` n ) / ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) )
112 39 subid1d 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( ( ( ( log ` n ) ^c A ) / ( n ^c B ) ) - 0 ) = ( ( ( log ` n ) ^c A ) / ( n ^c B ) ) )
113 112 fveq2d 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( abs ` ( ( ( ( log ` n ) ^c A ) / ( n ^c B ) ) - 0 ) ) = ( abs ` ( ( ( log ` n ) ^c A ) / ( n ^c B ) ) ) )
114 59 subid1d 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( ( ( ( log ` n ) / ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) - 0 ) = ( ( ( log ` n ) / ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) )
115 114 fveq2d 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( abs ` ( ( ( ( log ` n ) / ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) - 0 ) ) = ( abs ` ( ( ( log ` n ) / ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) )
116 111 113 115 3brtr4d 
 |-  ( ( ( A e. CC /\ B e. RR+ ) /\ ( n e. RR+ /\ 3 <_ n ) ) -> ( abs ` ( ( ( ( log ` n ) ^c A ) / ( n ^c B ) ) - 0 ) ) <_ ( abs ` ( ( ( ( log ` n ) / ( n ^c ( B / if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) ) ) ^c if ( 1 <_ ( Re ` A ) , ( Re ` A ) , 1 ) ) - 0 ) ) )
117 2 4 22 26 38 116 rlimsqzlem 
 |-  ( ( A e. CC /\ B e. RR+ ) -> ( n e. RR+ |-> ( ( ( log ` n ) ^c A ) / ( n ^c B ) ) ) ~~>r 0 )