| Step |
Hyp |
Ref |
Expression |
| 1 |
|
rpre |
⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ ) |
| 2 |
|
reefcl |
⊢ ( 𝐴 ∈ ℝ → ( exp ‘ 𝐴 ) ∈ ℝ ) |
| 3 |
1 2
|
syl |
⊢ ( 𝐴 ∈ ℝ+ → ( exp ‘ 𝐴 ) ∈ ℝ ) |
| 4 |
|
efgt1 |
⊢ ( 𝐴 ∈ ℝ+ → 1 < ( exp ‘ 𝐴 ) ) |
| 5 |
|
cxp2limlem |
⊢ ( ( ( exp ‘ 𝐴 ) ∈ ℝ ∧ 1 < ( exp ‘ 𝐴 ) ) → ( 𝑚 ∈ ℝ+ ↦ ( 𝑚 / ( ( exp ‘ 𝐴 ) ↑𝑐 𝑚 ) ) ) ⇝𝑟 0 ) |
| 6 |
3 4 5
|
syl2anc |
⊢ ( 𝐴 ∈ ℝ+ → ( 𝑚 ∈ ℝ+ ↦ ( 𝑚 / ( ( exp ‘ 𝐴 ) ↑𝑐 𝑚 ) ) ) ⇝𝑟 0 ) |
| 7 |
|
reefcl |
⊢ ( 𝑧 ∈ ℝ → ( exp ‘ 𝑧 ) ∈ ℝ ) |
| 8 |
7
|
adantl |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) → ( exp ‘ 𝑧 ) ∈ ℝ ) |
| 9 |
|
1re |
⊢ 1 ∈ ℝ |
| 10 |
|
ifcl |
⊢ ( ( ( exp ‘ 𝑧 ) ∈ ℝ ∧ 1 ∈ ℝ ) → if ( 1 ≤ ( exp ‘ 𝑧 ) , ( exp ‘ 𝑧 ) , 1 ) ∈ ℝ ) |
| 11 |
8 9 10
|
sylancl |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) → if ( 1 ≤ ( exp ‘ 𝑧 ) , ( exp ‘ 𝑧 ) , 1 ) ∈ ℝ ) |
| 12 |
|
rpre |
⊢ ( 𝑛 ∈ ℝ+ → 𝑛 ∈ ℝ ) |
| 13 |
|
maxlt |
⊢ ( ( 1 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℝ ∧ 𝑛 ∈ ℝ ) → ( if ( 1 ≤ ( exp ‘ 𝑧 ) , ( exp ‘ 𝑧 ) , 1 ) < 𝑛 ↔ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) |
| 14 |
9 8 12 13
|
mp3an3an |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ 𝑛 ∈ ℝ+ ) → ( if ( 1 ≤ ( exp ‘ 𝑧 ) , ( exp ‘ 𝑧 ) , 1 ) < 𝑛 ↔ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) |
| 15 |
|
simprrr |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → ( exp ‘ 𝑧 ) < 𝑛 ) |
| 16 |
|
reeflog |
⊢ ( 𝑛 ∈ ℝ+ → ( exp ‘ ( log ‘ 𝑛 ) ) = 𝑛 ) |
| 17 |
16
|
ad2antrl |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → ( exp ‘ ( log ‘ 𝑛 ) ) = 𝑛 ) |
| 18 |
15 17
|
breqtrrd |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → ( exp ‘ 𝑧 ) < ( exp ‘ ( log ‘ 𝑛 ) ) ) |
| 19 |
|
simplr |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → 𝑧 ∈ ℝ ) |
| 20 |
12
|
ad2antrl |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → 𝑛 ∈ ℝ ) |
| 21 |
|
simprrl |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → 1 < 𝑛 ) |
| 22 |
20 21
|
rplogcld |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → ( log ‘ 𝑛 ) ∈ ℝ+ ) |
| 23 |
22
|
rpred |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → ( log ‘ 𝑛 ) ∈ ℝ ) |
| 24 |
|
eflt |
⊢ ( ( 𝑧 ∈ ℝ ∧ ( log ‘ 𝑛 ) ∈ ℝ ) → ( 𝑧 < ( log ‘ 𝑛 ) ↔ ( exp ‘ 𝑧 ) < ( exp ‘ ( log ‘ 𝑛 ) ) ) ) |
| 25 |
19 23 24
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → ( 𝑧 < ( log ‘ 𝑛 ) ↔ ( exp ‘ 𝑧 ) < ( exp ‘ ( log ‘ 𝑛 ) ) ) ) |
| 26 |
18 25
|
mpbird |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → 𝑧 < ( log ‘ 𝑛 ) ) |
| 27 |
|
breq2 |
⊢ ( 𝑚 = ( log ‘ 𝑛 ) → ( 𝑧 < 𝑚 ↔ 𝑧 < ( log ‘ 𝑛 ) ) ) |
| 28 |
|
id |
⊢ ( 𝑚 = ( log ‘ 𝑛 ) → 𝑚 = ( log ‘ 𝑛 ) ) |
| 29 |
|
oveq2 |
⊢ ( 𝑚 = ( log ‘ 𝑛 ) → ( ( exp ‘ 𝐴 ) ↑𝑐 𝑚 ) = ( ( exp ‘ 𝐴 ) ↑𝑐 ( log ‘ 𝑛 ) ) ) |
| 30 |
28 29
|
oveq12d |
⊢ ( 𝑚 = ( log ‘ 𝑛 ) → ( 𝑚 / ( ( exp ‘ 𝐴 ) ↑𝑐 𝑚 ) ) = ( ( log ‘ 𝑛 ) / ( ( exp ‘ 𝐴 ) ↑𝑐 ( log ‘ 𝑛 ) ) ) ) |
| 31 |
30
|
fveq2d |
⊢ ( 𝑚 = ( log ‘ 𝑛 ) → ( abs ‘ ( 𝑚 / ( ( exp ‘ 𝐴 ) ↑𝑐 𝑚 ) ) ) = ( abs ‘ ( ( log ‘ 𝑛 ) / ( ( exp ‘ 𝐴 ) ↑𝑐 ( log ‘ 𝑛 ) ) ) ) ) |
| 32 |
31
|
breq1d |
⊢ ( 𝑚 = ( log ‘ 𝑛 ) → ( ( abs ‘ ( 𝑚 / ( ( exp ‘ 𝐴 ) ↑𝑐 𝑚 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( log ‘ 𝑛 ) / ( ( exp ‘ 𝐴 ) ↑𝑐 ( log ‘ 𝑛 ) ) ) ) < 𝑥 ) ) |
| 33 |
27 32
|
imbi12d |
⊢ ( 𝑚 = ( log ‘ 𝑛 ) → ( ( 𝑧 < 𝑚 → ( abs ‘ ( 𝑚 / ( ( exp ‘ 𝐴 ) ↑𝑐 𝑚 ) ) ) < 𝑥 ) ↔ ( 𝑧 < ( log ‘ 𝑛 ) → ( abs ‘ ( ( log ‘ 𝑛 ) / ( ( exp ‘ 𝐴 ) ↑𝑐 ( log ‘ 𝑛 ) ) ) ) < 𝑥 ) ) ) |
| 34 |
33
|
rspcv |
⊢ ( ( log ‘ 𝑛 ) ∈ ℝ+ → ( ∀ 𝑚 ∈ ℝ+ ( 𝑧 < 𝑚 → ( abs ‘ ( 𝑚 / ( ( exp ‘ 𝐴 ) ↑𝑐 𝑚 ) ) ) < 𝑥 ) → ( 𝑧 < ( log ‘ 𝑛 ) → ( abs ‘ ( ( log ‘ 𝑛 ) / ( ( exp ‘ 𝐴 ) ↑𝑐 ( log ‘ 𝑛 ) ) ) ) < 𝑥 ) ) ) |
| 35 |
22 34
|
syl |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → ( ∀ 𝑚 ∈ ℝ+ ( 𝑧 < 𝑚 → ( abs ‘ ( 𝑚 / ( ( exp ‘ 𝐴 ) ↑𝑐 𝑚 ) ) ) < 𝑥 ) → ( 𝑧 < ( log ‘ 𝑛 ) → ( abs ‘ ( ( log ‘ 𝑛 ) / ( ( exp ‘ 𝐴 ) ↑𝑐 ( log ‘ 𝑛 ) ) ) ) < 𝑥 ) ) ) |
| 36 |
26 35
|
mpid |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → ( ∀ 𝑚 ∈ ℝ+ ( 𝑧 < 𝑚 → ( abs ‘ ( 𝑚 / ( ( exp ‘ 𝐴 ) ↑𝑐 𝑚 ) ) ) < 𝑥 ) → ( abs ‘ ( ( log ‘ 𝑛 ) / ( ( exp ‘ 𝐴 ) ↑𝑐 ( log ‘ 𝑛 ) ) ) ) < 𝑥 ) ) |
| 37 |
1
|
ad2antrr |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → 𝐴 ∈ ℝ ) |
| 38 |
37
|
relogefd |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → ( log ‘ ( exp ‘ 𝐴 ) ) = 𝐴 ) |
| 39 |
38
|
oveq2d |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → ( ( log ‘ 𝑛 ) · ( log ‘ ( exp ‘ 𝐴 ) ) ) = ( ( log ‘ 𝑛 ) · 𝐴 ) ) |
| 40 |
22
|
rpcnd |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → ( log ‘ 𝑛 ) ∈ ℂ ) |
| 41 |
|
rpcn |
⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ ) |
| 42 |
41
|
ad2antrr |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → 𝐴 ∈ ℂ ) |
| 43 |
40 42
|
mulcomd |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → ( ( log ‘ 𝑛 ) · 𝐴 ) = ( 𝐴 · ( log ‘ 𝑛 ) ) ) |
| 44 |
39 43
|
eqtrd |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → ( ( log ‘ 𝑛 ) · ( log ‘ ( exp ‘ 𝐴 ) ) ) = ( 𝐴 · ( log ‘ 𝑛 ) ) ) |
| 45 |
44
|
fveq2d |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → ( exp ‘ ( ( log ‘ 𝑛 ) · ( log ‘ ( exp ‘ 𝐴 ) ) ) ) = ( exp ‘ ( 𝐴 · ( log ‘ 𝑛 ) ) ) ) |
| 46 |
3
|
ad2antrr |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → ( exp ‘ 𝐴 ) ∈ ℝ ) |
| 47 |
46
|
recnd |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → ( exp ‘ 𝐴 ) ∈ ℂ ) |
| 48 |
|
efne0 |
⊢ ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) ≠ 0 ) |
| 49 |
42 48
|
syl |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → ( exp ‘ 𝐴 ) ≠ 0 ) |
| 50 |
47 49 40
|
cxpefd |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → ( ( exp ‘ 𝐴 ) ↑𝑐 ( log ‘ 𝑛 ) ) = ( exp ‘ ( ( log ‘ 𝑛 ) · ( log ‘ ( exp ‘ 𝐴 ) ) ) ) ) |
| 51 |
|
rpcn |
⊢ ( 𝑛 ∈ ℝ+ → 𝑛 ∈ ℂ ) |
| 52 |
51
|
ad2antrl |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → 𝑛 ∈ ℂ ) |
| 53 |
|
rpne0 |
⊢ ( 𝑛 ∈ ℝ+ → 𝑛 ≠ 0 ) |
| 54 |
53
|
ad2antrl |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → 𝑛 ≠ 0 ) |
| 55 |
52 54 42
|
cxpefd |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → ( 𝑛 ↑𝑐 𝐴 ) = ( exp ‘ ( 𝐴 · ( log ‘ 𝑛 ) ) ) ) |
| 56 |
45 50 55
|
3eqtr4d |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → ( ( exp ‘ 𝐴 ) ↑𝑐 ( log ‘ 𝑛 ) ) = ( 𝑛 ↑𝑐 𝐴 ) ) |
| 57 |
56
|
oveq2d |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → ( ( log ‘ 𝑛 ) / ( ( exp ‘ 𝐴 ) ↑𝑐 ( log ‘ 𝑛 ) ) ) = ( ( log ‘ 𝑛 ) / ( 𝑛 ↑𝑐 𝐴 ) ) ) |
| 58 |
57
|
fveq2d |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → ( abs ‘ ( ( log ‘ 𝑛 ) / ( ( exp ‘ 𝐴 ) ↑𝑐 ( log ‘ 𝑛 ) ) ) ) = ( abs ‘ ( ( log ‘ 𝑛 ) / ( 𝑛 ↑𝑐 𝐴 ) ) ) ) |
| 59 |
58
|
breq1d |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → ( ( abs ‘ ( ( log ‘ 𝑛 ) / ( ( exp ‘ 𝐴 ) ↑𝑐 ( log ‘ 𝑛 ) ) ) ) < 𝑥 ↔ ( abs ‘ ( ( log ‘ 𝑛 ) / ( 𝑛 ↑𝑐 𝐴 ) ) ) < 𝑥 ) ) |
| 60 |
36 59
|
sylibd |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) ) ) → ( ∀ 𝑚 ∈ ℝ+ ( 𝑧 < 𝑚 → ( abs ‘ ( 𝑚 / ( ( exp ‘ 𝐴 ) ↑𝑐 𝑚 ) ) ) < 𝑥 ) → ( abs ‘ ( ( log ‘ 𝑛 ) / ( 𝑛 ↑𝑐 𝐴 ) ) ) < 𝑥 ) ) |
| 61 |
60
|
expr |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 1 < 𝑛 ∧ ( exp ‘ 𝑧 ) < 𝑛 ) → ( ∀ 𝑚 ∈ ℝ+ ( 𝑧 < 𝑚 → ( abs ‘ ( 𝑚 / ( ( exp ‘ 𝐴 ) ↑𝑐 𝑚 ) ) ) < 𝑥 ) → ( abs ‘ ( ( log ‘ 𝑛 ) / ( 𝑛 ↑𝑐 𝐴 ) ) ) < 𝑥 ) ) ) |
| 62 |
14 61
|
sylbid |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ 𝑛 ∈ ℝ+ ) → ( if ( 1 ≤ ( exp ‘ 𝑧 ) , ( exp ‘ 𝑧 ) , 1 ) < 𝑛 → ( ∀ 𝑚 ∈ ℝ+ ( 𝑧 < 𝑚 → ( abs ‘ ( 𝑚 / ( ( exp ‘ 𝐴 ) ↑𝑐 𝑚 ) ) ) < 𝑥 ) → ( abs ‘ ( ( log ‘ 𝑛 ) / ( 𝑛 ↑𝑐 𝐴 ) ) ) < 𝑥 ) ) ) |
| 63 |
62
|
com23 |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) ∧ 𝑛 ∈ ℝ+ ) → ( ∀ 𝑚 ∈ ℝ+ ( 𝑧 < 𝑚 → ( abs ‘ ( 𝑚 / ( ( exp ‘ 𝐴 ) ↑𝑐 𝑚 ) ) ) < 𝑥 ) → ( if ( 1 ≤ ( exp ‘ 𝑧 ) , ( exp ‘ 𝑧 ) , 1 ) < 𝑛 → ( abs ‘ ( ( log ‘ 𝑛 ) / ( 𝑛 ↑𝑐 𝐴 ) ) ) < 𝑥 ) ) ) |
| 64 |
63
|
ralrimdva |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) → ( ∀ 𝑚 ∈ ℝ+ ( 𝑧 < 𝑚 → ( abs ‘ ( 𝑚 / ( ( exp ‘ 𝐴 ) ↑𝑐 𝑚 ) ) ) < 𝑥 ) → ∀ 𝑛 ∈ ℝ+ ( if ( 1 ≤ ( exp ‘ 𝑧 ) , ( exp ‘ 𝑧 ) , 1 ) < 𝑛 → ( abs ‘ ( ( log ‘ 𝑛 ) / ( 𝑛 ↑𝑐 𝐴 ) ) ) < 𝑥 ) ) ) |
| 65 |
|
breq1 |
⊢ ( 𝑦 = if ( 1 ≤ ( exp ‘ 𝑧 ) , ( exp ‘ 𝑧 ) , 1 ) → ( 𝑦 < 𝑛 ↔ if ( 1 ≤ ( exp ‘ 𝑧 ) , ( exp ‘ 𝑧 ) , 1 ) < 𝑛 ) ) |
| 66 |
65
|
rspceaimv |
⊢ ( ( if ( 1 ≤ ( exp ‘ 𝑧 ) , ( exp ‘ 𝑧 ) , 1 ) ∈ ℝ ∧ ∀ 𝑛 ∈ ℝ+ ( if ( 1 ≤ ( exp ‘ 𝑧 ) , ( exp ‘ 𝑧 ) , 1 ) < 𝑛 → ( abs ‘ ( ( log ‘ 𝑛 ) / ( 𝑛 ↑𝑐 𝐴 ) ) ) < 𝑥 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ℝ+ ( 𝑦 < 𝑛 → ( abs ‘ ( ( log ‘ 𝑛 ) / ( 𝑛 ↑𝑐 𝐴 ) ) ) < 𝑥 ) ) |
| 67 |
11 64 66
|
syl6an |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑧 ∈ ℝ ) → ( ∀ 𝑚 ∈ ℝ+ ( 𝑧 < 𝑚 → ( abs ‘ ( 𝑚 / ( ( exp ‘ 𝐴 ) ↑𝑐 𝑚 ) ) ) < 𝑥 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ℝ+ ( 𝑦 < 𝑛 → ( abs ‘ ( ( log ‘ 𝑛 ) / ( 𝑛 ↑𝑐 𝐴 ) ) ) < 𝑥 ) ) ) |
| 68 |
67
|
rexlimdva |
⊢ ( 𝐴 ∈ ℝ+ → ( ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ ℝ+ ( 𝑧 < 𝑚 → ( abs ‘ ( 𝑚 / ( ( exp ‘ 𝐴 ) ↑𝑐 𝑚 ) ) ) < 𝑥 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ℝ+ ( 𝑦 < 𝑛 → ( abs ‘ ( ( log ‘ 𝑛 ) / ( 𝑛 ↑𝑐 𝐴 ) ) ) < 𝑥 ) ) ) |
| 69 |
68
|
ralimdv |
⊢ ( 𝐴 ∈ ℝ+ → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ ℝ+ ( 𝑧 < 𝑚 → ( abs ‘ ( 𝑚 / ( ( exp ‘ 𝐴 ) ↑𝑐 𝑚 ) ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ℝ+ ( 𝑦 < 𝑛 → ( abs ‘ ( ( log ‘ 𝑛 ) / ( 𝑛 ↑𝑐 𝐴 ) ) ) < 𝑥 ) ) ) |
| 70 |
|
simpr |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑚 ∈ ℝ+ ) → 𝑚 ∈ ℝ+ ) |
| 71 |
1
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑚 ∈ ℝ+ ) → 𝐴 ∈ ℝ ) |
| 72 |
71
|
rpefcld |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑚 ∈ ℝ+ ) → ( exp ‘ 𝐴 ) ∈ ℝ+ ) |
| 73 |
|
rpre |
⊢ ( 𝑚 ∈ ℝ+ → 𝑚 ∈ ℝ ) |
| 74 |
73
|
adantl |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑚 ∈ ℝ+ ) → 𝑚 ∈ ℝ ) |
| 75 |
72 74
|
rpcxpcld |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑚 ∈ ℝ+ ) → ( ( exp ‘ 𝐴 ) ↑𝑐 𝑚 ) ∈ ℝ+ ) |
| 76 |
70 75
|
rpdivcld |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑚 ∈ ℝ+ ) → ( 𝑚 / ( ( exp ‘ 𝐴 ) ↑𝑐 𝑚 ) ) ∈ ℝ+ ) |
| 77 |
76
|
rpcnd |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑚 ∈ ℝ+ ) → ( 𝑚 / ( ( exp ‘ 𝐴 ) ↑𝑐 𝑚 ) ) ∈ ℂ ) |
| 78 |
77
|
ralrimiva |
⊢ ( 𝐴 ∈ ℝ+ → ∀ 𝑚 ∈ ℝ+ ( 𝑚 / ( ( exp ‘ 𝐴 ) ↑𝑐 𝑚 ) ) ∈ ℂ ) |
| 79 |
|
rpssre |
⊢ ℝ+ ⊆ ℝ |
| 80 |
79
|
a1i |
⊢ ( 𝐴 ∈ ℝ+ → ℝ+ ⊆ ℝ ) |
| 81 |
78 80
|
rlim0lt |
⊢ ( 𝐴 ∈ ℝ+ → ( ( 𝑚 ∈ ℝ+ ↦ ( 𝑚 / ( ( exp ‘ 𝐴 ) ↑𝑐 𝑚 ) ) ) ⇝𝑟 0 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑧 ∈ ℝ ∀ 𝑚 ∈ ℝ+ ( 𝑧 < 𝑚 → ( abs ‘ ( 𝑚 / ( ( exp ‘ 𝐴 ) ↑𝑐 𝑚 ) ) ) < 𝑥 ) ) ) |
| 82 |
|
relogcl |
⊢ ( 𝑛 ∈ ℝ+ → ( log ‘ 𝑛 ) ∈ ℝ ) |
| 83 |
82
|
adantl |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) → ( log ‘ 𝑛 ) ∈ ℝ ) |
| 84 |
|
simpr |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) → 𝑛 ∈ ℝ+ ) |
| 85 |
1
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) → 𝐴 ∈ ℝ ) |
| 86 |
84 85
|
rpcxpcld |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 ↑𝑐 𝐴 ) ∈ ℝ+ ) |
| 87 |
83 86
|
rerpdivcld |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) → ( ( log ‘ 𝑛 ) / ( 𝑛 ↑𝑐 𝐴 ) ) ∈ ℝ ) |
| 88 |
87
|
recnd |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) → ( ( log ‘ 𝑛 ) / ( 𝑛 ↑𝑐 𝐴 ) ) ∈ ℂ ) |
| 89 |
88
|
ralrimiva |
⊢ ( 𝐴 ∈ ℝ+ → ∀ 𝑛 ∈ ℝ+ ( ( log ‘ 𝑛 ) / ( 𝑛 ↑𝑐 𝐴 ) ) ∈ ℂ ) |
| 90 |
89 80
|
rlim0lt |
⊢ ( 𝐴 ∈ ℝ+ → ( ( 𝑛 ∈ ℝ+ ↦ ( ( log ‘ 𝑛 ) / ( 𝑛 ↑𝑐 𝐴 ) ) ) ⇝𝑟 0 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ℝ+ ( 𝑦 < 𝑛 → ( abs ‘ ( ( log ‘ 𝑛 ) / ( 𝑛 ↑𝑐 𝐴 ) ) ) < 𝑥 ) ) ) |
| 91 |
69 81 90
|
3imtr4d |
⊢ ( 𝐴 ∈ ℝ+ → ( ( 𝑚 ∈ ℝ+ ↦ ( 𝑚 / ( ( exp ‘ 𝐴 ) ↑𝑐 𝑚 ) ) ) ⇝𝑟 0 → ( 𝑛 ∈ ℝ+ ↦ ( ( log ‘ 𝑛 ) / ( 𝑛 ↑𝑐 𝐴 ) ) ) ⇝𝑟 0 ) ) |
| 92 |
6 91
|
mpd |
⊢ ( 𝐴 ∈ ℝ+ → ( 𝑛 ∈ ℝ+ ↦ ( ( log ‘ 𝑛 ) / ( 𝑛 ↑𝑐 𝐴 ) ) ) ⇝𝑟 0 ) |