Step | Hyp | Ref
| Expression |
1 | | climrlim2.5 |
. 2
⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ 𝐵) ⇝ 𝐷) |
2 | | eluzelz 11573 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑗 ∈ ℤ) |
3 | | climrlim2.1 |
. . . . . . . . . . . . . . . 16
⊢ 𝑍 =
(ℤ≥‘𝑀) |
4 | 2, 3 | eleq2s 2706 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ 𝑍 → 𝑗 ∈ ℤ) |
5 | 4 | ad2antlr 759 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ (𝑥 ∈ 𝐴 ∧ 𝑗 ≤ 𝑥)) → 𝑗 ∈ ℤ) |
6 | | climrlim2.3 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
7 | 6 | sselda 3568 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ) |
8 | 7 | flcld 12461 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (⌊‘𝑥) ∈ ℤ) |
9 | 8 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ 𝐴) → (⌊‘𝑥) ∈ ℤ) |
10 | 9 | ad2ant2r 779 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ (𝑥 ∈ 𝐴 ∧ 𝑗 ≤ 𝑥)) → (⌊‘𝑥) ∈ ℤ) |
11 | | simprr 792 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ (𝑥 ∈ 𝐴 ∧ 𝑗 ≤ 𝑥)) → 𝑗 ≤ 𝑥) |
12 | 7 | adantlr 747 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ) |
13 | 12 | ad2ant2r 779 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ (𝑥 ∈ 𝐴 ∧ 𝑗 ≤ 𝑥)) → 𝑥 ∈ ℝ) |
14 | | flge 12468 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ ∧ 𝑗 ∈ ℤ) → (𝑗 ≤ 𝑥 ↔ 𝑗 ≤ (⌊‘𝑥))) |
15 | 13, 5, 14 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ (𝑥 ∈ 𝐴 ∧ 𝑗 ≤ 𝑥)) → (𝑗 ≤ 𝑥 ↔ 𝑗 ≤ (⌊‘𝑥))) |
16 | 11, 15 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ (𝑥 ∈ 𝐴 ∧ 𝑗 ≤ 𝑥)) → 𝑗 ≤ (⌊‘𝑥)) |
17 | | eluz2 11569 |
. . . . . . . . . . . . . 14
⊢
((⌊‘𝑥)
∈ (ℤ≥‘𝑗) ↔ (𝑗 ∈ ℤ ∧ (⌊‘𝑥) ∈ ℤ ∧ 𝑗 ≤ (⌊‘𝑥))) |
18 | 5, 10, 16, 17 | syl3anbrc 1239 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ (𝑥 ∈ 𝐴 ∧ 𝑗 ≤ 𝑥)) → (⌊‘𝑥) ∈ (ℤ≥‘𝑗)) |
19 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ∈ ℂ ∧ (abs‘(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) − 𝐷)) < 𝑦) → (abs‘(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) − 𝐷)) < 𝑦) |
20 | 19 | ralimi 2936 |
. . . . . . . . . . . . 13
⊢
(∀𝑘 ∈
(ℤ≥‘𝑗)(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ∈ ℂ ∧ (abs‘(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) − 𝐷)) < 𝑦) → ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) − 𝐷)) < 𝑦) |
21 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = (⌊‘𝑥) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘(⌊‘𝑥))) |
22 | 21 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = (⌊‘𝑥) → (((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) − 𝐷) = (((𝑛 ∈ 𝑍 ↦ 𝐵)‘(⌊‘𝑥)) − 𝐷)) |
23 | 22 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (⌊‘𝑥) → (abs‘(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) − 𝐷)) = (abs‘(((𝑛 ∈ 𝑍 ↦ 𝐵)‘(⌊‘𝑥)) − 𝐷))) |
24 | 23 | breq1d 4593 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (⌊‘𝑥) → ((abs‘(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) − 𝐷)) < 𝑦 ↔ (abs‘(((𝑛 ∈ 𝑍 ↦ 𝐵)‘(⌊‘𝑥)) − 𝐷)) < 𝑦)) |
25 | 24 | rspcv 3278 |
. . . . . . . . . . . . 13
⊢
((⌊‘𝑥)
∈ (ℤ≥‘𝑗) → (∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) − 𝐷)) < 𝑦 → (abs‘(((𝑛 ∈ 𝑍 ↦ 𝐵)‘(⌊‘𝑥)) − 𝐷)) < 𝑦)) |
26 | 18, 20, 25 | syl2im 39 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ (𝑥 ∈ 𝐴 ∧ 𝑗 ≤ 𝑥)) → (∀𝑘 ∈ (ℤ≥‘𝑗)(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ∈ ℂ ∧ (abs‘(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) − 𝐷)) < 𝑦) → (abs‘(((𝑛 ∈ 𝑍 ↦ 𝐵)‘(⌊‘𝑥)) − 𝐷)) < 𝑦)) |
27 | | climrlim2.4 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑀 ∈ ℤ) |
28 | 27 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑀 ∈ ℤ) |
29 | | climrlim2.7 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑀 ≤ 𝑥) |
30 | | flge 12468 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ ∧ 𝑀 ∈ ℤ) → (𝑀 ≤ 𝑥 ↔ 𝑀 ≤ (⌊‘𝑥))) |
31 | 7, 28, 30 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑀 ≤ 𝑥 ↔ 𝑀 ≤ (⌊‘𝑥))) |
32 | 29, 31 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑀 ≤ (⌊‘𝑥)) |
33 | | eluz2 11569 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((⌊‘𝑥)
∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (⌊‘𝑥) ∈ ℤ ∧ 𝑀 ≤ (⌊‘𝑥))) |
34 | 28, 8, 32, 33 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (⌊‘𝑥) ∈ (ℤ≥‘𝑀)) |
35 | 34, 3 | syl6eleqr 2699 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (⌊‘𝑥) ∈ 𝑍) |
36 | | climrlim2.6 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝐵 ∈ ℂ) |
37 | 36 | ralrimiva 2949 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ∀𝑛 ∈ 𝑍 𝐵 ∈ ℂ) |
38 | 37 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑛 ∈ 𝑍 𝐵 ∈ ℂ) |
39 | | climrlim2.2 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = (⌊‘𝑥) → 𝐵 = 𝐶) |
40 | 39 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = (⌊‘𝑥) → (𝐵 ∈ ℂ ↔ 𝐶 ∈ ℂ)) |
41 | 40 | rspcv 3278 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⌊‘𝑥)
∈ 𝑍 →
(∀𝑛 ∈ 𝑍 𝐵 ∈ ℂ → 𝐶 ∈ ℂ)) |
42 | 35, 38, 41 | sylc 63 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) |
43 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ 𝑍 ↦ 𝐵) = (𝑛 ∈ 𝑍 ↦ 𝐵) |
44 | 39, 43 | fvmptg 6189 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⌊‘𝑥)
∈ 𝑍 ∧ 𝐶 ∈ ℂ) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘(⌊‘𝑥)) = 𝐶) |
45 | 35, 42, 44 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘(⌊‘𝑥)) = 𝐶) |
46 | 45 | adantlr 747 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ 𝐴) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘(⌊‘𝑥)) = 𝐶) |
47 | 46 | ad2ant2r 779 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ (𝑥 ∈ 𝐴 ∧ 𝑗 ≤ 𝑥)) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘(⌊‘𝑥)) = 𝐶) |
48 | 47 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ (𝑥 ∈ 𝐴 ∧ 𝑗 ≤ 𝑥)) → (((𝑛 ∈ 𝑍 ↦ 𝐵)‘(⌊‘𝑥)) − 𝐷) = (𝐶 − 𝐷)) |
49 | 48 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ (𝑥 ∈ 𝐴 ∧ 𝑗 ≤ 𝑥)) → (abs‘(((𝑛 ∈ 𝑍 ↦ 𝐵)‘(⌊‘𝑥)) − 𝐷)) = (abs‘(𝐶 − 𝐷))) |
50 | 49 | breq1d 4593 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ (𝑥 ∈ 𝐴 ∧ 𝑗 ≤ 𝑥)) → ((abs‘(((𝑛 ∈ 𝑍 ↦ 𝐵)‘(⌊‘𝑥)) − 𝐷)) < 𝑦 ↔ (abs‘(𝐶 − 𝐷)) < 𝑦)) |
51 | 26, 50 | sylibd 228 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ (𝑥 ∈ 𝐴 ∧ 𝑗 ≤ 𝑥)) → (∀𝑘 ∈ (ℤ≥‘𝑗)(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ∈ ℂ ∧ (abs‘(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) − 𝐷)) < 𝑦) → (abs‘(𝐶 − 𝐷)) < 𝑦)) |
52 | 51 | expr 641 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 ∈ 𝐴) → (𝑗 ≤ 𝑥 → (∀𝑘 ∈ (ℤ≥‘𝑗)(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ∈ ℂ ∧ (abs‘(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) − 𝐷)) < 𝑦) → (abs‘(𝐶 − 𝐷)) < 𝑦))) |
53 | 52 | com23 84 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑥 ∈ 𝐴) → (∀𝑘 ∈ (ℤ≥‘𝑗)(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ∈ ℂ ∧ (abs‘(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) − 𝐷)) < 𝑦) → (𝑗 ≤ 𝑥 → (abs‘(𝐶 − 𝐷)) < 𝑦))) |
54 | 53 | ralrimdva 2952 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ∈ ℂ ∧ (abs‘(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) − 𝐷)) < 𝑦) → ∀𝑥 ∈ 𝐴 (𝑗 ≤ 𝑥 → (abs‘(𝐶 − 𝐷)) < 𝑦))) |
55 | | eluzelre 11574 |
. . . . . . . . . 10
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑗 ∈ ℝ) |
56 | 55, 3 | eleq2s 2706 |
. . . . . . . . 9
⊢ (𝑗 ∈ 𝑍 → 𝑗 ∈ ℝ) |
57 | 56 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ ℝ) |
58 | 54, 57 | jctild 564 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ∈ ℂ ∧ (abs‘(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) − 𝐷)) < 𝑦) → (𝑗 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (𝑗 ≤ 𝑥 → (abs‘(𝐶 − 𝐷)) < 𝑦)))) |
59 | 58 | expimpd 627 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → ((𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ∈ ℂ ∧ (abs‘(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) − 𝐷)) < 𝑦)) → (𝑗 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 (𝑗 ≤ 𝑥 → (abs‘(𝐶 − 𝐷)) < 𝑦)))) |
60 | 59 | reximdv2 2997 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
(∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ∈ ℂ ∧ (abs‘(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) − 𝐷)) < 𝑦) → ∃𝑗 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑗 ≤ 𝑥 → (abs‘(𝐶 − 𝐷)) < 𝑦))) |
61 | 60 | ralimdva 2945 |
. . . 4
⊢ (𝜑 → (∀𝑦 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ∈ ℂ ∧ (abs‘(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) − 𝐷)) < 𝑦) → ∀𝑦 ∈ ℝ+ ∃𝑗 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑗 ≤ 𝑥 → (abs‘(𝐶 − 𝐷)) < 𝑦))) |
62 | 61 | adantld 482 |
. . 3
⊢ (𝜑 → ((𝐷 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ∈ ℂ ∧ (abs‘(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) − 𝐷)) < 𝑦)) → ∀𝑦 ∈ ℝ+ ∃𝑗 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑗 ≤ 𝑥 → (abs‘(𝐶 − 𝐷)) < 𝑦))) |
63 | | climrel 14071 |
. . . . . 6
⊢ Rel
⇝ |
64 | 63 | brrelexi 5082 |
. . . . 5
⊢ ((𝑛 ∈ 𝑍 ↦ 𝐵) ⇝ 𝐷 → (𝑛 ∈ 𝑍 ↦ 𝐵) ∈ V) |
65 | 1, 64 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ 𝐵) ∈ V) |
66 | | eqidd 2611 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) = ((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘)) |
67 | 3, 27, 65, 66 | clim2 14083 |
. . 3
⊢ (𝜑 → ((𝑛 ∈ 𝑍 ↦ 𝐵) ⇝ 𝐷 ↔ (𝐷 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) ∈ ℂ ∧ (abs‘(((𝑛 ∈ 𝑍 ↦ 𝐵)‘𝑘) − 𝐷)) < 𝑦)))) |
68 | 42 | ralrimiva 2949 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐶 ∈ ℂ) |
69 | | climcl 14078 |
. . . . 5
⊢ ((𝑛 ∈ 𝑍 ↦ 𝐵) ⇝ 𝐷 → 𝐷 ∈ ℂ) |
70 | 1, 69 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ ℂ) |
71 | 68, 6, 70 | rlim2 14075 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐷 ↔ ∀𝑦 ∈ ℝ+
∃𝑗 ∈ ℝ
∀𝑥 ∈ 𝐴 (𝑗 ≤ 𝑥 → (abs‘(𝐶 − 𝐷)) < 𝑦))) |
72 | 62, 67, 71 | 3imtr4d 282 |
. 2
⊢ (𝜑 → ((𝑛 ∈ 𝑍 ↦ 𝐵) ⇝ 𝐷 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐷)) |
73 | 1, 72 | mpd 15 |
1
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⇝𝑟 𝐷) |