Step | Hyp | Ref
| Expression |
1 | | zaddcl 11417 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑘 + 𝑀) ∈ ℤ) |
2 | 1 | ancoms 469 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 + 𝑀) ∈ ℤ) |
3 | | eluzsub 11717 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑛 ∈
(ℤ≥‘(𝑘 + 𝑀))) → (𝑛 − 𝑀) ∈ (ℤ≥‘𝑘)) |
4 | 3 | 3com12 1269 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑛 ∈
(ℤ≥‘(𝑘 + 𝑀))) → (𝑛 − 𝑀) ∈ (ℤ≥‘𝑘)) |
5 | 4 | 3expa 1265 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ 𝑛 ∈
(ℤ≥‘(𝑘 + 𝑀))) → (𝑛 − 𝑀) ∈ (ℤ≥‘𝑘)) |
6 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑛 − 𝑀) → (𝐹‘𝑚) = (𝐹‘(𝑛 − 𝑀))) |
7 | 6 | eleq1d 2686 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛 − 𝑀) → ((𝐹‘𝑚) ∈ ℂ ↔ (𝐹‘(𝑛 − 𝑀)) ∈ ℂ)) |
8 | 6 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑛 − 𝑀) → ((𝐹‘𝑚) − 𝐴) = ((𝐹‘(𝑛 − 𝑀)) − 𝐴)) |
9 | 8 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑛 − 𝑀) → (abs‘((𝐹‘𝑚) − 𝐴)) = (abs‘((𝐹‘(𝑛 − 𝑀)) − 𝐴))) |
10 | 9 | breq1d 4663 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛 − 𝑀) → ((abs‘((𝐹‘𝑚) − 𝐴)) < 𝑥 ↔ (abs‘((𝐹‘(𝑛 − 𝑀)) − 𝐴)) < 𝑥)) |
11 | 7, 10 | anbi12d 747 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑛 − 𝑀) → (((𝐹‘𝑚) ∈ ℂ ∧ (abs‘((𝐹‘𝑚) − 𝐴)) < 𝑥) ↔ ((𝐹‘(𝑛 − 𝑀)) ∈ ℂ ∧ (abs‘((𝐹‘(𝑛 − 𝑀)) − 𝐴)) < 𝑥))) |
12 | 11 | rspcv 3305 |
. . . . . . . . 9
⊢ ((𝑛 − 𝑀) ∈ (ℤ≥‘𝑘) → (∀𝑚 ∈
(ℤ≥‘𝑘)((𝐹‘𝑚) ∈ ℂ ∧ (abs‘((𝐹‘𝑚) − 𝐴)) < 𝑥) → ((𝐹‘(𝑛 − 𝑀)) ∈ ℂ ∧ (abs‘((𝐹‘(𝑛 − 𝑀)) − 𝐴)) < 𝑥))) |
13 | 5, 12 | syl 17 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ 𝑛 ∈
(ℤ≥‘(𝑘 + 𝑀))) → (∀𝑚 ∈ (ℤ≥‘𝑘)((𝐹‘𝑚) ∈ ℂ ∧ (abs‘((𝐹‘𝑚) − 𝐴)) < 𝑥) → ((𝐹‘(𝑛 − 𝑀)) ∈ ℂ ∧ (abs‘((𝐹‘(𝑛 − 𝑀)) − 𝐴)) < 𝑥))) |
14 | | zcn 11382 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) |
15 | | eluzelcn 11699 |
. . . . . . . . . 10
⊢ (𝑛 ∈
(ℤ≥‘(𝑘 + 𝑀)) → 𝑛 ∈ ℂ) |
16 | | climshft.1 |
. . . . . . . . . . . . 13
⊢ 𝐹 ∈ V |
17 | 16 | shftval 13814 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℂ ∧ 𝑛 ∈ ℂ) → ((𝐹 shift 𝑀)‘𝑛) = (𝐹‘(𝑛 − 𝑀))) |
18 | 17 | eleq1d 2686 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ↔ (𝐹‘(𝑛 − 𝑀)) ∈ ℂ)) |
19 | 17 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (((𝐹 shift 𝑀)‘𝑛) − 𝐴) = ((𝐹‘(𝑛 − 𝑀)) − 𝐴)) |
20 | 19 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℂ ∧ 𝑛 ∈ ℂ) →
(abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) = (abs‘((𝐹‘(𝑛 − 𝑀)) − 𝐴))) |
21 | 20 | breq1d 4663 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℂ ∧ 𝑛 ∈ ℂ) →
((abs‘(((𝐹 shift
𝑀)‘𝑛) − 𝐴)) < 𝑥 ↔ (abs‘((𝐹‘(𝑛 − 𝑀)) − 𝐴)) < 𝑥)) |
22 | 18, 21 | anbi12d 747 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℂ ∧ 𝑛 ∈ ℂ) →
((((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ∧ (abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) < 𝑥) ↔ ((𝐹‘(𝑛 − 𝑀)) ∈ ℂ ∧ (abs‘((𝐹‘(𝑛 − 𝑀)) − 𝐴)) < 𝑥))) |
23 | 14, 15, 22 | syl2an 494 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑛 ∈
(ℤ≥‘(𝑘 + 𝑀))) → ((((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ∧ (abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) < 𝑥) ↔ ((𝐹‘(𝑛 − 𝑀)) ∈ ℂ ∧ (abs‘((𝐹‘(𝑛 − 𝑀)) − 𝐴)) < 𝑥))) |
24 | 23 | adantlr 751 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ 𝑛 ∈
(ℤ≥‘(𝑘 + 𝑀))) → ((((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ∧ (abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) < 𝑥) ↔ ((𝐹‘(𝑛 − 𝑀)) ∈ ℂ ∧ (abs‘((𝐹‘(𝑛 − 𝑀)) − 𝐴)) < 𝑥))) |
25 | 13, 24 | sylibrd 249 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ 𝑛 ∈
(ℤ≥‘(𝑘 + 𝑀))) → (∀𝑚 ∈ (ℤ≥‘𝑘)((𝐹‘𝑚) ∈ ℂ ∧ (abs‘((𝐹‘𝑚) − 𝐴)) < 𝑥) → (((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ∧ (abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) < 𝑥))) |
26 | 25 | ralrimdva 2969 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) →
(∀𝑚 ∈
(ℤ≥‘𝑘)((𝐹‘𝑚) ∈ ℂ ∧ (abs‘((𝐹‘𝑚) − 𝐴)) < 𝑥) → ∀𝑛 ∈ (ℤ≥‘(𝑘 + 𝑀))(((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ∧ (abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) < 𝑥))) |
27 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑚 = (𝑘 + 𝑀) → (ℤ≥‘𝑚) =
(ℤ≥‘(𝑘 + 𝑀))) |
28 | 27 | raleqdv 3144 |
. . . . . . 7
⊢ (𝑚 = (𝑘 + 𝑀) → (∀𝑛 ∈ (ℤ≥‘𝑚)(((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ∧ (abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) < 𝑥) ↔ ∀𝑛 ∈ (ℤ≥‘(𝑘 + 𝑀))(((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ∧ (abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) < 𝑥))) |
29 | 28 | rspcev 3309 |
. . . . . 6
⊢ (((𝑘 + 𝑀) ∈ ℤ ∧ ∀𝑛 ∈
(ℤ≥‘(𝑘 + 𝑀))(((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ∧ (abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) < 𝑥)) → ∃𝑚 ∈ ℤ ∀𝑛 ∈ (ℤ≥‘𝑚)(((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ∧ (abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) < 𝑥)) |
30 | 2, 26, 29 | syl6an 568 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) →
(∀𝑚 ∈
(ℤ≥‘𝑘)((𝐹‘𝑚) ∈ ℂ ∧ (abs‘((𝐹‘𝑚) − 𝐴)) < 𝑥) → ∃𝑚 ∈ ℤ ∀𝑛 ∈ (ℤ≥‘𝑚)(((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ∧ (abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) < 𝑥))) |
31 | 30 | rexlimdva 3031 |
. . . 4
⊢ (𝑀 ∈ ℤ →
(∃𝑘 ∈ ℤ
∀𝑚 ∈
(ℤ≥‘𝑘)((𝐹‘𝑚) ∈ ℂ ∧ (abs‘((𝐹‘𝑚) − 𝐴)) < 𝑥) → ∃𝑚 ∈ ℤ ∀𝑛 ∈ (ℤ≥‘𝑚)(((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ∧ (abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) < 𝑥))) |
32 | 31 | ralimdv 2963 |
. . 3
⊢ (𝑀 ∈ ℤ →
(∀𝑥 ∈
ℝ+ ∃𝑘 ∈ ℤ ∀𝑚 ∈ (ℤ≥‘𝑘)((𝐹‘𝑚) ∈ ℂ ∧ (abs‘((𝐹‘𝑚) − 𝐴)) < 𝑥) → ∀𝑥 ∈ ℝ+ ∃𝑚 ∈ ℤ ∀𝑛 ∈
(ℤ≥‘𝑚)(((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ∧ (abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) < 𝑥))) |
33 | 32 | anim2d 589 |
. 2
⊢ (𝑀 ∈ ℤ → ((𝐴 ∈ ℂ ∧
∀𝑥 ∈
ℝ+ ∃𝑘 ∈ ℤ ∀𝑚 ∈ (ℤ≥‘𝑘)((𝐹‘𝑚) ∈ ℂ ∧ (abs‘((𝐹‘𝑚) − 𝐴)) < 𝑥)) → (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑚 ∈ ℤ
∀𝑛 ∈
(ℤ≥‘𝑚)(((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ∧ (abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) < 𝑥)))) |
34 | 16 | a1i 11 |
. . 3
⊢ (𝑀 ∈ ℤ → 𝐹 ∈ V) |
35 | | eqidd 2623 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝐹‘𝑚) = (𝐹‘𝑚)) |
36 | 34, 35 | clim 14225 |
. 2
⊢ (𝑀 ∈ ℤ → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑘 ∈ ℤ
∀𝑚 ∈
(ℤ≥‘𝑘)((𝐹‘𝑚) ∈ ℂ ∧ (abs‘((𝐹‘𝑚) − 𝐴)) < 𝑥)))) |
37 | | ovexd 6680 |
. . 3
⊢ (𝑀 ∈ ℤ → (𝐹 shift 𝑀) ∈ V) |
38 | | eqidd 2623 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((𝐹 shift 𝑀)‘𝑛) = ((𝐹 shift 𝑀)‘𝑛)) |
39 | 37, 38 | clim 14225 |
. 2
⊢ (𝑀 ∈ ℤ → ((𝐹 shift 𝑀) ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑚 ∈ ℤ
∀𝑛 ∈
(ℤ≥‘𝑚)(((𝐹 shift 𝑀)‘𝑛) ∈ ℂ ∧ (abs‘(((𝐹 shift 𝑀)‘𝑛) − 𝐴)) < 𝑥)))) |
40 | 33, 36, 39 | 3imtr4d 283 |
1
⊢ (𝑀 ∈ ℤ → (𝐹 ⇝ 𝐴 → (𝐹 shift 𝑀) ⇝ 𝐴)) |