This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cxploglim

Description: The logarithm grows slower than any positive power. (Contributed by Mario Carneiro, 18-Sep-2014)

Ref Expression
Assertion cxploglim ( 𝐴 ∈ ℝ+ → ( 𝑛 ∈ ℝ+ ↦ ( ( log ‘ 𝑛 ) / ( 𝑛 ↑𝑐 𝐴 ) ) ) ⇝𝑟 0 )

Proof

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 )