Metamath Proof Explorer


Theorem cxp2lim

Description: Any power grows slower than any exponential with base greater than 1 . (Contributed by Mario Carneiro, 18-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 1re 1 ∈ ℝ
2 elicopnf ( 1 ∈ ℝ → ( 𝑛 ∈ ( 1 [,) +∞ ) ↔ ( 𝑛 ∈ ℝ ∧ 1 ≤ 𝑛 ) ) )
3 1 2 ax-mp ( 𝑛 ∈ ( 1 [,) +∞ ) ↔ ( 𝑛 ∈ ℝ ∧ 1 ≤ 𝑛 ) )
4 3 simplbi ( 𝑛 ∈ ( 1 [,) +∞ ) → 𝑛 ∈ ℝ )
5 0red ( 𝑛 ∈ ( 1 [,) +∞ ) → 0 ∈ ℝ )
6 1red ( 𝑛 ∈ ( 1 [,) +∞ ) → 1 ∈ ℝ )
7 0lt1 0 < 1
8 7 a1i ( 𝑛 ∈ ( 1 [,) +∞ ) → 0 < 1 )
9 3 simprbi ( 𝑛 ∈ ( 1 [,) +∞ ) → 1 ≤ 𝑛 )
10 5 6 4 8 9 ltletrd ( 𝑛 ∈ ( 1 [,) +∞ ) → 0 < 𝑛 )
11 4 10 elrpd ( 𝑛 ∈ ( 1 [,) +∞ ) → 𝑛 ∈ ℝ+ )
12 11 ssriv ( 1 [,) +∞ ) ⊆ ℝ+
13 resmpt ( ( 1 [,) +∞ ) ⊆ ℝ+ → ( ( 𝑛 ∈ ℝ+ ↦ ( ( 𝑛𝑐 𝐴 ) / ( 𝐵𝑐 𝑛 ) ) ) ↾ ( 1 [,) +∞ ) ) = ( 𝑛 ∈ ( 1 [,) +∞ ) ↦ ( ( 𝑛𝑐 𝐴 ) / ( 𝐵𝑐 𝑛 ) ) ) )
14 12 13 ax-mp ( ( 𝑛 ∈ ℝ+ ↦ ( ( 𝑛𝑐 𝐴 ) / ( 𝐵𝑐 𝑛 ) ) ) ↾ ( 1 [,) +∞ ) ) = ( 𝑛 ∈ ( 1 [,) +∞ ) ↦ ( ( 𝑛𝑐 𝐴 ) / ( 𝐵𝑐 𝑛 ) ) )
15 0red ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → 0 ∈ ℝ )
16 12 a1i ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( 1 [,) +∞ ) ⊆ ℝ+ )
17 rpre ( 𝑛 ∈ ℝ+𝑛 ∈ ℝ )
18 17 adantl ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → 𝑛 ∈ ℝ )
19 rpge0 ( 𝑛 ∈ ℝ+ → 0 ≤ 𝑛 )
20 19 adantl ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → 0 ≤ 𝑛 )
21 simpl2 ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → 𝐵 ∈ ℝ )
22 0red ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → 0 ∈ ℝ )
23 1red ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → 1 ∈ ℝ )
24 7 a1i ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → 0 < 1 )
25 simpl3 ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → 1 < 𝐵 )
26 22 23 21 24 25 lttrd ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → 0 < 𝐵 )
27 21 26 elrpd ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → 𝐵 ∈ ℝ+ )
28 27 18 rpcxpcld ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝐵𝑐 𝑛 ) ∈ ℝ+ )
29 simp1 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → 𝐴 ∈ ℝ )
30 ifcl ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ) → if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ∈ ℝ )
31 29 1 30 sylancl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ∈ ℝ )
32 1red ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → 1 ∈ ℝ )
33 7 a1i ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → 0 < 1 )
34 max1 ( ( 1 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → 1 ≤ if ( 1 ≤ 𝐴 , 𝐴 , 1 ) )
35 1 29 34 sylancr ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → 1 ≤ if ( 1 ≤ 𝐴 , 𝐴 , 1 ) )
36 15 32 31 33 35 ltletrd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → 0 < if ( 1 ≤ 𝐴 , 𝐴 , 1 ) )
37 31 36 elrpd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ∈ ℝ+ )
38 37 rprecred ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ∈ ℝ )
39 38 adantr ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ∈ ℝ )
40 28 39 rpcxpcld ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝐵𝑐 𝑛 ) ↑𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) ∈ ℝ+ )
41 31 recnd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ∈ ℂ )
42 41 adantr ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ∈ ℂ )
43 18 20 40 42 divcxpd ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝑛 / ( ( 𝐵𝑐 𝑛 ) ↑𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) ) ↑𝑐 if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) = ( ( 𝑛𝑐 if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) / ( ( ( 𝐵𝑐 𝑛 ) ↑𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) ↑𝑐 if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) )
44 37 adantr ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ∈ ℝ+ )
45 44 rpne0d ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ≠ 0 )
46 42 45 recid2d ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) · if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) = 1 )
47 46 oveq2d ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝐵𝑐 𝑛 ) ↑𝑐 ( ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) · if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) = ( ( 𝐵𝑐 𝑛 ) ↑𝑐 1 ) )
48 28 39 42 cxpmuld ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝐵𝑐 𝑛 ) ↑𝑐 ( ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) · if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) = ( ( ( 𝐵𝑐 𝑛 ) ↑𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) ↑𝑐 if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) )
49 28 rpcnd ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝐵𝑐 𝑛 ) ∈ ℂ )
50 49 cxp1d ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝐵𝑐 𝑛 ) ↑𝑐 1 ) = ( 𝐵𝑐 𝑛 ) )
51 47 48 50 3eqtr3d ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( ( 𝐵𝑐 𝑛 ) ↑𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) ↑𝑐 if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) = ( 𝐵𝑐 𝑛 ) )
52 51 oveq2d ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝑛𝑐 if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) / ( ( ( 𝐵𝑐 𝑛 ) ↑𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) ↑𝑐 if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) = ( ( 𝑛𝑐 if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) / ( 𝐵𝑐 𝑛 ) ) )
53 43 52 eqtrd ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝑛 / ( ( 𝐵𝑐 𝑛 ) ↑𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) ) ↑𝑐 if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) = ( ( 𝑛𝑐 if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) / ( 𝐵𝑐 𝑛 ) ) )
54 53 mpteq2dva ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( 𝑛 ∈ ℝ+ ↦ ( ( 𝑛 / ( ( 𝐵𝑐 𝑛 ) ↑𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) ) ↑𝑐 if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) = ( 𝑛 ∈ ℝ+ ↦ ( ( 𝑛𝑐 if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) / ( 𝐵𝑐 𝑛 ) ) ) )
55 ovexd ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 / ( ( 𝐵𝑐 𝑛 ) ↑𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) ) ∈ V )
56 18 recnd ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → 𝑛 ∈ ℂ )
57 38 recnd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ∈ ℂ )
58 57 adantr ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ∈ ℂ )
59 56 58 mulcomd ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 · ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) = ( ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) · 𝑛 ) )
60 59 oveq2d ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝐵𝑐 ( 𝑛 · ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) ) = ( 𝐵𝑐 ( ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) · 𝑛 ) ) )
61 27 18 58 cxpmuld ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝐵𝑐 ( 𝑛 · ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) ) = ( ( 𝐵𝑐 𝑛 ) ↑𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) )
62 27 39 56 cxpmuld ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝐵𝑐 ( ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) · 𝑛 ) ) = ( ( 𝐵𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) ↑𝑐 𝑛 ) )
63 60 61 62 3eqtr3d ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝐵𝑐 𝑛 ) ↑𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) = ( ( 𝐵𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) ↑𝑐 𝑛 ) )
64 63 oveq2d ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 / ( ( 𝐵𝑐 𝑛 ) ↑𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) ) = ( 𝑛 / ( ( 𝐵𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) ↑𝑐 𝑛 ) ) )
65 64 mpteq2dva ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( 𝑛 ∈ ℝ+ ↦ ( 𝑛 / ( ( 𝐵𝑐 𝑛 ) ↑𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) ) ) = ( 𝑛 ∈ ℝ+ ↦ ( 𝑛 / ( ( 𝐵𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) ↑𝑐 𝑛 ) ) ) )
66 simp2 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → 𝐵 ∈ ℝ )
67 simp3 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → 1 < 𝐵 )
68 15 32 66 33 67 lttrd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → 0 < 𝐵 )
69 66 68 elrpd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → 𝐵 ∈ ℝ+ )
70 69 38 rpcxpcld ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( 𝐵𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) ∈ ℝ+ )
71 70 rpred ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( 𝐵𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) ∈ ℝ )
72 57 1cxpd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( 1 ↑𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) = 1 )
73 0le1 0 ≤ 1
74 73 a1i ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → 0 ≤ 1 )
75 69 rpge0d ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → 0 ≤ 𝐵 )
76 37 rpreccld ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ∈ ℝ+ )
77 32 74 66 75 76 cxplt2d ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( 1 < 𝐵 ↔ ( 1 ↑𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) < ( 𝐵𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) ) )
78 67 77 mpbid ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( 1 ↑𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) < ( 𝐵𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) )
79 72 78 eqbrtrrd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → 1 < ( 𝐵𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) )
80 cxp2limlem ( ( ( 𝐵𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) ∈ ℝ ∧ 1 < ( 𝐵𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) ) → ( 𝑛 ∈ ℝ+ ↦ ( 𝑛 / ( ( 𝐵𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) ↑𝑐 𝑛 ) ) ) ⇝𝑟 0 )
81 71 79 80 syl2anc ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( 𝑛 ∈ ℝ+ ↦ ( 𝑛 / ( ( 𝐵𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) ↑𝑐 𝑛 ) ) ) ⇝𝑟 0 )
82 65 81 eqbrtrd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( 𝑛 ∈ ℝ+ ↦ ( 𝑛 / ( ( 𝐵𝑐 𝑛 ) ↑𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) ) ) ⇝𝑟 0 )
83 55 82 37 rlimcxp ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( 𝑛 ∈ ℝ+ ↦ ( ( 𝑛 / ( ( 𝐵𝑐 𝑛 ) ↑𝑐 ( 1 / if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) ) ↑𝑐 if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ) ⇝𝑟 0 )
84 54 83 eqbrtrrd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( 𝑛 ∈ ℝ+ ↦ ( ( 𝑛𝑐 if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) / ( 𝐵𝑐 𝑛 ) ) ) ⇝𝑟 0 )
85 16 84 rlimres2 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( 𝑛 ∈ ( 1 [,) +∞ ) ↦ ( ( 𝑛𝑐 if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) / ( 𝐵𝑐 𝑛 ) ) ) ⇝𝑟 0 )
86 simpr ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → 𝑛 ∈ ℝ+ )
87 31 adantr ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ∈ ℝ )
88 86 87 rpcxpcld ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛𝑐 if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ∈ ℝ+ )
89 88 28 rpdivcld ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝑛𝑐 if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) / ( 𝐵𝑐 𝑛 ) ) ∈ ℝ+ )
90 89 rpred ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝑛𝑐 if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) / ( 𝐵𝑐 𝑛 ) ) ∈ ℝ )
91 11 90 sylan2 ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ( 1 [,) +∞ ) ) → ( ( 𝑛𝑐 if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) / ( 𝐵𝑐 𝑛 ) ) ∈ ℝ )
92 simpl1 ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
93 86 92 rpcxpcld ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛𝑐 𝐴 ) ∈ ℝ+ )
94 93 28 rpdivcld ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝑛𝑐 𝐴 ) / ( 𝐵𝑐 𝑛 ) ) ∈ ℝ+ )
95 11 94 sylan2 ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ( 1 [,) +∞ ) ) → ( ( 𝑛𝑐 𝐴 ) / ( 𝐵𝑐 𝑛 ) ) ∈ ℝ+ )
96 95 rpred ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ( 1 [,) +∞ ) ) → ( ( 𝑛𝑐 𝐴 ) / ( 𝐵𝑐 𝑛 ) ) ∈ ℝ )
97 11 93 sylan2 ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ( 1 [,) +∞ ) ) → ( 𝑛𝑐 𝐴 ) ∈ ℝ+ )
98 97 rpred ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ( 1 [,) +∞ ) ) → ( 𝑛𝑐 𝐴 ) ∈ ℝ )
99 11 88 sylan2 ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ( 1 [,) +∞ ) ) → ( 𝑛𝑐 if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ∈ ℝ+ )
100 99 rpred ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ( 1 [,) +∞ ) ) → ( 𝑛𝑐 if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) ∈ ℝ )
101 11 28 sylan2 ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ( 1 [,) +∞ ) ) → ( 𝐵𝑐 𝑛 ) ∈ ℝ+ )
102 4 adantl ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ( 1 [,) +∞ ) ) → 𝑛 ∈ ℝ )
103 9 adantl ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ( 1 [,) +∞ ) ) → 1 ≤ 𝑛 )
104 simpl1 ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ( 1 [,) +∞ ) ) → 𝐴 ∈ ℝ )
105 31 adantr ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ( 1 [,) +∞ ) ) → if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ∈ ℝ )
106 max2 ( ( 1 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → 𝐴 ≤ if ( 1 ≤ 𝐴 , 𝐴 , 1 ) )
107 1 104 106 sylancr ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ( 1 [,) +∞ ) ) → 𝐴 ≤ if ( 1 ≤ 𝐴 , 𝐴 , 1 ) )
108 102 103 104 105 107 cxplead ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ( 1 [,) +∞ ) ) → ( 𝑛𝑐 𝐴 ) ≤ ( 𝑛𝑐 if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) )
109 98 100 101 108 lediv1dd ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ( 1 [,) +∞ ) ) → ( ( 𝑛𝑐 𝐴 ) / ( 𝐵𝑐 𝑛 ) ) ≤ ( ( 𝑛𝑐 if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) / ( 𝐵𝑐 𝑛 ) ) )
110 109 adantrr ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ( 1 [,) +∞ ) ∧ 0 ≤ 𝑛 ) ) → ( ( 𝑛𝑐 𝐴 ) / ( 𝐵𝑐 𝑛 ) ) ≤ ( ( 𝑛𝑐 if ( 1 ≤ 𝐴 , 𝐴 , 1 ) ) / ( 𝐵𝑐 𝑛 ) ) )
111 95 rpge0d ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ( 1 [,) +∞ ) ) → 0 ≤ ( ( 𝑛𝑐 𝐴 ) / ( 𝐵𝑐 𝑛 ) ) )
112 111 adantrr ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ( 1 [,) +∞ ) ∧ 0 ≤ 𝑛 ) ) → 0 ≤ ( ( 𝑛𝑐 𝐴 ) / ( 𝐵𝑐 𝑛 ) ) )
113 15 15 85 91 96 110 112 rlimsqz2 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( 𝑛 ∈ ( 1 [,) +∞ ) ↦ ( ( 𝑛𝑐 𝐴 ) / ( 𝐵𝑐 𝑛 ) ) ) ⇝𝑟 0 )
114 14 113 eqbrtrid ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( ( 𝑛 ∈ ℝ+ ↦ ( ( 𝑛𝑐 𝐴 ) / ( 𝐵𝑐 𝑛 ) ) ) ↾ ( 1 [,) +∞ ) ) ⇝𝑟 0 )
115 94 rpcnd ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝑛𝑐 𝐴 ) / ( 𝐵𝑐 𝑛 ) ) ∈ ℂ )
116 115 fmpttd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( 𝑛 ∈ ℝ+ ↦ ( ( 𝑛𝑐 𝐴 ) / ( 𝐵𝑐 𝑛 ) ) ) : ℝ+ ⟶ ℂ )
117 rpssre + ⊆ ℝ
118 117 a1i ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ℝ+ ⊆ ℝ )
119 116 118 32 rlimresb ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( ( 𝑛 ∈ ℝ+ ↦ ( ( 𝑛𝑐 𝐴 ) / ( 𝐵𝑐 𝑛 ) ) ) ⇝𝑟 0 ↔ ( ( 𝑛 ∈ ℝ+ ↦ ( ( 𝑛𝑐 𝐴 ) / ( 𝐵𝑐 𝑛 ) ) ) ↾ ( 1 [,) +∞ ) ) ⇝𝑟 0 ) )
120 114 119 mpbird ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( 𝑛 ∈ ℝ+ ↦ ( ( 𝑛𝑐 𝐴 ) / ( 𝐵𝑐 𝑛 ) ) ) ⇝𝑟 0 )