| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ulmshft.z | . . . . . 6
⊢ 𝑍 =
(ℤ≥‘𝑀) | 
| 2 |  | ulmshft.m | . . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 3 | 2 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) → 𝑀 ∈
ℤ) | 
| 4 |  | ulmshft.f | . . . . . . 7
⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) | 
| 5 | 4 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) | 
| 6 |  | eqidd 2737 | . . . . . 6
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ (𝑚 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → ((𝐹‘𝑚)‘𝑧) = ((𝐹‘𝑚)‘𝑧)) | 
| 7 |  | eqidd 2737 | . . . . . 6
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = (𝐺‘𝑧)) | 
| 8 |  | simplr 768 | . . . . . 6
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) → 𝐹(⇝𝑢‘𝑆)𝐺) | 
| 9 |  | simpr 484 | . . . . . 6
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) | 
| 10 | 1, 3, 5, 6, 7, 8, 9 | ulmi 26430 | . . . . 5
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) →
∃𝑖 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑖)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑚)‘𝑧) − (𝐺‘𝑧))) < 𝑥) | 
| 11 |  | simpr 484 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ 𝑍) | 
| 12 | 11, 1 | eleqtrdi 2850 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ (ℤ≥‘𝑀)) | 
| 13 |  | ulmshft.k | . . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ ℤ) | 
| 14 | 13 | ad3antrrr 730 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ 𝑖 ∈ 𝑍) → 𝐾 ∈ ℤ) | 
| 15 |  | eluzadd 12908 | . . . . . . . . 9
⊢ ((𝑖 ∈
(ℤ≥‘𝑀) ∧ 𝐾 ∈ ℤ) → (𝑖 + 𝐾) ∈
(ℤ≥‘(𝑀 + 𝐾))) | 
| 16 | 12, 14, 15 | syl2anc 584 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ 𝑖 ∈ 𝑍) → (𝑖 + 𝐾) ∈
(ℤ≥‘(𝑀 + 𝐾))) | 
| 17 |  | ulmshft.w | . . . . . . . 8
⊢ 𝑊 =
(ℤ≥‘(𝑀 + 𝐾)) | 
| 18 | 16, 17 | eleqtrrdi 2851 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ 𝑖 ∈ 𝑍) → (𝑖 + 𝐾) ∈ 𝑊) | 
| 19 |  | eluzelz 12889 | . . . . . . . . . . . 12
⊢ (𝑖 ∈
(ℤ≥‘𝑀) → 𝑖 ∈ ℤ) | 
| 20 | 12, 19 | syl 17 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ ℤ) | 
| 21 | 20 | adantr 480 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑖 + 𝐾))) → 𝑖 ∈ ℤ) | 
| 22 | 13 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) → 𝐾 ∈ ℤ) | 
| 23 | 22 | ad3antrrr 730 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑖 + 𝐾))) → 𝐾 ∈ ℤ) | 
| 24 |  | simpr 484 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑖 + 𝐾))) → 𝑘 ∈ (ℤ≥‘(𝑖 + 𝐾))) | 
| 25 |  | eluzsub 12909 | . . . . . . . . . 10
⊢ ((𝑖 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑘 ∈
(ℤ≥‘(𝑖 + 𝐾))) → (𝑘 − 𝐾) ∈ (ℤ≥‘𝑖)) | 
| 26 | 21, 23, 24, 25 | syl3anc 1372 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑖 + 𝐾))) → (𝑘 − 𝐾) ∈ (ℤ≥‘𝑖)) | 
| 27 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑘 − 𝐾) → (𝐹‘𝑚) = (𝐹‘(𝑘 − 𝐾))) | 
| 28 | 27 | fveq1d 6907 | . . . . . . . . . . . . 13
⊢ (𝑚 = (𝑘 − 𝐾) → ((𝐹‘𝑚)‘𝑧) = ((𝐹‘(𝑘 − 𝐾))‘𝑧)) | 
| 29 | 28 | fvoveq1d 7454 | . . . . . . . . . . . 12
⊢ (𝑚 = (𝑘 − 𝐾) → (abs‘(((𝐹‘𝑚)‘𝑧) − (𝐺‘𝑧))) = (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧)))) | 
| 30 | 29 | breq1d 5152 | . . . . . . . . . . 11
⊢ (𝑚 = (𝑘 − 𝐾) → ((abs‘(((𝐹‘𝑚)‘𝑧) − (𝐺‘𝑧))) < 𝑥 ↔ (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧))) < 𝑥)) | 
| 31 | 30 | ralbidv 3177 | . . . . . . . . . 10
⊢ (𝑚 = (𝑘 − 𝐾) → (∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑚)‘𝑧) − (𝐺‘𝑧))) < 𝑥 ↔ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧))) < 𝑥)) | 
| 32 | 31 | rspcv 3617 | . . . . . . . . 9
⊢ ((𝑘 − 𝐾) ∈ (ℤ≥‘𝑖) → (∀𝑚 ∈
(ℤ≥‘𝑖)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑚)‘𝑧) − (𝐺‘𝑧))) < 𝑥 → ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧))) < 𝑥)) | 
| 33 | 26, 32 | syl 17 | . . . . . . . 8
⊢
(((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑖 + 𝐾))) → (∀𝑚 ∈ (ℤ≥‘𝑖)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑚)‘𝑧) − (𝐺‘𝑧))) < 𝑥 → ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧))) < 𝑥)) | 
| 34 | 33 | ralrimdva 3153 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ 𝑖 ∈ 𝑍) → (∀𝑚 ∈ (ℤ≥‘𝑖)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑚)‘𝑧) − (𝐺‘𝑧))) < 𝑥 → ∀𝑘 ∈ (ℤ≥‘(𝑖 + 𝐾))∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧))) < 𝑥)) | 
| 35 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑗 = (𝑖 + 𝐾) → (ℤ≥‘𝑗) =
(ℤ≥‘(𝑖 + 𝐾))) | 
| 36 | 35 | raleqdv 3325 | . . . . . . . 8
⊢ (𝑗 = (𝑖 + 𝐾) → (∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧))) < 𝑥 ↔ ∀𝑘 ∈ (ℤ≥‘(𝑖 + 𝐾))∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧))) < 𝑥)) | 
| 37 | 36 | rspcev 3621 | . . . . . . 7
⊢ (((𝑖 + 𝐾) ∈ 𝑊 ∧ ∀𝑘 ∈ (ℤ≥‘(𝑖 + 𝐾))∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧))) < 𝑥) → ∃𝑗 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧))) < 𝑥) | 
| 38 | 18, 34, 37 | syl6an 684 | . . . . . 6
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) ∧ 𝑖 ∈ 𝑍) → (∀𝑚 ∈ (ℤ≥‘𝑖)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑚)‘𝑧) − (𝐺‘𝑧))) < 𝑥 → ∃𝑗 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧))) < 𝑥)) | 
| 39 | 38 | rexlimdva 3154 | . . . . 5
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) →
(∃𝑖 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑖)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑚)‘𝑧) − (𝐺‘𝑧))) < 𝑥 → ∃𝑗 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧))) < 𝑥)) | 
| 40 | 10, 39 | mpd 15 | . . . 4
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧))) < 𝑥) | 
| 41 | 40 | ralrimiva 3145 | . . 3
⊢ ((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧))) < 𝑥) | 
| 42 | 2, 13 | zaddcld 12728 | . . . . 5
⊢ (𝜑 → (𝑀 + 𝐾) ∈ ℤ) | 
| 43 | 42 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) → (𝑀 + 𝐾) ∈ ℤ) | 
| 44 |  | ulmshft.h | . . . . . 6
⊢ (𝜑 → 𝐻 = (𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾)))) | 
| 45 | 4 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑊) → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) | 
| 46 | 2 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑊) → 𝑀 ∈ ℤ) | 
| 47 | 13 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑊) → 𝐾 ∈ ℤ) | 
| 48 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑊) → 𝑛 ∈ 𝑊) | 
| 49 | 48, 17 | eleqtrdi 2850 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑊) → 𝑛 ∈ (ℤ≥‘(𝑀 + 𝐾))) | 
| 50 |  | eluzsub 12909 | . . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑛 ∈
(ℤ≥‘(𝑀 + 𝐾))) → (𝑛 − 𝐾) ∈ (ℤ≥‘𝑀)) | 
| 51 | 46, 47, 49, 50 | syl3anc 1372 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑊) → (𝑛 − 𝐾) ∈ (ℤ≥‘𝑀)) | 
| 52 | 51, 1 | eleqtrrdi 2851 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑊) → (𝑛 − 𝐾) ∈ 𝑍) | 
| 53 | 45, 52 | ffvelcdmd 7104 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑊) → (𝐹‘(𝑛 − 𝐾)) ∈ (ℂ ↑m 𝑆)) | 
| 54 | 44, 53 | fmpt3d 7135 | . . . . 5
⊢ (𝜑 → 𝐻:𝑊⟶(ℂ ↑m 𝑆)) | 
| 55 | 54 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) → 𝐻:𝑊⟶(ℂ ↑m 𝑆)) | 
| 56 | 44 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ (𝑘 ∈ 𝑊 ∧ 𝑧 ∈ 𝑆)) → 𝐻 = (𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾)))) | 
| 57 | 56 | fveq1d 6907 | . . . . . 6
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ (𝑘 ∈ 𝑊 ∧ 𝑧 ∈ 𝑆)) → (𝐻‘𝑘) = ((𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾)))‘𝑘)) | 
| 58 |  | fvoveq1 7455 | . . . . . . . 8
⊢ (𝑛 = 𝑘 → (𝐹‘(𝑛 − 𝐾)) = (𝐹‘(𝑘 − 𝐾))) | 
| 59 |  | eqid 2736 | . . . . . . . 8
⊢ (𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾))) = (𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾))) | 
| 60 |  | fvex 6918 | . . . . . . . 8
⊢ (𝐹‘(𝑘 − 𝐾)) ∈ V | 
| 61 | 58, 59, 60 | fvmpt 7015 | . . . . . . 7
⊢ (𝑘 ∈ 𝑊 → ((𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾)))‘𝑘) = (𝐹‘(𝑘 − 𝐾))) | 
| 62 | 61 | ad2antrl 728 | . . . . . 6
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ (𝑘 ∈ 𝑊 ∧ 𝑧 ∈ 𝑆)) → ((𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾)))‘𝑘) = (𝐹‘(𝑘 − 𝐾))) | 
| 63 | 57, 62 | eqtrd 2776 | . . . . 5
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ (𝑘 ∈ 𝑊 ∧ 𝑧 ∈ 𝑆)) → (𝐻‘𝑘) = (𝐹‘(𝑘 − 𝐾))) | 
| 64 | 63 | fveq1d 6907 | . . . 4
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ (𝑘 ∈ 𝑊 ∧ 𝑧 ∈ 𝑆)) → ((𝐻‘𝑘)‘𝑧) = ((𝐹‘(𝑘 − 𝐾))‘𝑧)) | 
| 65 |  | eqidd 2737 | . . . 4
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = (𝐺‘𝑧)) | 
| 66 |  | ulmcl 26425 | . . . . 5
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → 𝐺:𝑆⟶ℂ) | 
| 67 | 66 | adantl 481 | . . . 4
⊢ ((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) → 𝐺:𝑆⟶ℂ) | 
| 68 |  | ulmscl 26423 | . . . . 5
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → 𝑆 ∈ V) | 
| 69 | 68 | adantl 481 | . . . 4
⊢ ((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) → 𝑆 ∈ V) | 
| 70 | 17, 43, 55, 64, 65, 67, 69 | ulm2 26429 | . . 3
⊢ ((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) → (𝐻(⇝𝑢‘𝑆)𝐺 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘(𝑘 − 𝐾))‘𝑧) − (𝐺‘𝑧))) < 𝑥)) | 
| 71 | 41, 70 | mpbird 257 | . 2
⊢ ((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) → 𝐻(⇝𝑢‘𝑆)𝐺) | 
| 72 | 71 | ex 412 | 1
⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 → 𝐻(⇝𝑢‘𝑆)𝐺)) |