Metamath Proof Explorer


Theorem geomcau

Description: If the distance between consecutive points in a sequence is bounded by a geometric sequence, then the sequence is Cauchy. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 5-Jun-2014)

Ref Expression
Hypotheses lmclim2.2 ( 𝜑𝐷 ∈ ( Met ‘ 𝑋 ) )
lmclim2.3 ( 𝜑𝐹 : ℕ ⟶ 𝑋 )
geomcau.4 ( 𝜑𝐴 ∈ ℝ )
geomcau.5 ( 𝜑𝐵 ∈ ℝ+ )
geomcau.6 ( 𝜑𝐵 < 1 )
geomcau.7 ( ( 𝜑𝑘 ∈ ℕ ) → ( ( 𝐹𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( 𝐴 · ( 𝐵𝑘 ) ) )
Assertion geomcau ( 𝜑𝐹 ∈ ( Cau ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 lmclim2.2 ( 𝜑𝐷 ∈ ( Met ‘ 𝑋 ) )
2 lmclim2.3 ( 𝜑𝐹 : ℕ ⟶ 𝑋 )
3 geomcau.4 ( 𝜑𝐴 ∈ ℝ )
4 geomcau.5 ( 𝜑𝐵 ∈ ℝ+ )
5 geomcau.6 ( 𝜑𝐵 < 1 )
6 geomcau.7 ( ( 𝜑𝑘 ∈ ℕ ) → ( ( 𝐹𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( 𝐴 · ( 𝐵𝑘 ) ) )
7 nnuz ℕ = ( ℤ ‘ 1 )
8 1zzd ( 𝜑 → 1 ∈ ℤ )
9 4 rpcnd ( 𝜑𝐵 ∈ ℂ )
10 4 rpred ( 𝜑𝐵 ∈ ℝ )
11 4 rpge0d ( 𝜑 → 0 ≤ 𝐵 )
12 10 11 absidd ( 𝜑 → ( abs ‘ 𝐵 ) = 𝐵 )
13 12 5 eqbrtrd ( 𝜑 → ( abs ‘ 𝐵 ) < 1 )
14 9 13 expcnv ( 𝜑 → ( 𝑚 ∈ ℕ0 ↦ ( 𝐵𝑚 ) ) ⇝ 0 )
15 1re 1 ∈ ℝ
16 resubcl ( ( 1 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 1 − 𝐵 ) ∈ ℝ )
17 15 10 16 sylancr ( 𝜑 → ( 1 − 𝐵 ) ∈ ℝ )
18 posdif ( ( 𝐵 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝐵 < 1 ↔ 0 < ( 1 − 𝐵 ) ) )
19 10 15 18 sylancl ( 𝜑 → ( 𝐵 < 1 ↔ 0 < ( 1 − 𝐵 ) ) )
20 5 19 mpbid ( 𝜑 → 0 < ( 1 − 𝐵 ) )
21 17 20 elrpd ( 𝜑 → ( 1 − 𝐵 ) ∈ ℝ+ )
22 3 21 rerpdivcld ( 𝜑 → ( 𝐴 / ( 1 − 𝐵 ) ) ∈ ℝ )
23 22 recnd ( 𝜑 → ( 𝐴 / ( 1 − 𝐵 ) ) ∈ ℂ )
24 nnex ℕ ∈ V
25 24 mptex ( 𝑚 ∈ ℕ ↦ ( ( 𝐵𝑚 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) ∈ V
26 25 a1i ( 𝜑 → ( 𝑚 ∈ ℕ ↦ ( ( 𝐵𝑚 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) ∈ V )
27 nnnn0 ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
28 27 adantl ( ( 𝜑𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ0 )
29 oveq2 ( 𝑚 = 𝑛 → ( 𝐵𝑚 ) = ( 𝐵𝑛 ) )
30 eqid ( 𝑚 ∈ ℕ0 ↦ ( 𝐵𝑚 ) ) = ( 𝑚 ∈ ℕ0 ↦ ( 𝐵𝑚 ) )
31 ovex ( 𝐵𝑛 ) ∈ V
32 29 30 31 fvmpt ( 𝑛 ∈ ℕ0 → ( ( 𝑚 ∈ ℕ0 ↦ ( 𝐵𝑚 ) ) ‘ 𝑛 ) = ( 𝐵𝑛 ) )
33 28 32 syl ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ0 ↦ ( 𝐵𝑚 ) ) ‘ 𝑛 ) = ( 𝐵𝑛 ) )
34 nnz ( 𝑛 ∈ ℕ → 𝑛 ∈ ℤ )
35 rpexpcl ( ( 𝐵 ∈ ℝ+𝑛 ∈ ℤ ) → ( 𝐵𝑛 ) ∈ ℝ+ )
36 4 34 35 syl2an ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝐵𝑛 ) ∈ ℝ+ )
37 36 rpcnd ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝐵𝑛 ) ∈ ℂ )
38 33 37 eqeltrd ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ0 ↦ ( 𝐵𝑚 ) ) ‘ 𝑛 ) ∈ ℂ )
39 23 adantr ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝐴 / ( 1 − 𝐵 ) ) ∈ ℂ )
40 37 39 mulcomd ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 𝐵𝑛 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) = ( ( 𝐴 / ( 1 − 𝐵 ) ) · ( 𝐵𝑛 ) ) )
41 29 oveq1d ( 𝑚 = 𝑛 → ( ( 𝐵𝑚 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) = ( ( 𝐵𝑛 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) )
42 eqid ( 𝑚 ∈ ℕ ↦ ( ( 𝐵𝑚 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) = ( 𝑚 ∈ ℕ ↦ ( ( 𝐵𝑚 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) )
43 ovex ( ( 𝐵𝑛 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ∈ V
44 41 42 43 fvmpt ( 𝑛 ∈ ℕ → ( ( 𝑚 ∈ ℕ ↦ ( ( 𝐵𝑚 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) ‘ 𝑛 ) = ( ( 𝐵𝑛 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) )
45 44 adantl ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( ( 𝐵𝑚 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) ‘ 𝑛 ) = ( ( 𝐵𝑛 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) )
46 33 oveq2d ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 𝐴 / ( 1 − 𝐵 ) ) · ( ( 𝑚 ∈ ℕ0 ↦ ( 𝐵𝑚 ) ) ‘ 𝑛 ) ) = ( ( 𝐴 / ( 1 − 𝐵 ) ) · ( 𝐵𝑛 ) ) )
47 40 45 46 3eqtr4d ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( ( 𝐵𝑚 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) ‘ 𝑛 ) = ( ( 𝐴 / ( 1 − 𝐵 ) ) · ( ( 𝑚 ∈ ℕ0 ↦ ( 𝐵𝑚 ) ) ‘ 𝑛 ) ) )
48 7 8 14 23 26 38 47 climmulc2 ( 𝜑 → ( 𝑚 ∈ ℕ ↦ ( ( 𝐵𝑚 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) ⇝ ( ( 𝐴 / ( 1 − 𝐵 ) ) · 0 ) )
49 23 mul01d ( 𝜑 → ( ( 𝐴 / ( 1 − 𝐵 ) ) · 0 ) = 0 )
50 48 49 breqtrd ( 𝜑 → ( 𝑚 ∈ ℕ ↦ ( ( 𝐵𝑚 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) ⇝ 0 )
51 36 rpred ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝐵𝑛 ) ∈ ℝ )
52 22 adantr ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝐴 / ( 1 − 𝐵 ) ) ∈ ℝ )
53 51 52 remulcld ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 𝐵𝑛 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ∈ ℝ )
54 53 recnd ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 𝐵𝑛 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ∈ ℂ )
55 7 8 26 45 54 clim0c ( 𝜑 → ( ( 𝑚 ∈ ℕ ↦ ( ( 𝐵𝑚 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) ⇝ 0 ↔ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ℕ ∀ 𝑛 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐵𝑛 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) < 𝑥 ) )
56 50 55 mpbid ( 𝜑 → ∀ 𝑥 ∈ ℝ+𝑗 ∈ ℕ ∀ 𝑛 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐵𝑛 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) < 𝑥 )
57 nnz ( 𝑗 ∈ ℕ → 𝑗 ∈ ℤ )
58 57 adantl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℤ )
59 uzid ( 𝑗 ∈ ℤ → 𝑗 ∈ ( ℤ𝑗 ) )
60 oveq2 ( 𝑛 = 𝑗 → ( 𝐵𝑛 ) = ( 𝐵𝑗 ) )
61 60 fvoveq1d ( 𝑛 = 𝑗 → ( abs ‘ ( ( 𝐵𝑛 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) = ( abs ‘ ( ( 𝐵𝑗 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) )
62 61 breq1d ( 𝑛 = 𝑗 → ( ( abs ‘ ( ( 𝐵𝑛 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐵𝑗 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) < 𝑥 ) )
63 62 rspcv ( 𝑗 ∈ ( ℤ𝑗 ) → ( ∀ 𝑛 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐵𝑛 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) < 𝑥 → ( abs ‘ ( ( 𝐵𝑗 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) < 𝑥 ) )
64 58 59 63 3syl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ∀ 𝑛 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐵𝑛 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) < 𝑥 → ( abs ‘ ( ( 𝐵𝑗 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) < 𝑥 ) )
65 1 adantr ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
66 simpl ( ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) → 𝑗 ∈ ℕ )
67 ffvelrn ( ( 𝐹 : ℕ ⟶ 𝑋𝑗 ∈ ℕ ) → ( 𝐹𝑗 ) ∈ 𝑋 )
68 2 66 67 syl2an ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → ( 𝐹𝑗 ) ∈ 𝑋 )
69 eluznn ( ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) → 𝑛 ∈ ℕ )
70 ffvelrn ( ( 𝐹 : ℕ ⟶ 𝑋𝑛 ∈ ℕ ) → ( 𝐹𝑛 ) ∈ 𝑋 )
71 2 69 70 syl2an ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → ( 𝐹𝑛 ) ∈ 𝑋 )
72 metcl ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐹𝑗 ) ∈ 𝑋 ∧ ( 𝐹𝑛 ) ∈ 𝑋 ) → ( ( 𝐹𝑗 ) 𝐷 ( 𝐹𝑛 ) ) ∈ ℝ )
73 65 68 71 72 syl3anc ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → ( ( 𝐹𝑗 ) 𝐷 ( 𝐹𝑛 ) ) ∈ ℝ )
74 eqid ( ℤ𝑗 ) = ( ℤ𝑗 )
75 nnnn0 ( 𝑗 ∈ ℕ → 𝑗 ∈ ℕ0 )
76 75 ad2antrl ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → 𝑗 ∈ ℕ0 )
77 76 nn0zd ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → 𝑗 ∈ ℤ )
78 oveq2 ( 𝑚 = 𝑘 → ( 𝐵𝑚 ) = ( 𝐵𝑘 ) )
79 78 oveq2d ( 𝑚 = 𝑘 → ( 𝐴 · ( 𝐵𝑚 ) ) = ( 𝐴 · ( 𝐵𝑘 ) ) )
80 eqid ( 𝑚 ∈ ( ℤ𝑗 ) ↦ ( 𝐴 · ( 𝐵𝑚 ) ) ) = ( 𝑚 ∈ ( ℤ𝑗 ) ↦ ( 𝐴 · ( 𝐵𝑚 ) ) )
81 ovex ( 𝐴 · ( 𝐵𝑘 ) ) ∈ V
82 79 80 81 fvmpt ( 𝑘 ∈ ( ℤ𝑗 ) → ( ( 𝑚 ∈ ( ℤ𝑗 ) ↦ ( 𝐴 · ( 𝐵𝑚 ) ) ) ‘ 𝑘 ) = ( 𝐴 · ( 𝐵𝑘 ) ) )
83 82 adantl ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → ( ( 𝑚 ∈ ( ℤ𝑗 ) ↦ ( 𝐴 · ( 𝐵𝑚 ) ) ) ‘ 𝑘 ) = ( 𝐴 · ( 𝐵𝑘 ) ) )
84 3 ad2antrr ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → 𝐴 ∈ ℝ )
85 10 ad2antrr ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → 𝐵 ∈ ℝ )
86 eluznn0 ( ( 𝑗 ∈ ℕ0𝑘 ∈ ( ℤ𝑗 ) ) → 𝑘 ∈ ℕ0 )
87 76 86 sylan ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → 𝑘 ∈ ℕ0 )
88 85 87 reexpcld ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → ( 𝐵𝑘 ) ∈ ℝ )
89 84 88 remulcld ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → ( 𝐴 · ( 𝐵𝑘 ) ) ∈ ℝ )
90 89 recnd ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → ( 𝐴 · ( 𝐵𝑘 ) ) ∈ ℂ )
91 3 recnd ( 𝜑𝐴 ∈ ℂ )
92 91 adantr ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → 𝐴 ∈ ℂ )
93 9 adantr ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → 𝐵 ∈ ℂ )
94 13 adantr ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → ( abs ‘ 𝐵 ) < 1 )
95 eqid ( 𝑚 ∈ ( ℤ𝑗 ) ↦ ( 𝐵𝑚 ) ) = ( 𝑚 ∈ ( ℤ𝑗 ) ↦ ( 𝐵𝑚 ) )
96 ovex ( 𝐵𝑘 ) ∈ V
97 78 95 96 fvmpt ( 𝑘 ∈ ( ℤ𝑗 ) → ( ( 𝑚 ∈ ( ℤ𝑗 ) ↦ ( 𝐵𝑚 ) ) ‘ 𝑘 ) = ( 𝐵𝑘 ) )
98 97 adantl ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → ( ( 𝑚 ∈ ( ℤ𝑗 ) ↦ ( 𝐵𝑚 ) ) ‘ 𝑘 ) = ( 𝐵𝑘 ) )
99 93 94 76 98 geolim2 ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → seq 𝑗 ( + , ( 𝑚 ∈ ( ℤ𝑗 ) ↦ ( 𝐵𝑚 ) ) ) ⇝ ( ( 𝐵𝑗 ) / ( 1 − 𝐵 ) ) )
100 88 recnd ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → ( 𝐵𝑘 ) ∈ ℂ )
101 98 100 eqeltrd ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → ( ( 𝑚 ∈ ( ℤ𝑗 ) ↦ ( 𝐵𝑚 ) ) ‘ 𝑘 ) ∈ ℂ )
102 98 oveq2d ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → ( 𝐴 · ( ( 𝑚 ∈ ( ℤ𝑗 ) ↦ ( 𝐵𝑚 ) ) ‘ 𝑘 ) ) = ( 𝐴 · ( 𝐵𝑘 ) ) )
103 83 102 eqtr4d ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → ( ( 𝑚 ∈ ( ℤ𝑗 ) ↦ ( 𝐴 · ( 𝐵𝑚 ) ) ) ‘ 𝑘 ) = ( 𝐴 · ( ( 𝑚 ∈ ( ℤ𝑗 ) ↦ ( 𝐵𝑚 ) ) ‘ 𝑘 ) ) )
104 74 77 92 99 101 103 isermulc2 ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → seq 𝑗 ( + , ( 𝑚 ∈ ( ℤ𝑗 ) ↦ ( 𝐴 · ( 𝐵𝑚 ) ) ) ) ⇝ ( 𝐴 · ( ( 𝐵𝑗 ) / ( 1 − 𝐵 ) ) ) )
105 4 adantr ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → 𝐵 ∈ ℝ+ )
106 105 77 rpexpcld ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → ( 𝐵𝑗 ) ∈ ℝ+ )
107 106 rpcnd ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → ( 𝐵𝑗 ) ∈ ℂ )
108 17 recnd ( 𝜑 → ( 1 − 𝐵 ) ∈ ℂ )
109 108 adantr ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → ( 1 − 𝐵 ) ∈ ℂ )
110 21 rpne0d ( 𝜑 → ( 1 − 𝐵 ) ≠ 0 )
111 110 adantr ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → ( 1 − 𝐵 ) ≠ 0 )
112 92 107 109 111 div12d ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → ( 𝐴 · ( ( 𝐵𝑗 ) / ( 1 − 𝐵 ) ) ) = ( ( 𝐵𝑗 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) )
113 104 112 breqtrd ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → seq 𝑗 ( + , ( 𝑚 ∈ ( ℤ𝑗 ) ↦ ( 𝐴 · ( 𝐵𝑚 ) ) ) ) ⇝ ( ( 𝐵𝑗 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) )
114 74 77 83 90 113 isumclim ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → Σ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐴 · ( 𝐵𝑘 ) ) = ( ( 𝐵𝑗 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) )
115 seqex seq 𝑗 ( + , ( 𝑚 ∈ ( ℤ𝑗 ) ↦ ( 𝐴 · ( 𝐵𝑚 ) ) ) ) ∈ V
116 ovex ( 𝐴 · ( ( 𝐵𝑗 ) / ( 1 − 𝐵 ) ) ) ∈ V
117 115 116 breldm ( seq 𝑗 ( + , ( 𝑚 ∈ ( ℤ𝑗 ) ↦ ( 𝐴 · ( 𝐵𝑚 ) ) ) ) ⇝ ( 𝐴 · ( ( 𝐵𝑗 ) / ( 1 − 𝐵 ) ) ) → seq 𝑗 ( + , ( 𝑚 ∈ ( ℤ𝑗 ) ↦ ( 𝐴 · ( 𝐵𝑚 ) ) ) ) ∈ dom ⇝ )
118 104 117 syl ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → seq 𝑗 ( + , ( 𝑚 ∈ ( ℤ𝑗 ) ↦ ( 𝐴 · ( 𝐵𝑚 ) ) ) ) ∈ dom ⇝ )
119 74 77 83 89 118 isumrecl ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → Σ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐴 · ( 𝐵𝑘 ) ) ∈ ℝ )
120 114 119 eqeltrrd ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → ( ( 𝐵𝑗 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ∈ ℝ )
121 120 recnd ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → ( ( 𝐵𝑗 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ∈ ℂ )
122 121 abscld ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → ( abs ‘ ( ( 𝐵𝑗 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) ∈ ℝ )
123 fzfid ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → ( 𝑗 ... ( 𝑛 − 1 ) ) ∈ Fin )
124 simpll ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) ∧ 𝑘 ∈ ( 𝑗 ... ( 𝑛 − 1 ) ) ) → 𝜑 )
125 elfzuz ( 𝑘 ∈ ( 𝑗 ... ( 𝑛 − 1 ) ) → 𝑘 ∈ ( ℤ𝑗 ) )
126 simprl ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → 𝑗 ∈ ℕ )
127 eluznn ( ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → 𝑘 ∈ ℕ )
128 126 127 sylan ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → 𝑘 ∈ ℕ )
129 125 128 sylan2 ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) ∧ 𝑘 ∈ ( 𝑗 ... ( 𝑛 − 1 ) ) ) → 𝑘 ∈ ℕ )
130 1 adantr ( ( 𝜑𝑘 ∈ ℕ ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
131 2 ffvelrnda ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐹𝑘 ) ∈ 𝑋 )
132 peano2nn ( 𝑘 ∈ ℕ → ( 𝑘 + 1 ) ∈ ℕ )
133 ffvelrn ( ( 𝐹 : ℕ ⟶ 𝑋 ∧ ( 𝑘 + 1 ) ∈ ℕ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ 𝑋 )
134 2 132 133 syl2an ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ 𝑋 )
135 metcl ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐹𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ 𝑋 ) → ( ( 𝐹𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∈ ℝ )
136 130 131 134 135 syl3anc ( ( 𝜑𝑘 ∈ ℕ ) → ( ( 𝐹𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∈ ℝ )
137 124 129 136 syl2anc ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) ∧ 𝑘 ∈ ( 𝑗 ... ( 𝑛 − 1 ) ) ) → ( ( 𝐹𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∈ ℝ )
138 123 137 fsumrecl ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → Σ 𝑘 ∈ ( 𝑗 ... ( 𝑛 − 1 ) ) ( ( 𝐹𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∈ ℝ )
139 simprr ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → 𝑛 ∈ ( ℤ𝑗 ) )
140 elfzuz ( 𝑘 ∈ ( 𝑗 ... 𝑛 ) → 𝑘 ∈ ( ℤ𝑗 ) )
141 simpll ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → 𝜑 )
142 141 128 131 syl2anc ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → ( 𝐹𝑘 ) ∈ 𝑋 )
143 140 142 sylan2 ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) ∧ 𝑘 ∈ ( 𝑗 ... 𝑛 ) ) → ( 𝐹𝑘 ) ∈ 𝑋 )
144 65 139 143 mettrifi ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → ( ( 𝐹𝑗 ) 𝐷 ( 𝐹𝑛 ) ) ≤ Σ 𝑘 ∈ ( 𝑗 ... ( 𝑛 − 1 ) ) ( ( 𝐹𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
145 125 89 sylan2 ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) ∧ 𝑘 ∈ ( 𝑗 ... ( 𝑛 − 1 ) ) ) → ( 𝐴 · ( 𝐵𝑘 ) ) ∈ ℝ )
146 123 145 fsumrecl ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → Σ 𝑘 ∈ ( 𝑗 ... ( 𝑛 − 1 ) ) ( 𝐴 · ( 𝐵𝑘 ) ) ∈ ℝ )
147 124 129 6 syl2anc ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) ∧ 𝑘 ∈ ( 𝑗 ... ( 𝑛 − 1 ) ) ) → ( ( 𝐹𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( 𝐴 · ( 𝐵𝑘 ) ) )
148 123 137 145 147 fsumle ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → Σ 𝑘 ∈ ( 𝑗 ... ( 𝑛 − 1 ) ) ( ( 𝐹𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ Σ 𝑘 ∈ ( 𝑗 ... ( 𝑛 − 1 ) ) ( 𝐴 · ( 𝐵𝑘 ) ) )
149 fzssuz ( 𝑗 ... ( 𝑛 − 1 ) ) ⊆ ( ℤ𝑗 )
150 149 a1i ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → ( 𝑗 ... ( 𝑛 − 1 ) ) ⊆ ( ℤ𝑗 ) )
151 0red ( ( 𝜑𝑘 ∈ ℕ ) → 0 ∈ ℝ )
152 nnz ( 𝑘 ∈ ℕ → 𝑘 ∈ ℤ )
153 rpexpcl ( ( 𝐵 ∈ ℝ+𝑘 ∈ ℤ ) → ( 𝐵𝑘 ) ∈ ℝ+ )
154 4 152 153 syl2an ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐵𝑘 ) ∈ ℝ+ )
155 136 154 rerpdivcld ( ( 𝜑𝑘 ∈ ℕ ) → ( ( ( 𝐹𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) / ( 𝐵𝑘 ) ) ∈ ℝ )
156 3 adantr ( ( 𝜑𝑘 ∈ ℕ ) → 𝐴 ∈ ℝ )
157 metge0 ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐹𝑘 ) ∈ 𝑋 ∧ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ 𝑋 ) → 0 ≤ ( ( 𝐹𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
158 130 131 134 157 syl3anc ( ( 𝜑𝑘 ∈ ℕ ) → 0 ≤ ( ( 𝐹𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
159 136 154 158 divge0d ( ( 𝜑𝑘 ∈ ℕ ) → 0 ≤ ( ( ( 𝐹𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) / ( 𝐵𝑘 ) ) )
160 136 156 154 ledivmul2d ( ( 𝜑𝑘 ∈ ℕ ) → ( ( ( ( 𝐹𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) / ( 𝐵𝑘 ) ) ≤ 𝐴 ↔ ( ( 𝐹𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( 𝐴 · ( 𝐵𝑘 ) ) ) )
161 6 160 mpbird ( ( 𝜑𝑘 ∈ ℕ ) → ( ( ( 𝐹𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) / ( 𝐵𝑘 ) ) ≤ 𝐴 )
162 151 155 156 159 161 letrd ( ( 𝜑𝑘 ∈ ℕ ) → 0 ≤ 𝐴 )
163 141 128 162 syl2anc ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → 0 ≤ 𝐴 )
164 141 128 154 syl2anc ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → ( 𝐵𝑘 ) ∈ ℝ+ )
165 164 rpge0d ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → 0 ≤ ( 𝐵𝑘 ) )
166 84 88 163 165 mulge0d ( ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → 0 ≤ ( 𝐴 · ( 𝐵𝑘 ) ) )
167 74 77 123 150 83 89 166 118 isumless ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → Σ 𝑘 ∈ ( 𝑗 ... ( 𝑛 − 1 ) ) ( 𝐴 · ( 𝐵𝑘 ) ) ≤ Σ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐴 · ( 𝐵𝑘 ) ) )
168 138 146 119 148 167 letrd ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → Σ 𝑘 ∈ ( 𝑗 ... ( 𝑛 − 1 ) ) ( ( 𝐹𝑘 ) 𝐷 ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ Σ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐴 · ( 𝐵𝑘 ) ) )
169 73 138 119 144 168 letrd ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → ( ( 𝐹𝑗 ) 𝐷 ( 𝐹𝑛 ) ) ≤ Σ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐴 · ( 𝐵𝑘 ) ) )
170 169 114 breqtrd ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → ( ( 𝐹𝑗 ) 𝐷 ( 𝐹𝑛 ) ) ≤ ( ( 𝐵𝑗 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) )
171 120 leabsd ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → ( ( 𝐵𝑗 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ≤ ( abs ‘ ( ( 𝐵𝑗 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) )
172 73 120 122 170 171 letrd ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → ( ( 𝐹𝑗 ) 𝐷 ( 𝐹𝑛 ) ) ≤ ( abs ‘ ( ( 𝐵𝑗 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) )
173 172 adantlr ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → ( ( 𝐹𝑗 ) 𝐷 ( 𝐹𝑛 ) ) ≤ ( abs ‘ ( ( 𝐵𝑗 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) )
174 73 adantlr ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → ( ( 𝐹𝑗 ) 𝐷 ( 𝐹𝑛 ) ) ∈ ℝ )
175 122 adantlr ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → ( abs ‘ ( ( 𝐵𝑗 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) ∈ ℝ )
176 rpre ( 𝑥 ∈ ℝ+𝑥 ∈ ℝ )
177 176 ad2antlr ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → 𝑥 ∈ ℝ )
178 lelttr ( ( ( ( 𝐹𝑗 ) 𝐷 ( 𝐹𝑛 ) ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐵𝑗 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ( ( 𝐹𝑗 ) 𝐷 ( 𝐹𝑛 ) ) ≤ ( abs ‘ ( ( 𝐵𝑗 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) ∧ ( abs ‘ ( ( 𝐵𝑗 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) < 𝑥 ) → ( ( 𝐹𝑗 ) 𝐷 ( 𝐹𝑛 ) ) < 𝑥 ) )
179 174 175 177 178 syl3anc ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → ( ( ( ( 𝐹𝑗 ) 𝐷 ( 𝐹𝑛 ) ) ≤ ( abs ‘ ( ( 𝐵𝑗 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) ∧ ( abs ‘ ( ( 𝐵𝑗 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) < 𝑥 ) → ( ( 𝐹𝑗 ) 𝐷 ( 𝐹𝑛 ) ) < 𝑥 ) )
180 173 179 mpand ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ ℕ ∧ 𝑛 ∈ ( ℤ𝑗 ) ) ) → ( ( abs ‘ ( ( 𝐵𝑗 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) < 𝑥 → ( ( 𝐹𝑗 ) 𝐷 ( 𝐹𝑛 ) ) < 𝑥 ) )
181 180 anassrs ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( ℤ𝑗 ) ) → ( ( abs ‘ ( ( 𝐵𝑗 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) < 𝑥 → ( ( 𝐹𝑗 ) 𝐷 ( 𝐹𝑛 ) ) < 𝑥 ) )
182 181 ralrimdva ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ( abs ‘ ( ( 𝐵𝑗 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) < 𝑥 → ∀ 𝑛 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑗 ) 𝐷 ( 𝐹𝑛 ) ) < 𝑥 ) )
183 64 182 syld ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ ) → ( ∀ 𝑛 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐵𝑛 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) < 𝑥 → ∀ 𝑛 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑗 ) 𝐷 ( 𝐹𝑛 ) ) < 𝑥 ) )
184 183 reximdva ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ∃ 𝑗 ∈ ℕ ∀ 𝑛 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐵𝑛 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) < 𝑥 → ∃ 𝑗 ∈ ℕ ∀ 𝑛 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑗 ) 𝐷 ( 𝐹𝑛 ) ) < 𝑥 ) )
185 184 ralimdva ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+𝑗 ∈ ℕ ∀ 𝑛 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐵𝑛 ) · ( 𝐴 / ( 1 − 𝐵 ) ) ) ) < 𝑥 → ∀ 𝑥 ∈ ℝ+𝑗 ∈ ℕ ∀ 𝑛 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑗 ) 𝐷 ( 𝐹𝑛 ) ) < 𝑥 ) )
186 56 185 mpd ( 𝜑 → ∀ 𝑥 ∈ ℝ+𝑗 ∈ ℕ ∀ 𝑛 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑗 ) 𝐷 ( 𝐹𝑛 ) ) < 𝑥 )
187 metxmet ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
188 1 187 syl ( 𝜑𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
189 eqidd ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝐹𝑛 ) = ( 𝐹𝑛 ) )
190 eqidd ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐹𝑗 ) = ( 𝐹𝑗 ) )
191 7 188 8 189 190 2 iscauf ( 𝜑 → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ℕ ∀ 𝑛 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑗 ) 𝐷 ( 𝐹𝑛 ) ) < 𝑥 ) )
192 186 191 mpbird ( 𝜑𝐹 ∈ ( Cau ‘ 𝐷 ) )