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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+ ) → ( 𝑛 ∈ ℝ+ ↦ ( ( ( log ‘ 𝑛 ) ↑𝑐 𝐴 ) / ( 𝑛 ↑𝑐 𝐵 ) ) ) ⇝𝑟 0 )

Proof

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