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 )