Metamath Proof Explorer

Theorem bfplem2

Description: Lemma for bfp . Using the point found in bfplem1 , we show that this convergent point is a fixed point of F . Since for any positive x , the sequence G is in B ( x / 2 , P ) for all k e. ( ZZ>=j ) (where P = ( ( ~>tJ )G ) ), we have D ( G ( j + 1 ) , F ( P ) ) <_ D ( G ( j ) , P ) < x / 2 and D ( G ( j + 1 ) , P ) < x / 2 , so F ( P ) is in every neighborhood of P and P is a fixed point of F . (Contributed by Jeff Madsen, 5-Jun-2014)

Ref Expression
Hypotheses bfp.2 ⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
bfp.3 ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
bfp.4 ⊢ ( 𝜑 → 𝐾 ∈ ℝ+ )
bfp.5 ⊢ ( 𝜑 → 𝐾 < 1 )
bfp.6 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑋 )
bfp.7 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐾 · ( 𝑥 𝐷 𝑦 ) ) )
bfp.8 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
bfp.9 ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
bfp.10 ⊢ 𝐺 = seq 1 ( ( 𝐹 ∘ 1st ) , ( ℕ × { 𝐴 } ) )
Assertion bfplem2 ( 𝜑 → ∃ 𝑧 ∈ 𝑋 ( 𝐹 ‘ 𝑧 ) = 𝑧 )

Proof

