| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | itgulm.z | . . . 4
⊢ 𝑍 =
(ℤ≥‘𝑀) | 
| 2 |  | itgulm.m | . . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 3 |  | itgulm.f | . . . . . 6
⊢ (𝜑 → 𝐹:𝑍⟶𝐿1) | 
| 4 | 3 | ffnd 6737 | . . . . 5
⊢ (𝜑 → 𝐹 Fn 𝑍) | 
| 5 |  | itgulm.u | . . . . 5
⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺) | 
| 6 |  | ulmf2 26427 | . . . . 5
⊢ ((𝐹 Fn 𝑍 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) | 
| 7 | 4, 5, 6 | syl2anc 584 | . . . 4
⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) | 
| 8 |  | eqidd 2738 | . . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑥 ∈ 𝑆)) → ((𝐹‘𝑘)‘𝑥) = ((𝐹‘𝑘)‘𝑥)) | 
| 9 |  | eqidd 2738 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐺‘𝑥) = (𝐺‘𝑥)) | 
| 10 |  | 1rp 13038 | . . . . 5
⊢ 1 ∈
ℝ+ | 
| 11 | 10 | a1i 11 | . . . 4
⊢ (𝜑 → 1 ∈
ℝ+) | 
| 12 | 1, 2, 7, 8, 9, 5, 11 | ulmi 26429 | . . 3
⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1) | 
| 13 | 1 | r19.2uz 15390 | . . 3
⊢
(∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1 → ∃𝑘 ∈ 𝑍 ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1) | 
| 14 | 12, 13 | syl 17 | . 2
⊢ (𝜑 → ∃𝑘 ∈ 𝑍 ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1) | 
| 15 |  | ulmcl 26424 | . . . . . . 7
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → 𝐺:𝑆⟶ℂ) | 
| 16 | 5, 15 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝐺:𝑆⟶ℂ) | 
| 17 | 16 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1)) → 𝐺:𝑆⟶ℂ) | 
| 18 | 17 | feqmptd 6977 | . . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1)) → 𝐺 = (𝑧 ∈ 𝑆 ↦ (𝐺‘𝑧))) | 
| 19 | 7 | ffvelcdmda 7104 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ (ℂ ↑m 𝑆)) | 
| 20 |  | elmapi 8889 | . . . . . . . . 9
⊢ ((𝐹‘𝑘) ∈ (ℂ ↑m 𝑆) → (𝐹‘𝑘):𝑆⟶ℂ) | 
| 21 | 19, 20 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘):𝑆⟶ℂ) | 
| 22 | 21 | adantrr 717 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1)) → (𝐹‘𝑘):𝑆⟶ℂ) | 
| 23 | 22 | ffvelcdmda 7104 | . . . . . 6
⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1)) ∧ 𝑧 ∈ 𝑆) → ((𝐹‘𝑘)‘𝑧) ∈ ℂ) | 
| 24 | 17 | ffvelcdmda 7104 | . . . . . 6
⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1)) ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) ∈ ℂ) | 
| 25 | 23, 24 | nncand 11625 | . . . . 5
⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1)) ∧ 𝑧 ∈ 𝑆) → (((𝐹‘𝑘)‘𝑧) − (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) = (𝐺‘𝑧)) | 
| 26 | 25 | mpteq2dva 5242 | . . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1)) → (𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧)))) = (𝑧 ∈ 𝑆 ↦ (𝐺‘𝑧))) | 
| 27 | 18, 26 | eqtr4d 2780 | . . 3
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1)) → 𝐺 = (𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))))) | 
| 28 | 22 | feqmptd 6977 | . . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1)) → (𝐹‘𝑘) = (𝑧 ∈ 𝑆 ↦ ((𝐹‘𝑘)‘𝑧))) | 
| 29 | 3 | ffvelcdmda 7104 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈
𝐿1) | 
| 30 | 29 | adantrr 717 | . . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1)) → (𝐹‘𝑘) ∈
𝐿1) | 
| 31 | 28, 30 | eqeltrrd 2842 | . . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1)) → (𝑧 ∈ 𝑆 ↦ ((𝐹‘𝑘)‘𝑧)) ∈
𝐿1) | 
| 32 | 23, 24 | subcld 11620 | . . . 4
⊢ (((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1)) ∧ 𝑧 ∈ 𝑆) → (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧)) ∈ ℂ) | 
| 33 |  | ulmscl 26422 | . . . . . . . . 9
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → 𝑆 ∈ V) | 
| 34 | 5, 33 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ V) | 
| 35 | 34 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1)) → 𝑆 ∈ V) | 
| 36 | 35, 23, 24, 28, 18 | offval2 7717 | . . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1)) → ((𝐹‘𝑘) ∘f − 𝐺) = (𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧)))) | 
| 37 |  | iblmbf 25802 | . . . . . . . 8
⊢ ((𝐹‘𝑘) ∈ 𝐿1 → (𝐹‘𝑘) ∈ MblFn) | 
| 38 | 30, 37 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1)) → (𝐹‘𝑘) ∈ MblFn) | 
| 39 |  | iblmbf 25802 | . . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐿1
→ 𝑥 ∈
MblFn) | 
| 40 | 39 | ssriv 3987 | . . . . . . . . . 10
⊢
𝐿1 ⊆ MblFn | 
| 41 |  | fss 6752 | . . . . . . . . . 10
⊢ ((𝐹:𝑍⟶𝐿1 ∧
𝐿1 ⊆ MblFn) → 𝐹:𝑍⟶MblFn) | 
| 42 | 3, 40, 41 | sylancl 586 | . . . . . . . . 9
⊢ (𝜑 → 𝐹:𝑍⟶MblFn) | 
| 43 | 1, 2, 42, 5 | mbfulm 26449 | . . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ MblFn) | 
| 44 | 43 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1)) → 𝐺 ∈ MblFn) | 
| 45 | 38, 44 | mbfsub 25697 | . . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1)) → ((𝐹‘𝑘) ∘f − 𝐺) ∈ MblFn) | 
| 46 | 36, 45 | eqeltrrd 2842 | . . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1)) → (𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) ∈ MblFn) | 
| 47 |  | eqid 2737 | . . . . . . . 8
⊢ (𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) = (𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) | 
| 48 | 47, 32 | dmmptd 6713 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1)) → dom (𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) = 𝑆) | 
| 49 | 48 | fveq2d 6910 | . . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1)) → (vol‘dom (𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧)))) = (vol‘𝑆)) | 
| 50 |  | itgulm.s | . . . . . . 7
⊢ (𝜑 → (vol‘𝑆) ∈
ℝ) | 
| 51 | 50 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1)) → (vol‘𝑆) ∈
ℝ) | 
| 52 | 49, 51 | eqeltrd 2841 | . . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1)) → (vol‘dom (𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧)))) ∈ ℝ) | 
| 53 |  | 1re 11261 | . . . . . 6
⊢ 1 ∈
ℝ | 
| 54 | 21 | ffvelcdmda 7104 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → ((𝐹‘𝑘)‘𝑥) ∈ ℂ) | 
| 55 | 16 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐺:𝑆⟶ℂ) | 
| 56 | 55 | ffvelcdmda 7104 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → (𝐺‘𝑥) ∈ ℂ) | 
| 57 | 54, 56 | subcld 11620 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → (((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥)) ∈ ℂ) | 
| 58 | 57 | abscld 15475 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) ∈ ℝ) | 
| 59 |  | ltle 11349 | . . . . . . . . . . 11
⊢
(((abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) ∈ ℝ ∧ 1 ∈ ℝ)
→ ((abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1 → (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) ≤ 1)) | 
| 60 | 58, 53, 59 | sylancl 586 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → ((abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1 → (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) ≤ 1)) | 
| 61 |  | fveq2 6906 | . . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑥 → ((𝐹‘𝑘)‘𝑧) = ((𝐹‘𝑘)‘𝑥)) | 
| 62 |  | fveq2 6906 | . . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑥 → (𝐺‘𝑧) = (𝐺‘𝑥)) | 
| 63 | 61, 62 | oveq12d 7449 | . . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑥 → (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧)) = (((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) | 
| 64 |  | ovex 7464 | . . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥)) ∈ V | 
| 65 | 63, 47, 64 | fvmpt 7016 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝑆 → ((𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧)))‘𝑥) = (((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) | 
| 66 | 65 | adantl 481 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → ((𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧)))‘𝑥) = (((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) | 
| 67 | 66 | fveq2d 6910 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → (abs‘((𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧)))‘𝑥)) = (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥)))) | 
| 68 | 67 | breq1d 5153 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → ((abs‘((𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧)))‘𝑥)) ≤ 1 ↔ (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) ≤ 1)) | 
| 69 | 60, 68 | sylibrd 259 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → ((abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1 → (abs‘((𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧)))‘𝑥)) ≤ 1)) | 
| 70 | 69 | ralimdva 3167 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1 → ∀𝑥 ∈ 𝑆 (abs‘((𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧)))‘𝑥)) ≤ 1)) | 
| 71 | 70 | impr 454 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1)) → ∀𝑥 ∈ 𝑆 (abs‘((𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧)))‘𝑥)) ≤ 1) | 
| 72 | 71, 48 | raleqtrrdv 3330 | . . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1)) → ∀𝑥 ∈ dom (𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧)))(abs‘((𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧)))‘𝑥)) ≤ 1) | 
| 73 |  | brralrspcev 5203 | . . . . . 6
⊢ ((1
∈ ℝ ∧ ∀𝑥 ∈ dom (𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧)))(abs‘((𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧)))‘𝑥)) ≤ 1) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ dom (𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧)))(abs‘((𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧)))‘𝑥)) ≤ 𝑟) | 
| 74 | 53, 72, 73 | sylancr 587 | . . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1)) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ dom (𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧)))(abs‘((𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧)))‘𝑥)) ≤ 𝑟) | 
| 75 |  | bddibl 25875 | . . . . 5
⊢ (((𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) ∈ MblFn ∧ (vol‘dom (𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧)))) ∈ ℝ ∧ ∃𝑟 ∈ ℝ ∀𝑥 ∈ dom (𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧)))(abs‘((𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧)))‘𝑥)) ≤ 𝑟) → (𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) ∈
𝐿1) | 
| 76 | 46, 52, 74, 75 | syl3anc 1373 | . . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1)) → (𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) ∈
𝐿1) | 
| 77 | 23, 31, 32, 76 | iblsub 25857 | . . 3
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1)) → (𝑧 ∈ 𝑆 ↦ (((𝐹‘𝑘)‘𝑧) − (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧)))) ∈
𝐿1) | 
| 78 | 27, 77 | eqeltrd 2841 | . 2
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ ∀𝑥 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑥) − (𝐺‘𝑥))) < 1)) → 𝐺 ∈
𝐿1) | 
| 79 | 14, 78 | rexlimddv 3161 | 1
⊢ (𝜑 → 𝐺 ∈
𝐿1) |