Proof of Theorem cxp2lim
Step | Hyp | Ref
| Expression |
1 | | 1re 9918 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
2 | | elicopnf 12140 |
. . . . . . . 8
⊢ (1 ∈
ℝ → (𝑛 ∈
(1[,)+∞) ↔ (𝑛
∈ ℝ ∧ 1 ≤ 𝑛))) |
3 | 1, 2 | ax-mp 5 |
. . . . . . 7
⊢ (𝑛 ∈ (1[,)+∞) ↔
(𝑛 ∈ ℝ ∧ 1
≤ 𝑛)) |
4 | 3 | simplbi 475 |
. . . . . 6
⊢ (𝑛 ∈ (1[,)+∞) →
𝑛 ∈
ℝ) |
5 | | 0red 9920 |
. . . . . . 7
⊢ (𝑛 ∈ (1[,)+∞) → 0
∈ ℝ) |
6 | 1 | a1i 11 |
. . . . . . 7
⊢ (𝑛 ∈ (1[,)+∞) → 1
∈ ℝ) |
7 | | 0lt1 10429 |
. . . . . . . 8
⊢ 0 <
1 |
8 | 7 | a1i 11 |
. . . . . . 7
⊢ (𝑛 ∈ (1[,)+∞) → 0
< 1) |
9 | 3 | simprbi 479 |
. . . . . . 7
⊢ (𝑛 ∈ (1[,)+∞) → 1
≤ 𝑛) |
10 | 5, 6, 4, 8, 9 | ltletrd 10076 |
. . . . . 6
⊢ (𝑛 ∈ (1[,)+∞) → 0
< 𝑛) |
11 | 4, 10 | elrpd 11745 |
. . . . 5
⊢ (𝑛 ∈ (1[,)+∞) →
𝑛 ∈
ℝ+) |
12 | 11 | ssriv 3572 |
. . . 4
⊢
(1[,)+∞) ⊆ ℝ+ |
13 | | resmpt 5369 |
. . . 4
⊢
((1[,)+∞) ⊆ ℝ+ → ((𝑛 ∈ ℝ+ ↦ ((𝑛↑𝑐𝐴) / (𝐵↑𝑐𝑛))) ↾ (1[,)+∞)) = (𝑛 ∈ (1[,)+∞) ↦
((𝑛↑𝑐𝐴) / (𝐵↑𝑐𝑛)))) |
14 | 12, 13 | ax-mp 5 |
. . 3
⊢ ((𝑛 ∈ ℝ+
↦ ((𝑛↑𝑐𝐴) / (𝐵↑𝑐𝑛))) ↾ (1[,)+∞)) = (𝑛 ∈ (1[,)+∞) ↦
((𝑛↑𝑐𝐴) / (𝐵↑𝑐𝑛))) |
15 | | 0red 9920 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → 0 ∈
ℝ) |
16 | 12 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → (1[,)+∞)
⊆ ℝ+) |
17 | | rpre 11715 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ+
→ 𝑛 ∈
ℝ) |
18 | 17 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → 𝑛 ∈
ℝ) |
19 | | rpge0 11721 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ+
→ 0 ≤ 𝑛) |
20 | 19 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → 0 ≤
𝑛) |
21 | | simpl2 1058 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → 𝐵 ∈
ℝ) |
22 | | 0red 9920 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → 0 ∈
ℝ) |
23 | 1 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → 1 ∈
ℝ) |
24 | 7 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → 0 <
1) |
25 | | simpl3 1059 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → 1 <
𝐵) |
26 | 22, 23, 21, 24, 25 | lttrd 10077 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → 0 <
𝐵) |
27 | 21, 26 | elrpd 11745 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → 𝐵 ∈
ℝ+) |
28 | 27, 18 | rpcxpcld 24276 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → (𝐵↑𝑐𝑛) ∈
ℝ+) |
29 | | simp1 1054 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → 𝐴 ∈ ℝ) |
30 | | ifcl 4080 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ) → if(1 ≤ 𝐴, 𝐴, 1) ∈ ℝ) |
31 | 29, 1, 30 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → if(1 ≤ 𝐴, 𝐴, 1) ∈ ℝ) |
32 | 1 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → 1 ∈
ℝ) |
33 | 7 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → 0 <
1) |
34 | | max1 11890 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℝ ∧ 𝐴
∈ ℝ) → 1 ≤ if(1 ≤ 𝐴, 𝐴, 1)) |
35 | 1, 29, 34 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → 1 ≤ if(1 ≤
𝐴, 𝐴, 1)) |
36 | 15, 32, 31, 33, 35 | ltletrd 10076 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → 0 < if(1 ≤
𝐴, 𝐴, 1)) |
37 | 31, 36 | elrpd 11745 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → if(1 ≤ 𝐴, 𝐴, 1) ∈
ℝ+) |
38 | 37 | rprecred 11759 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → (1 / if(1 ≤
𝐴, 𝐴, 1)) ∈ ℝ) |
39 | 38 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → (1 / if(1
≤ 𝐴, 𝐴, 1)) ∈ ℝ) |
40 | 28, 39 | rpcxpcld 24276 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → ((𝐵↑𝑐𝑛)↑𝑐(1 /
if(1 ≤ 𝐴, 𝐴, 1))) ∈
ℝ+) |
41 | 31 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → if(1 ≤ 𝐴, 𝐴, 1) ∈ ℂ) |
42 | 41 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → if(1 ≤
𝐴, 𝐴, 1) ∈ ℂ) |
43 | 18, 20, 40, 42 | divcxpd 24268 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → ((𝑛 / ((𝐵↑𝑐𝑛)↑𝑐(1 / if(1 ≤
𝐴, 𝐴, 1))))↑𝑐if(1 ≤
𝐴, 𝐴, 1)) = ((𝑛↑𝑐if(1 ≤ 𝐴, 𝐴, 1)) / (((𝐵↑𝑐𝑛)↑𝑐(1 / if(1 ≤
𝐴, 𝐴, 1)))↑𝑐if(1 ≤
𝐴, 𝐴, 1)))) |
44 | 37 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → if(1 ≤
𝐴, 𝐴, 1) ∈
ℝ+) |
45 | 44 | rpne0d 11753 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → if(1 ≤
𝐴, 𝐴, 1) ≠ 0) |
46 | 42, 45 | recid2d 10676 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → ((1 /
if(1 ≤ 𝐴, 𝐴, 1)) · if(1 ≤ 𝐴, 𝐴, 1)) = 1) |
47 | 46 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → ((𝐵↑𝑐𝑛)↑𝑐((1 /
if(1 ≤ 𝐴, 𝐴, 1)) · if(1 ≤ 𝐴, 𝐴, 1))) = ((𝐵↑𝑐𝑛)↑𝑐1)) |
48 | 28, 39, 42 | cxpmuld 24280 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → ((𝐵↑𝑐𝑛)↑𝑐((1 /
if(1 ≤ 𝐴, 𝐴, 1)) · if(1 ≤ 𝐴, 𝐴, 1))) = (((𝐵↑𝑐𝑛)↑𝑐(1 / if(1 ≤
𝐴, 𝐴, 1)))↑𝑐if(1 ≤
𝐴, 𝐴, 1))) |
49 | 28 | rpcnd 11750 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → (𝐵↑𝑐𝑛) ∈
ℂ) |
50 | 49 | cxp1d 24252 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → ((𝐵↑𝑐𝑛)↑𝑐1) =
(𝐵↑𝑐𝑛)) |
51 | 47, 48, 50 | 3eqtr3d 2652 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → (((𝐵↑𝑐𝑛)↑𝑐(1 /
if(1 ≤ 𝐴, 𝐴,
1)))↑𝑐if(1 ≤ 𝐴, 𝐴, 1)) = (𝐵↑𝑐𝑛)) |
52 | 51 | oveq2d 6565 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → ((𝑛↑𝑐if(1
≤ 𝐴, 𝐴, 1)) / (((𝐵↑𝑐𝑛)↑𝑐(1 / if(1 ≤
𝐴, 𝐴, 1)))↑𝑐if(1 ≤
𝐴, 𝐴, 1))) = ((𝑛↑𝑐if(1 ≤ 𝐴, 𝐴, 1)) / (𝐵↑𝑐𝑛))) |
53 | 43, 52 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → ((𝑛 / ((𝐵↑𝑐𝑛)↑𝑐(1 / if(1 ≤
𝐴, 𝐴, 1))))↑𝑐if(1 ≤
𝐴, 𝐴, 1)) = ((𝑛↑𝑐if(1 ≤ 𝐴, 𝐴, 1)) / (𝐵↑𝑐𝑛))) |
54 | 53 | mpteq2dva 4672 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → (𝑛 ∈ ℝ+
↦ ((𝑛 / ((𝐵↑𝑐𝑛)↑𝑐(1 /
if(1 ≤ 𝐴, 𝐴,
1))))↑𝑐if(1 ≤ 𝐴, 𝐴, 1))) = (𝑛 ∈ ℝ+ ↦ ((𝑛↑𝑐if(1
≤ 𝐴, 𝐴, 1)) / (𝐵↑𝑐𝑛)))) |
55 | | ovex 6577 |
. . . . . . . 8
⊢ (𝑛 / ((𝐵↑𝑐𝑛)↑𝑐(1 / if(1 ≤
𝐴, 𝐴, 1)))) ∈ V |
56 | 55 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → (𝑛 / ((𝐵↑𝑐𝑛)↑𝑐(1 / if(1 ≤
𝐴, 𝐴, 1)))) ∈ V) |
57 | 18 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → 𝑛 ∈
ℂ) |
58 | 38 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → (1 / if(1 ≤
𝐴, 𝐴, 1)) ∈ ℂ) |
59 | 58 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → (1 / if(1
≤ 𝐴, 𝐴, 1)) ∈ ℂ) |
60 | 57, 59 | mulcomd 9940 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → (𝑛 · (1 / if(1 ≤ 𝐴, 𝐴, 1))) = ((1 / if(1 ≤ 𝐴, 𝐴, 1)) · 𝑛)) |
61 | 60 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → (𝐵↑𝑐(𝑛 · (1 / if(1 ≤ 𝐴, 𝐴, 1)))) = (𝐵↑𝑐((1 / if(1 ≤
𝐴, 𝐴, 1)) · 𝑛))) |
62 | 27, 18, 59 | cxpmuld 24280 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → (𝐵↑𝑐(𝑛 · (1 / if(1 ≤ 𝐴, 𝐴, 1)))) = ((𝐵↑𝑐𝑛)↑𝑐(1 / if(1 ≤
𝐴, 𝐴, 1)))) |
63 | 27, 39, 57 | cxpmuld 24280 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → (𝐵↑𝑐((1 /
if(1 ≤ 𝐴, 𝐴, 1)) · 𝑛)) = ((𝐵↑𝑐(1 / if(1 ≤
𝐴, 𝐴, 1)))↑𝑐𝑛)) |
64 | 61, 62, 63 | 3eqtr3d 2652 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → ((𝐵↑𝑐𝑛)↑𝑐(1 /
if(1 ≤ 𝐴, 𝐴, 1))) = ((𝐵↑𝑐(1 / if(1 ≤
𝐴, 𝐴, 1)))↑𝑐𝑛)) |
65 | 64 | oveq2d 6565 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → (𝑛 / ((𝐵↑𝑐𝑛)↑𝑐(1 / if(1 ≤
𝐴, 𝐴, 1)))) = (𝑛 / ((𝐵↑𝑐(1 / if(1 ≤
𝐴, 𝐴, 1)))↑𝑐𝑛))) |
66 | 65 | mpteq2dva 4672 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → (𝑛 ∈ ℝ+
↦ (𝑛 / ((𝐵↑𝑐𝑛)↑𝑐(1 /
if(1 ≤ 𝐴, 𝐴, 1))))) = (𝑛 ∈ ℝ+ ↦ (𝑛 / ((𝐵↑𝑐(1 / if(1 ≤
𝐴, 𝐴, 1)))↑𝑐𝑛)))) |
67 | | simp2 1055 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → 𝐵 ∈ ℝ) |
68 | | simp3 1056 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → 1 < 𝐵) |
69 | 15, 32, 67, 33, 68 | lttrd 10077 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → 0 < 𝐵) |
70 | 67, 69 | elrpd 11745 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → 𝐵 ∈
ℝ+) |
71 | 70, 38 | rpcxpcld 24276 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → (𝐵↑𝑐(1 /
if(1 ≤ 𝐴, 𝐴, 1))) ∈
ℝ+) |
72 | 71 | rpred 11748 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → (𝐵↑𝑐(1 /
if(1 ≤ 𝐴, 𝐴, 1))) ∈
ℝ) |
73 | 58 | 1cxpd 24253 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) →
(1↑𝑐(1 / if(1 ≤ 𝐴, 𝐴, 1))) = 1) |
74 | | 0le1 10430 |
. . . . . . . . . . . . 13
⊢ 0 ≤
1 |
75 | 74 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → 0 ≤
1) |
76 | 70 | rpge0d 11752 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → 0 ≤ 𝐵) |
77 | 37 | rpreccld 11758 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → (1 / if(1 ≤
𝐴, 𝐴, 1)) ∈
ℝ+) |
78 | 32, 75, 67, 76, 77 | cxplt2d 24272 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → (1 < 𝐵 ↔
(1↑𝑐(1 / if(1 ≤ 𝐴, 𝐴, 1))) < (𝐵↑𝑐(1 / if(1 ≤
𝐴, 𝐴, 1))))) |
79 | 68, 78 | mpbid 221 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) →
(1↑𝑐(1 / if(1 ≤ 𝐴, 𝐴, 1))) < (𝐵↑𝑐(1 / if(1 ≤
𝐴, 𝐴, 1)))) |
80 | 73, 79 | eqbrtrrd 4607 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → 1 < (𝐵↑𝑐(1 /
if(1 ≤ 𝐴, 𝐴, 1)))) |
81 | | cxp2limlem 24502 |
. . . . . . . . 9
⊢ (((𝐵↑𝑐(1 /
if(1 ≤ 𝐴, 𝐴, 1))) ∈ ℝ ∧ 1
< (𝐵↑𝑐(1 / if(1 ≤
𝐴, 𝐴, 1)))) → (𝑛 ∈ ℝ+ ↦ (𝑛 / ((𝐵↑𝑐(1 / if(1 ≤
𝐴, 𝐴, 1)))↑𝑐𝑛))) ⇝𝑟
0) |
82 | 72, 80, 81 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → (𝑛 ∈ ℝ+
↦ (𝑛 / ((𝐵↑𝑐(1 /
if(1 ≤ 𝐴, 𝐴,
1)))↑𝑐𝑛))) ⇝𝑟
0) |
83 | 66, 82 | eqbrtrd 4605 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → (𝑛 ∈ ℝ+
↦ (𝑛 / ((𝐵↑𝑐𝑛)↑𝑐(1 /
if(1 ≤ 𝐴, 𝐴, 1)))))
⇝𝑟 0) |
84 | 56, 83, 37 | rlimcxp 24500 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → (𝑛 ∈ ℝ+
↦ ((𝑛 / ((𝐵↑𝑐𝑛)↑𝑐(1 /
if(1 ≤ 𝐴, 𝐴,
1))))↑𝑐if(1 ≤ 𝐴, 𝐴, 1))) ⇝𝑟
0) |
85 | 54, 84 | eqbrtrrd 4607 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → (𝑛 ∈ ℝ+
↦ ((𝑛↑𝑐if(1 ≤ 𝐴, 𝐴, 1)) / (𝐵↑𝑐𝑛))) ⇝𝑟
0) |
86 | 16, 85 | rlimres2 14140 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → (𝑛 ∈ (1[,)+∞) ↦
((𝑛↑𝑐if(1 ≤ 𝐴, 𝐴, 1)) / (𝐵↑𝑐𝑛))) ⇝𝑟
0) |
87 | | simpr 476 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → 𝑛 ∈
ℝ+) |
88 | 31 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → if(1 ≤
𝐴, 𝐴, 1) ∈ ℝ) |
89 | 87, 88 | rpcxpcld 24276 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → (𝑛↑𝑐if(1
≤ 𝐴, 𝐴, 1)) ∈
ℝ+) |
90 | 89, 28 | rpdivcld 11765 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → ((𝑛↑𝑐if(1
≤ 𝐴, 𝐴, 1)) / (𝐵↑𝑐𝑛)) ∈
ℝ+) |
91 | 90 | rpred 11748 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → ((𝑛↑𝑐if(1
≤ 𝐴, 𝐴, 1)) / (𝐵↑𝑐𝑛)) ∈ ℝ) |
92 | 11, 91 | sylan2 490 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ (1[,)+∞)) → ((𝑛↑𝑐if(1
≤ 𝐴, 𝐴, 1)) / (𝐵↑𝑐𝑛)) ∈ ℝ) |
93 | | simpl1 1057 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈
ℝ) |
94 | 87, 93 | rpcxpcld 24276 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → (𝑛↑𝑐𝐴) ∈
ℝ+) |
95 | 94, 28 | rpdivcld 11765 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → ((𝑛↑𝑐𝐴) / (𝐵↑𝑐𝑛)) ∈
ℝ+) |
96 | 11, 95 | sylan2 490 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ (1[,)+∞)) → ((𝑛↑𝑐𝐴) / (𝐵↑𝑐𝑛)) ∈
ℝ+) |
97 | 96 | rpred 11748 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ (1[,)+∞)) → ((𝑛↑𝑐𝐴) / (𝐵↑𝑐𝑛)) ∈ ℝ) |
98 | 11, 94 | sylan2 490 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ (1[,)+∞)) → (𝑛↑𝑐𝐴) ∈
ℝ+) |
99 | 98 | rpred 11748 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ (1[,)+∞)) → (𝑛↑𝑐𝐴) ∈
ℝ) |
100 | 11, 89 | sylan2 490 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ (1[,)+∞)) → (𝑛↑𝑐if(1
≤ 𝐴, 𝐴, 1)) ∈
ℝ+) |
101 | 100 | rpred 11748 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ (1[,)+∞)) → (𝑛↑𝑐if(1
≤ 𝐴, 𝐴, 1)) ∈ ℝ) |
102 | 11, 28 | sylan2 490 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ (1[,)+∞)) → (𝐵↑𝑐𝑛) ∈
ℝ+) |
103 | 4 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ (1[,)+∞)) → 𝑛 ∈
ℝ) |
104 | 9 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ (1[,)+∞)) → 1 ≤ 𝑛) |
105 | | simpl1 1057 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ (1[,)+∞)) → 𝐴 ∈
ℝ) |
106 | 31 | adantr 480 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ (1[,)+∞)) → if(1 ≤
𝐴, 𝐴, 1) ∈ ℝ) |
107 | | max2 11892 |
. . . . . . . 8
⊢ ((1
∈ ℝ ∧ 𝐴
∈ ℝ) → 𝐴
≤ if(1 ≤ 𝐴, 𝐴, 1)) |
108 | 1, 105, 107 | sylancr 694 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ (1[,)+∞)) → 𝐴 ≤ if(1 ≤ 𝐴, 𝐴, 1)) |
109 | 103, 104,
105, 106, 108 | cxplead 24267 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ (1[,)+∞)) → (𝑛↑𝑐𝐴) ≤ (𝑛↑𝑐if(1 ≤ 𝐴, 𝐴, 1))) |
110 | 99, 101, 102, 109 | lediv1dd 11806 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ (1[,)+∞)) → ((𝑛↑𝑐𝐴) / (𝐵↑𝑐𝑛)) ≤ ((𝑛↑𝑐if(1 ≤ 𝐴, 𝐴, 1)) / (𝐵↑𝑐𝑛))) |
111 | 110 | adantrr 749 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ (1[,)+∞) ∧ 0
≤ 𝑛)) → ((𝑛↑𝑐𝐴) / (𝐵↑𝑐𝑛)) ≤ ((𝑛↑𝑐if(1 ≤ 𝐴, 𝐴, 1)) / (𝐵↑𝑐𝑛))) |
112 | 96 | rpge0d 11752 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ (1[,)+∞)) → 0 ≤ ((𝑛↑𝑐𝐴) / (𝐵↑𝑐𝑛))) |
113 | 112 | adantrr 749 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ (𝑛 ∈ (1[,)+∞) ∧ 0
≤ 𝑛)) → 0 ≤
((𝑛↑𝑐𝐴) / (𝐵↑𝑐𝑛))) |
114 | 15, 15, 86, 92, 97, 111, 113 | rlimsqz2 14229 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → (𝑛 ∈ (1[,)+∞) ↦
((𝑛↑𝑐𝐴) / (𝐵↑𝑐𝑛))) ⇝𝑟
0) |
115 | 14, 114 | syl5eqbr 4618 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → ((𝑛 ∈ ℝ+
↦ ((𝑛↑𝑐𝐴) / (𝐵↑𝑐𝑛))) ↾ (1[,)+∞))
⇝𝑟 0) |
116 | 95 | rpcnd 11750 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) ∧ 𝑛 ∈ ℝ+) → ((𝑛↑𝑐𝐴) / (𝐵↑𝑐𝑛)) ∈ ℂ) |
117 | | eqid 2610 |
. . . 4
⊢ (𝑛 ∈ ℝ+
↦ ((𝑛↑𝑐𝐴) / (𝐵↑𝑐𝑛))) = (𝑛 ∈ ℝ+ ↦ ((𝑛↑𝑐𝐴) / (𝐵↑𝑐𝑛))) |
118 | 116, 117 | fmptd 6292 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → (𝑛 ∈ ℝ+
↦ ((𝑛↑𝑐𝐴) / (𝐵↑𝑐𝑛))):ℝ+⟶ℂ) |
119 | | rpssre 11719 |
. . . 4
⊢
ℝ+ ⊆ ℝ |
120 | 119 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) →
ℝ+ ⊆ ℝ) |
121 | 118, 120,
32 | rlimresb 14144 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → ((𝑛 ∈ ℝ+
↦ ((𝑛↑𝑐𝐴) / (𝐵↑𝑐𝑛))) ⇝𝑟 0 ↔
((𝑛 ∈
ℝ+ ↦ ((𝑛↑𝑐𝐴) / (𝐵↑𝑐𝑛))) ↾ (1[,)+∞))
⇝𝑟 0)) |
122 | 115, 121 | mpbird 246 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → (𝑛 ∈ ℝ+
↦ ((𝑛↑𝑐𝐴) / (𝐵↑𝑐𝑛))) ⇝𝑟
0) |