Metamath Proof Explorer

Theorem cxp2limlem

Description: A linear factor grows slower than any exponential with base greater than 1 . (Contributed by Mario Carneiro, 15-Sep-2014)

Ref Expression
Assertion cxp2limlem ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( 𝑛 ∈ ℝ+ ↦ ( 𝑛 / ( 𝐴 ↑𝑐 𝑛 ) ) ) ⇝𝑟 0 )

Proof

Step Hyp Ref Expression
1 0red ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 0 ∈ ℝ )
2 2rp ⊢ 2 ∈ ℝ+
3 rplogcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( log ‘ 𝐴 ) ∈ ℝ+ )
4 2z ⊢ 2 ∈ ℤ
5 rpexpcl ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( ( log ‘ 𝐴 ) ↑ 2 ) ∈ ℝ+ )
6 3 4 5 sylancl ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( ( log ‘ 𝐴 ) ↑ 2 ) ∈ ℝ+ )
7 rpdivcl ⊢ ( ( 2 ∈ ℝ+ ∧ ( ( log ‘ 𝐴 ) ↑ 2 ) ∈ ℝ+ ) → ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ∈ ℝ+ )
8 2 6 7 sylancr ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ∈ ℝ+ )
9 8 rpcnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ∈ ℂ )
10 divrcnv ⊢ ( ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ∈ ℂ → ( 𝑛 ∈ ℝ+ ↦ ( ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) / 𝑛 ) ) ⇝𝑟 0 )
11 9 10 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( 𝑛 ∈ ℝ+ ↦ ( ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) / 𝑛 ) ) ⇝𝑟 0 )
12 8 rpred ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ∈ ℝ )
13 rerpdivcl ⊢ ( ( ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ∈ ℝ ∧ 𝑛 ∈ ℝ+ ) → ( ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) / 𝑛 ) ∈ ℝ )
14 12 13 sylan ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) / 𝑛 ) ∈ ℝ )
15 simpr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → 𝑛 ∈ ℝ+ )
16 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 𝐴 ∈ ℝ )
17 1red ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 1 ∈ ℝ )
18 0lt1 ⊢ 0 < 1
19 18 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 0 < 1 )
20 simpr ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 1 < 𝐴 )
21 1 17 16 19 20 lttrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 0 < 𝐴 )
22 16 21 elrpd ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 𝐴 ∈ ℝ+ )
23 rpre ⊢ ( 𝑛 ∈ ℝ+ → 𝑛 ∈ ℝ )
24 rpcxpcl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑛 ∈ ℝ ) → ( 𝐴 ↑𝑐 𝑛 ) ∈ ℝ+ )
25 22 23 24 syl2an ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝐴 ↑𝑐 𝑛 ) ∈ ℝ+ )
26 15 25 rpdivcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 / ( 𝐴 ↑𝑐 𝑛 ) ) ∈ ℝ+ )
27 26 rpred ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 / ( 𝐴 ↑𝑐 𝑛 ) ) ∈ ℝ )
28 3 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( log ‘ 𝐴 ) ∈ ℝ+ )
29 15 28 rpmulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 · ( log ‘ 𝐴 ) ) ∈ ℝ+ )
30 29 rpred ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 · ( log ‘ 𝐴 ) ) ∈ ℝ )
31 30 resqcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝑛 · ( log ‘ 𝐴 ) ) ↑ 2 ) ∈ ℝ )
32 31 rehalfcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( ( 𝑛 · ( log ‘ 𝐴 ) ) ↑ 2 ) / 2 ) ∈ ℝ )
33 1rp ⊢ 1 ∈ ℝ+
34 rpaddcl ⊢ ( ( 1 ∈ ℝ+ ∧ ( 𝑛 · ( log ‘ 𝐴 ) ) ∈ ℝ+ ) → ( 1 + ( 𝑛 · ( log ‘ 𝐴 ) ) ) ∈ ℝ+ )
35 33 29 34 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 1 + ( 𝑛 · ( log ‘ 𝐴 ) ) ) ∈ ℝ+ )
36 35 rpred ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 1 + ( 𝑛 · ( log ‘ 𝐴 ) ) ) ∈ ℝ )
37 36 32 readdcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 1 + ( 𝑛 · ( log ‘ 𝐴 ) ) ) + ( ( ( 𝑛 · ( log ‘ 𝐴 ) ) ↑ 2 ) / 2 ) ) ∈ ℝ )
38 30 reefcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( exp ‘ ( 𝑛 · ( log ‘ 𝐴 ) ) ) ∈ ℝ )
39 32 35 ltaddrp2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( ( 𝑛 · ( log ‘ 𝐴 ) ) ↑ 2 ) / 2 ) < ( ( 1 + ( 𝑛 · ( log ‘ 𝐴 ) ) ) + ( ( ( 𝑛 · ( log ‘ 𝐴 ) ) ↑ 2 ) / 2 ) ) )
40 efgt1p2 ⊢ ( ( 𝑛 · ( log ‘ 𝐴 ) ) ∈ ℝ+ → ( ( 1 + ( 𝑛 · ( log ‘ 𝐴 ) ) ) + ( ( ( 𝑛 · ( log ‘ 𝐴 ) ) ↑ 2 ) / 2 ) ) < ( exp ‘ ( 𝑛 · ( log ‘ 𝐴 ) ) ) )
41 29 40 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 1 + ( 𝑛 · ( log ‘ 𝐴 ) ) ) + ( ( ( 𝑛 · ( log ‘ 𝐴 ) ) ↑ 2 ) / 2 ) ) < ( exp ‘ ( 𝑛 · ( log ‘ 𝐴 ) ) ) )
42 32 37 38 39 41 lttrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( ( 𝑛 · ( log ‘ 𝐴 ) ) ↑ 2 ) / 2 ) < ( exp ‘ ( 𝑛 · ( log ‘ 𝐴 ) ) ) )
43 23 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → 𝑛 ∈ ℝ )
44 43 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → 𝑛 ∈ ℂ )
45 44 sqcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 ↑ 2 ) ∈ ℂ )
46 2cnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → 2 ∈ ℂ )
47 6 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( log ‘ 𝐴 ) ↑ 2 ) ∈ ℝ+ )
48 47 rpcnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( log ‘ 𝐴 ) ↑ 2 ) ∈ ℂ )
49 2ne0 ⊢ 2 ≠ 0
50 49 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → 2 ≠ 0 )
51 47 rpne0d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( log ‘ 𝐴 ) ↑ 2 ) ≠ 0 )
52 45 46 48 50 51 divdiv2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝑛 ↑ 2 ) / ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ) = ( ( ( 𝑛 ↑ 2 ) · ( ( log ‘ 𝐴 ) ↑ 2 ) ) / 2 ) )
53 3 rpcnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( log ‘ 𝐴 ) ∈ ℂ )
54 53 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( log ‘ 𝐴 ) ∈ ℂ )
55 44 54 sqmuld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝑛 · ( log ‘ 𝐴 ) ) ↑ 2 ) = ( ( 𝑛 ↑ 2 ) · ( ( log ‘ 𝐴 ) ↑ 2 ) ) )
56 55 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( ( 𝑛 · ( log ‘ 𝐴 ) ) ↑ 2 ) / 2 ) = ( ( ( 𝑛 ↑ 2 ) · ( ( log ‘ 𝐴 ) ↑ 2 ) ) / 2 ) )
57 52 56 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝑛 ↑ 2 ) / ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ) = ( ( ( 𝑛 · ( log ‘ 𝐴 ) ) ↑ 2 ) / 2 ) )
58 16 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 𝐴 ∈ ℂ )
59 58 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → 𝐴 ∈ ℂ )
60 22 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → 𝐴 ∈ ℝ+ )
61 60 rpne0d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → 𝐴 ≠ 0 )
62 59 61 44 cxpefd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝐴 ↑𝑐 𝑛 ) = ( exp ‘ ( 𝑛 · ( log ‘ 𝐴 ) ) ) )
63 42 57 62 3brtr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝑛 ↑ 2 ) / ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ) < ( 𝐴 ↑𝑐 𝑛 ) )
64 rpexpcl ⊢ ( ( 𝑛 ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( 𝑛 ↑ 2 ) ∈ ℝ+ )
65 15 4 64 sylancl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 ↑ 2 ) ∈ ℝ+ )
66 8 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ∈ ℝ+ )
67 65 66 rpdivcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝑛 ↑ 2 ) / ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ) ∈ ℝ+ )
68 67 25 15 ltdiv2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( ( 𝑛 ↑ 2 ) / ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ) < ( 𝐴 ↑𝑐 𝑛 ) ↔ ( 𝑛 / ( 𝐴 ↑𝑐 𝑛 ) ) < ( 𝑛 / ( ( 𝑛 ↑ 2 ) / ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ) ) ) )
69 63 68 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 / ( 𝐴 ↑𝑐 𝑛 ) ) < ( 𝑛 / ( ( 𝑛 ↑ 2 ) / ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ) ) )
70 9 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ∈ ℂ )
71 65 rpne0d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 ↑ 2 ) ≠ 0 )
72 66 rpne0d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ≠ 0 )
73 44 45 70 71 72 divdiv2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 / ( ( 𝑛 ↑ 2 ) / ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ) ) = ( ( 𝑛 · ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ) / ( 𝑛 ↑ 2 ) ) )
74 44 sqvald ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 ↑ 2 ) = ( 𝑛 · 𝑛 ) )
75 74 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝑛 · ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ) / ( 𝑛 ↑ 2 ) ) = ( ( 𝑛 · ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ) / ( 𝑛 · 𝑛 ) ) )
76 rpne0 ⊢ ( 𝑛 ∈ ℝ+ → 𝑛 ≠ 0 )
77 76 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → 𝑛 ≠ 0 )
78 70 44 44 77 77 divcan5d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝑛 · ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ) / ( 𝑛 · 𝑛 ) ) = ( ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) / 𝑛 ) )
79 73 75 78 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 / ( ( 𝑛 ↑ 2 ) / ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ) ) = ( ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) / 𝑛 ) )
80 69 79 breqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 / ( 𝐴 ↑𝑐 𝑛 ) ) < ( ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) / 𝑛 ) )
81 27 14 80 ltled ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 / ( 𝐴 ↑𝑐 𝑛 ) ) ≤ ( ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) / 𝑛 ) )
82 81 adantrr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝑛 ∈ ℝ+ ∧ 0 ≤ 𝑛 ) ) → ( 𝑛 / ( 𝐴 ↑𝑐 𝑛 ) ) ≤ ( ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) / 𝑛 ) )
83 26 rpge0d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → 0 ≤ ( 𝑛 / ( 𝐴 ↑𝑐 𝑛 ) ) )
84 83 adantrr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝑛 ∈ ℝ+ ∧ 0 ≤ 𝑛 ) ) → 0 ≤ ( 𝑛 / ( 𝐴 ↑𝑐 𝑛 ) ) )
85 1 1 11 14 27 82 84 rlimsqz2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( 𝑛 ∈ ℝ+ ↦ ( 𝑛 / ( 𝐴 ↑𝑐 𝑛 ) ) ) ⇝𝑟 0 )