Proof of Theorem cxploglim2
Step | Hyp | Ref
| Expression |
1 | | 3re 10971 |
. . 3
⊢ 3 ∈
ℝ |
2 | 1 | a1i 11 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
→ 3 ∈ ℝ) |
3 | | 0red 9920 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
→ 0 ∈ ℝ) |
4 | 3 | recnd 9947 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
→ 0 ∈ ℂ) |
5 | | ovex 6577 |
. . . 4
⊢
((log‘𝑛) /
(𝑛↑𝑐(𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1)))) ∈ V |
6 | 5 | a1i 11 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ 𝑛 ∈
ℝ+) → ((log‘𝑛) / (𝑛↑𝑐(𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1)))) ∈ V) |
7 | | simpr 476 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
→ 𝐵 ∈
ℝ+) |
8 | | recl 13698 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℝ) |
9 | 8 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
→ (ℜ‘𝐴)
∈ ℝ) |
10 | | 1re 9918 |
. . . . . . 7
⊢ 1 ∈
ℝ |
11 | | ifcl 4080 |
. . . . . . 7
⊢
(((ℜ‘𝐴)
∈ ℝ ∧ 1 ∈ ℝ) → if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1) ∈
ℝ) |
12 | 9, 10, 11 | sylancl 693 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
→ if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1) ∈ ℝ) |
13 | 10 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
→ 1 ∈ ℝ) |
14 | | 0lt1 10429 |
. . . . . . . 8
⊢ 0 <
1 |
15 | 14 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
→ 0 < 1) |
16 | | max1 11890 |
. . . . . . . 8
⊢ ((1
∈ ℝ ∧ (ℜ‘𝐴) ∈ ℝ) → 1 ≤ if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴),
1)) |
17 | 10, 9, 16 | sylancr 694 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
→ 1 ≤ if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1)) |
18 | 3, 13, 12, 15, 17 | ltletrd 10076 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
→ 0 < if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1)) |
19 | 12, 18 | elrpd 11745 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
→ if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1) ∈
ℝ+) |
20 | 7, 19 | rpdivcld 11765 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
→ (𝐵 / if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴), 1))
∈ ℝ+) |
21 | | cxploglim 24504 |
. . . 4
⊢ ((𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1)) ∈
ℝ+ → (𝑛 ∈ ℝ+ ↦
((log‘𝑛) / (𝑛↑𝑐(𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1)))))
⇝𝑟 0) |
22 | 20, 21 | syl 17 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
→ (𝑛 ∈
ℝ+ ↦ ((log‘𝑛) / (𝑛↑𝑐(𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1))))) ⇝𝑟
0) |
23 | 6, 22, 19 | rlimcxp 24500 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
→ (𝑛 ∈
ℝ+ ↦ (((log‘𝑛) / (𝑛↑𝑐(𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1))))↑𝑐if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴), 1)))
⇝𝑟 0) |
24 | 6, 22 | rlimmptrcl 14186 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ 𝑛 ∈
ℝ+) → ((log‘𝑛) / (𝑛↑𝑐(𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1)))) ∈ ℂ) |
25 | 12 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ 𝑛 ∈
ℝ+) → if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1) ∈ ℝ) |
26 | 25 | recnd 9947 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ 𝑛 ∈
ℝ+) → if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1) ∈ ℂ) |
27 | 24, 26 | cxpcld 24254 |
. 2
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ 𝑛 ∈
ℝ+) → (((log‘𝑛) / (𝑛↑𝑐(𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1))))↑𝑐if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴), 1))
∈ ℂ) |
28 | | relogcl 24126 |
. . . . . 6
⊢ (𝑛 ∈ ℝ+
→ (log‘𝑛) ∈
ℝ) |
29 | 28 | adantl 481 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ 𝑛 ∈
ℝ+) → (log‘𝑛) ∈ ℝ) |
30 | 29 | recnd 9947 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ 𝑛 ∈
ℝ+) → (log‘𝑛) ∈ ℂ) |
31 | | simpll 786 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ 𝑛 ∈
ℝ+) → 𝐴 ∈ ℂ) |
32 | 30, 31 | cxpcld 24254 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ 𝑛 ∈
ℝ+) → ((log‘𝑛)↑𝑐𝐴) ∈ ℂ) |
33 | | simpr 476 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ 𝑛 ∈
ℝ+) → 𝑛 ∈ ℝ+) |
34 | | rpre 11715 |
. . . . . 6
⊢ (𝐵 ∈ ℝ+
→ 𝐵 ∈
ℝ) |
35 | 34 | ad2antlr 759 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ 𝑛 ∈
ℝ+) → 𝐵 ∈ ℝ) |
36 | 33, 35 | rpcxpcld 24276 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ 𝑛 ∈
ℝ+) → (𝑛↑𝑐𝐵) ∈
ℝ+) |
37 | 36 | rpcnd 11750 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ 𝑛 ∈
ℝ+) → (𝑛↑𝑐𝐵) ∈ ℂ) |
38 | 36 | rpne0d 11753 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ 𝑛 ∈
ℝ+) → (𝑛↑𝑐𝐵) ≠ 0) |
39 | 32, 37, 38 | divcld 10680 |
. 2
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ 𝑛 ∈
ℝ+) → (((log‘𝑛)↑𝑐𝐴) / (𝑛↑𝑐𝐵)) ∈ ℂ) |
40 | 39 | adantrr 749 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (((log‘𝑛)↑𝑐𝐴) / (𝑛↑𝑐𝐵)) ∈ ℂ) |
41 | 40 | abscld 14023 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (abs‘(((log‘𝑛)↑𝑐𝐴) / (𝑛↑𝑐𝐵))) ∈ ℝ) |
42 | | rpre 11715 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℝ+
→ 𝑛 ∈
ℝ) |
43 | 42 | ad2antrl 760 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → 𝑛 ∈ ℝ) |
44 | 10 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → 1 ∈ ℝ) |
45 | 1 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → 3 ∈ ℝ) |
46 | | 1lt3 11073 |
. . . . . . . . . 10
⊢ 1 <
3 |
47 | 46 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → 1 < 3) |
48 | | simprr 792 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → 3 ≤ 𝑛) |
49 | 44, 45, 43, 47, 48 | ltletrd 10076 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → 1 < 𝑛) |
50 | 43, 49 | rplogcld 24179 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (log‘𝑛) ∈
ℝ+) |
51 | 33 | adantrr 749 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → 𝑛 ∈ ℝ+) |
52 | 34 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → 𝐵 ∈ ℝ) |
53 | 19 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1) ∈
ℝ+) |
54 | 52, 53 | rerpdivcld 11779 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1)) ∈ ℝ) |
55 | 51, 54 | rpcxpcld 24276 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (𝑛↑𝑐(𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1))) ∈
ℝ+) |
56 | 50, 55 | rpdivcld 11765 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → ((log‘𝑛) / (𝑛↑𝑐(𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1)))) ∈
ℝ+) |
57 | 12 | adantr 480 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1) ∈
ℝ) |
58 | 56, 57 | rpcxpcld 24276 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (((log‘𝑛) / (𝑛↑𝑐(𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1))))↑𝑐if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴), 1))
∈ ℝ+) |
59 | 58 | rpred 11748 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (((log‘𝑛) / (𝑛↑𝑐(𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1))))↑𝑐if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴), 1))
∈ ℝ) |
60 | 27 | adantrr 749 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (((log‘𝑛) / (𝑛↑𝑐(𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1))))↑𝑐if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴), 1))
∈ ℂ) |
61 | 60 | abscld 14023 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (abs‘(((log‘𝑛) / (𝑛↑𝑐(𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1))))↑𝑐if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴), 1)))
∈ ℝ) |
62 | 32 | adantrr 749 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → ((log‘𝑛)↑𝑐𝐴) ∈ ℂ) |
63 | 62 | abscld 14023 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (abs‘((log‘𝑛)↑𝑐𝐴)) ∈
ℝ) |
64 | 50, 57 | rpcxpcld 24276 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → ((log‘𝑛)↑𝑐if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴), 1))
∈ ℝ+) |
65 | 64 | rpred 11748 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → ((log‘𝑛)↑𝑐if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴), 1))
∈ ℝ) |
66 | 36 | adantrr 749 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (𝑛↑𝑐𝐵) ∈
ℝ+) |
67 | | simpll 786 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → 𝐴 ∈ ℂ) |
68 | | abscxp 24238 |
. . . . . . . 8
⊢
(((log‘𝑛)
∈ ℝ+ ∧ 𝐴 ∈ ℂ) →
(abs‘((log‘𝑛)↑𝑐𝐴)) = ((log‘𝑛)↑𝑐(ℜ‘𝐴))) |
69 | 50, 67, 68 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (abs‘((log‘𝑛)↑𝑐𝐴)) = ((log‘𝑛)↑𝑐(ℜ‘𝐴))) |
70 | 67 | recld 13782 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (ℜ‘𝐴) ∈ ℝ) |
71 | | max2 11892 |
. . . . . . . . 9
⊢ ((1
∈ ℝ ∧ (ℜ‘𝐴) ∈ ℝ) → (ℜ‘𝐴) ≤ if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴),
1)) |
72 | 10, 70, 71 | sylancr 694 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (ℜ‘𝐴) ≤ if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1)) |
73 | 28 | ad2antrl 760 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (log‘𝑛) ∈ ℝ) |
74 | | loge 24137 |
. . . . . . . . . 10
⊢
(log‘e) = 1 |
75 | | ere 14658 |
. . . . . . . . . . . . 13
⊢ e ∈
ℝ |
76 | 75 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → e ∈ ℝ) |
77 | | egt2lt3 14773 |
. . . . . . . . . . . . . 14
⊢ (2 < e
∧ e < 3) |
78 | 77 | simpri 477 |
. . . . . . . . . . . . 13
⊢ e <
3 |
79 | 78 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → e < 3) |
80 | 76, 45, 43, 79, 48 | ltletrd 10076 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → e < 𝑛) |
81 | | epr 14775 |
. . . . . . . . . . . 12
⊢ e ∈
ℝ+ |
82 | | logltb 24150 |
. . . . . . . . . . . 12
⊢ ((e
∈ ℝ+ ∧ 𝑛 ∈ ℝ+) → (e <
𝑛 ↔ (log‘e) <
(log‘𝑛))) |
83 | 81, 51, 82 | sylancr 694 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (e < 𝑛 ↔ (log‘e) < (log‘𝑛))) |
84 | 80, 83 | mpbid 221 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (log‘e) < (log‘𝑛)) |
85 | 74, 84 | syl5eqbrr 4619 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → 1 < (log‘𝑛)) |
86 | 73, 85, 70, 57 | cxpled 24266 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → ((ℜ‘𝐴) ≤ if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1) ↔ ((log‘𝑛)↑𝑐(ℜ‘𝐴)) ≤ ((log‘𝑛)↑𝑐if(1
≤ (ℜ‘𝐴),
(ℜ‘𝐴),
1)))) |
87 | 72, 86 | mpbid 221 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → ((log‘𝑛)↑𝑐(ℜ‘𝐴)) ≤ ((log‘𝑛)↑𝑐if(1
≤ (ℜ‘𝐴),
(ℜ‘𝐴),
1))) |
88 | 69, 87 | eqbrtrd 4605 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (abs‘((log‘𝑛)↑𝑐𝐴)) ≤ ((log‘𝑛)↑𝑐if(1
≤ (ℜ‘𝐴),
(ℜ‘𝐴),
1))) |
89 | 63, 65, 66, 88 | lediv1dd 11806 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → ((abs‘((log‘𝑛)↑𝑐𝐴)) / (𝑛↑𝑐𝐵)) ≤ (((log‘𝑛)↑𝑐if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴), 1)) /
(𝑛↑𝑐𝐵))) |
90 | 32, 37, 38 | absdivd 14042 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ 𝑛 ∈
ℝ+) → (abs‘(((log‘𝑛)↑𝑐𝐴) / (𝑛↑𝑐𝐵))) = ((abs‘((log‘𝑛)↑𝑐𝐴)) / (abs‘(𝑛↑𝑐𝐵)))) |
91 | 90 | adantrr 749 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (abs‘(((log‘𝑛)↑𝑐𝐴) / (𝑛↑𝑐𝐵))) = ((abs‘((log‘𝑛)↑𝑐𝐴)) / (abs‘(𝑛↑𝑐𝐵)))) |
92 | 66 | rprege0d 11755 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → ((𝑛↑𝑐𝐵) ∈ ℝ ∧ 0 ≤ (𝑛↑𝑐𝐵))) |
93 | | absid 13884 |
. . . . . . . 8
⊢ (((𝑛↑𝑐𝐵) ∈ ℝ ∧ 0 ≤
(𝑛↑𝑐𝐵)) → (abs‘(𝑛↑𝑐𝐵)) = (𝑛↑𝑐𝐵)) |
94 | 92, 93 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (abs‘(𝑛↑𝑐𝐵)) = (𝑛↑𝑐𝐵)) |
95 | 94 | oveq2d 6565 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → ((abs‘((log‘𝑛)↑𝑐𝐴)) / (abs‘(𝑛↑𝑐𝐵))) =
((abs‘((log‘𝑛)↑𝑐𝐴)) / (𝑛↑𝑐𝐵))) |
96 | 91, 95 | eqtrd 2644 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (abs‘(((log‘𝑛)↑𝑐𝐴) / (𝑛↑𝑐𝐵))) = ((abs‘((log‘𝑛)↑𝑐𝐴)) / (𝑛↑𝑐𝐵))) |
97 | 50 | rprege0d 11755 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → ((log‘𝑛) ∈ ℝ ∧ 0 ≤
(log‘𝑛))) |
98 | 12 | recnd 9947 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
→ if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1) ∈ ℂ) |
99 | 98 | adantr 480 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1) ∈
ℂ) |
100 | | divcxp 24233 |
. . . . . . 7
⊢
((((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)))) |
101 | 97, 55, 99, 100 | syl3anc 1318 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (((log‘𝑛) / (𝑛↑𝑐(𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1))))↑𝑐if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴), 1)) =
(((log‘𝑛)↑𝑐if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴), 1)) /
((𝑛↑𝑐(𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1)))↑𝑐if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴),
1)))) |
102 | 51, 54, 99 | cxpmuld 24280 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (𝑛↑𝑐((𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1)) · if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴), 1))) =
((𝑛↑𝑐(𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1)))↑𝑐if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴),
1))) |
103 | 52 | recnd 9947 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → 𝐵 ∈ ℂ) |
104 | 53 | rpne0d 11753 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1) ≠ 0) |
105 | 103, 99, 104 | divcan1d 10681 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → ((𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1)) · if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴), 1)) =
𝐵) |
106 | 105 | oveq2d 6565 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (𝑛↑𝑐((𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1)) · if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴), 1))) =
(𝑛↑𝑐𝐵)) |
107 | 102, 106 | eqtr3d 2646 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → ((𝑛↑𝑐(𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1)))↑𝑐if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴), 1)) =
(𝑛↑𝑐𝐵)) |
108 | 107 | oveq2d 6565 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (((log‘𝑛)↑𝑐if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴), 1)) /
((𝑛↑𝑐(𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1)))↑𝑐if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴), 1))) =
(((log‘𝑛)↑𝑐if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴), 1)) /
(𝑛↑𝑐𝐵))) |
109 | 101, 108 | eqtrd 2644 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (((log‘𝑛) / (𝑛↑𝑐(𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1))))↑𝑐if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴), 1)) =
(((log‘𝑛)↑𝑐if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴), 1)) /
(𝑛↑𝑐𝐵))) |
110 | 89, 96, 109 | 3brtr4d 4615 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (abs‘(((log‘𝑛)↑𝑐𝐴) / (𝑛↑𝑐𝐵))) ≤ (((log‘𝑛) / (𝑛↑𝑐(𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1))))↑𝑐if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴),
1))) |
111 | 59 | leabsd 14001 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (((log‘𝑛) / (𝑛↑𝑐(𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1))))↑𝑐if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴), 1)) ≤
(abs‘(((log‘𝑛)
/ (𝑛↑𝑐(𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1))))↑𝑐if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴),
1)))) |
112 | 41, 59, 61, 110, 111 | letrd 10073 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (abs‘(((log‘𝑛)↑𝑐𝐴) / (𝑛↑𝑐𝐵))) ≤ (abs‘(((log‘𝑛) / (𝑛↑𝑐(𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1))))↑𝑐if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴),
1)))) |
113 | 40 | subid1d 10260 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → ((((log‘𝑛)↑𝑐𝐴) / (𝑛↑𝑐𝐵)) − 0) = (((log‘𝑛)↑𝑐𝐴) / (𝑛↑𝑐𝐵))) |
114 | 113 | fveq2d 6107 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (abs‘((((log‘𝑛)↑𝑐𝐴) / (𝑛↑𝑐𝐵)) − 0)) =
(abs‘(((log‘𝑛)↑𝑐𝐴) / (𝑛↑𝑐𝐵)))) |
115 | 60 | subid1d 10260 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → ((((log‘𝑛) / (𝑛↑𝑐(𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1))))↑𝑐if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴), 1))
− 0) = (((log‘𝑛) / (𝑛↑𝑐(𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1))))↑𝑐if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴),
1))) |
116 | 115 | fveq2d 6107 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (abs‘((((log‘𝑛) / (𝑛↑𝑐(𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1))))↑𝑐if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴), 1))
− 0)) = (abs‘(((log‘𝑛) / (𝑛↑𝑐(𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1))))↑𝑐if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴),
1)))) |
117 | 112, 114,
116 | 3brtr4d 4615 |
. 2
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ 3 ≤ 𝑛)) → (abs‘((((log‘𝑛)↑𝑐𝐴) / (𝑛↑𝑐𝐵)) − 0)) ≤
(abs‘((((log‘𝑛)
/ (𝑛↑𝑐(𝐵 / if(1 ≤ (ℜ‘𝐴), (ℜ‘𝐴), 1))))↑𝑐if(1 ≤
(ℜ‘𝐴),
(ℜ‘𝐴), 1))
− 0))) |
118 | 2, 4, 23, 27, 39, 117 | rlimsqzlem 14227 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+)
→ (𝑛 ∈
ℝ+ ↦ (((log‘𝑛)↑𝑐𝐴) / (𝑛↑𝑐𝐵))) ⇝𝑟
0) |