# 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

### Proof

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