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

Theorem geomcau 37363
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 12898 . . . . . 6 ℕ = (ℤ‘1)
2 1zzd 12626 . . . . . 6 (𝜑 → 1 ∈ ℤ)
3 geomcau.5 . . . . . . . 8 (𝜑𝐵 ∈ ℝ+)
43rpcnd 13053 . . . . . . 7 (𝜑𝐵 ∈ ℂ)
53rpred 13051 . . . . . . . . 9 (𝜑𝐵 ∈ ℝ)
63rpge0d 13055 . . . . . . . . 9 (𝜑 → 0 ≤ 𝐵)
75, 6absidd 15405 . . . . . . . 8 (𝜑 → (abs‘𝐵) = 𝐵)
8 geomcau.6 . . . . . . . 8 (𝜑𝐵 < 1)
97, 8eqbrtrd 5171 . . . . . . 7 (𝜑 → (abs‘𝐵) < 1)
104, 9expcnv 15846 . . . . . 6 (𝜑 → (𝑚 ∈ ℕ0 ↦ (𝐵𝑚)) ⇝ 0)
11 geomcau.4 . . . . . . . 8 (𝜑𝐴 ∈ ℝ)
12 1re 11246 . . . . . . . . . 10 1 ∈ ℝ
13 resubcl 11556 . . . . . . . . . 10 ((1 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (1 − 𝐵) ∈ ℝ)
1412, 5, 13sylancr 585 . . . . . . . . 9 (𝜑 → (1 − 𝐵) ∈ ℝ)
15 posdif 11739 . . . . . . . . . . 11 ((𝐵 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐵 < 1 ↔ 0 < (1 − 𝐵)))
165, 12, 15sylancl 584 . . . . . . . . . 10 (𝜑 → (𝐵 < 1 ↔ 0 < (1 − 𝐵)))
178, 16mpbid 231 . . . . . . . . 9 (𝜑 → 0 < (1 − 𝐵))
1814, 17elrpd 13048 . . . . . . . 8 (𝜑 → (1 − 𝐵) ∈ ℝ+)
1911, 18rerpdivcld 13082 . . . . . . 7 (𝜑 → (𝐴 / (1 − 𝐵)) ∈ ℝ)
2019recnd 11274 . . . . . 6 (𝜑 → (𝐴 / (1 − 𝐵)) ∈ ℂ)
21 nnex 12251 . . . . . . . 8 ℕ ∈ V
2221mptex 7235 . . . . . . 7 (𝑚 ∈ ℕ ↦ ((𝐵𝑚) · (𝐴 / (1 − 𝐵)))) ∈ V
2322a1i 11 . . . . . 6 (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐵𝑚) · (𝐴 / (1 − 𝐵)))) ∈ V)
24 nnnn0 12512 . . . . . . . . 9 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
2524adantl 480 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0)
26 oveq2 7427 . . . . . . . . 9 (𝑚 = 𝑛 → (𝐵𝑚) = (𝐵𝑛))
27 eqid 2725 . . . . . . . . 9 (𝑚 ∈ ℕ0 ↦ (𝐵𝑚)) = (𝑚 ∈ ℕ0 ↦ (𝐵𝑚))
28 ovex 7452 . . . . . . . . 9 (𝐵𝑛) ∈ V
2926, 27, 28fvmpt 7004 . . . . . . . 8 (𝑛 ∈ ℕ0 → ((𝑚 ∈ ℕ0 ↦ (𝐵𝑚))‘𝑛) = (𝐵𝑛))
3025, 29syl 17 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ0 ↦ (𝐵𝑚))‘𝑛) = (𝐵𝑛))
31 nnz 12612 . . . . . . . . 9 (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
32 rpexpcl 14081 . . . . . . . . 9 ((𝐵 ∈ ℝ+𝑛 ∈ ℤ) → (𝐵𝑛) ∈ ℝ+)
333, 31, 32syl2an 594 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝐵𝑛) ∈ ℝ+)
3433rpcnd 13053 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐵𝑛) ∈ ℂ)
3530, 34eqeltrd 2825 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ0 ↦ (𝐵𝑚))‘𝑛) ∈ ℂ)
3620adantr 479 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝐴 / (1 − 𝐵)) ∈ ℂ)
3734, 36mulcomd 11267 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((𝐵𝑛) · (𝐴 / (1 − 𝐵))) = ((𝐴 / (1 − 𝐵)) · (𝐵𝑛)))
3826oveq1d 7434 . . . . . . . . 9 (𝑚 = 𝑛 → ((𝐵𝑚) · (𝐴 / (1 − 𝐵))) = ((𝐵𝑛) · (𝐴 / (1 − 𝐵))))
39 eqid 2725 . . . . . . . . 9 (𝑚 ∈ ℕ ↦ ((𝐵𝑚) · (𝐴 / (1 − 𝐵)))) = (𝑚 ∈ ℕ ↦ ((𝐵𝑚) · (𝐴 / (1 − 𝐵))))
40 ovex 7452 . . . . . . . . 9 ((𝐵𝑛) · (𝐴 / (1 − 𝐵))) ∈ V
4138, 39, 40fvmpt 7004 . . . . . . . 8 (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((𝐵𝑚) · (𝐴 / (1 − 𝐵))))‘𝑛) = ((𝐵𝑛) · (𝐴 / (1 − 𝐵))))
4241adantl 480 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((𝐵𝑚) · (𝐴 / (1 − 𝐵))))‘𝑛) = ((𝐵𝑛) · (𝐴 / (1 − 𝐵))))
4330oveq2d 7435 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((𝐴 / (1 − 𝐵)) · ((𝑚 ∈ ℕ0 ↦ (𝐵𝑚))‘𝑛)) = ((𝐴 / (1 − 𝐵)) · (𝐵𝑛)))
4437, 42, 433eqtr4d 2775 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((𝐵𝑚) · (𝐴 / (1 − 𝐵))))‘𝑛) = ((𝐴 / (1 − 𝐵)) · ((𝑚 ∈ ℕ0 ↦ (𝐵𝑚))‘𝑛)))
451, 2, 10, 20, 23, 35, 44climmulc2 15617 . . . . 5 (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐵𝑚) · (𝐴 / (1 − 𝐵)))) ⇝ ((𝐴 / (1 − 𝐵)) · 0))
4620mul01d 11445 . . . . 5 (𝜑 → ((𝐴 / (1 − 𝐵)) · 0) = 0)
4745, 46breqtrd 5175 . . . 4 (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐵𝑚) · (𝐴 / (1 − 𝐵)))) ⇝ 0)
4833rpred 13051 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐵𝑛) ∈ ℝ)
4919adantr 479 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐴 / (1 − 𝐵)) ∈ ℝ)
5048, 49remulcld 11276 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((𝐵𝑛) · (𝐴 / (1 − 𝐵))) ∈ ℝ)
5150recnd 11274 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ((𝐵𝑛) · (𝐴 / (1 − 𝐵))) ∈ ℂ)
521, 2, 23, 42, 51clim0c 15487 . . . 4 (𝜑 → ((𝑚 ∈ ℕ ↦ ((𝐵𝑚) · (𝐴 / (1 − 𝐵)))) ⇝ 0 ↔ ∀𝑥 ∈ ℝ+𝑗 ∈ ℕ ∀𝑛 ∈ (ℤ𝑗)(abs‘((𝐵𝑛) · (𝐴 / (1 − 𝐵)))) < 𝑥))
5347, 52mpbid 231 . . 3 (𝜑 → ∀𝑥 ∈ ℝ+𝑗 ∈ ℕ ∀𝑛 ∈ (ℤ𝑗)(abs‘((𝐵𝑛) · (𝐴 / (1 − 𝐵)))) < 𝑥)
54 nnz 12612 . . . . . . . 8 (𝑗 ∈ ℕ → 𝑗 ∈ ℤ)
5554adantl 480 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℤ)
56 uzid 12870 . . . . . . 7 (𝑗 ∈ ℤ → 𝑗 ∈ (ℤ𝑗))
57 oveq2 7427 . . . . . . . . . 10 (𝑛 = 𝑗 → (𝐵𝑛) = (𝐵𝑗))
5857fvoveq1d 7441 . . . . . . . . 9 (𝑛 = 𝑗 → (abs‘((𝐵𝑛) · (𝐴 / (1 − 𝐵)))) = (abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))))
5958breq1d 5159 . . . . . . . 8 (𝑛 = 𝑗 → ((abs‘((𝐵𝑛) · (𝐴 / (1 − 𝐵)))) < 𝑥 ↔ (abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))) < 𝑥))
6059rspcv 3602 . . . . . . 7 (𝑗 ∈ (ℤ𝑗) → (∀𝑛 ∈ (ℤ𝑗)(abs‘((𝐵𝑛) · (𝐴 / (1 − 𝐵)))) < 𝑥 → (abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))) < 𝑥))
6155, 56, 603syl 18 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (∀𝑛 ∈ (ℤ𝑗)(abs‘((𝐵𝑛) · (𝐴 / (1 − 𝐵)))) < 𝑥 → (abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))) < 𝑥))
62 lmclim2.2 . . . . . . . . . . . . 13 (𝜑𝐷 ∈ (Met‘𝑋))
6362adantr 479 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → 𝐷 ∈ (Met‘𝑋))
64 lmclim2.3 . . . . . . . . . . . . 13 (𝜑𝐹:ℕ⟶𝑋)
65 simpl 481 . . . . . . . . . . . . 13 ((𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗)) → 𝑗 ∈ ℕ)
66 ffvelcdm 7090 . . . . . . . . . . . . 13 ((𝐹:ℕ⟶𝑋𝑗 ∈ ℕ) → (𝐹𝑗) ∈ 𝑋)
6764, 65, 66syl2an 594 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → (𝐹𝑗) ∈ 𝑋)
68 eluznn 12935 . . . . . . . . . . . . 13 ((𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗)) → 𝑛 ∈ ℕ)
69 ffvelcdm 7090 . . . . . . . . . . . . 13 ((𝐹:ℕ⟶𝑋𝑛 ∈ ℕ) → (𝐹𝑛) ∈ 𝑋)
7064, 68, 69syl2an 594 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → (𝐹𝑛) ∈ 𝑋)
71 metcl 24282 . . . . . . . . . . . 12 ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹𝑗) ∈ 𝑋 ∧ (𝐹𝑛) ∈ 𝑋) → ((𝐹𝑗)𝐷(𝐹𝑛)) ∈ ℝ)
7263, 67, 70, 71syl3anc 1368 . . . . . . . . . . 11 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → ((𝐹𝑗)𝐷(𝐹𝑛)) ∈ ℝ)
73 eqid 2725 . . . . . . . . . . . . 13 (ℤ𝑗) = (ℤ𝑗)
74 nnnn0 12512 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ → 𝑗 ∈ ℕ0)
7574ad2antrl 726 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → 𝑗 ∈ ℕ0)
7675nn0zd 12617 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → 𝑗 ∈ ℤ)
77 oveq2 7427 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑘 → (𝐵𝑚) = (𝐵𝑘))
7877oveq2d 7435 . . . . . . . . . . . . . . 15 (𝑚 = 𝑘 → (𝐴 · (𝐵𝑚)) = (𝐴 · (𝐵𝑘)))
79 eqid 2725 . . . . . . . . . . . . . . 15 (𝑚 ∈ (ℤ𝑗) ↦ (𝐴 · (𝐵𝑚))) = (𝑚 ∈ (ℤ𝑗) ↦ (𝐴 · (𝐵𝑚)))
80 ovex 7452 . . . . . . . . . . . . . . 15 (𝐴 · (𝐵𝑘)) ∈ V
8178, 79, 80fvmpt 7004 . . . . . . . . . . . . . 14 (𝑘 ∈ (ℤ𝑗) → ((𝑚 ∈ (ℤ𝑗) ↦ (𝐴 · (𝐵𝑚)))‘𝑘) = (𝐴 · (𝐵𝑘)))
8281adantl 480 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → ((𝑚 ∈ (ℤ𝑗) ↦ (𝐴 · (𝐵𝑚)))‘𝑘) = (𝐴 · (𝐵𝑘)))
8311ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝐴 ∈ ℝ)
845ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝐵 ∈ ℝ)
85 eluznn0 12934 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ ℕ0𝑘 ∈ (ℤ𝑗)) → 𝑘 ∈ ℕ0)
8675, 85sylan 578 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑘 ∈ ℕ0)
8784, 86reexpcld 14163 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐵𝑘) ∈ ℝ)
8883, 87remulcld 11276 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐴 · (𝐵𝑘)) ∈ ℝ)
8988recnd 11274 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐴 · (𝐵𝑘)) ∈ ℂ)
9011recnd 11274 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ ℂ)
9190adantr 479 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → 𝐴 ∈ ℂ)
924adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → 𝐵 ∈ ℂ)
939adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → (abs‘𝐵) < 1)
94 eqid 2725 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ (ℤ𝑗) ↦ (𝐵𝑚)) = (𝑚 ∈ (ℤ𝑗) ↦ (𝐵𝑚))
95 ovex 7452 . . . . . . . . . . . . . . . . . 18 (𝐵𝑘) ∈ V
9677, 94, 95fvmpt 7004 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (ℤ𝑗) → ((𝑚 ∈ (ℤ𝑗) ↦ (𝐵𝑚))‘𝑘) = (𝐵𝑘))
9796adantl 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → ((𝑚 ∈ (ℤ𝑗) ↦ (𝐵𝑚))‘𝑘) = (𝐵𝑘))
9892, 93, 75, 97geolim2 15853 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → seq𝑗( + , (𝑚 ∈ (ℤ𝑗) ↦ (𝐵𝑚))) ⇝ ((𝐵𝑗) / (1 − 𝐵)))
9987recnd 11274 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐵𝑘) ∈ ℂ)
10097, 99eqeltrd 2825 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → ((𝑚 ∈ (ℤ𝑗) ↦ (𝐵𝑚))‘𝑘) ∈ ℂ)
10197oveq2d 7435 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐴 · ((𝑚 ∈ (ℤ𝑗) ↦ (𝐵𝑚))‘𝑘)) = (𝐴 · (𝐵𝑘)))
10282, 101eqtr4d 2768 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → ((𝑚 ∈ (ℤ𝑗) ↦ (𝐴 · (𝐵𝑚)))‘𝑘) = (𝐴 · ((𝑚 ∈ (ℤ𝑗) ↦ (𝐵𝑚))‘𝑘)))
10373, 76, 91, 98, 100, 102isermulc2 15640 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → seq𝑗( + , (𝑚 ∈ (ℤ𝑗) ↦ (𝐴 · (𝐵𝑚)))) ⇝ (𝐴 · ((𝐵𝑗) / (1 − 𝐵))))
1043adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → 𝐵 ∈ ℝ+)
105104, 76rpexpcld 14245 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → (𝐵𝑗) ∈ ℝ+)
106105rpcnd 13053 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → (𝐵𝑗) ∈ ℂ)
10714recnd 11274 . . . . . . . . . . . . . . . 16 (𝜑 → (1 − 𝐵) ∈ ℂ)
108107adantr 479 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → (1 − 𝐵) ∈ ℂ)
10918rpne0d 13056 . . . . . . . . . . . . . . . 16 (𝜑 → (1 − 𝐵) ≠ 0)
110109adantr 479 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → (1 − 𝐵) ≠ 0)
11191, 106, 108, 110div12d 12059 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → (𝐴 · ((𝐵𝑗) / (1 − 𝐵))) = ((𝐵𝑗) · (𝐴 / (1 − 𝐵))))
112103, 111breqtrd 5175 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → seq𝑗( + , (𝑚 ∈ (ℤ𝑗) ↦ (𝐴 · (𝐵𝑚)))) ⇝ ((𝐵𝑗) · (𝐴 / (1 − 𝐵))))
11373, 76, 82, 89, 112isumclim 15739 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → Σ𝑘 ∈ (ℤ𝑗)(𝐴 · (𝐵𝑘)) = ((𝐵𝑗) · (𝐴 / (1 − 𝐵))))
114 seqex 14004 . . . . . . . . . . . . . . 15 seq𝑗( + , (𝑚 ∈ (ℤ𝑗) ↦ (𝐴 · (𝐵𝑚)))) ∈ V
115 ovex 7452 . . . . . . . . . . . . . . 15 (𝐴 · ((𝐵𝑗) / (1 − 𝐵))) ∈ V
116114, 115breldm 5911 . . . . . . . . . . . . . 14 (seq𝑗( + , (𝑚 ∈ (ℤ𝑗) ↦ (𝐴 · (𝐵𝑚)))) ⇝ (𝐴 · ((𝐵𝑗) / (1 − 𝐵))) → seq𝑗( + , (𝑚 ∈ (ℤ𝑗) ↦ (𝐴 · (𝐵𝑚)))) ∈ dom ⇝ )
117103, 116syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → seq𝑗( + , (𝑚 ∈ (ℤ𝑗) ↦ (𝐴 · (𝐵𝑚)))) ∈ dom ⇝ )
11873, 76, 82, 88, 117isumrecl 15747 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → Σ𝑘 ∈ (ℤ𝑗)(𝐴 · (𝐵𝑘)) ∈ ℝ)
119113, 118eqeltrrd 2826 . . . . . . . . . . 11 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → ((𝐵𝑗) · (𝐴 / (1 − 𝐵))) ∈ ℝ)
120119recnd 11274 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → ((𝐵𝑗) · (𝐴 / (1 − 𝐵))) ∈ ℂ)
121120abscld 15419 . . . . . . . . . . 11 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → (abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))) ∈ ℝ)
122 fzfid 13974 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → (𝑗...(𝑛 − 1)) ∈ Fin)
123 simpll 765 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑗...(𝑛 − 1))) → 𝜑)
124 elfzuz 13532 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (𝑗...(𝑛 − 1)) → 𝑘 ∈ (ℤ𝑗))
125 simprl 769 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → 𝑗 ∈ ℕ)
126 eluznn 12935 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑘 ∈ ℕ)
127125, 126sylan 578 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑘 ∈ ℕ)
128124, 127sylan2 591 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑗...(𝑛 − 1))) → 𝑘 ∈ ℕ)
12962adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → 𝐷 ∈ (Met‘𝑋))
13064ffvelcdmda 7093 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) ∈ 𝑋)
131 peano2nn 12257 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
132 ffvelcdm 7090 . . . . . . . . . . . . . . . . 17 ((𝐹:ℕ⟶𝑋 ∧ (𝑘 + 1) ∈ ℕ) → (𝐹‘(𝑘 + 1)) ∈ 𝑋)
13364, 131, 132syl2an 594 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ∈ 𝑋)
134 metcl 24282 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹𝑘) ∈ 𝑋 ∧ (𝐹‘(𝑘 + 1)) ∈ 𝑋) → ((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ∈ ℝ)
135129, 130, 133, 134syl3anc 1368 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ℕ) → ((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ∈ ℝ)
136123, 128, 135syl2anc 582 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑗...(𝑛 − 1))) → ((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ∈ ℝ)
137122, 136fsumrecl 15716 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → Σ𝑘 ∈ (𝑗...(𝑛 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ∈ ℝ)
138 simprr 771 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → 𝑛 ∈ (ℤ𝑗))
139 elfzuz 13532 . . . . . . . . . . . . . . 15 (𝑘 ∈ (𝑗...𝑛) → 𝑘 ∈ (ℤ𝑗))
140 simpll 765 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝜑)
141140, 127, 130syl2anc 582 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) ∈ 𝑋)
142139, 141sylan2 591 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑗...𝑛)) → (𝐹𝑘) ∈ 𝑋)
14363, 138, 142mettrifi 37361 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → ((𝐹𝑗)𝐷(𝐹𝑛)) ≤ Σ𝑘 ∈ (𝑗...(𝑛 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))
144124, 88sylan2 591 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑗...(𝑛 − 1))) → (𝐴 · (𝐵𝑘)) ∈ ℝ)
145122, 144fsumrecl 15716 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → Σ𝑘 ∈ (𝑗...(𝑛 − 1))(𝐴 · (𝐵𝑘)) ∈ ℝ)
146 geomcau.7 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → ((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (𝐵𝑘)))
147123, 128, 146syl2anc 582 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑗...(𝑛 − 1))) → ((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (𝐵𝑘)))
148122, 136, 144, 147fsumle 15781 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → Σ𝑘 ∈ (𝑗...(𝑛 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ≤ Σ𝑘 ∈ (𝑗...(𝑛 − 1))(𝐴 · (𝐵𝑘)))
149 fzssuz 13577 . . . . . . . . . . . . . . . 16 (𝑗...(𝑛 − 1)) ⊆ (ℤ𝑗)
150149a1i 11 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → (𝑗...(𝑛 − 1)) ⊆ (ℤ𝑗))
151 0red 11249 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → 0 ∈ ℝ)
152 nnz 12612 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
153 rpexpcl 14081 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ∈ ℝ+𝑘 ∈ ℤ) → (𝐵𝑘) ∈ ℝ+)
1543, 152, 153syl2an 594 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → (𝐵𝑘) ∈ ℝ+)
155135, 154rerpdivcld 13082 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) / (𝐵𝑘)) ∈ ℝ)
15611adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → 𝐴 ∈ ℝ)
157 metge0 24295 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹𝑘) ∈ 𝑋 ∧ (𝐹‘(𝑘 + 1)) ∈ 𝑋) → 0 ≤ ((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))
158129, 130, 133, 157syl3anc 1368 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → 0 ≤ ((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))))
159135, 154, 158divge0d 13091 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → 0 ≤ (((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) / (𝐵𝑘)))
160135, 156, 154ledivmul2d 13105 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ℕ) → ((((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) / (𝐵𝑘)) ≤ 𝐴 ↔ ((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (𝐵𝑘))))
161146, 160mpbird 256 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ℕ) → (((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) / (𝐵𝑘)) ≤ 𝐴)
162151, 155, 156, 159, 161letrd 11403 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → 0 ≤ 𝐴)
163140, 127, 162syl2anc 582 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → 0 ≤ 𝐴)
164140, 127, 154syl2anc 582 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐵𝑘) ∈ ℝ+)
165164rpge0d 13055 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → 0 ≤ (𝐵𝑘))
16683, 87, 163, 165mulge0d 11823 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (ℤ𝑗)) → 0 ≤ (𝐴 · (𝐵𝑘)))
16773, 76, 122, 150, 82, 88, 166, 117isumless 15827 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → Σ𝑘 ∈ (𝑗...(𝑛 − 1))(𝐴 · (𝐵𝑘)) ≤ Σ𝑘 ∈ (ℤ𝑗)(𝐴 · (𝐵𝑘)))
168137, 145, 118, 148, 167letrd 11403 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → Σ𝑘 ∈ (𝑗...(𝑛 − 1))((𝐹𝑘)𝐷(𝐹‘(𝑘 + 1))) ≤ Σ𝑘 ∈ (ℤ𝑗)(𝐴 · (𝐵𝑘)))
16972, 137, 118, 143, 168letrd 11403 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → ((𝐹𝑗)𝐷(𝐹𝑛)) ≤ Σ𝑘 ∈ (ℤ𝑗)(𝐴 · (𝐵𝑘)))
170169, 113breqtrd 5175 . . . . . . . . . . 11 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → ((𝐹𝑗)𝐷(𝐹𝑛)) ≤ ((𝐵𝑗) · (𝐴 / (1 − 𝐵))))
171119leabsd 15397 . . . . . . . . . . 11 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → ((𝐵𝑗) · (𝐴 / (1 − 𝐵))) ≤ (abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))))
17272, 119, 121, 170, 171letrd 11403 . . . . . . . . . 10 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → ((𝐹𝑗)𝐷(𝐹𝑛)) ≤ (abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))))
173172adantlr 713 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → ((𝐹𝑗)𝐷(𝐹𝑛)) ≤ (abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))))
17472adantlr 713 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → ((𝐹𝑗)𝐷(𝐹𝑛)) ∈ ℝ)
175121adantlr 713 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → (abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))) ∈ ℝ)
176 rpre 13017 . . . . . . . . . . 11 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
177176ad2antlr 725 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → 𝑥 ∈ ℝ)
178 lelttr 11336 . . . . . . . . . 10 ((((𝐹𝑗)𝐷(𝐹𝑛)) ∈ ℝ ∧ (abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((((𝐹𝑗)𝐷(𝐹𝑛)) ≤ (abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))) ∧ (abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))) < 𝑥) → ((𝐹𝑗)𝐷(𝐹𝑛)) < 𝑥))
179174, 175, 177, 178syl3anc 1368 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → ((((𝐹𝑗)𝐷(𝐹𝑛)) ≤ (abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))) ∧ (abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))) < 𝑥) → ((𝐹𝑗)𝐷(𝐹𝑛)) < 𝑥))
180173, 179mpand 693 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑗))) → ((abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))) < 𝑥 → ((𝐹𝑗)𝐷(𝐹𝑛)) < 𝑥))
181180anassrs 466 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (ℤ𝑗)) → ((abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))) < 𝑥 → ((𝐹𝑗)𝐷(𝐹𝑛)) < 𝑥))
182181ralrimdva 3143 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → ((abs‘((𝐵𝑗) · (𝐴 / (1 − 𝐵)))) < 𝑥 → ∀𝑛 ∈ (ℤ𝑗)((𝐹𝑗)𝐷(𝐹𝑛)) < 𝑥))
18361, 182syld 47 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (∀𝑛 ∈ (ℤ𝑗)(abs‘((𝐵𝑛) · (𝐴 / (1 − 𝐵)))) < 𝑥 → ∀𝑛 ∈ (ℤ𝑗)((𝐹𝑗)𝐷(𝐹𝑛)) < 𝑥))
184183reximdva 3157 . . . 4 ((𝜑𝑥 ∈ ℝ+) → (∃𝑗 ∈ ℕ ∀𝑛 ∈ (ℤ𝑗)(abs‘((𝐵𝑛) · (𝐴 / (1 − 𝐵)))) < 𝑥 → ∃𝑗 ∈ ℕ ∀𝑛 ∈ (ℤ𝑗)((𝐹𝑗)𝐷(𝐹𝑛)) < 𝑥))
185184ralimdva 3156 . . 3 (𝜑 → (∀𝑥 ∈ ℝ+𝑗 ∈ ℕ ∀𝑛 ∈ (ℤ𝑗)(abs‘((𝐵𝑛) · (𝐴 / (1 − 𝐵)))) < 𝑥 → ∀𝑥 ∈ ℝ+𝑗 ∈ ℕ ∀𝑛 ∈ (ℤ𝑗)((𝐹𝑗)𝐷(𝐹𝑛)) < 𝑥))
18653, 185mpd 15 . 2 (𝜑 → ∀𝑥 ∈ ℝ+𝑗 ∈ ℕ ∀𝑛 ∈ (ℤ𝑗)((𝐹𝑗)𝐷(𝐹𝑛)) < 𝑥)
187 metxmet 24284 . . . 4 (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
18862, 187syl 17 . . 3 (𝜑𝐷 ∈ (∞Met‘𝑋))
189 eqidd 2726 . . 3 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) = (𝐹𝑛))
190 eqidd 2726 . . 3 ((𝜑𝑗 ∈ ℕ) → (𝐹𝑗) = (𝐹𝑗))
1911, 188, 2, 189, 190, 64iscauf 25252 . 2 (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ ∀𝑥 ∈ ℝ+𝑗 ∈ ℕ ∀𝑛 ∈ (ℤ𝑗)((𝐹𝑗)𝐷(𝐹𝑛)) < 𝑥))
192186, 191mpbird 256 1 (𝜑𝐹 ∈ (Cau‘𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1533  wcel 2098  wne 2929  wral 3050  wrex 3059  Vcvv 3461  wss 3944   class class class wbr 5149  cmpt 5232  dom cdm 5678  wf 6545  cfv 6549  (class class class)co 7419  cc 11138  cr 11139  0cc0 11140  1c1 11141   + caddc 11143   · cmul 11145   < clt 11280  cle 11281  cmin 11476   / cdiv 11903  cn 12245  0cn0 12505  cz 12591  cuz 12855  +crp 13009  ...cfz 13519  seqcseq 14002  cexp 14062  abscabs 15217  cli 15464  Σcsu 15668  ∞Metcxmet 21281  Metcmet 21282  Cauccau 25225
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-inf2 9666  ax-cnex 11196  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216  ax-pre-mulgt0 11217  ax-pre-sup 11218
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-int 4951  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-isom 6558  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7872  df-1st 7994  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-er 8725  df-map 8847  df-pm 8848  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-sup 9467  df-inf 9468  df-oi 9535  df-card 9964  df-pnf 11282  df-mnf 11283  df-xr 11284  df-ltxr 11285  df-le 11286  df-sub 11478  df-neg 11479  df-div 11904  df-nn 12246  df-2 12308  df-3 12309  df-n0 12506  df-z 12592  df-uz 12856  df-rp 13010  df-xneg 13127  df-xadd 13128  df-xmul 13129  df-ico 13365  df-fz 13520  df-fzo 13663  df-fl 13793  df-seq 14003  df-exp 14063  df-hash 14326  df-cj 15082  df-re 15083  df-im 15084  df-sqrt 15218  df-abs 15219  df-clim 15468  df-rlim 15469  df-sum 15669  df-psmet 21288  df-xmet 21289  df-met 21290  df-bl 21291  df-cau 25228
This theorem is referenced by:  bfplem1  37426
  Copyright terms: Public domain W3C validator