Metamath Proof Explorer

Theorem ulmbdd

Description: A uniform limit of bounded functions is bounded. (Contributed by Mario Carneiro, 27-Feb-2015)

Ref Expression
Hypotheses ulmbdd.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
ulmbdd.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
ulmbdd.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
ulmbdd.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 )
ulmbdd.u ⊢ ( 𝜑 → 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 )
Assertion ulmbdd ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑥 )

Proof

Step Hyp Ref Expression
1 ulmbdd.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 ulmbdd.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 ulmbdd.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
4 ulmbdd.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 )
5 ulmbdd.u ⊢ ( 𝜑 → 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 )
6 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) )
7 eqidd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
8 1rp ⊢ 1 ∈ ℝ+
9 8 a1i ⊢ ( 𝜑 → 1 ∈ ℝ+ )
10 1 2 3 6 7 5 9 ulmi ⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 )
11 1 r19.2uz ⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 → ∃ 𝑘 ∈ 𝑍 ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 )
12 r19.26 ⊢ ( ∀ 𝑧 ∈ 𝑆 ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) ↔ ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) )
13 peano2re ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 + 1 ) ∈ ℝ )
14 13 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 + 1 ) ∈ ℝ )
15 ulmcl ⊢ ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → 𝐺 : 𝑆 ⟶ ℂ )
16 5 15 syl ⊢ ( 𝜑 → 𝐺 : 𝑆 ⟶ ℂ )
17 16 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) ) ) → 𝐺 : 𝑆 ⟶ ℂ )
18 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) ) ) → 𝑧 ∈ 𝑆 )
19 17 18 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
20 19 abscld ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) ) ) → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ℝ )
21 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) ) ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
22 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) ) ) → 𝑘 ∈ 𝑍 )
23 21 22 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℂ ↑m 𝑆 ) )
24 elmapi ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ( ℂ ↑m 𝑆 ) → ( 𝐹 ‘ 𝑘 ) : 𝑆 ⟶ ℂ )
25 23 24 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) : 𝑆 ⟶ ℂ )
26 25 18 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) ) ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ∈ ℂ )
27 26 abscld ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ∈ ℝ )
28 19 26 subcld ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) ) ) → ( ( 𝐺 ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ∈ ℂ )
29 28 abscld ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ) ∈ ℝ )
30 27 29 readdcld ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) + ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ) ) ∈ ℝ )
31 14 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) ) ) → ( 𝑥 + 1 ) ∈ ℝ )
32 26 19 pncan3d ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) ) ) → ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) + ( ( 𝐺 ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ) = ( 𝐺 ‘ 𝑧 ) )
33 32 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) + ( ( 𝐺 ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ) ) = ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) )
34 26 28 abstrid ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) + ( ( 𝐺 ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ) ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) + ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ) ) )
35 33 34 eqbrtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) ) ) → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) + ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ) ) )
36 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) ) ) → 𝑥 ∈ ℝ )
37 1re ⊢ 1 ∈ ℝ
38 37 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) ) ) → 1 ∈ ℝ )
39 simprrl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 )
40 19 26 abssubd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) )
41 simprrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 )
42 40 41 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ) < 1 )
43 ltle ⊢ ( ( ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ) < 1 → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ) ≤ 1 ) )
44 29 37 43 sylancl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) ) ) → ( ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ) < 1 → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ) ≤ 1 ) )
45 42 44 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ) ≤ 1 )
46 27 29 36 38 39 45 le2addd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) + ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ) ) ≤ ( 𝑥 + 1 ) )
47 20 30 31 35 46 letrd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧 ∈ 𝑆 ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) ) ) → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ ( 𝑥 + 1 ) )
48 47 expr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ 𝑆 ) → ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ ( 𝑥 + 1 ) ) )
49 48 ralimdva ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑧 ∈ 𝑆 ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) → ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ ( 𝑥 + 1 ) ) )
50 brralrspcev ⊢ ( ( ( 𝑥 + 1 ) ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ ( 𝑥 + 1 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑦 )
51 14 49 50 syl6an ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑧 ∈ 𝑆 ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑦 ) )
52 12 51 biimtrrid ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) → ( ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑦 ) )
53 52 expd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑦 ) ) )
54 53 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑦 ) ) )
55 4 54 mpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑦 ) )
56 breq2 ⊢ ( 𝑦 = 𝑥 → ( ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑦 ↔ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑥 ) )
57 56 ralbidv ⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑦 ↔ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑥 ) )
58 57 cbvrexvw ⊢ ( ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑦 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑥 )
59 55 58 imbitrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑥 ) )
60 59 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ 𝑍 ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑥 ) )
61 11 60 syl5 ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 1 → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑥 ) )
62 10 61 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ 𝑥 )