Step Hyp Ref Expression
1 bfp.2 ⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
2 bfp.3 ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
3 bfp.4 ⊢ ( 𝜑 → 𝐾 ∈ ℝ+ )
4 bfp.5 ⊢ ( 𝜑 → 𝐾 < 1 )
5 bfp.6 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑋 )
6 bfp.7 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐾 · ( 𝑥 𝐷 𝑦 ) ) )
7 bfp.8 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
8 bfp.9 ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
9 bfp.10 ⊢ 𝐺 = seq 1 ( ( 𝐹 ∘ 1st ) , ( ℕ × { 𝐴 } ) )
10 cmetmet ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
11 1 10 syl ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
12 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
13 7 mopntopon ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
14 11 12 13 3syl ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
15 1 2 3 4 5 6 7 8 9 bfplem1 ⊢ ( 𝜑 → 𝐺 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) )
16 lmcl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐺 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) → ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ∈ 𝑋 )
17 14 15 16 syl2anc ⊢ ( 𝜑 → ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ∈ 𝑋 )
18 11 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
19 18 12 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
20 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
21 1zzd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 1 ∈ ℤ )
22 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
23 15 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐺 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) )
24 rphalfcl ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 / 2 ) ∈ ℝ+ )
25 24 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 / 2 ) ∈ ℝ+ )
26 7 19 20 21 22 23 25 lmmcvg ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) ) )
27 simpr ⊢ ( ( ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) ) → ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) )
28 27 ralimi ⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) )
29 nnz ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℤ )
30 29 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℤ )
31 uzid ⊢ ( 𝑗 ∈ ℤ → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
32 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑗 ) )
33 32 oveq1d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) = ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) )
34 33 breq1d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) ↔ ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) ) )
35 34 rspcv ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) → ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) ) )
36 30 31 35 3syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) → ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) ) )
37 30 31 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
38 peano2uz ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) → ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ 𝑗 ) )
39 fveq2 ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ ( 𝑗 + 1 ) ) )
40 39 oveq1d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) = ( ( 𝐺 ‘ ( 𝑗 + 1 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) )
41 40 breq1d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) ↔ ( ( 𝐺 ‘ ( 𝑗 + 1 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) ) )
42 41 rspcv ⊢ ( ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ 𝑗 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) → ( ( 𝐺 ‘ ( 𝑗 + 1 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) ) )
43 37 38 42 3syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) → ( ( 𝐺 ‘ ( 𝑗 + 1 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) ) )
44 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
45 20 9 44 8 5 algrp1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐺 ‘ ( 𝑗 + 1 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) )
46 45 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐺 ‘ ( 𝑗 + 1 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) )
47 46 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐺 ‘ ( 𝑗 + 1 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) = ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) )
48 47 breq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ( ( 𝐺 ‘ ( 𝑗 + 1 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) ↔ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) ) )
49 43 48 sylibd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) ) )
50 36 49 jcad ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) → ( ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) ) ) )
51 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
52 20 9 44 8 5 algrf ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ 𝑋 )
53 52 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐺 : ℕ ⟶ 𝑋 )
54 53 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐺 ‘ 𝑗 ) ∈ 𝑋 )
55 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ∈ 𝑋 )
56 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐺 ‘ 𝑗 ) ∈ 𝑋 ∧ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ∈ 𝑋 ) → ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ∈ ℝ )
57 51 54 55 56 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ∈ ℝ )
58 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → 𝐹 : 𝑋 ⟶ 𝑋 )
59 58 54 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ 𝑋 )
60 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ 𝑋 ∧ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ∈ 𝑋 ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ∈ ℝ )
61 51 59 55 60 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ∈ ℝ )
62 rpre ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
63 62 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → 𝑥 ∈ ℝ )
64 lt2halves ⊢ ( ( ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ∈ ℝ ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) ) → ( ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) + ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) < 𝑥 ) )
65 57 61 63 64 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ( ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) ) → ( ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) + ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) < 𝑥 ) )
66 5 17 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ∈ 𝑋 )
67 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ∈ 𝑋 ∧ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ∈ 𝑋 ) → ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ∈ ℝ )
68 11 66 17 67 syl3anc ⊢ ( 𝜑 → ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ∈ ℝ )
69 68 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ∈ ℝ )
70 58 55 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ∈ 𝑋 )
71 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ 𝑋 ∧ ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ∈ 𝑋 ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) ∈ ℝ )
72 51 59 70 71 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) ∈ ℝ )
73 72 61 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) + ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) ∈ ℝ )
74 57 61 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) + ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) ∈ ℝ )
75 mettri2 ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ 𝑋 ∧ ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ∈ 𝑋 ∧ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ∈ 𝑋 ) ) → ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ≤ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) + ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) )
76 51 59 70 55 75 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ≤ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) + ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) )
77 3 rpred ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
78 77 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → 𝐾 ∈ ℝ )
79 78 57 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐾 · ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) ∈ ℝ )
80 54 55 jca ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐺 ‘ 𝑗 ) ∈ 𝑋 ∧ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ∈ 𝑋 ) )
81 6 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐾 · ( 𝑥 𝐷 𝑦 ) ) )
82 81 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐾 · ( 𝑥 𝐷 𝑦 ) ) )
83 fveq2 ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑗 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) )
84 83 oveq1d ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑗 ) → ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) )
85 oveq1 ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑗 ) → ( 𝑥 𝐷 𝑦 ) = ( ( 𝐺 ‘ 𝑗 ) 𝐷 𝑦 ) )
86 85 oveq2d ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑗 ) → ( 𝐾 · ( 𝑥 𝐷 𝑦 ) ) = ( 𝐾 · ( ( 𝐺 ‘ 𝑗 ) 𝐷 𝑦 ) ) )
87 84 86 breq12d ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑗 ) → ( ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐾 · ( 𝑥 𝐷 𝑦 ) ) ↔ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐾 · ( ( 𝐺 ‘ 𝑗 ) 𝐷 𝑦 ) ) ) )
88 fveq2 ⊢ ( 𝑦 = ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) )
89 88 oveq2d ⊢ ( 𝑦 = ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) )
90 oveq2 ⊢ ( 𝑦 = ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) → ( ( 𝐺 ‘ 𝑗 ) 𝐷 𝑦 ) = ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) )
91 90 oveq2d ⊢ ( 𝑦 = ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) → ( 𝐾 · ( ( 𝐺 ‘ 𝑗 ) 𝐷 𝑦 ) ) = ( 𝐾 · ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) )
92 89 91 breq12d ⊢ ( 𝑦 = ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) → ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐾 · ( ( 𝐺 ‘ 𝑗 ) 𝐷 𝑦 ) ) ↔ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) ≤ ( 𝐾 · ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) ) )
93 87 92 rspc2v ⊢ ( ( ( 𝐺 ‘ 𝑗 ) ∈ 𝑋 ∧ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐾 · ( 𝑥 𝐷 𝑦 ) ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) ≤ ( 𝐾 · ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) ) )
94 80 82 93 sylc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) ≤ ( 𝐾 · ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) )
95 1red ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → 1 ∈ ℝ )
96 metge0 ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐺 ‘ 𝑗 ) ∈ 𝑋 ∧ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ∈ 𝑋 ) → 0 ≤ ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) )
97 51 54 55 96 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → 0 ≤ ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) )
98 1re ⊢ 1 ∈ ℝ
99 ltle ⊢ ( ( 𝐾 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝐾 < 1 → 𝐾 ≤ 1 ) )
100 77 98 99 sylancl ⊢ ( 𝜑 → ( 𝐾 < 1 → 𝐾 ≤ 1 ) )
101 4 100 mpd ⊢ ( 𝜑 → 𝐾 ≤ 1 )
102 101 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → 𝐾 ≤ 1 )
103 78 95 57 97 102 lemul1ad ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐾 · ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) ≤ ( 1 · ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) )
104 57 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ∈ ℂ )
105 104 mulid2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( 1 · ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) = ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) )
106 103 105 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐾 · ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) ≤ ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) )
107 72 79 57 94 106 letrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) ≤ ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) )
108 72 57 61 107 leadd1dd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) + ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) ≤ ( ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) + ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) )
109 69 73 74 76 108 letrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ≤ ( ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) + ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) )
110 lelttr ⊢ ( ( ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ∈ ℝ ∧ ( ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) + ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ≤ ( ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) + ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) + ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) < 𝑥 ) → ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < 𝑥 ) )
111 69 74 63 110 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ( ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ≤ ( ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) + ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) + ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) < 𝑥 ) → ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < 𝑥 ) )
112 109 111 mpand ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ( ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) + ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) < 𝑥 → ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < 𝑥 ) )
113 50 65 112 3syld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) → ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < 𝑥 ) )
114 28 113 syl5 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) ) → ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < 𝑥 ) )
115 114 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < ( 𝑥 / 2 ) ) → ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < 𝑥 ) )
116 26 115 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < 𝑥 )
117 ltle ⊢ ( ( ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < 𝑥 → ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ≤ 𝑥 ) )
118 68 62 117 syl2an ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) < 𝑥 → ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ≤ 𝑥 ) )
119 116 118 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ≤ 𝑥 )
120 62 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ )
121 120 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℂ )
122 121 addid2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 0 + 𝑥 ) = 𝑥 )
123 119 122 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ≤ ( 0 + 𝑥 ) )
124 123 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ≤ ( 0 + 𝑥 ) )
125 0re ⊢ 0 ∈ ℝ
126 alrple ⊢ ( ( ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ≤ 0 ↔ ∀ 𝑥 ∈ ℝ+ ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ≤ ( 0 + 𝑥 ) ) )
127 68 125 126 sylancl ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ≤ 0 ↔ ∀ 𝑥 ∈ ℝ+ ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ≤ ( 0 + 𝑥 ) ) )
128 124 127 mpbird ⊢ ( 𝜑 → ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ≤ 0 )
129 metge0 ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ∈ 𝑋 ∧ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ∈ 𝑋 ) → 0 ≤ ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) )
130 11 66 17 129 syl3anc ⊢ ( 𝜑 → 0 ≤ ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) )
131 letri3 ⊢ ( ( ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) = 0 ↔ ( ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ≤ 0 ∧ 0 ≤ ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) ) )
132 68 125 131 sylancl ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) = 0 ↔ ( ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ≤ 0 ∧ 0 ≤ ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ) ) )
133 128 130 132 mpbir2and ⊢ ( 𝜑 → ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) = 0 )
134 meteq0 ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ∈ 𝑋 ∧ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ∈ 𝑋 ) → ( ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) = 0 ↔ ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) = ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) )
135 11 66 17 134 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) = 0 ↔ ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) = ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) )
136 133 135 mpbid ⊢ ( 𝜑 → ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) = ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) )
137 fveq2 ⊢ ( 𝑧 = ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) )
138 id ⊢ ( 𝑧 = ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) → 𝑧 = ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) )
139 137 138 eqeq12d ⊢ ( 𝑧 = ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) → ( ( 𝐹 ‘ 𝑧 ) = 𝑧 ↔ ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) = ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) )
140 139 rspcev ⊢ ( ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ∈ 𝑋 ∧ ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) = ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) → ∃ 𝑧 ∈ 𝑋 ( 𝐹 ‘ 𝑧 ) = 𝑧 )
141 17 136 140 syl2anc ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑋 ( 𝐹 ‘ 𝑧 ) = 𝑧 )