Mathbox for Jeff Madsen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  geomcau Structured version   Visualization version   GIF version

Theorem geomcau 35499
 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.)
Hypotheses
Ref Expression
lmclim2.2 (𝜑𝐷 ∈ (Met‘𝑋))
lmclim2.3 (𝜑𝐹:ℕ⟶𝑋)
geomcau.4 (𝜑𝐴 ∈ ℝ)
geomcau.5 (𝜑𝐵 ∈ ℝ+)
geomcau.6 (𝜑𝐵 < 1)
geomcau.7 ((𝜑𝑘 ∈ ℕ) → ((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (𝐵𝑘)))
Assertion
Ref Expression
geomcau (𝜑𝐹 ∈ (Cau‘𝐷))
Distinct variable groups:   𝐷,𝑘   𝑘,𝐹   𝑘,𝑋   𝐴,𝑘   𝐵,𝑘   𝜑,𝑘

Proof of Theorem geomcau
Dummy variables 𝑗 𝑛 𝑥 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 12321 . . . . . 6 ℕ = (ℤ‘1)
2 1zzd 12052 . . . . . 6 (𝜑 → 1 ∈ ℤ)
3 geomcau.5 . . . . . . . 8 (𝜑𝐵 ∈ ℝ+)
43rpcnd 12474 . . . . . . 7 (𝜑𝐵 ∈ ℂ)
53rpred 12472 . . . . . . . . 9 (𝜑𝐵 ∈ ℝ)
63rpge0d 12476 . . . . . . . . 9 (𝜑 → 0 ≤ 𝐵)
75, 6absidd 14830 . . . . . . . 8 (𝜑 → (abs‘𝐵) = 𝐵)
8 geomcau.6 . . . . . . . 8 (𝜑𝐵 < 1)
97, 8eqbrtrd 5054 . . . . . . 7 (𝜑 → (abs‘𝐵) < 1)
104, 9expcnv 15267 . . . . . 6 (𝜑 → (𝑚 ∈ ℕ0 ↦ (𝐵𝑚)) ⇝ 0)
11 geomcau.4 . . . . . . . 8 (𝜑𝐴 ∈ ℝ)
12 1re 10679 . . . . . . . . . 10 1 ∈ ℝ
13 resubcl 10988 . . . . . . . . . 10 ((1 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (1 − 𝐵) ∈ ℝ)
1412, 5, 13sylancr 590 . . . . . . . . 9 (𝜑 → (1 − 𝐵) ∈ ℝ)
15 posdif 11171 . . . . . . . . . . 11 ((𝐵 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐵 < 1 ↔ 0 < (1 − 𝐵)))
165, 12, 15sylancl 589 . . . . . . . . . 10 (𝜑 → (𝐵 < 1 ↔ 0 < (1 − 𝐵)))
178, 16mpbid 235 . . . . . . . . 9 (𝜑 → 0 < (1 − 𝐵))
1814, 17elrpd 12469 . . . . . . . 8 (𝜑 → (1 − 𝐵) ∈ ℝ+)
1911, 18rerpdivcld 12503 . . . . . . 7 (𝜑 → (𝐴 / (1 − 𝐵)) ∈ ℝ)
2019recnd 10707 . . . . . 6 (𝜑 → (𝐴 / (1 − 𝐵)) ∈ ℂ)
21 nnex 11680 . . . . . . . 8 ℕ ∈ V
2221mptex 6977 . . . . . . 7 (𝑚 ∈ ℕ ↦ ((𝐵𝑚) · (𝐴 / (1 − 𝐵)))) ∈ V
2322a1i 11 . . . . . 6 (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐵𝑚) · (𝐴 / (1 − 𝐵)))) ∈ V)
24 nnnn0 11941 . . . . . . . . 9 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
2524adantl 485 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0)
26 oveq2 7158 . . . . . . . . 9 (𝑚 = 𝑛 → (𝐵𝑚) = (𝐵𝑛))
27 eqid 2758 . . . . . . . . 9 (𝑚 ∈ ℕ0 ↦ (𝐵𝑚)) = (𝑚 ∈ ℕ0 ↦ (𝐵𝑚))
28 ovex 7183 . . . . . . . . 9 (𝐵𝑛) ∈ V
2926, 27, 28fvmpt 6759 . . . . . . . 8 (𝑛 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ (𝐵𝑚))‘𝑛) = (𝐵𝑛))
3025, 29syl 17 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ0 ↦ (𝐵𝑚))‘𝑛) = (𝐵𝑛))
31 nnz 12043 . . . . . . . . 9 (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
32 rpexpcl 13498 . . . . . . . . 9 ((𝐵 ∈ ℝ+𝑛 ∈ ℤ) → (𝐵𝑛) ∈ ℝ+)
333, 31, 32syl2an 598 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝐵𝑛) ∈ ℝ+)
3433rpcnd 12474 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐵𝑛) ∈ ℂ)
3530, 34eqeltrd 2852 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ0 ↦ (𝐵𝑚))‘𝑛) ∈ ℂ)
3620adantr 484 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝐴 / (1 − 𝐵)) ∈ ℂ)
3734, 36mulcomd 10700 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((𝐵𝑛) · (𝐴 / (1 − 𝐵))) = ((𝐴 / (1 − 𝐵)) · (𝐵𝑛)))
3826oveq1d 7165 . . . . . . . . 9 (𝑚 = 𝑛 → ((𝐵𝑚) · (𝐴 / (1 − 𝐵))) = ((𝐵𝑛) · (𝐴 / (1 − 𝐵))))
39 eqid 2758 . . . . . . . . 9 (𝑚 ∈ ℕ ↦ ((𝐵𝑚) · (𝐴 / (1 − 𝐵)))) = (𝑚 ∈ ℕ ↦ ((𝐵𝑚) · (𝐴 / (1 − 𝐵))))
40 ovex 7183 . . . . . . . . 9 ((𝐵𝑛) · (𝐴 / (1 − 𝐵))) ∈ V
4138, 39, 40fvmpt 6759 . . . . . . . 8 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((𝐵𝑚) · (𝐴 / (1 − 𝐵))))‘𝑛) = ((𝐵𝑛) · (𝐴 / (1 − 𝐵))))
4241adantl 485 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((𝐵𝑚) · (𝐴 / (1 − 𝐵))))‘𝑛) = ((𝐵𝑛) · (𝐴 / (1 − 𝐵))))
4330oveq2d 7166 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((𝐴 / (1 − 𝐵)) · ((𝑚 ∈ ℕ0 ↦ (𝐵𝑚))‘𝑛)) = ((𝐴 / (1 − 𝐵)) · (𝐵𝑛)))
4437, 42, 433eqtr4d 2803 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((𝐵𝑚) · (𝐴 / (1 − 𝐵))))‘𝑛) = ((𝐴 / (1 − 𝐵)) · ((𝑚 ∈ ℕ0 ↦ (𝐵𝑚))‘𝑛)))
451, 2, 10, 20, 23, 35, 44climmulc2 15041 . . . . 5 (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐵𝑚) · (𝐴 / (1 − 𝐵)))) ⇝ ((𝐴 / (1 − 𝐵)) · 0))
4620mul01d 10877 . . . . 5 (𝜑 → ((𝐴 / (1 − 𝐵)) · 0) = 0)
4745, 46breqtrd 5058 . . . 4 (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐵𝑚) · (𝐴 / (1 − 𝐵)))) ⇝ 0)
4833rpred 12472 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐵𝑛) ∈ ℝ)
4919adantr 484 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐴 / (1 − 𝐵)) ∈ ℝ)
5048, 49remulcld 10709 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((𝐵𝑛) · (𝐴 / (1 − 𝐵))) ∈ ℝ)
5150recnd 10707 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ((𝐵𝑛) · (𝐴 / (1 − 𝐵))) ∈ ℂ)
521, 2, 23, 42, 51clim0c 14912 . . . 4 (𝜑 → ((𝑚 ∈ ℕ ↦ ((𝐵𝑚) · (𝐴 / (1 − 𝐵)))) ⇝ 0 ↔ ∀𝑥 ∈ ℝ+𝑗 ∈ ℕ ∀𝑛 ∈ (ℤ𝑗)(abs‘((𝐵𝑛) · (𝐴 / (1 − 𝐵)))) < 𝑥))
5347, 52mpbid 235 . . 3 (𝜑 → ∀𝑥 ∈ ℝ+𝑗 ∈ ℕ ∀𝑛 ∈ (ℤ𝑗)(abs‘((𝐵𝑛) · (𝐴 / (1 − 𝐵)))) < 𝑥)
54 nnz 12043 . . . . . . . 8 (𝑗 ∈ ℕ → 𝑗 ∈ ℤ)
5554adantl 485 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℤ)
56 uzid 12297 . . . . . . 7 (𝑗 ∈ ℤ → 𝑗 ∈ (ℤ𝑗))
57 oveq2 7158 . . . . . . . . . 10 (𝑛 = 𝑗 → (𝐵𝑛) = (𝐵𝑗))
5857fvoveq1d 7172 . . . . . . . . 9 (𝑛 = 𝑗 → (abs‘((𝐵𝑛) · (𝐴 / (1 − 𝐵)))) = (abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))))
5958breq1d 5042 . . . . . . . 8 (𝑛 = 𝑗 → ((abs‘((𝐵𝑛) · (𝐴 / (1 − 𝐵)))) < 𝑥 ↔ (abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))) < 𝑥))
6059rspcv 3536 . . . . . . 7 (𝑗 ∈ (ℤ𝑗) → (∀𝑛 ∈ (ℤ𝑗)(abs‘((𝐵𝑛) · (𝐴 / (1 − 𝐵)))) < 𝑥 → (abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))) < 𝑥))
6155, 56, 603syl 18 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (∀𝑛 ∈ (ℤ𝑗)(abs‘((𝐵𝑛) · (𝐴 / (1 − 𝐵)))) < 𝑥 → (abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))) < 𝑥))
62 lmclim2.2 . . . . . . . . . . . . 13 (𝜑𝐷 ∈ (Met‘𝑋))
6362adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → 𝐷 ∈ (Met‘𝑋))
64 lmclim2.3 . . . . . . . . . . . . 13 (𝜑𝐹:ℕ⟶𝑋)
65 simpl 486 . . . . . . . . . . . . 13 ((𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗)) → 𝑗 ∈ ℕ)
66 ffvelrn 6840 . . . . . . . . . . . . 13 ((𝐹:ℕ⟶𝑋𝑗 ∈ ℕ) → (𝐹𝑗) ∈ 𝑋)
6764, 65, 66syl2an 598 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → (𝐹𝑗) ∈ 𝑋)
68 eluznn 12358 . . . . . . . . . . . . 13 ((𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗)) → 𝑛 ∈ ℕ)
69 ffvelrn 6840 . . . . . . . . . . . . 13 ((𝐹:ℕ⟶𝑋𝑛 ∈ ℕ) → (𝐹𝑛) ∈ 𝑋)
7064, 68, 69syl2an 598 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → (𝐹𝑛) ∈ 𝑋)
71 metcl 23034 . . . . . . . . . . . 12 ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹𝑗) ∈ 𝑋 ∧ (𝐹𝑛) ∈ 𝑋) → ((𝐹𝑗)𝐷(𝐹𝑛)) ∈ ℝ)
7263, 67, 70, 71syl3anc 1368 . . . . . . . . . . 11 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → ((𝐹𝑗)𝐷(𝐹𝑛)) ∈ ℝ)
73 eqid 2758 . . . . . . . . . . . . 13 (ℤ𝑗) = (ℤ𝑗)
74 nnnn0 11941 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ → 𝑗 ∈ ℕ0)
7574ad2antrl 727 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → 𝑗 ∈ ℕ0)
7675nn0zd 12124 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → 𝑗 ∈ ℤ)
77 oveq2 7158 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑘 → (𝐵𝑚) = (𝐵𝑘))
7877oveq2d 7166 . . . . . . . . . . . . . . 15 (𝑚 = 𝑘 → (𝐴 · (𝐵𝑚)) = (𝐴 · (𝐵𝑘)))
79 eqid 2758 . . . . . . . . . . . . . . 15 (𝑚 ∈ (ℤ𝑗) ↦ (𝐴 · (𝐵𝑚))) = (𝑚 ∈ (ℤ𝑗) ↦ (𝐴 · (𝐵𝑚)))
80 ovex 7183 . . . . . . . . . . . . . . 15 (𝐴 · (𝐵𝑘)) ∈ V
8178, 79, 80fvmpt 6759 . . . . . . . . . . . . . 14 (𝑘 ∈ (ℤ𝑗) → ((𝑚 ∈ (ℤ𝑗) ↦ (𝐴 · (𝐵𝑚)))‘𝑘) = (𝐴 · (𝐵𝑘)))
8281adantl 485 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → ((𝑚 ∈ (ℤ𝑗) ↦ (𝐴 · (𝐵𝑚)))‘𝑘) = (𝐴 · (𝐵𝑘)))
8311ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝐴 ∈ ℝ)
845ad2antrr 725 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝐵 ∈ ℝ)
85 eluznn0 12357 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ ℕ0𝑘 ∈ (ℤ𝑗)) → 𝑘 ∈ ℕ0)
8675, 85sylan 583 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑘 ∈ ℕ0)
8784, 86reexpcld 13577 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐵𝑘) ∈ ℝ)
8883, 87remulcld 10709 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐴 · (𝐵𝑘)) ∈ ℝ)
8988recnd 10707 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐴 · (𝐵𝑘)) ∈ ℂ)
9011recnd 10707 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ ℂ)
9190adantr 484 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → 𝐴 ∈ ℂ)
924adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → 𝐵 ∈ ℂ)
939adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → (abs‘𝐵) < 1)
94 eqid 2758 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ (ℤ𝑗) ↦ (𝐵𝑚)) = (𝑚 ∈ (ℤ𝑗) ↦ (𝐵𝑚))
95 ovex 7183 . . . . . . . . . . . . . . . . . 18 (𝐵𝑘) ∈ V
9677, 94, 95fvmpt 6759 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (ℤ𝑗) → ((𝑚 ∈ (ℤ𝑗) ↦ (𝐵𝑚))‘𝑘) = (𝐵𝑘))
9796adantl 485 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → ((𝑚 ∈ (ℤ𝑗) ↦ (𝐵𝑚))‘𝑘) = (𝐵𝑘))
9892, 93, 75, 97geolim2 15275 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → seq𝑗( + , (𝑚 ∈ (ℤ𝑗) ↦ (𝐵𝑚))) ⇝ ((𝐵𝑗) / (1 − 𝐵)))
9987recnd 10707 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐵𝑘) ∈ ℂ)
10097, 99eqeltrd 2852 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → ((𝑚 ∈ (ℤ𝑗) ↦ (𝐵𝑚))‘𝑘) ∈ ℂ)
10197oveq2d 7166 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐴 · ((𝑚 ∈ (ℤ𝑗) ↦ (𝐵𝑚))‘𝑘)) = (𝐴 · (𝐵𝑘)))
10282, 101eqtr4d 2796 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → ((𝑚 ∈ (ℤ𝑗) ↦ (𝐴 · (𝐵𝑚)))‘𝑘) = (𝐴 · ((𝑚 ∈ (ℤ𝑗) ↦ (𝐵𝑚))‘𝑘)))
10373, 76, 91, 98, 100, 102isermulc2 15062 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → seq𝑗( + , (𝑚 ∈ (ℤ𝑗) ↦ (𝐴 · (𝐵𝑚)))) ⇝ (𝐴 · ((𝐵𝑗) / (1 − 𝐵))))
1043adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → 𝐵 ∈ ℝ+)
105104, 76rpexpcld 13658 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → (𝐵𝑗) ∈ ℝ+)
106105rpcnd 12474 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → (𝐵𝑗) ∈ ℂ)
10714recnd 10707 . . . . . . . . . . . . . . . 16 (𝜑 → (1 − 𝐵) ∈ ℂ)
108107adantr 484 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → (1 − 𝐵) ∈ ℂ)
10918rpne0d 12477 . . . . . . . . . . . . . . . 16 (𝜑 → (1 − 𝐵) ≠ 0)
110109adantr 484 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → (1 − 𝐵) ≠ 0)
11191, 106, 108, 110div12d 11490 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → (𝐴 · ((𝐵𝑗) / (1 − 𝐵))) = ((𝐵𝑗) · (𝐴 / (1 − 𝐵))))
112103, 111breqtrd 5058 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → seq𝑗( + , (𝑚 ∈ (ℤ𝑗) ↦ (𝐴 · (𝐵𝑚)))) ⇝ ((𝐵𝑗) · (𝐴 / (1 − 𝐵))))
11373, 76, 82, 89, 112isumclim 15160 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → Σ𝑘 ∈ (ℤ𝑗)(𝐴 · (𝐵𝑘)) = ((𝐵𝑗) · (𝐴 / (1 − 𝐵))))
114 seqex 13420 . . . . . . . . . . . . . . 15 seq𝑗( + , (𝑚 ∈ (ℤ𝑗) ↦ (𝐴 · (𝐵𝑚)))) ∈ V
115 ovex 7183 . . . . . . . . . . . . . . 15 (𝐴 · ((𝐵𝑗) / (1 − 𝐵))) ∈ V
116114, 115breldm 5748 . . . . . . . . . . . . . 14 (seq𝑗( + , (𝑚 ∈ (ℤ𝑗) ↦ (𝐴 · (𝐵𝑚)))) ⇝ (𝐴 · ((𝐵𝑗) / (1 − 𝐵))) → seq𝑗( + , (𝑚 ∈ (ℤ𝑗) ↦ (𝐴 · (𝐵𝑚)))) ∈ dom ⇝ )
117103, 116syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → seq𝑗( + , (𝑚 ∈ (ℤ𝑗) ↦ (𝐴 · (𝐵𝑚)))) ∈ dom ⇝ )
11873, 76, 82, 88, 117isumrecl 15168 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → Σ𝑘 ∈ (ℤ𝑗)(𝐴 · (𝐵𝑘)) ∈ ℝ)
119113, 118eqeltrrd 2853 . . . . . . . . . . 11 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → ((𝐵𝑗) · (𝐴 / (1 − 𝐵))) ∈ ℝ)
120119recnd 10707 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → ((𝐵𝑗) · (𝐴 / (1 − 𝐵))) ∈ ℂ)
121120abscld 14844 . . . . . . . . . . 11 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → (abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))) ∈ ℝ)
122 fzfid 13390 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → (𝑗...(𝑛 − 1)) ∈ Fin)
123 simpll 766 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑗...(𝑛 − 1))) → 𝜑)
124 elfzuz 12952 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (𝑗...(𝑛 − 1)) → 𝑘 ∈ (ℤ𝑗))
125 simprl 770 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → 𝑗 ∈ ℕ)
126 eluznn 12358 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑘 ∈ ℕ)
127125, 126sylan 583 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑘 ∈ ℕ)
128124, 127sylan2 595 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑗...(𝑛 − 1))) → 𝑘 ∈ ℕ)
12962adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → 𝐷 ∈ (Met‘𝑋))
13064ffvelrnda 6842 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) ∈ 𝑋)
131 peano2nn 11686 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
132 ffvelrn 6840 . . . . . . . . . . . . . . . . 17 ((𝐹:ℕ⟶𝑋 ∧ (𝑘 + 1) ∈ ℕ) → (𝐹‘(𝑘 + 1)) ∈ 𝑋)
13364, 131, 132syl2an 598 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ∈ 𝑋)
134 metcl 23034 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹𝑘) ∈ 𝑋 ∧ (𝐹‘(𝑘 + 1)) ∈ 𝑋) → ((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ∈ ℝ)
135129, 130, 133, 134syl3anc 1368 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → ((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ∈ ℝ)
136123, 128, 135syl2anc 587 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑗...(𝑛 − 1))) → ((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ∈ ℝ)
137122, 136fsumrecl 15139 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → Σ𝑘 ∈ (𝑗...(𝑛 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ∈ ℝ)
138 simprr 772 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → 𝑛 ∈ (ℤ𝑗))
139 elfzuz 12952 . . . . . . . . . . . . . . 15 (𝑘 ∈ (𝑗...𝑛) → 𝑘 ∈ (ℤ𝑗))
140 simpll 766 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝜑)
141140, 127, 130syl2anc 587 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) ∈ 𝑋)
142139, 141sylan2 595 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑗...𝑛)) → (𝐹𝑘) ∈ 𝑋)
14363, 138, 142mettrifi 35497 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → ((𝐹𝑗)𝐷(𝐹𝑛)) ≤ Σ𝑘 ∈ (𝑗...(𝑛 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))
144124, 88sylan2 595 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑗...(𝑛 − 1))) → (𝐴 · (𝐵𝑘)) ∈ ℝ)
145122, 144fsumrecl 15139 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → Σ𝑘 ∈ (𝑗...(𝑛 − 1))(𝐴 · (𝐵𝑘)) ∈ ℝ)
146 geomcau.7 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → ((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (𝐵𝑘)))
147123, 128, 146syl2anc 587 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑗...(𝑛 − 1))) → ((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (𝐵𝑘)))
148122, 136, 144, 147fsumle 15202 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → Σ𝑘 ∈ (𝑗...(𝑛 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ≤ Σ𝑘 ∈ (𝑗...(𝑛 − 1))(𝐴 · (𝐵𝑘)))
149 fzssuz 12997 . . . . . . . . . . . . . . . 16 (𝑗...(𝑛 − 1)) ⊆ (ℤ𝑗)
150149a1i 11 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → (𝑗...(𝑛 − 1)) ⊆ (ℤ𝑗))
151 0red 10682 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → 0 ∈ ℝ)
152 nnz 12043 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
153 rpexpcl 13498 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ∈ ℝ+𝑘 ∈ ℤ) → (𝐵𝑘) ∈ ℝ+)
1543, 152, 153syl2an 598 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → (𝐵𝑘) ∈ ℝ+)
155135, 154rerpdivcld 12503 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) / (𝐵𝑘)) ∈ ℝ)
15611adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → 𝐴 ∈ ℝ)
157 metge0 23047 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹𝑘) ∈ 𝑋 ∧ (𝐹‘(𝑘 + 1)) ∈ 𝑋) → 0 ≤ ((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))
158129, 130, 133, 157syl3anc 1368 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → 0 ≤ ((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))
159135, 154, 158divge0d 12512 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → 0 ≤ (((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) / (𝐵𝑘)))
160135, 156, 154ledivmul2d 12526 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → ((((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) / (𝐵𝑘)) ≤ 𝐴 ↔ ((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (𝐵𝑘))))
161146, 160mpbird 260 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) / (𝐵𝑘)) ≤ 𝐴)
162151, 155, 156, 159, 161letrd 10835 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → 0 ≤ 𝐴)
163140, 127, 162syl2anc 587 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → 0 ≤ 𝐴)
164140, 127, 154syl2anc 587 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐵𝑘) ∈ ℝ+)
165164rpge0d 12476 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → 0 ≤ (𝐵𝑘))
16683, 87, 163, 165mulge0d 11255 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → 0 ≤ (𝐴 · (𝐵𝑘)))
16773, 76, 122, 150, 82, 88, 166, 117isumless 15248 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → Σ𝑘 ∈ (𝑗...(𝑛 − 1))(𝐴 · (𝐵𝑘)) ≤ Σ𝑘 ∈ (ℤ𝑗)(𝐴 · (𝐵𝑘)))
168137, 145, 118, 148, 167letrd 10835 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → Σ𝑘 ∈ (𝑗...(𝑛 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ≤ Σ𝑘 ∈ (ℤ𝑗)(𝐴 · (𝐵𝑘)))
16972, 137, 118, 143, 168letrd 10835 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → ((𝐹𝑗)𝐷(𝐹𝑛)) ≤ Σ𝑘 ∈ (ℤ𝑗)(𝐴 · (𝐵𝑘)))
170169, 113breqtrd 5058 . . . . . . . . . . 11 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → ((𝐹𝑗)𝐷(𝐹𝑛)) ≤ ((𝐵𝑗) · (𝐴 / (1 − 𝐵))))
171119leabsd 14822 . . . . . . . . . . 11 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → ((𝐵𝑗) · (𝐴 / (1 − 𝐵))) ≤ (abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))))
17272, 119, 121, 170, 171letrd 10835 . . . . . . . . . 10 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → ((𝐹𝑗)𝐷(𝐹𝑛)) ≤ (abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))))
173172adantlr 714 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → ((𝐹𝑗)𝐷(𝐹𝑛)) ≤ (abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))))
17472adantlr 714 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → ((𝐹𝑗)𝐷(𝐹𝑛)) ∈ ℝ)
175121adantlr 714 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → (abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))) ∈ ℝ)
176 rpre 12438 . . . . . . . . . . 11 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
177176ad2antlr 726 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → 𝑥 ∈ ℝ)
178 lelttr 10769 . . . . . . . . . 10 ((((𝐹𝑗)𝐷(𝐹𝑛)) ∈ ℝ ∧ (abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((((𝐹𝑗)𝐷(𝐹𝑛)) ≤ (abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))) ∧ (abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))) < 𝑥) → ((𝐹𝑗)𝐷(𝐹𝑛)) < 𝑥))
179174, 175, 177, 178syl3anc 1368 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → ((((𝐹𝑗)𝐷(𝐹𝑛)) ≤ (abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))) ∧ (abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))) < 𝑥) → ((𝐹𝑗)𝐷(𝐹𝑛)) < 𝑥))
180173, 179mpand 694 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → ((abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))) < 𝑥 → ((𝐹𝑗)𝐷(𝐹𝑛)) < 𝑥))
181180anassrs 471 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (ℤ𝑗)) → ((abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))) < 𝑥 → ((𝐹𝑗)𝐷(𝐹𝑛)) < 𝑥))
182181ralrimdva 3118 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → ((abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))) < 𝑥 → ∀𝑛 ∈ (ℤ𝑗)((𝐹𝑗)𝐷(𝐹𝑛)) < 𝑥))
18361, 182syld 47 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (∀𝑛 ∈ (ℤ𝑗)(abs‘((𝐵𝑛) · (𝐴 / (1 − 𝐵)))) < 𝑥 → ∀𝑛 ∈ (ℤ𝑗)((𝐹𝑗)𝐷(𝐹𝑛)) < 𝑥))
184183reximdva 3198 . . . 4 ((𝜑𝑥 ∈ ℝ+) → (∃𝑗 ∈ ℕ ∀𝑛 ∈ (ℤ𝑗)(abs‘((𝐵𝑛) · (𝐴 / (1 − 𝐵)))) < 𝑥 → ∃𝑗 ∈ ℕ ∀𝑛 ∈ (ℤ𝑗)((𝐹𝑗)𝐷(𝐹𝑛)) < 𝑥))
185184ralimdva 3108 . . 3 (𝜑 → (∀𝑥 ∈ ℝ+𝑗 ∈ ℕ ∀𝑛 ∈ (ℤ𝑗)(abs‘((𝐵𝑛) · (𝐴 / (1 − 𝐵)))) < 𝑥 → ∀𝑥 ∈ ℝ+𝑗 ∈ ℕ ∀𝑛 ∈ (ℤ𝑗)((𝐹𝑗)𝐷(𝐹𝑛)) < 𝑥))
18653, 185mpd 15 . 2 (𝜑 → ∀𝑥 ∈ ℝ+𝑗 ∈ ℕ ∀𝑛 ∈ (ℤ𝑗)((𝐹𝑗)𝐷(𝐹𝑛)) < 𝑥)
187 metxmet 23036 . . . 4 (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
18862, 187syl 17 . . 3 (𝜑𝐷 ∈ (∞Met‘𝑋))
189 eqidd 2759 . . 3 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) = (𝐹𝑛))
190 eqidd 2759 . . 3 ((𝜑𝑗 ∈ ℕ) → (𝐹𝑗) = (𝐹𝑗))
1911, 188, 2, 189, 190, 64iscauf 23980 . 2 (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ ∀𝑥 ∈ ℝ+𝑗 ∈ ℕ ∀𝑛 ∈ (ℤ𝑗)((𝐹𝑗)𝐷(𝐹𝑛)) < 𝑥))
192186, 191mpbird 260 1 (𝜑𝐹 ∈ (Cau‘𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ≠ wne 2951  ∀wral 3070  ∃wrex 3071  Vcvv 3409   ⊆ wss 3858   class class class wbr 5032   ↦ cmpt 5112  dom cdm 5524  ⟶wf 6331  ‘cfv 6335  (class class class)co 7150  ℂcc 10573  ℝcr 10574  0cc0 10575  1c1 10576   + caddc 10578   · cmul 10580   < clt 10713   ≤ cle 10714   − cmin 10908   / cdiv 11335  ℕcn 11674  ℕ0cn0 11934  ℤcz 12020  ℤ≥cuz 12282  ℝ+crp 12430  ...cfz 12939  seqcseq 13418  ↑cexp 13479  abscabs 14641   ⇝ cli 14889  Σcsu 15090  ∞Metcxmet 20151  Metcmet 20152  Cauccau 23953 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5156  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459  ax-inf2 9137  ax-cnex 10631  ax-resscn 10632  ax-1cn 10633  ax-icn 10634  ax-addcl 10635  ax-addrcl 10636  ax-mulcl 10637  ax-mulrcl 10638  ax-mulcom 10639  ax-addass 10640  ax-mulass 10641  ax-distr 10642  ax-i2m1 10643  ax-1ne0 10644  ax-1rid 10645  ax-rnegex 10646  ax-rrecex 10647  ax-cnre 10648  ax-pre-lttri 10649  ax-pre-lttrn 10650  ax-pre-ltadd 10651  ax-pre-mulgt0 10652  ax-pre-sup 10653 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-tp 4527  df-op 4529  df-uni 4799  df-int 4839  df-iun 4885  df-br 5033  df-opab 5095  df-mpt 5113  df-tr 5139  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5483  df-se 5484  df-we 5485  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-isom 6344  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7580  df-1st 7693  df-2nd 7694  df-wrecs 7957  df-recs 8018  df-rdg 8056  df-1o 8112  df-er 8299  df-map 8418  df-pm 8419  df-en 8528  df-dom 8529  df-sdom 8530  df-fin 8531  df-sup 8939  df-inf 8940  df-oi 9007  df-card 9401  df-pnf 10715  df-mnf 10716  df-xr 10717  df-ltxr 10718  df-le 10719  df-sub 10910  df-neg 10911  df-div 11336  df-nn 11675  df-2 11737  df-3 11738  df-n0 11935  df-z 12021  df-uz 12283  df-rp 12431  df-xneg 12548  df-xadd 12549  df-xmul 12550  df-ico 12785  df-fz 12940  df-fzo 13083  df-fl 13211  df-seq 13419  df-exp 13480  df-hash 13741  df-cj 14506  df-re 14507  df-im 14508  df-sqrt 14642  df-abs 14643  df-clim 14893  df-rlim 14894  df-sum 15091  df-psmet 20158  df-xmet 20159  df-met 20160  df-bl 20161  df-cau 23956 This theorem is referenced by:  bfplem1  35562
 Copyright terms: Public domain W3C validator