Step | Hyp | Ref
| Expression |
1 | | rlimcxp.2 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ 𝐴 ↦ 𝐵) ⇝𝑟
0) |
2 | | rlimf 14961 |
. . . . . . . . 9
⊢ ((𝑛 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 0 →
(𝑛 ∈ 𝐴 ↦ 𝐵):dom (𝑛 ∈ 𝐴 ↦ 𝐵)⟶ℂ) |
3 | 1, 2 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑛 ∈ 𝐴 ↦ 𝐵):dom (𝑛 ∈ 𝐴 ↦ 𝐵)⟶ℂ) |
4 | | rlimcxp.1 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
5 | 4 | ralrimiva 3097 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑛 ∈ 𝐴 𝐵 ∈ 𝑉) |
6 | | dmmptg 6084 |
. . . . . . . . . 10
⊢
(∀𝑛 ∈
𝐴 𝐵 ∈ 𝑉 → dom (𝑛 ∈ 𝐴 ↦ 𝐵) = 𝐴) |
7 | 5, 6 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → dom (𝑛 ∈ 𝐴 ↦ 𝐵) = 𝐴) |
8 | 7 | feq2d 6501 |
. . . . . . . 8
⊢ (𝜑 → ((𝑛 ∈ 𝐴 ↦ 𝐵):dom (𝑛 ∈ 𝐴 ↦ 𝐵)⟶ℂ ↔ (𝑛 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ)) |
9 | 3, 8 | mpbid 235 |
. . . . . . 7
⊢ (𝜑 → (𝑛 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
10 | | eqid 2739 |
. . . . . . . 8
⊢ (𝑛 ∈ 𝐴 ↦ 𝐵) = (𝑛 ∈ 𝐴 ↦ 𝐵) |
11 | 10 | fmpt 6897 |
. . . . . . 7
⊢
(∀𝑛 ∈
𝐴 𝐵 ∈ ℂ ↔ (𝑛 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
12 | 9, 11 | sylibr 237 |
. . . . . 6
⊢ (𝜑 → ∀𝑛 ∈ 𝐴 𝐵 ∈ ℂ) |
13 | 12 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∀𝑛 ∈ 𝐴 𝐵 ∈ ℂ) |
14 | | simpr 488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
15 | | rlimcxp.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
16 | 15 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐶 ∈
ℝ+) |
17 | 16 | rprecred 12538 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1 /
𝐶) ∈
ℝ) |
18 | 14, 17 | rpcxpcld 25488 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥↑𝑐(1 /
𝐶)) ∈
ℝ+) |
19 | 1 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑛 ∈ 𝐴 ↦ 𝐵) ⇝𝑟
0) |
20 | 13, 18, 19 | rlimi 14973 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈ ℝ
∀𝑛 ∈ 𝐴 (𝑦 ≤ 𝑛 → (abs‘(𝐵 − 0)) < (𝑥↑𝑐(1 / 𝐶)))) |
21 | 4, 1 | rlimmptrcl 15068 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐵 ∈ ℂ) |
22 | 21 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ 𝐴) → 𝐵 ∈ ℂ) |
23 | 22 | abscld 14899 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ 𝐴) → (abs‘𝐵) ∈ ℝ) |
24 | 22 | absge0d 14907 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ 𝐴) → 0 ≤ (abs‘𝐵)) |
25 | 18 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ 𝐴) → (𝑥↑𝑐(1 / 𝐶)) ∈
ℝ+) |
26 | 25 | rpred 12527 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ 𝐴) → (𝑥↑𝑐(1 / 𝐶)) ∈
ℝ) |
27 | 25 | rpge0d 12531 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ 𝐴) → 0 ≤ (𝑥↑𝑐(1 / 𝐶))) |
28 | 15 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ 𝐴) → 𝐶 ∈
ℝ+) |
29 | 23, 24, 26, 27, 28 | cxplt2d 25482 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ 𝐴) → ((abs‘𝐵) < (𝑥↑𝑐(1 / 𝐶)) ↔ ((abs‘𝐵)↑𝑐𝐶) < ((𝑥↑𝑐(1 / 𝐶))↑𝑐𝐶))) |
30 | 22 | subid1d 11077 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ 𝐴) → (𝐵 − 0) = 𝐵) |
31 | 30 | fveq2d 6691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ 𝐴) → (abs‘(𝐵 − 0)) = (abs‘𝐵)) |
32 | 31 | breq1d 5050 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ 𝐴) → ((abs‘(𝐵 − 0)) < (𝑥↑𝑐(1 / 𝐶)) ↔ (abs‘𝐵) < (𝑥↑𝑐(1 / 𝐶)))) |
33 | 28 | rpred 12527 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ 𝐴) → 𝐶 ∈ ℝ) |
34 | | abscxp2 25449 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ) →
(abs‘(𝐵↑𝑐𝐶)) = ((abs‘𝐵)↑𝑐𝐶)) |
35 | 22, 33, 34 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ 𝐴) → (abs‘(𝐵↑𝑐𝐶)) = ((abs‘𝐵)↑𝑐𝐶)) |
36 | 28 | rpcnd 12529 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ 𝐴) → 𝐶 ∈ ℂ) |
37 | 28 | rpne0d 12532 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ 𝐴) → 𝐶 ≠ 0) |
38 | 36, 37 | recid2d 11503 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ 𝐴) → ((1 / 𝐶) · 𝐶) = 1) |
39 | 38 | oveq2d 7199 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ 𝐴) → (𝑥↑𝑐((1 / 𝐶) · 𝐶)) = (𝑥↑𝑐1)) |
40 | | simplr 769 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ 𝐴) → 𝑥 ∈ ℝ+) |
41 | 17 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ 𝐴) → (1 / 𝐶) ∈ ℝ) |
42 | 40, 41, 36 | cxpmuld 25492 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ 𝐴) → (𝑥↑𝑐((1 / 𝐶) · 𝐶)) = ((𝑥↑𝑐(1 / 𝐶))↑𝑐𝐶)) |
43 | 40 | rpcnd 12529 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ 𝐴) → 𝑥 ∈ ℂ) |
44 | 43 | cxp1d 25462 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ 𝐴) → (𝑥↑𝑐1) = 𝑥) |
45 | 39, 42, 44 | 3eqtr3rd 2783 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ 𝐴) → 𝑥 = ((𝑥↑𝑐(1 / 𝐶))↑𝑐𝐶)) |
46 | 35, 45 | breq12d 5053 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ 𝐴) → ((abs‘(𝐵↑𝑐𝐶)) < 𝑥 ↔ ((abs‘𝐵)↑𝑐𝐶) < ((𝑥↑𝑐(1 / 𝐶))↑𝑐𝐶))) |
47 | 29, 32, 46 | 3bitr4d 314 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ 𝐴) → ((abs‘(𝐵 − 0)) < (𝑥↑𝑐(1 / 𝐶)) ↔ (abs‘(𝐵↑𝑐𝐶)) < 𝑥)) |
48 | 47 | biimpd 232 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ 𝐴) → ((abs‘(𝐵 − 0)) < (𝑥↑𝑐(1 / 𝐶)) → (abs‘(𝐵↑𝑐𝐶)) < 𝑥)) |
49 | 48 | imim2d 57 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ 𝐴) → ((𝑦 ≤ 𝑛 → (abs‘(𝐵 − 0)) < (𝑥↑𝑐(1 / 𝐶))) → (𝑦 ≤ 𝑛 → (abs‘(𝐵↑𝑐𝐶)) < 𝑥))) |
50 | 49 | ralimdva 3092 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(∀𝑛 ∈ 𝐴 (𝑦 ≤ 𝑛 → (abs‘(𝐵 − 0)) < (𝑥↑𝑐(1 / 𝐶))) → ∀𝑛 ∈ 𝐴 (𝑦 ≤ 𝑛 → (abs‘(𝐵↑𝑐𝐶)) < 𝑥))) |
51 | 50 | reximdv 3184 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(∃𝑦 ∈ ℝ
∀𝑛 ∈ 𝐴 (𝑦 ≤ 𝑛 → (abs‘(𝐵 − 0)) < (𝑥↑𝑐(1 / 𝐶))) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝐴 (𝑦 ≤ 𝑛 → (abs‘(𝐵↑𝑐𝐶)) < 𝑥))) |
52 | 20, 51 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈ ℝ
∀𝑛 ∈ 𝐴 (𝑦 ≤ 𝑛 → (abs‘(𝐵↑𝑐𝐶)) < 𝑥)) |
53 | 52 | ralrimiva 3097 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝐴 (𝑦 ≤ 𝑛 → (abs‘(𝐵↑𝑐𝐶)) < 𝑥)) |
54 | 15 | rpcnd 12529 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℂ) |
55 | 54 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐶 ∈ ℂ) |
56 | 21, 55 | cxpcld 25464 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐵↑𝑐𝐶) ∈ ℂ) |
57 | 56 | ralrimiva 3097 |
. . 3
⊢ (𝜑 → ∀𝑛 ∈ 𝐴 (𝐵↑𝑐𝐶) ∈ ℂ) |
58 | | rlimss 14962 |
. . . . 5
⊢ ((𝑛 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 0 → dom
(𝑛 ∈ 𝐴 ↦ 𝐵) ⊆ ℝ) |
59 | 1, 58 | syl 17 |
. . . 4
⊢ (𝜑 → dom (𝑛 ∈ 𝐴 ↦ 𝐵) ⊆ ℝ) |
60 | 7, 59 | eqsstrrd 3926 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
61 | 57, 60 | rlim0 14968 |
. 2
⊢ (𝜑 → ((𝑛 ∈ 𝐴 ↦ (𝐵↑𝑐𝐶)) ⇝𝑟 0 ↔
∀𝑥 ∈
ℝ+ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝐴 (𝑦 ≤ 𝑛 → (abs‘(𝐵↑𝑐𝐶)) < 𝑥))) |
62 | 53, 61 | mpbird 260 |
1
⊢ (𝜑 → (𝑛 ∈ 𝐴 ↦ (𝐵↑𝑐𝐶)) ⇝𝑟
0) |