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

Metamath Proof Explorer

Theorem ulm2

Description: Simplify ulmval when F and G are known to be functions. (Contributed by Mario Carneiro, 26-Feb-2015)

Ref Expression
Hypotheses ulm2.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
ulm2.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
ulm2.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
ulm2.b ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) = 𝐵 )
ulm2.a ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑧 ) = 𝐴 )
ulm2.g ⊢ ( 𝜑 → 𝐺 : 𝑆 ⟶ ℂ )
ulm2.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
Assertion ulm2 ( 𝜑 → ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) )

Proof

Step Hyp Ref Expression
1 ulm2.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 ulm2.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 ulm2.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
4 ulm2.b ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) = 𝐵 )
5 ulm2.a ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑧 ) = 𝐴 )
6 ulm2.g ⊢ ( 𝜑 → 𝐺 : 𝑆 ⟶ ℂ )
7 ulm2.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
8 ulmval ⊢ ( 𝑆 ∈ 𝑉 → ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ↔ ∃ 𝑛 ∈ ℤ ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝐺 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) ) )
9 7 8 syl ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ↔ ∃ 𝑛 ∈ ℤ ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝐺 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) ) )
10 3anan12 ⊢ ( ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝐺 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) ↔ ( 𝐺 : 𝑆 ⟶ ℂ ∧ ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) ) )
11 3 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝑍 )
12 fdm ⊢ ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) → dom 𝐹 = ( ℤ≥ ‘ 𝑛 ) )
13 11 12 sylan9req ⊢ ( ( 𝜑 ∧ 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → 𝑍 = ( ℤ≥ ‘ 𝑛 ) )
14 1 13 eqtr3id ⊢ ( ( 𝜑 ∧ 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑛 ) )
15 2 adantr ⊢ ( ( 𝜑 ∧ 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → 𝑀 ∈ ℤ )
16 uz11 ⊢ ( 𝑀 ∈ ℤ → ( ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑛 ) ↔ 𝑀 = 𝑛 ) )
17 15 16 syl ⊢ ( ( 𝜑 ∧ 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → ( ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑛 ) ↔ 𝑀 = 𝑛 ) )
18 14 17 mpbid ⊢ ( ( 𝜑 ∧ 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → 𝑀 = 𝑛 )
19 18 eqcomd ⊢ ( ( 𝜑 ∧ 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ) → 𝑛 = 𝑀 )
20 fveq2 ⊢ ( 𝑛 = 𝑀 → ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ 𝑀 ) )
21 20 1 eqtr4di ⊢ ( 𝑛 = 𝑀 → ( ℤ≥ ‘ 𝑛 ) = 𝑍 )
22 21 feq2d ⊢ ( 𝑛 = 𝑀 → ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ↔ 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) ) )
23 22 biimparc ⊢ ( ( 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝑛 = 𝑀 ) → 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) )
24 3 23 sylan ⊢ ( ( 𝜑 ∧ 𝑛 = 𝑀 ) → 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) )
25 19 24 impbida ⊢ ( 𝜑 → ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ↔ 𝑛 = 𝑀 ) )
26 25 anbi1d ⊢ ( 𝜑 → ( ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) ↔ ( 𝑛 = 𝑀 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) ) )
27 6 biantrurd ⊢ ( 𝜑 → ( ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) ↔ ( 𝐺 : 𝑆 ⟶ ℂ ∧ ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) ) ) )
28 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 = 𝑀 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑧 ∈ 𝑆 ) → 𝜑 )
29 simpr ⊢ ( ( 𝜑 ∧ 𝑛 = 𝑀 ) → 𝑛 = 𝑀 )
30 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
31 2 30 syl ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
32 31 1 eleqtrrdi ⊢ ( 𝜑 → 𝑀 ∈ 𝑍 )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑛 = 𝑀 ) → 𝑀 ∈ 𝑍 )
34 29 33 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 = 𝑀 ) → 𝑛 ∈ 𝑍 )
35 1 uztrn2 ⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑗 ∈ 𝑍 )
36 34 35 sylan ⊢ ( ( ( 𝜑 ∧ 𝑛 = 𝑀 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ) → 𝑗 ∈ 𝑍 )
37 1 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
38 36 37 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑛 = 𝑀 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
39 38 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 = 𝑀 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑧 ∈ 𝑆 ) → 𝑘 ∈ 𝑍 )
40 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 = 𝑀 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑧 ∈ 𝑆 ) → 𝑧 ∈ 𝑆 )
41 28 39 40 4 syl12anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 = 𝑀 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) = 𝐵 )
42 28 5 sylancom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 = 𝑀 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑧 ) = 𝐴 )
43 41 42 oveq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 = 𝑀 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) = ( 𝐵 − 𝐴 ) )
44 43 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 = 𝑀 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) = ( abs ‘ ( 𝐵 − 𝐴 ) ) )
45 44 breq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 = 𝑀 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ↔ ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) )
46 45 ralbidva ⊢ ( ( ( ( 𝜑 ∧ 𝑛 = 𝑀 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) )
47 46 ralbidva ⊢ ( ( ( 𝜑 ∧ 𝑛 = 𝑀 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) )
48 47 rexbidva ⊢ ( ( 𝜑 ∧ 𝑛 = 𝑀 ) → ( ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ↔ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) )
49 48 ralbidv ⊢ ( ( 𝜑 ∧ 𝑛 = 𝑀 ) → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) )
50 49 pm5.32da ⊢ ( 𝜑 → ( ( 𝑛 = 𝑀 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) ↔ ( 𝑛 = 𝑀 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) )
51 26 27 50 3bitr3d ⊢ ( 𝜑 → ( ( 𝐺 : 𝑆 ⟶ ℂ ∧ ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) ) ↔ ( 𝑛 = 𝑀 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) )
52 10 51 bitrid ⊢ ( 𝜑 → ( ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝐺 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) ↔ ( 𝑛 = 𝑀 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) )
53 52 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ℤ ( 𝐹 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝐺 : 𝑆 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑥 ) ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 = 𝑀 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ) )
54 21 rexeqdv ⊢ ( 𝑛 = 𝑀 → ( ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) )
55 54 ralbidv ⊢ ( 𝑛 = 𝑀 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) )
56 55 ceqsrexv ⊢ ( 𝑀 ∈ ℤ → ( ∃ 𝑛 ∈ ℤ ( 𝑛 = 𝑀 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) )
57 2 56 syl ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ℤ ( 𝑛 = 𝑀 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) )
58 9 53 57 3bitrd ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝑥 ) )