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 ffvelrnd ( ( ( ( 𝜑𝑘𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧𝑆 ∧ ( ( 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 ffvelrnd ( ( ( ( 𝜑𝑘𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧𝑆 ∧ ( ( abs ‘ ( ( 𝐹𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 1 ) ) ) → ( 𝐹𝑘 ) ∈ ( ℂ ↑m 𝑆 ) )
24 elmapi ( ( 𝐹𝑘 ) ∈ ( ℂ ↑m 𝑆 ) → ( 𝐹𝑘 ) : 𝑆 ⟶ ℂ )
25 23 24 syl ( ( ( ( 𝜑𝑘𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧𝑆 ∧ ( ( abs ‘ ( ( 𝐹𝑘 ) ‘ 𝑧 ) ) ≤ 𝑥 ∧ ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 1 ) ) ) → ( 𝐹𝑘 ) : 𝑆 ⟶ ℂ )
26 25 18 ffvelrnd ( ( ( ( 𝜑𝑘𝑍 ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑧𝑆 ∧ ( ( 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 syl5bir ( ( ( 𝜑𝑘𝑍 ) ∧ 𝑥 ∈ ℝ ) → ( ( ∀ 𝑧𝑆 ( 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 syl6ib ( ( 𝜑𝑘𝑍 ) → ( ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 1 → ∃ 𝑥 ∈ ℝ ∀ 𝑧𝑆 ( abs ‘ ( 𝐺𝑧 ) ) ≤ 𝑥 ) )
60 59 rexlimdva ( 𝜑 → ( ∃ 𝑘𝑍𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 1 → ∃ 𝑥 ∈ ℝ ∀ 𝑧𝑆 ( abs ‘ ( 𝐺𝑧 ) ) ≤ 𝑥 ) )
61 11 60 syl5 ( 𝜑 → ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑧𝑆 ( abs ‘ ( ( ( 𝐹𝑘 ) ‘ 𝑧 ) − ( 𝐺𝑧 ) ) ) < 1 → ∃ 𝑥 ∈ ℝ ∀ 𝑧𝑆 ( abs ‘ ( 𝐺𝑧 ) ) ≤ 𝑥 ) )
62 10 61 mpd ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑧𝑆 ( abs ‘ ( 𝐺𝑧 ) ) ≤ 𝑥 )