Step | Hyp | Ref
| Expression |
1 | | ulmshft.z |
. . . . . 6
⊢ 𝑍 =
(ℤ≥‘𝑀) |
2 | | ulmshft.m |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℤ) |
3 | 2 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) → 𝑀 ∈
ℤ) |
4 | | ulmshft.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑𝑚
𝑆)) |
5 | 4 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) → 𝐹:𝑍⟶(ℂ ↑𝑚
𝑆)) |
6 | | eqidd 2611 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ (𝑚 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → ((𝐹‘𝑚)‘𝑧) = ((𝐹‘𝑚)‘𝑧)) |
7 | | eqidd 2611 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = (𝐺‘𝑧)) |
8 | | simplr 788 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) → 𝐹(⇝𝑢‘𝑆)𝐺) |
9 | | simpr 476 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
10 | 1, 3, 5, 6, 7, 8, 9 | ulmi 23944 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) →
∃𝑖 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑖)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑚)‘𝑧) − (𝐺‘𝑧))) < 𝑥) |
11 | | simpr 476 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ 𝑍) |
12 | 11, 1 | syl6eleq 2698 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ (ℤ≥‘𝑀)) |
13 | | ulmshft.k |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ ℤ) |
14 | 13 | ad3antrrr 762 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ 𝑖 ∈ 𝑍) → 𝐾 ∈ ℤ) |
15 | | eluzadd 11592 |
. . . . . . . . 9
⊢ ((𝑖 ∈
(ℤ≥‘𝑀) ∧ 𝐾 ∈ ℤ) → (𝑖 + 𝐾) ∈
(ℤ≥‘(𝑀 + 𝐾))) |
16 | 12, 14, 15 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ 𝑖 ∈ 𝑍) → (𝑖 + 𝐾) ∈
(ℤ≥‘(𝑀 + 𝐾))) |
17 | | ulmshft.w |
. . . . . . . 8
⊢ 𝑊 =
(ℤ≥‘(𝑀 + 𝐾)) |
18 | 16, 17 | syl6eleqr 2699 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ 𝑖 ∈ 𝑍) → (𝑖 + 𝐾) ∈ 𝑊) |
19 | | eluzelz 11573 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈
(ℤ≥‘𝑀) → 𝑖 ∈ ℤ) |
20 | 12, 19 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ ℤ) |
21 | 20 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑖 + 𝐾))) → 𝑖 ∈ ℤ) |
22 | 13 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) → 𝐾 ∈ ℤ) |
23 | 22 | ad3antrrr 762 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑖 + 𝐾))) → 𝐾 ∈ ℤ) |
24 | | simpr 476 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑖 + 𝐾))) → 𝑘 ∈ (ℤ≥‘(𝑖 + 𝐾))) |
25 | | eluzsub 11593 |
. . . . . . . . . 10
⊢ ((𝑖 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑘 ∈
(ℤ≥‘(𝑖 + 𝐾))) → (𝑘 − 𝐾) ∈ (ℤ≥‘𝑖)) |
26 | 21, 23, 24, 25 | syl3anc 1318 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑖 + 𝐾))) → (𝑘 − 𝐾) ∈ (ℤ≥‘𝑖)) |
27 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = (𝑘 − 𝐾) → (𝐹‘𝑚) = (𝐹‘(𝑘 − 𝐾))) |
28 | 27 | fveq1d 6105 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑘 − 𝐾) → ((𝐹‘𝑚)‘𝑧) = ((𝐹‘(𝑘 − 𝐾))‘𝑧)) |
29 | 28 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑘 − 𝐾) → (((𝐹‘𝑚)‘𝑧) − (𝐺‘𝑧)) = (((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧))) |
30 | 29 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑘 − 𝐾) → (abs‘(((𝐹‘𝑚)‘𝑧) − (𝐺‘𝑧))) = (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧)))) |
31 | 30 | breq1d 4593 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑘 − 𝐾) → ((abs‘(((𝐹‘𝑚)‘𝑧) − (𝐺‘𝑧))) < 𝑥 ↔ (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧))) < 𝑥)) |
32 | 31 | ralbidv 2969 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑘 − 𝐾) → (∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑚)‘𝑧) − (𝐺‘𝑧))) < 𝑥 ↔ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧))) < 𝑥)) |
33 | 32 | rspcv 3278 |
. . . . . . . . 9
⊢ ((𝑘 − 𝐾) ∈ (ℤ≥‘𝑖) → (∀𝑚 ∈
(ℤ≥‘𝑖)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑚)‘𝑧) − (𝐺‘𝑧))) < 𝑥 → ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧))) < 𝑥)) |
34 | 26, 33 | syl 17 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑖 + 𝐾))) → (∀𝑚 ∈ (ℤ≥‘𝑖)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑚)‘𝑧) − (𝐺‘𝑧))) < 𝑥 → ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧))) < 𝑥)) |
35 | 34 | ralrimdva 2952 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ 𝑖 ∈ 𝑍) → (∀𝑚 ∈ (ℤ≥‘𝑖)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑚)‘𝑧) − (𝐺‘𝑧))) < 𝑥 → ∀𝑘 ∈ (ℤ≥‘(𝑖 + 𝐾))∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧))) < 𝑥)) |
36 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑗 = (𝑖 + 𝐾) → (ℤ≥‘𝑗) =
(ℤ≥‘(𝑖 + 𝐾))) |
37 | 36 | raleqdv 3121 |
. . . . . . . 8
⊢ (𝑗 = (𝑖 + 𝐾) → (∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧))) < 𝑥 ↔ ∀𝑘 ∈ (ℤ≥‘(𝑖 + 𝐾))∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧))) < 𝑥)) |
38 | 37 | rspcev 3282 |
. . . . . . 7
⊢ (((𝑖 + 𝐾) ∈ 𝑊 ∧ ∀𝑘 ∈ (ℤ≥‘(𝑖 + 𝐾))∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧))) < 𝑥) → ∃𝑗 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧))) < 𝑥) |
39 | 18, 35, 38 | syl6an 566 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ 𝑖 ∈ 𝑍) → (∀𝑚 ∈ (ℤ≥‘𝑖)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑚)‘𝑧) − (𝐺‘𝑧))) < 𝑥 → ∃𝑗 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧))) < 𝑥)) |
40 | 39 | rexlimdva 3013 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) →
(∃𝑖 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑖)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑚)‘𝑧) − (𝐺‘𝑧))) < 𝑥 → ∃𝑗 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧))) < 𝑥)) |
41 | 10, 40 | mpd 15 |
. . . 4
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧))) < 𝑥) |
42 | 41 | ralrimiva 2949 |
. . 3
⊢ ((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧))) < 𝑥) |
43 | 2, 13 | zaddcld 11362 |
. . . . 5
⊢ (𝜑 → (𝑀 + 𝐾) ∈ ℤ) |
44 | 43 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) → (𝑀 + 𝐾) ∈ ℤ) |
45 | 4 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑊) → 𝐹:𝑍⟶(ℂ ↑𝑚
𝑆)) |
46 | 2 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑊) → 𝑀 ∈ ℤ) |
47 | 13 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑊) → 𝐾 ∈ ℤ) |
48 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑊) → 𝑛 ∈ 𝑊) |
49 | 48, 17 | syl6eleq 2698 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑊) → 𝑛 ∈ (ℤ≥‘(𝑀 + 𝐾))) |
50 | | eluzsub 11593 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑛 ∈
(ℤ≥‘(𝑀 + 𝐾))) → (𝑛 − 𝐾) ∈ (ℤ≥‘𝑀)) |
51 | 46, 47, 49, 50 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑊) → (𝑛 − 𝐾) ∈ (ℤ≥‘𝑀)) |
52 | 51, 1 | syl6eleqr 2699 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑊) → (𝑛 − 𝐾) ∈ 𝑍) |
53 | 45, 52 | ffvelrnd 6268 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑊) → (𝐹‘(𝑛 − 𝐾)) ∈ (ℂ
↑𝑚 𝑆)) |
54 | | eqid 2610 |
. . . . . . 7
⊢ (𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾))) = (𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾))) |
55 | 53, 54 | fmptd 6292 |
. . . . . 6
⊢ (𝜑 → (𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾))):𝑊⟶(ℂ ↑𝑚
𝑆)) |
56 | | ulmshft.h |
. . . . . . 7
⊢ (𝜑 → 𝐻 = (𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾)))) |
57 | 56 | feq1d 5943 |
. . . . . 6
⊢ (𝜑 → (𝐻:𝑊⟶(ℂ ↑𝑚
𝑆) ↔ (𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾))):𝑊⟶(ℂ ↑𝑚
𝑆))) |
58 | 55, 57 | mpbird 246 |
. . . . 5
⊢ (𝜑 → 𝐻:𝑊⟶(ℂ ↑𝑚
𝑆)) |
59 | 58 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) → 𝐻:𝑊⟶(ℂ ↑𝑚
𝑆)) |
60 | 56 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ (𝑘 ∈ 𝑊 ∧ 𝑧 ∈ 𝑆)) → 𝐻 = (𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾)))) |
61 | 60 | fveq1d 6105 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ (𝑘 ∈ 𝑊 ∧ 𝑧 ∈ 𝑆)) → (𝐻‘𝑘) = ((𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾)))‘𝑘)) |
62 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → (𝑛 − 𝐾) = (𝑘 − 𝐾)) |
63 | 62 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → (𝐹‘(𝑛 − 𝐾)) = (𝐹‘(𝑘 − 𝐾))) |
64 | | fvex 6113 |
. . . . . . . 8
⊢ (𝐹‘(𝑘 − 𝐾)) ∈ V |
65 | 63, 54, 64 | fvmpt 6191 |
. . . . . . 7
⊢ (𝑘 ∈ 𝑊 → ((𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾)))‘𝑘) = (𝐹‘(𝑘 − 𝐾))) |
66 | 65 | ad2antrl 760 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ (𝑘 ∈ 𝑊 ∧ 𝑧 ∈ 𝑆)) → ((𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾)))‘𝑘) = (𝐹‘(𝑘 − 𝐾))) |
67 | 61, 66 | eqtrd 2644 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ (𝑘 ∈ 𝑊 ∧ 𝑧 ∈ 𝑆)) → (𝐻‘𝑘) = (𝐹‘(𝑘 − 𝐾))) |
68 | 67 | fveq1d 6105 |
. . . 4
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ (𝑘 ∈ 𝑊 ∧ 𝑧 ∈ 𝑆)) → ((𝐻‘𝑘)‘𝑧) = ((𝐹‘(𝑘 − 𝐾))‘𝑧)) |
69 | | eqidd 2611 |
. . . 4
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = (𝐺‘𝑧)) |
70 | | ulmcl 23939 |
. . . . 5
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → 𝐺:𝑆⟶ℂ) |
71 | 70 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) → 𝐺:𝑆⟶ℂ) |
72 | | ulmscl 23937 |
. . . . 5
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → 𝑆 ∈ V) |
73 | 72 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) → 𝑆 ∈ V) |
74 | 17, 44, 59, 68, 69, 71, 73 | ulm2 23943 |
. . 3
⊢ ((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) → (𝐻(⇝𝑢‘𝑆)𝐺 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧))) < 𝑥)) |
75 | 42, 74 | mpbird 246 |
. 2
⊢ ((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) → 𝐻(⇝𝑢‘𝑆)𝐺) |
76 | 75 | ex 449 |
1
⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 → 𝐻(⇝𝑢‘𝑆)𝐺)) |