This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ulmcaulem

Description: Lemma for ulmcau and ulmcau2 : show the equivalence of the four- and five-quantifier forms of the Cauchy convergence condition. Compare cau3 . (Contributed by Mario Carneiro, 1-Mar-2015)

Ref Expression
Hypotheses ulmcau.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
ulmcau.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
ulmcau.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
ulmcau.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
Assertion ulmcaulem ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) )

Proof

Step Hyp Ref Expression
1 ulmcau.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 ulmcau.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 ulmcau.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
4 ulmcau.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
5 breq2 ⊢ ( 𝑥 = 𝑤 → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑤 ) )
6 5 ralbidv ⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑤 ) )
7 6 rexralbidv ⊢ ( 𝑥 = 𝑤 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑤 ) )
8 7 cbvralvw ⊢ ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑤 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑤 )
9 rphalfcl ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 / 2 ) ∈ ℝ+ )
10 breq2 ⊢ ( 𝑤 = ( 𝑥 / 2 ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑤 ↔ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) )
11 10 ralbidv ⊢ ( 𝑤 = ( 𝑥 / 2 ) → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑤 ↔ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) )
12 11 rexralbidv ⊢ ( 𝑤 = ( 𝑥 / 2 ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑤 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) )
13 12 rspcv ⊢ ( ( 𝑥 / 2 ) ∈ ℝ+ → ( ∀ 𝑤 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑤 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) )
14 9 13 syl ⊢ ( 𝑥 ∈ ℝ+ → ( ∀ 𝑤 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑤 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∀ 𝑤 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑤 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) )
16 fveq2 ⊢ ( 𝑘 = 𝑚 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑚 ) )
17 16 fveq1d ⊢ ( 𝑘 = 𝑚 → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) )
18 17 fvoveq1d ⊢ ( 𝑘 = 𝑚 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) )
19 18 breq1d ⊢ ( 𝑘 = 𝑚 → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ↔ ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) )
20 19 ralbidv ⊢ ( 𝑘 = 𝑚 → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ↔ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) )
21 20 cbvralvw ⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) )
22 21 biimpi ⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) )
23 uzss ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) → ( ℤ≥ ‘ 𝑘 ) ⊆ ( ℤ≥ ‘ 𝑗 ) )
24 23 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) → ( ℤ≥ ‘ 𝑘 ) ⊆ ( ℤ≥ ‘ 𝑗 ) )
25 ssralv ⊢ ( ( ℤ≥ ‘ 𝑘 ) ⊆ ( ℤ≥ ‘ 𝑗 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) )
26 24 25 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) )
27 r19.26 ⊢ ( ∀ 𝑧 ∈ 𝑆 ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) ↔ ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) )
28 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
29 28 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
30 1 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
31 30 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
32 1 uztrn2 ⊢ ( ( 𝑘 ∈ 𝑍 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ) → 𝑚 ∈ 𝑍 )
33 31 32 sylan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ) → 𝑚 ∈ 𝑍 )
34 29 33 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( 𝐹 ‘ 𝑚 ) ∈ ( ℂ ↑m 𝑆 ) )
35 elmapi ⊢ ( ( 𝐹 ‘ 𝑚 ) ∈ ( ℂ ↑m 𝑆 ) → ( 𝐹 ‘ 𝑚 ) : 𝑆 ⟶ ℂ )
36 34 35 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( 𝐹 ‘ 𝑚 ) : 𝑆 ⟶ ℂ )
37 36 ffvelcdmda ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ∈ ℂ )
38 28 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ( ℂ ↑m 𝑆 ) )
39 38 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ( ℂ ↑m 𝑆 ) )
40 elmapi ⊢ ( ( 𝐹 ‘ 𝑗 ) ∈ ( ℂ ↑m 𝑆 ) → ( 𝐹 ‘ 𝑗 ) : 𝑆 ⟶ ℂ )
41 39 40 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( 𝐹 ‘ 𝑗 ) : 𝑆 ⟶ ℂ )
42 41 ffvelcdmda ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ∈ ℂ )
43 37 42 abssubd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) )
44 43 breq1d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ↔ ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) )
45 44 biimpd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) )
46 ffvelcdm ⊢ ( ( 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℂ ↑m 𝑆 ) )
47 28 30 46 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℂ ↑m 𝑆 ) )
48 47 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℂ ↑m 𝑆 ) )
49 48 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℂ ↑m 𝑆 ) )
50 elmapi ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ( ℂ ↑m 𝑆 ) → ( 𝐹 ‘ 𝑘 ) : 𝑆 ⟶ ℂ )
51 49 50 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( 𝐹 ‘ 𝑘 ) : 𝑆 ⟶ ℂ )
52 51 ffvelcdmda ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ∈ ℂ )
53 rpre ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
54 53 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → 𝑥 ∈ ℝ )
55 54 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ) ∧ 𝑧 ∈ 𝑆 ) → 𝑥 ∈ ℝ )
56 abs3lem ⊢ ( ( ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ∈ ℂ ∧ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ∈ ℂ ) ∧ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ∈ ℂ ∧ 𝑥 ∈ ℝ ) ) → ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
57 52 37 42 55 56 syl22anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
58 45 57 sylan2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
59 58 ralimdva ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( ∀ 𝑧 ∈ 𝑆 ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ∧ ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) → ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
60 27 59 biimtrrid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) → ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
61 60 expdimp ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ) ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) → ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
62 61 an32s ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) → ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
63 62 ralimdva ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
64 26 63 syld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
65 64 impancom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
66 65 an32s ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
67 66 ralimdva ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
68 67 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) ) )
69 68 com23 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) ) )
70 22 69 mpdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
71 70 reximdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < ( 𝑥 / 2 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
72 15 71 syld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∀ 𝑤 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑤 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
73 72 ralrimdva ⊢ ( 𝜑 → ( ∀ 𝑤 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑤 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
74 8 73 biimtrid ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
75 eluzelz ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑗 ∈ ℤ )
76 75 1 eleq2s ⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ℤ )
77 uzid ⊢ ( 𝑗 ∈ ℤ → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
78 76 77 syl ⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
79 78 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
80 fveq2 ⊢ ( 𝑘 = 𝑗 → ( ℤ≥ ‘ 𝑘 ) = ( ℤ≥ ‘ 𝑗 ) )
81 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
82 81 fveq1d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) )
83 82 fvoveq1d ⊢ ( 𝑘 = 𝑗 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) )
84 83 breq1d ⊢ ( 𝑘 = 𝑗 → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
85 84 ralbidv ⊢ ( 𝑘 = 𝑗 → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
86 80 85 raleqbidv ⊢ ( 𝑘 = 𝑗 → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
87 86 rspcv ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
88 79 87 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
89 fveq2 ⊢ ( 𝑚 = 𝑘 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑘 ) )
90 89 fveq1d ⊢ ( 𝑚 = 𝑘 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) )
91 90 oveq2d ⊢ ( 𝑚 = 𝑘 → ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) = ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) )
92 91 fveq2d ⊢ ( 𝑚 = 𝑘 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ) )
93 92 breq1d ⊢ ( 𝑚 = 𝑘 → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
94 93 ralbidv ⊢ ( 𝑚 = 𝑘 → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
95 94 cbvralvw ⊢ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ) < 𝑥 )
96 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ( ℂ ↑m 𝑆 ) )
97 96 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ( ℂ ↑m 𝑆 ) )
98 97 40 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) : 𝑆 ⟶ ℂ )
99 98 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ∈ ℂ )
100 4 30 46 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℂ ↑m 𝑆 ) )
101 100 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℂ ↑m 𝑆 ) )
102 101 50 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) : 𝑆 ⟶ ℂ )
103 102 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ∈ ℂ )
104 99 103 abssubd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) )
105 104 breq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
106 105 ralbidva ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
107 106 ralbidva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
108 95 107 bitrid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
109 88 108 sylibd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
110 109 reximdva ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
111 110 ralimdv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ) )
112 74 111 impbid ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) < 𝑥 ) )