Metamath Proof Explorer

Theorem bfplem1

Description: Lemma for bfp . The sequence G , which simply starts from any point in the space and iterates F , satisfies the property that the distance from G ( n ) to G ( n + 1 ) decreases by at least K after each step. Thus, the total distance from any G ( i ) to G ( j ) is bounded by a geometric series, and the sequence is Cauchy. Therefore, it converges to a point ( ( ~>tJ )G ) since the space is complete. (Contributed by Jeff Madsen, 17-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 bfplem1 ( 𝜑 → 𝐺 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) )

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 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
13 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
14 12 9 13 8 5 algrf ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ 𝑋 )
15 5 8 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ 𝑋 )
16 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑋 ) → ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ )
17 11 8 15 16 syl3anc ⊢ ( 𝜑 → ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ )
18 17 3 rerpdivcld ⊢ ( 𝜑 → ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) ∈ ℝ )
19 fveq2 ⊢ ( 𝑗 = 1 → ( 𝐺 ‘ 𝑗 ) = ( 𝐺 ‘ 1 ) )
20 fvoveq1 ⊢ ( 𝑗 = 1 → ( 𝐺 ‘ ( 𝑗 + 1 ) ) = ( 𝐺 ‘ ( 1 + 1 ) ) )
21 19 20 oveq12d ⊢ ( 𝑗 = 1 → ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) = ( ( 𝐺 ‘ 1 ) 𝐷 ( 𝐺 ‘ ( 1 + 1 ) ) ) )
22 oveq2 ⊢ ( 𝑗 = 1 → ( 𝐾 ↑ 𝑗 ) = ( 𝐾 ↑ 1 ) )
23 22 oveq2d ⊢ ( 𝑗 = 1 → ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 𝑗 ) ) = ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 1 ) ) )
24 21 23 breq12d ⊢ ( 𝑗 = 1 → ( ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 𝑗 ) ) ↔ ( ( 𝐺 ‘ 1 ) 𝐷 ( 𝐺 ‘ ( 1 + 1 ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 1 ) ) ) )
25 24 imbi2d ⊢ ( 𝑗 = 1 → ( ( 𝜑 → ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 𝑗 ) ) ) ↔ ( 𝜑 → ( ( 𝐺 ‘ 1 ) 𝐷 ( 𝐺 ‘ ( 1 + 1 ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 1 ) ) ) ) )
26 fveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝐺 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑘 ) )
27 fvoveq1 ⊢ ( 𝑗 = 𝑘 → ( 𝐺 ‘ ( 𝑗 + 1 ) ) = ( 𝐺 ‘ ( 𝑘 + 1 ) ) )
28 26 27 oveq12d ⊢ ( 𝑗 = 𝑘 → ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) = ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) )
29 oveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝐾 ↑ 𝑗 ) = ( 𝐾 ↑ 𝑘 ) )
30 29 oveq2d ⊢ ( 𝑗 = 𝑘 → ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 𝑗 ) ) = ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 𝑘 ) ) )
31 28 30 breq12d ⊢ ( 𝑗 = 𝑘 → ( ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 𝑗 ) ) ↔ ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 𝑘 ) ) ) )
32 31 imbi2d ⊢ ( 𝑗 = 𝑘 → ( ( 𝜑 → ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 𝑗 ) ) ) ↔ ( 𝜑 → ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 𝑘 ) ) ) ) )
33 fveq2 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝐺 ‘ 𝑗 ) = ( 𝐺 ‘ ( 𝑘 + 1 ) ) )
34 fvoveq1 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝐺 ‘ ( 𝑗 + 1 ) ) = ( 𝐺 ‘ ( ( 𝑘 + 1 ) + 1 ) ) )
35 33 34 oveq12d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) = ( ( 𝐺 ‘ ( 𝑘 + 1 ) ) 𝐷 ( 𝐺 ‘ ( ( 𝑘 + 1 ) + 1 ) ) ) )
36 oveq2 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝐾 ↑ 𝑗 ) = ( 𝐾 ↑ ( 𝑘 + 1 ) ) )
37 36 oveq2d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 𝑗 ) ) = ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ ( 𝑘 + 1 ) ) ) )
38 35 37 breq12d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 𝑗 ) ) ↔ ( ( 𝐺 ‘ ( 𝑘 + 1 ) ) 𝐷 ( 𝐺 ‘ ( ( 𝑘 + 1 ) + 1 ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ ( 𝑘 + 1 ) ) ) ) )
39 38 imbi2d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝜑 → ( ( 𝐺 ‘ 𝑗 ) 𝐷 ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 𝑗 ) ) ) ↔ ( 𝜑 → ( ( 𝐺 ‘ ( 𝑘 + 1 ) ) 𝐷 ( 𝐺 ‘ ( ( 𝑘 + 1 ) + 1 ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ ( 𝑘 + 1 ) ) ) ) ) )
40 17 leidd ⊢ ( 𝜑 → ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) ≤ ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) )
41 12 9 13 8 algr0 ⊢ ( 𝜑 → ( 𝐺 ‘ 1 ) = 𝐴 )
42 1nn ⊢ 1 ∈ ℕ
43 12 9 13 8 5 algrp1 ⊢ ( ( 𝜑 ∧ 1 ∈ ℕ ) → ( 𝐺 ‘ ( 1 + 1 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 1 ) ) )
44 42 43 mpan2 ⊢ ( 𝜑 → ( 𝐺 ‘ ( 1 + 1 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 1 ) ) )
45 41 fveq2d ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐺 ‘ 1 ) ) = ( 𝐹 ‘ 𝐴 ) )
46 44 45 eqtrd ⊢ ( 𝜑 → ( 𝐺 ‘ ( 1 + 1 ) ) = ( 𝐹 ‘ 𝐴 ) )
47 41 46 oveq12d ⊢ ( 𝜑 → ( ( 𝐺 ‘ 1 ) 𝐷 ( 𝐺 ‘ ( 1 + 1 ) ) ) = ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) )
48 3 rpred ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
49 48 recnd ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
50 49 exp1d ⊢ ( 𝜑 → ( 𝐾 ↑ 1 ) = 𝐾 )
51 50 oveq2d ⊢ ( 𝜑 → ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 1 ) ) = ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · 𝐾 ) )
52 17 recnd ⊢ ( 𝜑 → ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) ∈ ℂ )
53 3 rpne0d ⊢ ( 𝜑 → 𝐾 ≠ 0 )
54 52 49 53 divcan1d ⊢ ( 𝜑 → ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · 𝐾 ) = ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) )
55 51 54 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 1 ) ) = ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) )
56 40 47 55 3brtr4d ⊢ ( 𝜑 → ( ( 𝐺 ‘ 1 ) 𝐷 ( 𝐺 ‘ ( 1 + 1 ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 1 ) ) )
57 14 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 )
58 peano2nn ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 + 1 ) ∈ ℕ )
59 ffvelrn ⊢ ( ( 𝐺 : ℕ ⟶ 𝑋 ∧ ( 𝑘 + 1 ) ∈ ℕ ) → ( 𝐺 ‘ ( 𝑘 + 1 ) ) ∈ 𝑋 )
60 14 58 59 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ ( 𝑘 + 1 ) ) ∈ 𝑋 )
61 57 60 jca ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ∈ 𝑋 ) )
62 6 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐾 · ( 𝑥 𝐷 𝑦 ) ) )
63 62 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐾 · ( 𝑥 𝐷 𝑦 ) ) )
64 fveq2 ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑘 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) )
65 64 oveq1d ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) )
66 oveq1 ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑘 ) → ( 𝑥 𝐷 𝑦 ) = ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) )
67 66 oveq2d ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑘 ) → ( 𝐾 · ( 𝑥 𝐷 𝑦 ) ) = ( 𝐾 · ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) ) )
68 65 67 breq12d ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑘 ) → ( ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐾 · ( 𝑥 𝐷 𝑦 ) ) ↔ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐾 · ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) ) ) )
69 fveq2 ⊢ ( 𝑦 = ( 𝐺 ‘ ( 𝑘 + 1 ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) )
70 69 oveq2d ⊢ ( 𝑦 = ( 𝐺 ‘ ( 𝑘 + 1 ) ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) 𝐷 ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) )
71 oveq2 ⊢ ( 𝑦 = ( 𝐺 ‘ ( 𝑘 + 1 ) ) → ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) = ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) )
72 71 oveq2d ⊢ ( 𝑦 = ( 𝐺 ‘ ( 𝑘 + 1 ) ) → ( 𝐾 · ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) ) = ( 𝐾 · ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) )
73 70 72 breq12d ⊢ ( 𝑦 = ( 𝐺 ‘ ( 𝑘 + 1 ) ) → ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐾 · ( ( 𝐺 ‘ 𝑘 ) 𝐷 𝑦 ) ) ↔ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) 𝐷 ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) ≤ ( 𝐾 · ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) ) )
74 68 73 rspc2v ⊢ ( ( ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐾 · ( 𝑥 𝐷 𝑦 ) ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) 𝐷 ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) ≤ ( 𝐾 · ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) ) )
75 61 63 74 sylc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) 𝐷 ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) ≤ ( 𝐾 · ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) )
76 11 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
77 5 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐹 : 𝑋 ⟶ 𝑋 )
78 77 57 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ 𝑋 )
79 77 60 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ∈ 𝑋 )
80 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ 𝑋 ∧ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ∈ 𝑋 ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) 𝐷 ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) ∈ ℝ )
81 76 78 79 80 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) 𝐷 ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) ∈ ℝ )
82 48 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐾 ∈ ℝ )
83 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐺 ‘ 𝑘 ) ∈ 𝑋 ∧ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ∈ 𝑋 ) → ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ∈ ℝ )
84 76 57 60 83 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ∈ ℝ )
85 82 84 remulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐾 · ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) ∈ ℝ )
86 18 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) ∈ ℝ )
87 58 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑘 + 1 ) ∈ ℕ )
88 87 nnnn0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑘 + 1 ) ∈ ℕ0 )
89 82 88 reexpcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐾 ↑ ( 𝑘 + 1 ) ) ∈ ℝ )
90 86 89 remulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ ( 𝑘 + 1 ) ) ) ∈ ℝ )
91 letr ⊢ ( ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) 𝐷 ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) ∈ ℝ ∧ ( 𝐾 · ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) ∈ ℝ ∧ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ ( 𝑘 + 1 ) ) ) ∈ ℝ ) → ( ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) 𝐷 ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) ≤ ( 𝐾 · ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) ∧ ( 𝐾 · ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ ( 𝑘 + 1 ) ) ) ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) 𝐷 ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ ( 𝑘 + 1 ) ) ) ) )
92 81 85 90 91 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) 𝐷 ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) ≤ ( 𝐾 · ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) ∧ ( 𝐾 · ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ ( 𝑘 + 1 ) ) ) ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) 𝐷 ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ ( 𝑘 + 1 ) ) ) ) )
93 75 92 mpand ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝐾 · ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ ( 𝑘 + 1 ) ) ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) 𝐷 ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ ( 𝑘 + 1 ) ) ) ) )
94 nnnn0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
95 reexpcl ⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐾 ↑ 𝑘 ) ∈ ℝ )
96 48 94 95 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐾 ↑ 𝑘 ) ∈ ℝ )
97 86 96 remulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 𝑘 ) ) ∈ ℝ )
98 3 rpgt0d ⊢ ( 𝜑 → 0 < 𝐾 )
99 98 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 0 < 𝐾 )
100 lemul1 ⊢ ( ( ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ∈ ℝ ∧ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 𝑘 ) ) ∈ ℝ ∧ ( 𝐾 ∈ ℝ ∧ 0 < 𝐾 ) ) → ( ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 𝑘 ) ) ↔ ( ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) · 𝐾 ) ≤ ( ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 𝑘 ) ) · 𝐾 ) ) )
101 84 97 82 99 100 syl112anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 𝑘 ) ) ↔ ( ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) · 𝐾 ) ≤ ( ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 𝑘 ) ) · 𝐾 ) ) )
102 84 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ∈ ℂ )
103 49 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐾 ∈ ℂ )
104 102 103 mulcomd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) · 𝐾 ) = ( 𝐾 · ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) )
105 86 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) ∈ ℂ )
106 96 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐾 ↑ 𝑘 ) ∈ ℂ )
107 105 106 103 mulassd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 𝑘 ) ) · 𝐾 ) = ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( ( 𝐾 ↑ 𝑘 ) · 𝐾 ) ) )
108 expp1 ⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐾 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐾 ↑ 𝑘 ) · 𝐾 ) )
109 49 94 108 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐾 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐾 ↑ 𝑘 ) · 𝐾 ) )
110 109 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ ( 𝑘 + 1 ) ) ) = ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( ( 𝐾 ↑ 𝑘 ) · 𝐾 ) ) )
111 107 110 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 𝑘 ) ) · 𝐾 ) = ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ ( 𝑘 + 1 ) ) ) )
112 104 111 breq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) · 𝐾 ) ≤ ( ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 𝑘 ) ) · 𝐾 ) ↔ ( 𝐾 · ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ ( 𝑘 + 1 ) ) ) ) )
113 101 112 bitrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 𝑘 ) ) ↔ ( 𝐾 · ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ ( 𝑘 + 1 ) ) ) ) )
114 12 9 13 8 5 algrp1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ ( 𝑘 + 1 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) )
115 12 9 13 8 5 algrp1 ⊢ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ℕ ) → ( 𝐺 ‘ ( ( 𝑘 + 1 ) + 1 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) )
116 58 115 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ ( ( 𝑘 + 1 ) + 1 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) )
117 114 116 oveq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝐺 ‘ ( 𝑘 + 1 ) ) 𝐷 ( 𝐺 ‘ ( ( 𝑘 + 1 ) + 1 ) ) ) = ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) 𝐷 ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) )
118 117 breq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐺 ‘ ( 𝑘 + 1 ) ) 𝐷 ( 𝐺 ‘ ( ( 𝑘 + 1 ) + 1 ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ ( 𝑘 + 1 ) ) ) ↔ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) 𝐷 ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ ( 𝑘 + 1 ) ) ) ) )
119 93 113 118 3imtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 𝑘 ) ) → ( ( 𝐺 ‘ ( 𝑘 + 1 ) ) 𝐷 ( 𝐺 ‘ ( ( 𝑘 + 1 ) + 1 ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ ( 𝑘 + 1 ) ) ) ) )
120 119 expcom ⊢ ( 𝑘 ∈ ℕ → ( 𝜑 → ( ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 𝑘 ) ) → ( ( 𝐺 ‘ ( 𝑘 + 1 ) ) 𝐷 ( 𝐺 ‘ ( ( 𝑘 + 1 ) + 1 ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ ( 𝑘 + 1 ) ) ) ) ) )
121 120 a2d ⊢ ( 𝑘 ∈ ℕ → ( ( 𝜑 → ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 𝑘 ) ) ) → ( 𝜑 → ( ( 𝐺 ‘ ( 𝑘 + 1 ) ) 𝐷 ( 𝐺 ‘ ( ( 𝑘 + 1 ) + 1 ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ ( 𝑘 + 1 ) ) ) ) ) )
122 25 32 39 32 56 121 nnind ⊢ ( 𝑘 ∈ ℕ → ( 𝜑 → ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 𝑘 ) ) ) )
123 122 impcom ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝐺 ‘ 𝑘 ) 𝐷 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ) ≤ ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝐴 ) ) / 𝐾 ) · ( 𝐾 ↑ 𝑘 ) ) )
124 11 14 18 3 4 123 geomcau ⊢ ( 𝜑 → 𝐺 ∈ ( Cau ‘ 𝐷 ) )
125 7 cmetcau ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐺 ∈ ( Cau ‘ 𝐷 ) ) → 𝐺 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) )
126 1 124 125 syl2anc ⊢ ( 𝜑 → 𝐺 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) )
127 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
128 7 methaus ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Haus )
129 11 127 128 3syl ⊢ ( 𝜑 → 𝐽 ∈ Haus )
130 lmfun ⊢ ( 𝐽 ∈ Haus → Fun ( ⇝𝑡 ‘ 𝐽 ) )
131 funfvbrb ⊢ ( Fun ( ⇝𝑡 ‘ 𝐽 ) → ( 𝐺 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) ↔ 𝐺 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) )
132 129 130 131 3syl ⊢ ( 𝜑 → ( 𝐺 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) ↔ 𝐺 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) ) )
133 126 132 mpbid ⊢ ( 𝜑 → 𝐺 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐺 ) )