Metamath Proof Explorer

Theorem ulmcn

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

Ref Expression
Hypotheses ulmcn.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
ulmcn.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
ulmcn.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( 𝑆 –cn→ ℂ ) )
ulmcn.u ⊢ ( 𝜑 → 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 )
Assertion ulmcn ( 𝜑 → 𝐺 ∈ ( 𝑆 –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 ulmcn.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 ulmcn.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 ulmcn.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( 𝑆 –cn→ ℂ ) )
4 ulmcn.u ⊢ ( 𝜑 → 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 )
5 ulmcl ⊢ ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → 𝐺 : 𝑆 ⟶ ℂ )
6 4 5 syl ⊢ ( 𝜑 → 𝐺 : 𝑆 ⟶ ℂ )
7 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) → 𝑀 ∈ ℤ )
8 cncff ⊢ ( 𝑥 ∈ ( 𝑆 –cn→ ℂ ) → 𝑥 : 𝑆 ⟶ ℂ )
9 cnex ⊢ ℂ ∈ V
10 cncfrss ⊢ ( 𝑥 ∈ ( 𝑆 –cn→ ℂ ) → 𝑆 ⊆ ℂ )
11 ssexg ⊢ ( ( 𝑆 ⊆ ℂ ∧ ℂ ∈ V ) → 𝑆 ∈ V )
12 10 9 11 sylancl ⊢ ( 𝑥 ∈ ( 𝑆 –cn→ ℂ ) → 𝑆 ∈ V )
13 elmapg ⊢ ( ( ℂ ∈ V ∧ 𝑆 ∈ V ) → ( 𝑥 ∈ ( ℂ ↑m 𝑆 ) ↔ 𝑥 : 𝑆 ⟶ ℂ ) )
14 9 12 13 sylancr ⊢ ( 𝑥 ∈ ( 𝑆 –cn→ ℂ ) → ( 𝑥 ∈ ( ℂ ↑m 𝑆 ) ↔ 𝑥 : 𝑆 ⟶ ℂ ) )
15 8 14 mpbird ⊢ ( 𝑥 ∈ ( 𝑆 –cn→ ℂ ) → 𝑥 ∈ ( ℂ ↑m 𝑆 ) )
16 15 ssriv ⊢ ( 𝑆 –cn→ ℂ ) ⊆ ( ℂ ↑m 𝑆 )
17 fss ⊢ ( ( 𝐹 : 𝑍 ⟶ ( 𝑆 –cn→ ℂ ) ∧ ( 𝑆 –cn→ ℂ ) ⊆ ( ℂ ↑m 𝑆 ) ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
18 3 16 17 sylancl ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
19 18 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
20 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑤 ∈ 𝑆 ) ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) = ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) )
21 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) )
22 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) → 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 )
23 rphalfcl ⊢ ( 𝑦 ∈ ℝ+ → ( 𝑦 / 2 ) ∈ ℝ+ )
24 23 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) → ( 𝑦 / 2 ) ∈ ℝ+ )
25 24 rphalfcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) → ( ( 𝑦 / 2 ) / 2 ) ∈ ℝ+ )
26 1 7 19 20 21 22 25 ulmi ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑤 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) )
27 1 r19.2uz ⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑤 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) → ∃ 𝑘 ∈ 𝑍 ∀ 𝑤 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) )
28 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) → 𝑥 ∈ 𝑆 )
29 fveq2 ⊢ ( 𝑤 = 𝑥 → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) = ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) )
30 fveq2 ⊢ ( 𝑤 = 𝑥 → ( 𝐺 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑥 ) )
31 29 30 oveq12d ⊢ ( 𝑤 = 𝑥 → ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) = ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) )
32 31 fveq2d ⊢ ( 𝑤 = 𝑥 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) )
33 32 breq1d ⊢ ( 𝑤 = 𝑥 → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ↔ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ) )
34 33 rspcv ⊢ ( 𝑥 ∈ 𝑆 → ( ∀ 𝑤 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ) )
35 28 34 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) → ( ∀ 𝑤 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ) )
36 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) → 𝐹 : 𝑍 ⟶ ( 𝑆 –cn→ ℂ ) )
37 36 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑆 –cn→ ℂ ) )
38 24 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝑦 / 2 ) ∈ ℝ+ )
39 cncfi ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑆 –cn→ ℂ ) ∧ 𝑥 ∈ 𝑆 ∧ ( 𝑦 / 2 ) ∈ ℝ+ ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑆 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) )
40 37 28 38 39 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑆 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) )
41 40 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ ∀ 𝑤 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑆 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) )
42 r19.26 ⊢ ( ∀ 𝑤 ∈ 𝑆 ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) ↔ ( ∀ 𝑤 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ∧ ∀ 𝑤 ∈ 𝑆 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) )
43 19 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
44 simplr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → 𝑘 ∈ 𝑍 )
45 43 44 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℂ ↑m 𝑆 ) )
46 elmapi ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ( ℂ ↑m 𝑆 ) → ( 𝐹 ‘ 𝑘 ) : 𝑆 ⟶ ℂ )
47 45 46 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝐹 ‘ 𝑘 ) : 𝑆 ⟶ ℂ )
48 28 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
49 47 48 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ∈ ℂ )
50 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → 𝐺 : 𝑆 ⟶ ℂ )
51 50 48 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
52 49 51 subcld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ∈ ℂ )
53 52 abscld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) ∈ ℝ )
54 ffvelrn ⊢ ( ( ( 𝐹 ‘ 𝑘 ) : 𝑆 ⟶ ℂ ∧ 𝑤 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) ∈ ℂ )
55 47 54 sylancom ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) ∈ ℂ )
56 ffvelrn ⊢ ( ( 𝐺 : 𝑆 ⟶ ℂ ∧ 𝑤 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑤 ) ∈ ℂ )
57 50 56 sylancom ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑤 ) ∈ ℂ )
58 55 57 subcld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ∈ ℂ )
59 58 abscld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) ∈ ℝ )
60 38 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝑦 / 2 ) ∈ ℝ+ )
61 60 rphalfcld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( 𝑦 / 2 ) / 2 ) ∈ ℝ+ )
62 61 rpred ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( 𝑦 / 2 ) / 2 ) ∈ ℝ )
63 lt2add ⊢ ( ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) ∈ ℝ ) ∧ ( ( ( 𝑦 / 2 ) / 2 ) ∈ ℝ ∧ ( ( 𝑦 / 2 ) / 2 ) ∈ ℝ ) ) → ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) < ( ( ( 𝑦 / 2 ) / 2 ) + ( ( 𝑦 / 2 ) / 2 ) ) ) )
64 53 59 62 62 63 syl22anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) < ( ( ( 𝑦 / 2 ) / 2 ) + ( ( 𝑦 / 2 ) / 2 ) ) ) )
65 60 rpred ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝑦 / 2 ) ∈ ℝ )
66 65 recnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝑦 / 2 ) ∈ ℂ )
67 66 2halvesd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( ( 𝑦 / 2 ) / 2 ) + ( ( 𝑦 / 2 ) / 2 ) ) = ( 𝑦 / 2 ) )
68 67 breq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) < ( ( ( 𝑦 / 2 ) / 2 ) + ( ( 𝑦 / 2 ) / 2 ) ) ↔ ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) < ( 𝑦 / 2 ) ) )
69 53 59 readdcld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) ∈ ℝ )
70 55 49 subcld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ ℂ )
71 70 abscld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ∈ ℝ )
72 lt2add ⊢ ( ( ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) ∈ ℝ ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ∈ ℝ ) ∧ ( ( 𝑦 / 2 ) ∈ ℝ ∧ ( 𝑦 / 2 ) ∈ ℝ ) ) → ( ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) < ( 𝑦 / 2 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) → ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) < ( ( 𝑦 / 2 ) + ( 𝑦 / 2 ) ) ) )
73 69 71 65 65 72 syl22anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) < ( 𝑦 / 2 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) → ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) < ( ( 𝑦 / 2 ) + ( 𝑦 / 2 ) ) ) )
74 rpre ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ )
75 74 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) → 𝑦 ∈ ℝ )
76 75 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → 𝑦 ∈ ℝ )
77 76 recnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → 𝑦 ∈ ℂ )
78 77 2halvesd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( 𝑦 / 2 ) + ( 𝑦 / 2 ) ) = 𝑦 )
79 78 breq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) < ( ( 𝑦 / 2 ) + ( 𝑦 / 2 ) ) ↔ ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) < 𝑦 ) )
80 57 51 subcld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ∈ ℂ )
81 80 abscld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) ∈ ℝ )
82 57 49 subcld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( 𝐺 ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ∈ ℂ )
83 82 abscld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ∈ ℝ )
84 53 83 readdcld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) ∈ ℝ )
85 69 71 readdcld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) ∈ ℝ )
86 57 51 49 abs3difd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) ≤ ( ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) ) )
87 83 recnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ∈ ℂ )
88 53 recnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) ∈ ℂ )
89 87 88 addcomd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) ) = ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) )
90 86 89 breqtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) ≤ ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) )
91 59 71 readdcld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) ∈ ℝ )
92 57 49 55 abs3difd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ≤ ( ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) )
93 57 55 abssubd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) )
94 93 oveq1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) = ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) )
95 92 94 breqtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ≤ ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) )
96 83 91 53 95 leadd2dd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) ≤ ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) ) )
97 59 recnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) ∈ ℂ )
98 71 recnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ∈ ℂ )
99 88 97 98 addassd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) = ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) ) )
100 96 99 breqtrrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) ≤ ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) )
101 81 84 85 90 100 letrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) ≤ ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) )
102 lelttr ⊢ ( ( ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) ∈ ℝ ∧ ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) ≤ ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) ∧ ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) )
103 81 85 76 102 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) ≤ ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) ∧ ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) )
104 101 103 mpand ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) < 𝑦 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) )
105 79 104 sylbid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) ) < ( ( 𝑦 / 2 ) + ( 𝑦 / 2 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) )
106 73 105 syld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) < ( 𝑦 / 2 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) )
107 106 expd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) < ( 𝑦 / 2 ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
108 68 107 sylbid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) + ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) ) < ( ( ( 𝑦 / 2 ) / 2 ) + ( ( 𝑦 / 2 ) / 2 ) ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
109 64 108 syld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
110 109 expdimp ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 ∈ 𝑆 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
111 110 an32s ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ) ∧ 𝑤 ∈ 𝑆 ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
112 111 imp ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ) ∧ 𝑤 ∈ 𝑆 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) )
113 112 imim2d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ) ∧ 𝑤 ∈ 𝑆 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ) → ( ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) → ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
114 113 expimpd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ) ∧ 𝑤 ∈ 𝑆 ) → ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) → ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
115 114 ralimdva ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ) → ( ∀ 𝑤 ∈ 𝑆 ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ∧ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) → ∀ 𝑤 ∈ 𝑆 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
116 42 115 syl5bir ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ) → ( ( ∀ 𝑤 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ∧ ∀ 𝑤 ∈ 𝑆 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) ) → ∀ 𝑤 ∈ 𝑆 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
117 116 expdimp ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ) ∧ ∀ 𝑤 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ) → ( ∀ 𝑤 ∈ 𝑆 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) → ∀ 𝑤 ∈ 𝑆 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
118 117 an32s ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ ∀ 𝑤 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ) → ( ∀ 𝑤 ∈ 𝑆 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) → ∀ 𝑤 ∈ 𝑆 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
119 118 reximdv ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ ∀ 𝑤 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ) → ( ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑆 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) ) ) < ( 𝑦 / 2 ) ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑆 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
120 41 119 mpd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) ∧ ∀ 𝑤 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑆 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) )
121 120 exp31 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) → ( ∀ 𝑤 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑆 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) ) ) )
122 35 121 mpdd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) → ( ∀ 𝑤 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑆 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
123 122 rexlimdva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) → ( ∃ 𝑘 ∈ 𝑍 ∀ 𝑤 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑆 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
124 27 123 syl5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑤 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑤 ) − ( 𝐺 ‘ 𝑤 ) ) ) < ( ( 𝑦 / 2 ) / 2 ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑆 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
125 26 124 mpd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ℝ+ ) ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑆 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) )
126 125 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑆 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) )
127 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
128 2 127 syl ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
129 128 1 eleqtrrdi ⊢ ( 𝜑 → 𝑀 ∈ 𝑍 )
130 3 129 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ∈ ( 𝑆 –cn→ ℂ ) )
131 cncfrss ⊢ ( ( 𝐹 ‘ 𝑀 ) ∈ ( 𝑆 –cn→ ℂ ) → 𝑆 ⊆ ℂ )
132 130 131 syl ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
133 ssid ⊢ ℂ ⊆ ℂ
134 elcncf2 ⊢ ( ( 𝑆 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝐺 ∈ ( 𝑆 –cn→ ℂ ) ↔ ( 𝐺 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑆 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) ) ) )
135 132 133 134 sylancl ⊢ ( 𝜑 → ( 𝐺 ∈ ( 𝑆 –cn→ ℂ ) ↔ ( 𝐺 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑆 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐺 ‘ 𝑤 ) − ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) ) ) )
136 6 126 135 mpbir2and ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑆 –cn→ ℂ ) )