Step | Hyp | Ref
| Expression |
1 | | nnuz 11723 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 11408 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℤ) |
3 | | geomcau.5 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
4 | 3 | rpcnd 11874 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℂ) |
5 | 3 | rpred 11872 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ ℝ) |
6 | 3 | rpge0d 11876 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ 𝐵) |
7 | 5, 6 | absidd 14161 |
. . . . . . . 8
⊢ (𝜑 → (abs‘𝐵) = 𝐵) |
8 | | geomcau.6 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 < 1) |
9 | 7, 8 | eqbrtrd 4675 |
. . . . . . 7
⊢ (𝜑 → (abs‘𝐵) < 1) |
10 | 4, 9 | expcnv 14596 |
. . . . . 6
⊢ (𝜑 → (𝑚 ∈ ℕ0 ↦ (𝐵↑𝑚)) ⇝ 0) |
11 | | geomcau.4 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℝ) |
12 | | 1re 10039 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ |
13 | | resubcl 10345 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ 𝐵
∈ ℝ) → (1 − 𝐵) ∈ ℝ) |
14 | 12, 5, 13 | sylancr 695 |
. . . . . . . . 9
⊢ (𝜑 → (1 − 𝐵) ∈
ℝ) |
15 | | posdif 10521 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ ∧ 1 ∈
ℝ) → (𝐵 < 1
↔ 0 < (1 − 𝐵))) |
16 | 5, 12, 15 | sylancl 694 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 < 1 ↔ 0 < (1 − 𝐵))) |
17 | 8, 16 | mpbid 222 |
. . . . . . . . 9
⊢ (𝜑 → 0 < (1 − 𝐵)) |
18 | 14, 17 | elrpd 11869 |
. . . . . . . 8
⊢ (𝜑 → (1 − 𝐵) ∈
ℝ+) |
19 | 11, 18 | rerpdivcld 11903 |
. . . . . . 7
⊢ (𝜑 → (𝐴 / (1 − 𝐵)) ∈ ℝ) |
20 | 19 | recnd 10068 |
. . . . . 6
⊢ (𝜑 → (𝐴 / (1 − 𝐵)) ∈ ℂ) |
21 | | nnex 11026 |
. . . . . . . 8
⊢ ℕ
∈ V |
22 | 21 | mptex 6486 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ ↦ ((𝐵↑𝑚) · (𝐴 / (1 − 𝐵)))) ∈ V |
23 | 22 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐵↑𝑚) · (𝐴 / (1 − 𝐵)))) ∈ V) |
24 | | nnnn0 11299 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
25 | 24 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0) |
26 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → (𝐵↑𝑚) = (𝐵↑𝑛)) |
27 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ0
↦ (𝐵↑𝑚)) = (𝑚 ∈ ℕ0 ↦ (𝐵↑𝑚)) |
28 | | ovex 6678 |
. . . . . . . . 9
⊢ (𝐵↑𝑛) ∈ V |
29 | 26, 27, 28 | fvmpt 6282 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ ((𝑚 ∈
ℕ0 ↦ (𝐵↑𝑚))‘𝑛) = (𝐵↑𝑛)) |
30 | 25, 29 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ0 ↦ (𝐵↑𝑚))‘𝑛) = (𝐵↑𝑛)) |
31 | | nnz 11399 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℤ) |
32 | | rpexpcl 12879 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ+
∧ 𝑛 ∈ ℤ)
→ (𝐵↑𝑛) ∈
ℝ+) |
33 | 3, 31, 32 | syl2an 494 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐵↑𝑛) ∈
ℝ+) |
34 | 33 | rpcnd 11874 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐵↑𝑛) ∈ ℂ) |
35 | 30, 34 | eqeltrd 2701 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ0 ↦ (𝐵↑𝑚))‘𝑛) ∈ ℂ) |
36 | 20 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴 / (1 − 𝐵)) ∈ ℂ) |
37 | 34, 36 | mulcomd 10061 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐵↑𝑛) · (𝐴 / (1 − 𝐵))) = ((𝐴 / (1 − 𝐵)) · (𝐵↑𝑛))) |
38 | 26 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → ((𝐵↑𝑚) · (𝐴 / (1 − 𝐵))) = ((𝐵↑𝑛) · (𝐴 / (1 − 𝐵)))) |
39 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ ↦ ((𝐵↑𝑚) · (𝐴 / (1 − 𝐵)))) = (𝑚 ∈ ℕ ↦ ((𝐵↑𝑚) · (𝐴 / (1 − 𝐵)))) |
40 | | ovex 6678 |
. . . . . . . . 9
⊢ ((𝐵↑𝑛) · (𝐴 / (1 − 𝐵))) ∈ V |
41 | 38, 39, 40 | fvmpt 6282 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((𝐵↑𝑚) · (𝐴 / (1 − 𝐵))))‘𝑛) = ((𝐵↑𝑛) · (𝐴 / (1 − 𝐵)))) |
42 | 41 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((𝐵↑𝑚) · (𝐴 / (1 − 𝐵))))‘𝑛) = ((𝐵↑𝑛) · (𝐴 / (1 − 𝐵)))) |
43 | 30 | oveq2d 6666 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴 / (1 − 𝐵)) · ((𝑚 ∈ ℕ0 ↦ (𝐵↑𝑚))‘𝑛)) = ((𝐴 / (1 − 𝐵)) · (𝐵↑𝑛))) |
44 | 37, 42, 43 | 3eqtr4d 2666 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((𝐵↑𝑚) · (𝐴 / (1 − 𝐵))))‘𝑛) = ((𝐴 / (1 − 𝐵)) · ((𝑚 ∈ ℕ0 ↦ (𝐵↑𝑚))‘𝑛))) |
45 | 1, 2, 10, 20, 23, 35, 44 | climmulc2 14367 |
. . . . 5
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐵↑𝑚) · (𝐴 / (1 − 𝐵)))) ⇝ ((𝐴 / (1 − 𝐵)) · 0)) |
46 | 20 | mul01d 10235 |
. . . . 5
⊢ (𝜑 → ((𝐴 / (1 − 𝐵)) · 0) = 0) |
47 | 45, 46 | breqtrd 4679 |
. . . 4
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐵↑𝑚) · (𝐴 / (1 − 𝐵)))) ⇝ 0) |
48 | 33 | rpred 11872 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐵↑𝑛) ∈ ℝ) |
49 | 19 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴 / (1 − 𝐵)) ∈ ℝ) |
50 | 48, 49 | remulcld 10070 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐵↑𝑛) · (𝐴 / (1 − 𝐵))) ∈ ℝ) |
51 | 50 | recnd 10068 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐵↑𝑛) · (𝐴 / (1 − 𝐵))) ∈ ℂ) |
52 | 1, 2, 23, 42, 51 | clim0c 14238 |
. . . 4
⊢ (𝜑 → ((𝑚 ∈ ℕ ↦ ((𝐵↑𝑚) · (𝐴 / (1 − 𝐵)))) ⇝ 0 ↔ ∀𝑥 ∈ ℝ+
∃𝑗 ∈ ℕ
∀𝑛 ∈
(ℤ≥‘𝑗)(abs‘((𝐵↑𝑛) · (𝐴 / (1 − 𝐵)))) < 𝑥)) |
53 | 47, 52 | mpbid 222 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑛 ∈
(ℤ≥‘𝑗)(abs‘((𝐵↑𝑛) · (𝐴 / (1 − 𝐵)))) < 𝑥) |
54 | | nnz 11399 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℤ) |
55 | 54 | adantl 482 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℤ) |
56 | | uzid 11702 |
. . . . . . 7
⊢ (𝑗 ∈ ℤ → 𝑗 ∈
(ℤ≥‘𝑗)) |
57 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑗 → (𝐵↑𝑛) = (𝐵↑𝑗)) |
58 | 57 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑗 → ((𝐵↑𝑛) · (𝐴 / (1 − 𝐵))) = ((𝐵↑𝑗) · (𝐴 / (1 − 𝐵)))) |
59 | 58 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑛 = 𝑗 → (abs‘((𝐵↑𝑛) · (𝐴 / (1 − 𝐵)))) = (abs‘((𝐵↑𝑗) · (𝐴 / (1 − 𝐵))))) |
60 | 59 | breq1d 4663 |
. . . . . . . 8
⊢ (𝑛 = 𝑗 → ((abs‘((𝐵↑𝑛) · (𝐴 / (1 − 𝐵)))) < 𝑥 ↔ (abs‘((𝐵↑𝑗) · (𝐴 / (1 − 𝐵)))) < 𝑥)) |
61 | 60 | rspcv 3305 |
. . . . . . 7
⊢ (𝑗 ∈
(ℤ≥‘𝑗) → (∀𝑛 ∈ (ℤ≥‘𝑗)(abs‘((𝐵↑𝑛) · (𝐴 / (1 − 𝐵)))) < 𝑥 → (abs‘((𝐵↑𝑗) · (𝐴 / (1 − 𝐵)))) < 𝑥)) |
62 | 55, 56, 61 | 3syl 18 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) →
(∀𝑛 ∈
(ℤ≥‘𝑗)(abs‘((𝐵↑𝑛) · (𝐴 / (1 − 𝐵)))) < 𝑥 → (abs‘((𝐵↑𝑗) · (𝐴 / (1 − 𝐵)))) < 𝑥)) |
63 | | lmclim2.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) |
64 | 63 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → 𝐷 ∈ (Met‘𝑋)) |
65 | | lmclim2.3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:ℕ⟶𝑋) |
66 | | simpl 473 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ ℕ ∧ 𝑛 ∈
(ℤ≥‘𝑗)) → 𝑗 ∈ ℕ) |
67 | | ffvelrn 6357 |
. . . . . . . . . . . . 13
⊢ ((𝐹:ℕ⟶𝑋 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ 𝑋) |
68 | 65, 66, 67 | syl2an 494 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (𝐹‘𝑗) ∈ 𝑋) |
69 | | eluznn 11758 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ ℕ ∧ 𝑛 ∈
(ℤ≥‘𝑗)) → 𝑛 ∈ ℕ) |
70 | | ffvelrn 6357 |
. . . . . . . . . . . . 13
⊢ ((𝐹:ℕ⟶𝑋 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ 𝑋) |
71 | 65, 69, 70 | syl2an 494 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (𝐹‘𝑛) ∈ 𝑋) |
72 | | metcl 22137 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘𝑗) ∈ 𝑋 ∧ (𝐹‘𝑛) ∈ 𝑋) → ((𝐹‘𝑗)𝐷(𝐹‘𝑛)) ∈ ℝ) |
73 | 64, 68, 71, 72 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → ((𝐹‘𝑗)𝐷(𝐹‘𝑛)) ∈ ℝ) |
74 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(ℤ≥‘𝑗) = (ℤ≥‘𝑗) |
75 | | nnnn0 11299 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℕ0) |
76 | 75 | ad2antrl 764 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → 𝑗 ∈ ℕ0) |
77 | 76 | nn0zd 11480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → 𝑗 ∈ ℤ) |
78 | | oveq2 6658 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = 𝑘 → (𝐵↑𝑚) = (𝐵↑𝑘)) |
79 | 78 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑘 → (𝐴 · (𝐵↑𝑚)) = (𝐴 · (𝐵↑𝑘))) |
80 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈
(ℤ≥‘𝑗) ↦ (𝐴 · (𝐵↑𝑚))) = (𝑚 ∈ (ℤ≥‘𝑗) ↦ (𝐴 · (𝐵↑𝑚))) |
81 | | ovex 6678 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 · (𝐵↑𝑘)) ∈ V |
82 | 79, 80, 81 | fvmpt 6282 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈
(ℤ≥‘𝑗) → ((𝑚 ∈ (ℤ≥‘𝑗) ↦ (𝐴 · (𝐵↑𝑚)))‘𝑘) = (𝐴 · (𝐵↑𝑘))) |
83 | 82 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝑚 ∈ (ℤ≥‘𝑗) ↦ (𝐴 · (𝐵↑𝑚)))‘𝑘) = (𝐴 · (𝐵↑𝑘))) |
84 | 11 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝐴 ∈ ℝ) |
85 | 5 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝐵 ∈ ℝ) |
86 | | eluznn0 11757 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘𝑗)) → 𝑘 ∈ ℕ0) |
87 | 76, 86 | sylan 488 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ ℕ0) |
88 | 85, 87 | reexpcld 13025 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐵↑𝑘) ∈ ℝ) |
89 | 84, 88 | remulcld 10070 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐴 · (𝐵↑𝑘)) ∈ ℝ) |
90 | 89 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐴 · (𝐵↑𝑘)) ∈ ℂ) |
91 | 11 | recnd 10068 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈ ℂ) |
92 | 91 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → 𝐴 ∈ ℂ) |
93 | 4 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → 𝐵 ∈ ℂ) |
94 | 9 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (abs‘𝐵) < 1) |
95 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈
(ℤ≥‘𝑗) ↦ (𝐵↑𝑚)) = (𝑚 ∈ (ℤ≥‘𝑗) ↦ (𝐵↑𝑚)) |
96 | | ovex 6678 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐵↑𝑘) ∈ V |
97 | 78, 95, 96 | fvmpt 6282 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈
(ℤ≥‘𝑗) → ((𝑚 ∈ (ℤ≥‘𝑗) ↦ (𝐵↑𝑚))‘𝑘) = (𝐵↑𝑘)) |
98 | 97 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝑚 ∈ (ℤ≥‘𝑗) ↦ (𝐵↑𝑚))‘𝑘) = (𝐵↑𝑘)) |
99 | 93, 94, 76, 98 | geolim2 14602 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → seq𝑗( + , (𝑚 ∈ (ℤ≥‘𝑗) ↦ (𝐵↑𝑚))) ⇝ ((𝐵↑𝑗) / (1 − 𝐵))) |
100 | 88 | recnd 10068 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐵↑𝑘) ∈ ℂ) |
101 | 98, 100 | eqeltrd 2701 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝑚 ∈ (ℤ≥‘𝑗) ↦ (𝐵↑𝑚))‘𝑘) ∈ ℂ) |
102 | 98 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐴 · ((𝑚 ∈ (ℤ≥‘𝑗) ↦ (𝐵↑𝑚))‘𝑘)) = (𝐴 · (𝐵↑𝑘))) |
103 | 83, 102 | eqtr4d 2659 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝑚 ∈ (ℤ≥‘𝑗) ↦ (𝐴 · (𝐵↑𝑚)))‘𝑘) = (𝐴 · ((𝑚 ∈ (ℤ≥‘𝑗) ↦ (𝐵↑𝑚))‘𝑘))) |
104 | 74, 77, 92, 99, 101, 103 | isermulc2 14388 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → seq𝑗( + , (𝑚 ∈ (ℤ≥‘𝑗) ↦ (𝐴 · (𝐵↑𝑚)))) ⇝ (𝐴 · ((𝐵↑𝑗) / (1 − 𝐵)))) |
105 | 3 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → 𝐵 ∈
ℝ+) |
106 | 105, 77 | rpexpcld 13032 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (𝐵↑𝑗) ∈
ℝ+) |
107 | 106 | rpcnd 11874 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (𝐵↑𝑗) ∈ ℂ) |
108 | 14 | recnd 10068 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 − 𝐵) ∈
ℂ) |
109 | 108 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (1 − 𝐵) ∈
ℂ) |
110 | 18 | rpne0d 11877 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 − 𝐵) ≠ 0) |
111 | 110 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (1 − 𝐵) ≠ 0) |
112 | 92, 107, 109, 111 | div12d 10837 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (𝐴 · ((𝐵↑𝑗) / (1 − 𝐵))) = ((𝐵↑𝑗) · (𝐴 / (1 − 𝐵)))) |
113 | 104, 112 | breqtrd 4679 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → seq𝑗( + , (𝑚 ∈ (ℤ≥‘𝑗) ↦ (𝐴 · (𝐵↑𝑚)))) ⇝ ((𝐵↑𝑗) · (𝐴 / (1 − 𝐵)))) |
114 | 74, 77, 83, 90, 113 | isumclim 14488 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → Σ𝑘 ∈
(ℤ≥‘𝑗)(𝐴 · (𝐵↑𝑘)) = ((𝐵↑𝑗) · (𝐴 / (1 − 𝐵)))) |
115 | | seqex 12803 |
. . . . . . . . . . . . . . 15
⊢ seq𝑗( + , (𝑚 ∈ (ℤ≥‘𝑗) ↦ (𝐴 · (𝐵↑𝑚)))) ∈ V |
116 | | ovex 6678 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 · ((𝐵↑𝑗) / (1 − 𝐵))) ∈ V |
117 | 115, 116 | breldm 5329 |
. . . . . . . . . . . . . 14
⊢ (seq𝑗( + , (𝑚 ∈ (ℤ≥‘𝑗) ↦ (𝐴 · (𝐵↑𝑚)))) ⇝ (𝐴 · ((𝐵↑𝑗) / (1 − 𝐵))) → seq𝑗( + , (𝑚 ∈ (ℤ≥‘𝑗) ↦ (𝐴 · (𝐵↑𝑚)))) ∈ dom ⇝ ) |
118 | 104, 117 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → seq𝑗( + , (𝑚 ∈ (ℤ≥‘𝑗) ↦ (𝐴 · (𝐵↑𝑚)))) ∈ dom ⇝ ) |
119 | 74, 77, 83, 89, 118 | isumrecl 14496 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → Σ𝑘 ∈
(ℤ≥‘𝑗)(𝐴 · (𝐵↑𝑘)) ∈ ℝ) |
120 | 114, 119 | eqeltrrd 2702 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → ((𝐵↑𝑗) · (𝐴 / (1 − 𝐵))) ∈ ℝ) |
121 | 120 | recnd 10068 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → ((𝐵↑𝑗) · (𝐴 / (1 − 𝐵))) ∈ ℂ) |
122 | 121 | abscld 14175 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (abs‘((𝐵↑𝑗) · (𝐴 / (1 − 𝐵)))) ∈ ℝ) |
123 | | fzfid 12772 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (𝑗...(𝑛 − 1)) ∈ Fin) |
124 | | simpll 790 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ 𝑘 ∈ (𝑗...(𝑛 − 1))) → 𝜑) |
125 | | elfzuz 12338 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (𝑗...(𝑛 − 1)) → 𝑘 ∈ (ℤ≥‘𝑗)) |
126 | | simprl 794 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → 𝑗 ∈ ℕ) |
127 | | eluznn 11758 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → 𝑘 ∈ ℕ) |
128 | 126, 127 | sylan 488 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ ℕ) |
129 | 125, 128 | sylan2 491 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ 𝑘 ∈ (𝑗...(𝑛 − 1))) → 𝑘 ∈ ℕ) |
130 | 63 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐷 ∈ (Met‘𝑋)) |
131 | 65 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ 𝑋) |
132 | | peano2nn 11032 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) |
133 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹:ℕ⟶𝑋 ∧ (𝑘 + 1) ∈ ℕ) → (𝐹‘(𝑘 + 1)) ∈ 𝑋) |
134 | 65, 132, 133 | syl2an 494 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ∈ 𝑋) |
135 | | metcl 22137 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘(𝑘 + 1)) ∈ 𝑋) → ((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) ∈ ℝ) |
136 | 130, 131,
134, 135 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) ∈ ℝ) |
137 | 124, 129,
136 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ 𝑘 ∈ (𝑗...(𝑛 − 1))) → ((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) ∈ ℝ) |
138 | 123, 137 | fsumrecl 14465 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → Σ𝑘 ∈ (𝑗...(𝑛 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) ∈ ℝ) |
139 | | simprr 796 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → 𝑛 ∈ (ℤ≥‘𝑗)) |
140 | | elfzuz 12338 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (𝑗...𝑛) → 𝑘 ∈ (ℤ≥‘𝑗)) |
141 | | simpll 790 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝜑) |
142 | 141, 128,
131 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ∈ 𝑋) |
143 | 140, 142 | sylan2 491 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ 𝑘 ∈ (𝑗...𝑛)) → (𝐹‘𝑘) ∈ 𝑋) |
144 | 64, 139, 143 | mettrifi 33553 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → ((𝐹‘𝑗)𝐷(𝐹‘𝑛)) ≤ Σ𝑘 ∈ (𝑗...(𝑛 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))) |
145 | 125, 89 | sylan2 491 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ 𝑘 ∈ (𝑗...(𝑛 − 1))) → (𝐴 · (𝐵↑𝑘)) ∈ ℝ) |
146 | 123, 145 | fsumrecl 14465 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → Σ𝑘 ∈ (𝑗...(𝑛 − 1))(𝐴 · (𝐵↑𝑘)) ∈ ℝ) |
147 | | geomcau.7 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (𝐵↑𝑘))) |
148 | 124, 129,
147 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ 𝑘 ∈ (𝑗...(𝑛 − 1))) → ((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (𝐵↑𝑘))) |
149 | 123, 137,
145, 148 | fsumle 14531 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → Σ𝑘 ∈ (𝑗...(𝑛 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) ≤ Σ𝑘 ∈ (𝑗...(𝑛 − 1))(𝐴 · (𝐵↑𝑘))) |
150 | | fzssuz 12382 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗...(𝑛 − 1)) ⊆
(ℤ≥‘𝑗) |
151 | 150 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (𝑗...(𝑛 − 1)) ⊆
(ℤ≥‘𝑗)) |
152 | | 0red 10041 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ∈
ℝ) |
153 | | nnz 11399 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) |
154 | | rpexpcl 12879 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈ ℝ+
∧ 𝑘 ∈ ℤ)
→ (𝐵↑𝑘) ∈
ℝ+) |
155 | 3, 153, 154 | syl2an 494 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐵↑𝑘) ∈
ℝ+) |
156 | 136, 155 | rerpdivcld 11903 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) / (𝐵↑𝑘)) ∈ ℝ) |
157 | 11 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ℝ) |
158 | | metge0 22150 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘(𝑘 + 1)) ∈ 𝑋) → 0 ≤ ((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))) |
159 | 130, 131,
134, 158 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ≤ ((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1)))) |
160 | 136, 155,
159 | divge0d 11912 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ≤ (((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) / (𝐵↑𝑘))) |
161 | 136, 157,
155 | ledivmul2d 11926 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) / (𝐵↑𝑘)) ≤ 𝐴 ↔ ((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (𝐵↑𝑘)))) |
162 | 147, 161 | mpbird 247 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) / (𝐵↑𝑘)) ≤ 𝐴) |
163 | 152, 156,
157, 160, 162 | letrd 10194 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ≤ 𝐴) |
164 | 141, 128,
163 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 0 ≤ 𝐴) |
165 | 141, 128,
155 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐵↑𝑘) ∈
ℝ+) |
166 | 165 | rpge0d 11876 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 0 ≤ (𝐵↑𝑘)) |
167 | 84, 88, 164, 166 | mulge0d 10604 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 0 ≤ (𝐴 · (𝐵↑𝑘))) |
168 | 74, 77, 123, 151, 83, 89, 167, 118 | isumless 14577 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → Σ𝑘 ∈ (𝑗...(𝑛 − 1))(𝐴 · (𝐵↑𝑘)) ≤ Σ𝑘 ∈ (ℤ≥‘𝑗)(𝐴 · (𝐵↑𝑘))) |
169 | 138, 146,
119, 149, 168 | letrd 10194 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → Σ𝑘 ∈ (𝑗...(𝑛 − 1))((𝐹‘𝑘)𝐷(𝐹‘(𝑘 + 1))) ≤ Σ𝑘 ∈ (ℤ≥‘𝑗)(𝐴 · (𝐵↑𝑘))) |
170 | 73, 138, 119, 144, 169 | letrd 10194 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → ((𝐹‘𝑗)𝐷(𝐹‘𝑛)) ≤ Σ𝑘 ∈ (ℤ≥‘𝑗)(𝐴 · (𝐵↑𝑘))) |
171 | 170, 114 | breqtrd 4679 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → ((𝐹‘𝑗)𝐷(𝐹‘𝑛)) ≤ ((𝐵↑𝑗) · (𝐴 / (1 − 𝐵)))) |
172 | 120 | leabsd 14153 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → ((𝐵↑𝑗) · (𝐴 / (1 − 𝐵))) ≤ (abs‘((𝐵↑𝑗) · (𝐴 / (1 − 𝐵))))) |
173 | 73, 120, 122, 171, 172 | letrd 10194 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → ((𝐹‘𝑗)𝐷(𝐹‘𝑛)) ≤ (abs‘((𝐵↑𝑗) · (𝐴 / (1 − 𝐵))))) |
174 | 173 | adantlr 751 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈
(ℤ≥‘𝑗))) → ((𝐹‘𝑗)𝐷(𝐹‘𝑛)) ≤ (abs‘((𝐵↑𝑗) · (𝐴 / (1 − 𝐵))))) |
175 | 73 | adantlr 751 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈
(ℤ≥‘𝑗))) → ((𝐹‘𝑗)𝐷(𝐹‘𝑛)) ∈ ℝ) |
176 | 122 | adantlr 751 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈
(ℤ≥‘𝑗))) → (abs‘((𝐵↑𝑗) · (𝐴 / (1 − 𝐵)))) ∈ ℝ) |
177 | | rpre 11839 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
178 | 177 | ad2antlr 763 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈
(ℤ≥‘𝑗))) → 𝑥 ∈ ℝ) |
179 | | lelttr 10128 |
. . . . . . . . . 10
⊢ ((((𝐹‘𝑗)𝐷(𝐹‘𝑛)) ∈ ℝ ∧ (abs‘((𝐵↑𝑗) · (𝐴 / (1 − 𝐵)))) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((((𝐹‘𝑗)𝐷(𝐹‘𝑛)) ≤ (abs‘((𝐵↑𝑗) · (𝐴 / (1 − 𝐵)))) ∧ (abs‘((𝐵↑𝑗) · (𝐴 / (1 − 𝐵)))) < 𝑥) → ((𝐹‘𝑗)𝐷(𝐹‘𝑛)) < 𝑥)) |
180 | 175, 176,
178, 179 | syl3anc 1326 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈
(ℤ≥‘𝑗))) → ((((𝐹‘𝑗)𝐷(𝐹‘𝑛)) ≤ (abs‘((𝐵↑𝑗) · (𝐴 / (1 − 𝐵)))) ∧ (abs‘((𝐵↑𝑗) · (𝐴 / (1 − 𝐵)))) < 𝑥) → ((𝐹‘𝑗)𝐷(𝐹‘𝑛)) < 𝑥)) |
181 | 174, 180 | mpand 711 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈
(ℤ≥‘𝑗))) → ((abs‘((𝐵↑𝑗) · (𝐴 / (1 − 𝐵)))) < 𝑥 → ((𝐹‘𝑗)𝐷(𝐹‘𝑛)) < 𝑥)) |
182 | 181 | anassrs 680 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈
(ℤ≥‘𝑗)) → ((abs‘((𝐵↑𝑗) · (𝐴 / (1 − 𝐵)))) < 𝑥 → ((𝐹‘𝑗)𝐷(𝐹‘𝑛)) < 𝑥)) |
183 | 182 | ralrimdva 2969 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) →
((abs‘((𝐵↑𝑗) · (𝐴 / (1 − 𝐵)))) < 𝑥 → ∀𝑛 ∈ (ℤ≥‘𝑗)((𝐹‘𝑗)𝐷(𝐹‘𝑛)) < 𝑥)) |
184 | 62, 183 | syld 47 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) →
(∀𝑛 ∈
(ℤ≥‘𝑗)(abs‘((𝐵↑𝑛) · (𝐴 / (1 − 𝐵)))) < 𝑥 → ∀𝑛 ∈ (ℤ≥‘𝑗)((𝐹‘𝑗)𝐷(𝐹‘𝑛)) < 𝑥)) |
185 | 184 | reximdva 3017 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(∃𝑗 ∈ ℕ
∀𝑛 ∈
(ℤ≥‘𝑗)(abs‘((𝐵↑𝑛) · (𝐴 / (1 − 𝐵)))) < 𝑥 → ∃𝑗 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑗)((𝐹‘𝑗)𝐷(𝐹‘𝑛)) < 𝑥)) |
186 | 185 | ralimdva 2962 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ ℝ+
∃𝑗 ∈ ℕ
∀𝑛 ∈
(ℤ≥‘𝑗)(abs‘((𝐵↑𝑛) · (𝐴 / (1 − 𝐵)))) < 𝑥 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑛 ∈
(ℤ≥‘𝑗)((𝐹‘𝑗)𝐷(𝐹‘𝑛)) < 𝑥)) |
187 | 53, 186 | mpd 15 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑛 ∈
(ℤ≥‘𝑗)((𝐹‘𝑗)𝐷(𝐹‘𝑛)) < 𝑥) |
188 | | metxmet 22139 |
. . . 4
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
189 | 63, 188 | syl 17 |
. . 3
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
190 | | eqidd 2623 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = (𝐹‘𝑛)) |
191 | | eqidd 2623 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = (𝐹‘𝑗)) |
192 | 1, 189, 2, 190, 191, 65 | iscauf 23078 |
. 2
⊢ (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑛 ∈
(ℤ≥‘𝑗)((𝐹‘𝑗)𝐷(𝐹‘𝑛)) < 𝑥)) |
193 | 187, 192 | mpbird 247 |
1
⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷)) |