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 ‘ 𝐷 ) )