Step | Hyp | Ref
| Expression |
1 | | rpre 11715 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ) |
2 | | reefcl 14656 |
. . . 4
⊢ (𝐴 ∈ ℝ →
(exp‘𝐴) ∈
ℝ) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ (exp‘𝐴) ∈
ℝ) |
4 | | efgt1 14685 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ 1 < (exp‘𝐴)) |
5 | | cxp2limlem 24502 |
. . 3
⊢
(((exp‘𝐴)
∈ ℝ ∧ 1 < (exp‘𝐴)) → (𝑚 ∈ ℝ+ ↦ (𝑚 / ((exp‘𝐴)↑𝑐𝑚))) ⇝𝑟
0) |
6 | 3, 4, 5 | syl2anc 691 |
. 2
⊢ (𝐴 ∈ ℝ+
→ (𝑚 ∈
ℝ+ ↦ (𝑚 / ((exp‘𝐴)↑𝑐𝑚))) ⇝𝑟
0) |
7 | | reefcl 14656 |
. . . . . . . 8
⊢ (𝑧 ∈ ℝ →
(exp‘𝑧) ∈
ℝ) |
8 | 7 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
→ (exp‘𝑧) ∈
ℝ) |
9 | | 1re 9918 |
. . . . . . 7
⊢ 1 ∈
ℝ |
10 | | ifcl 4080 |
. . . . . . 7
⊢
(((exp‘𝑧)
∈ ℝ ∧ 1 ∈ ℝ) → if(1 ≤ (exp‘𝑧), (exp‘𝑧), 1) ∈ ℝ) |
11 | 8, 9, 10 | sylancl 693 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
→ if(1 ≤ (exp‘𝑧), (exp‘𝑧), 1) ∈ ℝ) |
12 | 9 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ 𝑛 ∈
ℝ+) → 1 ∈ ℝ) |
13 | 8 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ 𝑛 ∈
ℝ+) → (exp‘𝑧) ∈ ℝ) |
14 | | rpre 11715 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ 𝑛 ∈
ℝ) |
15 | 14 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ 𝑛 ∈
ℝ+) → 𝑛 ∈ ℝ) |
16 | | maxlt 11898 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ (exp‘𝑧) ∈ ℝ ∧ 𝑛 ∈ ℝ) → (if(1 ≤
(exp‘𝑧),
(exp‘𝑧), 1) <
𝑛 ↔ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) |
17 | 12, 13, 15, 16 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ 𝑛 ∈
ℝ+) → (if(1 ≤ (exp‘𝑧), (exp‘𝑧), 1) < 𝑛 ↔ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) |
18 | | simprrr 801 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → (exp‘𝑧) < 𝑛) |
19 | | reeflog 24131 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℝ+
→ (exp‘(log‘𝑛)) = 𝑛) |
20 | 19 | ad2antrl 760 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → (exp‘(log‘𝑛)) = 𝑛) |
21 | 18, 20 | breqtrrd 4611 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → (exp‘𝑧) < (exp‘(log‘𝑛))) |
22 | | simplr 788 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → 𝑧 ∈ ℝ) |
23 | 14 | ad2antrl 760 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → 𝑛 ∈ ℝ) |
24 | | simprrl 800 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → 1 < 𝑛) |
25 | 23, 24 | rplogcld 24179 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → (log‘𝑛) ∈
ℝ+) |
26 | 25 | rpred 11748 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → (log‘𝑛) ∈ ℝ) |
27 | | eflt 14686 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℝ ∧
(log‘𝑛) ∈
ℝ) → (𝑧 <
(log‘𝑛) ↔
(exp‘𝑧) <
(exp‘(log‘𝑛)))) |
28 | 22, 26, 27 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → (𝑧 < (log‘𝑛) ↔ (exp‘𝑧) < (exp‘(log‘𝑛)))) |
29 | 21, 28 | mpbird 246 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → 𝑧 < (log‘𝑛)) |
30 | | breq2 4587 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = (log‘𝑛) → (𝑧 < 𝑚 ↔ 𝑧 < (log‘𝑛))) |
31 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 = (log‘𝑛) → 𝑚 = (log‘𝑛)) |
32 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 = (log‘𝑛) → ((exp‘𝐴)↑𝑐𝑚) = ((exp‘𝐴)↑𝑐(log‘𝑛))) |
33 | 31, 32 | oveq12d 6567 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = (log‘𝑛) → (𝑚 / ((exp‘𝐴)↑𝑐𝑚)) = ((log‘𝑛) / ((exp‘𝐴)↑𝑐(log‘𝑛)))) |
34 | 33 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = (log‘𝑛) → (abs‘(𝑚 / ((exp‘𝐴)↑𝑐𝑚))) =
(abs‘((log‘𝑛) /
((exp‘𝐴)↑𝑐(log‘𝑛))))) |
35 | 34 | breq1d 4593 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = (log‘𝑛) → ((abs‘(𝑚 / ((exp‘𝐴)↑𝑐𝑚))) < 𝑥 ↔ (abs‘((log‘𝑛) / ((exp‘𝐴)↑𝑐(log‘𝑛)))) < 𝑥)) |
36 | 30, 35 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (log‘𝑛) → ((𝑧 < 𝑚 → (abs‘(𝑚 / ((exp‘𝐴)↑𝑐𝑚))) < 𝑥) ↔ (𝑧 < (log‘𝑛) → (abs‘((log‘𝑛) / ((exp‘𝐴)↑𝑐(log‘𝑛)))) < 𝑥))) |
37 | 36 | rspcv 3278 |
. . . . . . . . . . . . 13
⊢
((log‘𝑛)
∈ ℝ+ → (∀𝑚 ∈ ℝ+ (𝑧 < 𝑚 → (abs‘(𝑚 / ((exp‘𝐴)↑𝑐𝑚))) < 𝑥) → (𝑧 < (log‘𝑛) → (abs‘((log‘𝑛) / ((exp‘𝐴)↑𝑐(log‘𝑛)))) < 𝑥))) |
38 | 25, 37 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → (∀𝑚 ∈ ℝ+ (𝑧 < 𝑚 → (abs‘(𝑚 / ((exp‘𝐴)↑𝑐𝑚))) < 𝑥) → (𝑧 < (log‘𝑛) → (abs‘((log‘𝑛) / ((exp‘𝐴)↑𝑐(log‘𝑛)))) < 𝑥))) |
39 | 29, 38 | mpid 43 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → (∀𝑚 ∈ ℝ+ (𝑧 < 𝑚 → (abs‘(𝑚 / ((exp‘𝐴)↑𝑐𝑚))) < 𝑥) → (abs‘((log‘𝑛) / ((exp‘𝐴)↑𝑐(log‘𝑛)))) < 𝑥)) |
40 | 1 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → 𝐴 ∈ ℝ) |
41 | 40 | relogefd 24178 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → (log‘(exp‘𝐴)) = 𝐴) |
42 | 41 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → ((log‘𝑛) · (log‘(exp‘𝐴))) = ((log‘𝑛) · 𝐴)) |
43 | 25 | rpcnd 11750 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → (log‘𝑛) ∈ ℂ) |
44 | | rpcn 11717 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℂ) |
45 | 44 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → 𝐴 ∈ ℂ) |
46 | 43, 45 | mulcomd 9940 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → ((log‘𝑛) · 𝐴) = (𝐴 · (log‘𝑛))) |
47 | 42, 46 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → ((log‘𝑛) · (log‘(exp‘𝐴))) = (𝐴 · (log‘𝑛))) |
48 | 47 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → (exp‘((log‘𝑛) ·
(log‘(exp‘𝐴))))
= (exp‘(𝐴 ·
(log‘𝑛)))) |
49 | 3 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → (exp‘𝐴) ∈ ℝ) |
50 | 49 | recnd 9947 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → (exp‘𝐴) ∈ ℂ) |
51 | | efne0 14666 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ →
(exp‘𝐴) ≠
0) |
52 | 45, 51 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → (exp‘𝐴) ≠ 0) |
53 | 50, 52, 43 | cxpefd 24258 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → ((exp‘𝐴)↑𝑐(log‘𝑛)) =
(exp‘((log‘𝑛)
· (log‘(exp‘𝐴))))) |
54 | | rpcn 11717 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℝ+
→ 𝑛 ∈
ℂ) |
55 | 54 | ad2antrl 760 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → 𝑛 ∈ ℂ) |
56 | | rpne0 11724 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℝ+
→ 𝑛 ≠
0) |
57 | 56 | ad2antrl 760 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → 𝑛 ≠ 0) |
58 | 55, 57, 45 | cxpefd 24258 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → (𝑛↑𝑐𝐴) = (exp‘(𝐴 · (log‘𝑛)))) |
59 | 48, 53, 58 | 3eqtr4d 2654 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → ((exp‘𝐴)↑𝑐(log‘𝑛)) = (𝑛↑𝑐𝐴)) |
60 | 59 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → ((log‘𝑛) / ((exp‘𝐴)↑𝑐(log‘𝑛))) = ((log‘𝑛) / (𝑛↑𝑐𝐴))) |
61 | 60 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → (abs‘((log‘𝑛) / ((exp‘𝐴)↑𝑐(log‘𝑛)))) =
(abs‘((log‘𝑛) /
(𝑛↑𝑐𝐴)))) |
62 | 61 | breq1d 4593 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → ((abs‘((log‘𝑛) / ((exp‘𝐴)↑𝑐(log‘𝑛)))) < 𝑥 ↔ (abs‘((log‘𝑛) / (𝑛↑𝑐𝐴))) < 𝑥)) |
63 | 39, 62 | sylibd 228 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ (𝑛 ∈
ℝ+ ∧ (1 < 𝑛 ∧ (exp‘𝑧) < 𝑛))) → (∀𝑚 ∈ ℝ+ (𝑧 < 𝑚 → (abs‘(𝑚 / ((exp‘𝐴)↑𝑐𝑚))) < 𝑥) → (abs‘((log‘𝑛) / (𝑛↑𝑐𝐴))) < 𝑥)) |
64 | 63 | expr 641 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ 𝑛 ∈
ℝ+) → ((1 < 𝑛 ∧ (exp‘𝑧) < 𝑛) → (∀𝑚 ∈ ℝ+ (𝑧 < 𝑚 → (abs‘(𝑚 / ((exp‘𝐴)↑𝑐𝑚))) < 𝑥) → (abs‘((log‘𝑛) / (𝑛↑𝑐𝐴))) < 𝑥))) |
65 | 17, 64 | sylbid 229 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ 𝑛 ∈
ℝ+) → (if(1 ≤ (exp‘𝑧), (exp‘𝑧), 1) < 𝑛 → (∀𝑚 ∈ ℝ+ (𝑧 < 𝑚 → (abs‘(𝑚 / ((exp‘𝐴)↑𝑐𝑚))) < 𝑥) → (abs‘((log‘𝑛) / (𝑛↑𝑐𝐴))) < 𝑥))) |
66 | 65 | com23 84 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
∧ 𝑛 ∈
ℝ+) → (∀𝑚 ∈ ℝ+ (𝑧 < 𝑚 → (abs‘(𝑚 / ((exp‘𝐴)↑𝑐𝑚))) < 𝑥) → (if(1 ≤ (exp‘𝑧), (exp‘𝑧), 1) < 𝑛 → (abs‘((log‘𝑛) / (𝑛↑𝑐𝐴))) < 𝑥))) |
67 | 66 | ralrimdva 2952 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
→ (∀𝑚 ∈
ℝ+ (𝑧 <
𝑚 → (abs‘(𝑚 / ((exp‘𝐴)↑𝑐𝑚))) < 𝑥) → ∀𝑛 ∈ ℝ+ (if(1 ≤
(exp‘𝑧),
(exp‘𝑧), 1) <
𝑛 →
(abs‘((log‘𝑛) /
(𝑛↑𝑐𝐴))) < 𝑥))) |
68 | | breq1 4586 |
. . . . . . . . 9
⊢ (𝑦 = if(1 ≤ (exp‘𝑧), (exp‘𝑧), 1) → (𝑦 < 𝑛 ↔ if(1 ≤ (exp‘𝑧), (exp‘𝑧), 1) < 𝑛)) |
69 | 68 | imbi1d 330 |
. . . . . . . 8
⊢ (𝑦 = if(1 ≤ (exp‘𝑧), (exp‘𝑧), 1) → ((𝑦 < 𝑛 → (abs‘((log‘𝑛) / (𝑛↑𝑐𝐴))) < 𝑥) ↔ (if(1 ≤ (exp‘𝑧), (exp‘𝑧), 1) < 𝑛 → (abs‘((log‘𝑛) / (𝑛↑𝑐𝐴))) < 𝑥))) |
70 | 69 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑦 = if(1 ≤ (exp‘𝑧), (exp‘𝑧), 1) → (∀𝑛 ∈ ℝ+ (𝑦 < 𝑛 → (abs‘((log‘𝑛) / (𝑛↑𝑐𝐴))) < 𝑥) ↔ ∀𝑛 ∈ ℝ+ (if(1 ≤
(exp‘𝑧),
(exp‘𝑧), 1) <
𝑛 →
(abs‘((log‘𝑛) /
(𝑛↑𝑐𝐴))) < 𝑥))) |
71 | 70 | rspcev 3282 |
. . . . . 6
⊢ ((if(1
≤ (exp‘𝑧),
(exp‘𝑧), 1) ∈
ℝ ∧ ∀𝑛
∈ ℝ+ (if(1 ≤ (exp‘𝑧), (exp‘𝑧), 1) < 𝑛 → (abs‘((log‘𝑛) / (𝑛↑𝑐𝐴))) < 𝑥)) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℝ+ (𝑦 < 𝑛 → (abs‘((log‘𝑛) / (𝑛↑𝑐𝐴))) < 𝑥)) |
72 | 11, 67, 71 | syl6an 566 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 𝑧 ∈ ℝ)
→ (∀𝑚 ∈
ℝ+ (𝑧 <
𝑚 → (abs‘(𝑚 / ((exp‘𝐴)↑𝑐𝑚))) < 𝑥) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℝ+ (𝑦 < 𝑛 → (abs‘((log‘𝑛) / (𝑛↑𝑐𝐴))) < 𝑥))) |
73 | 72 | rexlimdva 3013 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (∃𝑧 ∈
ℝ ∀𝑚 ∈
ℝ+ (𝑧 <
𝑚 → (abs‘(𝑚 / ((exp‘𝐴)↑𝑐𝑚))) < 𝑥) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℝ+ (𝑦 < 𝑛 → (abs‘((log‘𝑛) / (𝑛↑𝑐𝐴))) < 𝑥))) |
74 | 73 | ralimdv 2946 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ (∀𝑥 ∈
ℝ+ ∃𝑧 ∈ ℝ ∀𝑚 ∈ ℝ+ (𝑧 < 𝑚 → (abs‘(𝑚 / ((exp‘𝐴)↑𝑐𝑚))) < 𝑥) → ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℝ+
(𝑦 < 𝑛 → (abs‘((log‘𝑛) / (𝑛↑𝑐𝐴))) < 𝑥))) |
75 | | simpr 476 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝑚 ∈
ℝ+) → 𝑚 ∈ ℝ+) |
76 | 1 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑚 ∈
ℝ+) → 𝐴 ∈ ℝ) |
77 | 76 | rpefcld 14674 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑚 ∈
ℝ+) → (exp‘𝐴) ∈
ℝ+) |
78 | | rpre 11715 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℝ+
→ 𝑚 ∈
ℝ) |
79 | 78 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑚 ∈
ℝ+) → 𝑚 ∈ ℝ) |
80 | 77, 79 | rpcxpcld 24276 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝑚 ∈
ℝ+) → ((exp‘𝐴)↑𝑐𝑚) ∈
ℝ+) |
81 | 75, 80 | rpdivcld 11765 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 𝑚 ∈
ℝ+) → (𝑚 / ((exp‘𝐴)↑𝑐𝑚)) ∈
ℝ+) |
82 | 81 | rpcnd 11750 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 𝑚 ∈
ℝ+) → (𝑚 / ((exp‘𝐴)↑𝑐𝑚)) ∈
ℂ) |
83 | 82 | ralrimiva 2949 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ ∀𝑚 ∈
ℝ+ (𝑚 /
((exp‘𝐴)↑𝑐𝑚)) ∈
ℂ) |
84 | | rpssre 11719 |
. . . . 5
⊢
ℝ+ ⊆ ℝ |
85 | 84 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ ℝ+ ⊆ ℝ) |
86 | 83, 85 | rlim0lt 14088 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ ((𝑚 ∈
ℝ+ ↦ (𝑚 / ((exp‘𝐴)↑𝑐𝑚))) ⇝𝑟
0 ↔ ∀𝑥 ∈
ℝ+ ∃𝑧 ∈ ℝ ∀𝑚 ∈ ℝ+ (𝑧 < 𝑚 → (abs‘(𝑚 / ((exp‘𝐴)↑𝑐𝑚))) < 𝑥))) |
87 | | relogcl 24126 |
. . . . . . . 8
⊢ (𝑛 ∈ ℝ+
→ (log‘𝑛) ∈
ℝ) |
88 | 87 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
ℝ+) → (log‘𝑛) ∈ ℝ) |
89 | | simpr 476 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
ℝ+) → 𝑛 ∈ ℝ+) |
90 | 1 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
ℝ+) → 𝐴 ∈ ℝ) |
91 | 89, 90 | rpcxpcld 24276 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
ℝ+) → (𝑛↑𝑐𝐴) ∈
ℝ+) |
92 | 88, 91 | rerpdivcld 11779 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
ℝ+) → ((log‘𝑛) / (𝑛↑𝑐𝐴)) ∈ ℝ) |
93 | 92 | recnd 9947 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
ℝ+) → ((log‘𝑛) / (𝑛↑𝑐𝐴)) ∈ ℂ) |
94 | 93 | ralrimiva 2949 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ ∀𝑛 ∈
ℝ+ ((log‘𝑛) / (𝑛↑𝑐𝐴)) ∈ ℂ) |
95 | 94, 85 | rlim0lt 14088 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ ((𝑛 ∈
ℝ+ ↦ ((log‘𝑛) / (𝑛↑𝑐𝐴))) ⇝𝑟 0 ↔
∀𝑥 ∈
ℝ+ ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℝ+ (𝑦 < 𝑛 → (abs‘((log‘𝑛) / (𝑛↑𝑐𝐴))) < 𝑥))) |
96 | 74, 86, 95 | 3imtr4d 282 |
. 2
⊢ (𝐴 ∈ ℝ+
→ ((𝑚 ∈
ℝ+ ↦ (𝑚 / ((exp‘𝐴)↑𝑐𝑚))) ⇝𝑟
0 → (𝑛 ∈
ℝ+ ↦ ((log‘𝑛) / (𝑛↑𝑐𝐴))) ⇝𝑟
0)) |
97 | 6, 96 | mpd 15 |
1
⊢ (𝐴 ∈ ℝ+
→ (𝑛 ∈
ℝ+ ↦ ((log‘𝑛) / (𝑛↑𝑐𝐴))) ⇝𝑟
0) |