Step | Hyp | Ref
| Expression |
1 | | zaddcl 11294 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑘 + 𝑀) ∈ ℤ) |
2 | 1 | ancoms 468 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 + 𝑀) ∈ ℤ) |
3 | | eluzsub 11593 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑛 ∈
(ℤ≥‘(𝑘 + 𝑀))) → (𝑛 − 𝑀) ∈ (ℤ≥‘𝑘)) |
4 | 3 | 3com12 1261 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑛 ∈
(ℤ≥‘(𝑘 + 𝑀))) → (𝑛 − 𝑀) ∈ (ℤ≥‘𝑘)) |
5 | 4 | 3expa 1257 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ 𝑛 ∈
(ℤ≥‘(𝑘 + 𝑀))) → (𝑛 − 𝑀) ∈ (ℤ≥‘𝑘)) |
6 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑛 − 𝑀) → (𝐹‘𝑚) = (𝐹‘(𝑛 − 𝑀))) |
7 | 6 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛 − 𝑀) → ((𝐹‘𝑚) ∈ ℂ ↔ (𝐹‘(𝑛 − 𝑀)) ∈ ℂ)) |
8 | 6 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑛 − 𝑀) → ((𝐹‘𝑚) − 𝐴) = ((𝐹‘(𝑛 − 𝑀)) − 𝐴)) |
9 | 8 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑛 − 𝑀) → (abs‘((𝐹‘𝑚) − 𝐴)) = (abs‘((𝐹‘(𝑛 − 𝑀)) − 𝐴))) |
10 | 9 | breq1d 4593 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛 − 𝑀) → ((abs‘((𝐹‘𝑚) − 𝐴)) < 𝑥 ↔ (abs‘((𝐹‘(𝑛 − 𝑀)) − 𝐴)) < 𝑥)) |
11 | 7, 10 | anbi12d 743 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑛 − 𝑀) → (((𝐹‘𝑚) ∈ ℂ ∧ (abs‘((𝐹‘𝑚) − 𝐴)) < 𝑥) ↔ ((𝐹‘(𝑛 − 𝑀)) ∈ ℂ ∧ (abs‘((𝐹‘(𝑛 − 𝑀)) − 𝐴)) < 𝑥))) |
12 | 11 | rspcv 3278 |
. . . . . . . . 9
⊢ ((𝑛 − 𝑀) ∈ (ℤ≥‘𝑘) → (∀𝑚 ∈
(ℤ≥‘𝑘)((𝐹‘𝑚) ∈ ℂ ∧ (abs‘((𝐹‘𝑚) − 𝐴)) < 𝑥) → ((𝐹‘(𝑛 − 𝑀)) ∈ ℂ ∧ (abs‘((𝐹‘(𝑛 − 𝑀)) − 𝐴)) < 𝑥))) |
13 | 5, 12 | syl 17 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ 𝑛 ∈
(ℤ≥‘(𝑘 + 𝑀))) → (∀𝑚 ∈ (ℤ≥‘𝑘)((𝐹‘𝑚) ∈ ℂ ∧ (abs‘((𝐹‘𝑚) − 𝐴)) < 𝑥) → ((𝐹‘(𝑛 − 𝑀)) ∈ ℂ ∧ (abs‘((𝐹‘(𝑛 − 𝑀)) − 𝐴)) < 𝑥))) |
14 | | zcn 11259 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) |
15 | | eluzelcn 11575 |
. . . . . . . . . 10
⊢ (𝑛 ∈
(ℤ≥‘(𝑘 + 𝑀)) → 𝑛 ∈ ℂ) |
16 | | climshft.1 |
. . . . . . . . . . . . 13
⊢ 𝐹 ∈ V |
17 | 16 | shftval 13662 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℂ ∧ 𝑛 ∈ ℂ) → ((𝐹 shift 𝑀)‘𝑛) = (𝐹‘(𝑛 − 𝑀))) |
18 | 17 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ↔ (𝐹‘(𝑛 − 𝑀)) ∈ ℂ)) |
19 | 17 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (((𝐹 shift 𝑀)‘𝑛) − 𝐴) = ((𝐹‘(𝑛 − 𝑀)) − 𝐴)) |
20 | 19 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℂ ∧ 𝑛 ∈ ℂ) →
(abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) = (abs‘((𝐹‘(𝑛 − 𝑀)) − 𝐴))) |
21 | 20 | breq1d 4593 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℂ ∧ 𝑛 ∈ ℂ) →
((abs‘(((𝐹 shift
𝑀)‘𝑛) − 𝐴)) < 𝑥 ↔ (abs‘((𝐹‘(𝑛 − 𝑀)) − 𝐴)) < 𝑥)) |
22 | 18, 21 | anbi12d 743 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℂ ∧ 𝑛 ∈ ℂ) →
((((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ∧ (abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) < 𝑥) ↔ ((𝐹‘(𝑛 − 𝑀)) ∈ ℂ ∧ (abs‘((𝐹‘(𝑛 − 𝑀)) − 𝐴)) < 𝑥))) |
23 | 14, 15, 22 | syl2an 493 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑛 ∈
(ℤ≥‘(𝑘 + 𝑀))) → ((((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ∧ (abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) < 𝑥) ↔ ((𝐹‘(𝑛 − 𝑀)) ∈ ℂ ∧ (abs‘((𝐹‘(𝑛 − 𝑀)) − 𝐴)) < 𝑥))) |
24 | 23 | adantlr 747 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ 𝑛 ∈
(ℤ≥‘(𝑘 + 𝑀))) → ((((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ∧ (abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) < 𝑥) ↔ ((𝐹‘(𝑛 − 𝑀)) ∈ ℂ ∧ (abs‘((𝐹‘(𝑛 − 𝑀)) − 𝐴)) < 𝑥))) |
25 | 13, 24 | sylibrd 248 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ 𝑛 ∈
(ℤ≥‘(𝑘 + 𝑀))) → (∀𝑚 ∈ (ℤ≥‘𝑘)((𝐹‘𝑚) ∈ ℂ ∧ (abs‘((𝐹‘𝑚) − 𝐴)) < 𝑥) → (((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ∧ (abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) < 𝑥))) |
26 | 25 | ralrimdva 2952 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) →
(∀𝑚 ∈
(ℤ≥‘𝑘)((𝐹‘𝑚) ∈ ℂ ∧ (abs‘((𝐹‘𝑚) − 𝐴)) < 𝑥) → ∀𝑛 ∈ (ℤ≥‘(𝑘 + 𝑀))(((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ∧ (abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) < 𝑥))) |
27 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑚 = (𝑘 + 𝑀) → (ℤ≥‘𝑚) =
(ℤ≥‘(𝑘 + 𝑀))) |
28 | 27 | raleqdv 3121 |
. . . . . . 7
⊢ (𝑚 = (𝑘 + 𝑀) → (∀𝑛 ∈ (ℤ≥‘𝑚)(((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ∧ (abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) < 𝑥) ↔ ∀𝑛 ∈ (ℤ≥‘(𝑘 + 𝑀))(((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ∧ (abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) < 𝑥))) |
29 | 28 | rspcev 3282 |
. . . . . 6
⊢ (((𝑘 + 𝑀) ∈ ℤ ∧ ∀𝑛 ∈
(ℤ≥‘(𝑘 + 𝑀))(((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ∧ (abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) < 𝑥)) → ∃𝑚 ∈ ℤ ∀𝑛 ∈ (ℤ≥‘𝑚)(((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ∧ (abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) < 𝑥)) |
30 | 2, 26, 29 | syl6an 566 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) →
(∀𝑚 ∈
(ℤ≥‘𝑘)((𝐹‘𝑚) ∈ ℂ ∧ (abs‘((𝐹‘𝑚) − 𝐴)) < 𝑥) → ∃𝑚 ∈ ℤ ∀𝑛 ∈ (ℤ≥‘𝑚)(((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ∧ (abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) < 𝑥))) |
31 | 30 | rexlimdva 3013 |
. . . 4
⊢ (𝑀 ∈ ℤ →
(∃𝑘 ∈ ℤ
∀𝑚 ∈
(ℤ≥‘𝑘)((𝐹‘𝑚) ∈ ℂ ∧ (abs‘((𝐹‘𝑚) − 𝐴)) < 𝑥) → ∃𝑚 ∈ ℤ ∀𝑛 ∈ (ℤ≥‘𝑚)(((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ∧ (abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) < 𝑥))) |
32 | 31 | ralimdv 2946 |
. . 3
⊢ (𝑀 ∈ ℤ →
(∀𝑥 ∈
ℝ+ ∃𝑘 ∈ ℤ ∀𝑚 ∈ (ℤ≥‘𝑘)((𝐹‘𝑚) ∈ ℂ ∧ (abs‘((𝐹‘𝑚) − 𝐴)) < 𝑥) → ∀𝑥 ∈ ℝ+ ∃𝑚 ∈ ℤ ∀𝑛 ∈
(ℤ≥‘𝑚)(((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ∧ (abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) < 𝑥))) |
33 | 32 | anim2d 587 |
. 2
⊢ (𝑀 ∈ ℤ → ((𝐴 ∈ ℂ ∧
∀𝑥 ∈
ℝ+ ∃𝑘 ∈ ℤ ∀𝑚 ∈ (ℤ≥‘𝑘)((𝐹‘𝑚) ∈ ℂ ∧ (abs‘((𝐹‘𝑚) − 𝐴)) < 𝑥)) → (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑚 ∈ ℤ
∀𝑛 ∈
(ℤ≥‘𝑚)(((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ∧ (abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) < 𝑥)))) |
34 | 16 | a1i 11 |
. . 3
⊢ (𝑀 ∈ ℤ → 𝐹 ∈ V) |
35 | | eqidd 2611 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝐹‘𝑚) = (𝐹‘𝑚)) |
36 | 34, 35 | clim 14073 |
. 2
⊢ (𝑀 ∈ ℤ → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑘 ∈ ℤ
∀𝑚 ∈
(ℤ≥‘𝑘)((𝐹‘𝑚) ∈ ℂ ∧ (abs‘((𝐹‘𝑚) − 𝐴)) < 𝑥)))) |
37 | | ovex 6577 |
. . . 4
⊢ (𝐹 shift 𝑀) ∈ V |
38 | 37 | a1i 11 |
. . 3
⊢ (𝑀 ∈ ℤ → (𝐹 shift 𝑀) ∈ V) |
39 | | eqidd 2611 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((𝐹 shift 𝑀)‘𝑛) = ((𝐹 shift 𝑀)‘𝑛)) |
40 | 38, 39 | clim 14073 |
. 2
⊢ (𝑀 ∈ ℤ → ((𝐹 shift 𝑀) ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑚 ∈ ℤ
∀𝑛 ∈
(ℤ≥‘𝑚)(((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ∧ (abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) < 𝑥)))) |
41 | 33, 36, 40 | 3imtr4d 282 |
1
⊢ (𝑀 ∈ ℤ → (𝐹 ⇝ 𝐴 → (𝐹 shift 𝑀) ⇝ 𝐴)) |