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	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐺 ‘ 𝑗 ) ∈ 𝑋 )
55	17	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ∈ 𝑋 )
56		metcl	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐺 ‘ 𝑗 ) ∈ 𝑋 ∧ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ∈ 𝑋 ) → ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ∈ ℝ )
57	51 54 55 56	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ∈ ℝ )
58	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → 𝐹 : 𝑋 ⟶ 𝑋 )
59	58 54	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ 𝑋 )
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	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ∈ 𝑋 )
67		metcl	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ∈ 𝑋 ∧ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ∈ 𝑋 ) → ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ∈ ℝ )
68	11 66 17 67	syl3anc	⊢ ( 𝜑 → ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ∈ ℝ )
69	68	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ∈ ℝ )
70	58 55	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) ∈ 𝑋 )
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	mullidd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( 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	addlidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 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	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑋 ( 𝐹 ‘ 𝑧 ) = 𝑧 )