MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cvgcmp Structured version   Visualization version   GIF version

Theorem cvgcmp 14755
Description: A comparison test for convergence of a real infinite series. Exercise 3 of [Gleason] p. 182. (Contributed by NM, 1-May-2005.) (Revised by Mario Carneiro, 24-Mar-2014.)
Hypotheses
Ref Expression
cvgcmp.1 𝑍 = (ℤ𝑀)
cvgcmp.2 (𝜑𝑁𝑍)
cvgcmp.3 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)
cvgcmp.4 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℝ)
cvgcmp.5 (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )
cvgcmp.6 ((𝜑𝑘 ∈ (ℤ𝑁)) → 0 ≤ (𝐺𝑘))
cvgcmp.7 ((𝜑𝑘 ∈ (ℤ𝑁)) → (𝐺𝑘) ≤ (𝐹𝑘))
Assertion
Ref Expression
cvgcmp (𝜑 → seq𝑀( + , 𝐺) ∈ dom ⇝ )
Distinct variable groups:   𝑘,𝐹   𝑘,𝐺   𝜑,𝑘   𝑘,𝑀   𝑘,𝑁   𝑘,𝑍

Proof of Theorem cvgcmp
Dummy variables 𝑛 𝑚 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cvgcmp.1 . 2 𝑍 = (ℤ𝑀)
2 seqex 13010 . . 3 seq𝑀( + , 𝐺) ∈ V
32a1i 11 . 2 (𝜑 → seq𝑀( + , 𝐺) ∈ V)
4 cvgcmp.2 . . . . . . . 8 (𝜑𝑁𝑍)
54, 1syl6eleq 2860 . . . . . . 7 (𝜑𝑁 ∈ (ℤ𝑀))
6 eluzel2 11893 . . . . . . 7 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
75, 6syl 17 . . . . . 6 (𝜑𝑀 ∈ ℤ)
8 cvgcmp.5 . . . . . 6 (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )
91climcau 14609 . . . . . 6 ((𝑀 ∈ ℤ ∧ seq𝑀( + , 𝐹) ∈ dom ⇝ ) → ∀𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ (ℤ𝑚)(abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚))) < 𝑥)
107, 8, 9syl2anc 573 . . . . 5 (𝜑 → ∀𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ (ℤ𝑚)(abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚))) < 𝑥)
11 cvgcmp.3 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)
121, 7, 11serfre 13037 . . . . . . . . . 10 (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ)
1312ffvelrnda 6502 . . . . . . . . 9 ((𝜑𝑛𝑍) → (seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ)
1413recnd 10270 . . . . . . . 8 ((𝜑𝑛𝑍) → (seq𝑀( + , 𝐹)‘𝑛) ∈ ℂ)
1514ralrimiva 3115 . . . . . . 7 (𝜑 → ∀𝑛𝑍 (seq𝑀( + , 𝐹)‘𝑛) ∈ ℂ)
161r19.29uz 14298 . . . . . . . 8 ((∀𝑛𝑍 (seq𝑀( + , 𝐹)‘𝑛) ∈ ℂ ∧ ∃𝑚𝑍𝑛 ∈ (ℤ𝑚)(abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚))) < 𝑥) → ∃𝑚𝑍𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚))) < 𝑥))
1716ex 397 . . . . . . 7 (∀𝑛𝑍 (seq𝑀( + , 𝐹)‘𝑛) ∈ ℂ → (∃𝑚𝑍𝑛 ∈ (ℤ𝑚)(abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚))) < 𝑥 → ∃𝑚𝑍𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚))) < 𝑥)))
1815, 17syl 17 . . . . . 6 (𝜑 → (∃𝑚𝑍𝑛 ∈ (ℤ𝑚)(abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚))) < 𝑥 → ∃𝑚𝑍𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚))) < 𝑥)))
1918ralimdv 3112 . . . . 5 (𝜑 → (∀𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ (ℤ𝑚)(abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚))) < 𝑥 → ∀𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚))) < 𝑥)))
2010, 19mpd 15 . . . 4 (𝜑 → ∀𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚))) < 𝑥))
211uztrn2 11906 . . . . . . . . . . 11 ((𝑁𝑍𝑛 ∈ (ℤ𝑁)) → 𝑛𝑍)
224, 21sylan 569 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → 𝑛𝑍)
23 cvgcmp.4 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℝ)
241, 7, 23serfre 13037 . . . . . . . . . . . 12 (𝜑 → seq𝑀( + , 𝐺):𝑍⟶ℝ)
2524ffvelrnda 6502 . . . . . . . . . . 11 ((𝜑𝑛𝑍) → (seq𝑀( + , 𝐺)‘𝑛) ∈ ℝ)
2625recnd 10270 . . . . . . . . . 10 ((𝜑𝑛𝑍) → (seq𝑀( + , 𝐺)‘𝑛) ∈ ℂ)
2722, 26syldan 579 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝑁)) → (seq𝑀( + , 𝐺)‘𝑛) ∈ ℂ)
2827ralrimiva 3115 . . . . . . . 8 (𝜑 → ∀𝑛 ∈ (ℤ𝑁)(seq𝑀( + , 𝐺)‘𝑛) ∈ ℂ)
2928adantr 466 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → ∀𝑛 ∈ (ℤ𝑁)(seq𝑀( + , 𝐺)‘𝑛) ∈ ℂ)
30 simpll 750 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → 𝜑)
3130, 12syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → seq𝑀( + , 𝐹):𝑍⟶ℝ)
3230, 4syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → 𝑁𝑍)
33 simprl 754 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → 𝑚 ∈ (ℤ𝑁))
341uztrn2 11906 . . . . . . . . . . . . . . . 16 ((𝑁𝑍𝑚 ∈ (ℤ𝑁)) → 𝑚𝑍)
3532, 33, 34syl2anc 573 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → 𝑚𝑍)
3631, 35ffvelrnd 6503 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → (seq𝑀( + , 𝐹)‘𝑚) ∈ ℝ)
37 eqid 2771 . . . . . . . . . . . . . . . . . 18 (ℤ𝑁) = (ℤ𝑁)
3837uztrn2 11906 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚)) → 𝑛 ∈ (ℤ𝑁))
3938adantl 467 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → 𝑛 ∈ (ℤ𝑁))
4032, 39, 21syl2anc 573 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → 𝑛𝑍)
4130, 40, 13syl2anc 573 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → (seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ)
4230, 40, 25syl2anc 573 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → (seq𝑀( + , 𝐺)‘𝑛) ∈ ℝ)
4330, 24syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → seq𝑀( + , 𝐺):𝑍⟶ℝ)
4443, 35ffvelrnd 6503 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → (seq𝑀( + , 𝐺)‘𝑚) ∈ ℝ)
4542, 44resubcld 10660 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → ((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚)) ∈ ℝ)
4635, 1syl6eleq 2860 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → 𝑚 ∈ (ℤ𝑀))
47 simprr 756 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → 𝑛 ∈ (ℤ𝑚))
48 elfzuz 12545 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ (𝑀...𝑛) → 𝑘 ∈ (ℤ𝑀))
4948, 1syl6eleqr 2861 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (𝑀...𝑛) → 𝑘𝑍)
50 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 = 𝑘 → (𝐹𝑚) = (𝐹𝑘))
51 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 = 𝑘 → (𝐺𝑚) = (𝐺𝑘))
5250, 51oveq12d 6811 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑘 → ((𝐹𝑚) − (𝐺𝑚)) = ((𝐹𝑘) − (𝐺𝑘)))
53 eqid 2771 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚𝑍 ↦ ((𝐹𝑚) − (𝐺𝑚))) = (𝑚𝑍 ↦ ((𝐹𝑚) − (𝐺𝑚)))
54 ovex 6823 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑘) − (𝐺𝑘)) ∈ V
5552, 53, 54fvmpt 6424 . . . . . . . . . . . . . . . . . . . . 21 (𝑘𝑍 → ((𝑚𝑍 ↦ ((𝐹𝑚) − (𝐺𝑚)))‘𝑘) = ((𝐹𝑘) − (𝐺𝑘)))
5655adantl 467 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝑍) → ((𝑚𝑍 ↦ ((𝐹𝑚) − (𝐺𝑚)))‘𝑘) = ((𝐹𝑘) − (𝐺𝑘)))
5711, 23resubcld 10660 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘𝑍) → ((𝐹𝑘) − (𝐺𝑘)) ∈ ℝ)
5856, 57eqeltrd 2850 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑍) → ((𝑚𝑍 ↦ ((𝐹𝑚) − (𝐺𝑚)))‘𝑘) ∈ ℝ)
5930, 49, 58syl2an 583 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) ∧ 𝑘 ∈ (𝑀...𝑛)) → ((𝑚𝑍 ↦ ((𝐹𝑚) − (𝐺𝑚)))‘𝑘) ∈ ℝ)
60 elfzuz 12545 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ((𝑚 + 1)...𝑛) → 𝑘 ∈ (ℤ‘(𝑚 + 1)))
61 peano2uz 11943 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ (ℤ𝑁) → (𝑚 + 1) ∈ (ℤ𝑁))
6233, 61syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → (𝑚 + 1) ∈ (ℤ𝑁))
6337uztrn2 11906 . . . . . . . . . . . . . . . . . . . . 21 (((𝑚 + 1) ∈ (ℤ𝑁) ∧ 𝑘 ∈ (ℤ‘(𝑚 + 1))) → 𝑘 ∈ (ℤ𝑁))
6462, 63sylan 569 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) ∧ 𝑘 ∈ (ℤ‘(𝑚 + 1))) → 𝑘 ∈ (ℤ𝑁))
65 cvgcmp.7 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ (ℤ𝑁)) → (𝐺𝑘) ≤ (𝐹𝑘))
661uztrn2 11906 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑁𝑍𝑘 ∈ (ℤ𝑁)) → 𝑘𝑍)
674, 66sylan 569 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ (ℤ𝑁)) → 𝑘𝑍)
6811, 23subge0d 10819 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘𝑍) → (0 ≤ ((𝐹𝑘) − (𝐺𝑘)) ↔ (𝐺𝑘) ≤ (𝐹𝑘)))
6967, 68syldan 579 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ (ℤ𝑁)) → (0 ≤ ((𝐹𝑘) − (𝐺𝑘)) ↔ (𝐺𝑘) ≤ (𝐹𝑘)))
7065, 69mpbird 247 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (ℤ𝑁)) → 0 ≤ ((𝐹𝑘) − (𝐺𝑘)))
7167, 55syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (ℤ𝑁)) → ((𝑚𝑍 ↦ ((𝐹𝑚) − (𝐺𝑚)))‘𝑘) = ((𝐹𝑘) − (𝐺𝑘)))
7270, 71breqtrrd 4814 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (ℤ𝑁)) → 0 ≤ ((𝑚𝑍 ↦ ((𝐹𝑚) − (𝐺𝑚)))‘𝑘))
7330, 72sylan 569 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) ∧ 𝑘 ∈ (ℤ𝑁)) → 0 ≤ ((𝑚𝑍 ↦ ((𝐹𝑚) − (𝐺𝑚)))‘𝑘))
7464, 73syldan 579 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) ∧ 𝑘 ∈ (ℤ‘(𝑚 + 1))) → 0 ≤ ((𝑚𝑍 ↦ ((𝐹𝑚) − (𝐺𝑚)))‘𝑘))
7560, 74sylan2 580 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) ∧ 𝑘 ∈ ((𝑚 + 1)...𝑛)) → 0 ≤ ((𝑚𝑍 ↦ ((𝐹𝑚) − (𝐺𝑚)))‘𝑘))
7646, 47, 59, 75sermono 13040 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → (seq𝑀( + , (𝑚𝑍 ↦ ((𝐹𝑚) − (𝐺𝑚))))‘𝑚) ≤ (seq𝑀( + , (𝑚𝑍 ↦ ((𝐹𝑚) − (𝐺𝑚))))‘𝑛))
77 elfzuz 12545 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ (𝑀...𝑚) → 𝑘 ∈ (ℤ𝑀))
7877, 1syl6eleqr 2861 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (𝑀...𝑚) → 𝑘𝑍)
7911recnd 10270 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)
8030, 78, 79syl2an 583 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) ∧ 𝑘 ∈ (𝑀...𝑚)) → (𝐹𝑘) ∈ ℂ)
8123recnd 10270 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℂ)
8230, 78, 81syl2an 583 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) ∧ 𝑘 ∈ (𝑀...𝑚)) → (𝐺𝑘) ∈ ℂ)
8330, 78, 56syl2an 583 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) ∧ 𝑘 ∈ (𝑀...𝑚)) → ((𝑚𝑍 ↦ ((𝐹𝑚) − (𝐺𝑚)))‘𝑘) = ((𝐹𝑘) − (𝐺𝑘)))
8446, 80, 82, 83sersub 13051 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → (seq𝑀( + , (𝑚𝑍 ↦ ((𝐹𝑚) − (𝐺𝑚))))‘𝑚) = ((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐺)‘𝑚)))
8540, 1syl6eleq 2860 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → 𝑛 ∈ (ℤ𝑀))
8630, 49, 79syl2an 583 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) ∧ 𝑘 ∈ (𝑀...𝑛)) → (𝐹𝑘) ∈ ℂ)
8730, 49, 81syl2an 583 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) ∧ 𝑘 ∈ (𝑀...𝑛)) → (𝐺𝑘) ∈ ℂ)
8830, 49, 56syl2an 583 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) ∧ 𝑘 ∈ (𝑀...𝑛)) → ((𝑚𝑍 ↦ ((𝐹𝑚) − (𝐺𝑚)))‘𝑘) = ((𝐹𝑘) − (𝐺𝑘)))
8985, 86, 87, 88sersub 13051 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → (seq𝑀( + , (𝑚𝑍 ↦ ((𝐹𝑚) − (𝐺𝑚))))‘𝑛) = ((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑛)))
9076, 84, 893brtr3d 4817 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → ((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐺)‘𝑚)) ≤ ((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑛)))
9141, 42resubcld 10660 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → ((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑛)) ∈ ℝ)
9236, 44, 91lesubaddd 10826 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → (((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐺)‘𝑚)) ≤ ((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑛)) ↔ (seq𝑀( + , 𝐹)‘𝑚) ≤ (((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑛)) + (seq𝑀( + , 𝐺)‘𝑚))))
9390, 92mpbid 222 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → (seq𝑀( + , 𝐹)‘𝑚) ≤ (((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑛)) + (seq𝑀( + , 𝐺)‘𝑚)))
9441recnd 10270 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → (seq𝑀( + , 𝐹)‘𝑛) ∈ ℂ)
9542recnd 10270 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → (seq𝑀( + , 𝐺)‘𝑛) ∈ ℂ)
9644recnd 10270 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → (seq𝑀( + , 𝐺)‘𝑚) ∈ ℂ)
9794, 95, 96subsubd 10622 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → ((seq𝑀( + , 𝐹)‘𝑛) − ((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) = (((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑛)) + (seq𝑀( + , 𝐺)‘𝑚)))
9893, 97breqtrrd 4814 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → (seq𝑀( + , 𝐹)‘𝑚) ≤ ((seq𝑀( + , 𝐹)‘𝑛) − ((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))))
9936, 41, 45, 98lesubd 10833 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → ((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚)) ≤ ((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚)))
10041, 36resubcld 10660 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → ((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚)) ∈ ℝ)
101 rpre 12042 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
102101ad2antlr 706 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → 𝑥 ∈ ℝ)
103 lelttr 10330 . . . . . . . . . . . . . 14 ((((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚)) ∈ ℝ ∧ ((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚)) ≤ ((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚)) ∧ ((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚)) < 𝑥) → ((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚)) < 𝑥))
10445, 100, 102, 103syl3anc 1476 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → ((((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚)) ≤ ((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚)) ∧ ((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚)) < 𝑥) → ((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚)) < 𝑥))
10599, 104mpand 675 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → (((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚)) < 𝑥 → ((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚)) < 𝑥))
10630, 49, 11syl2an 583 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) ∧ 𝑘 ∈ (𝑀...𝑛)) → (𝐹𝑘) ∈ ℝ)
10760, 64sylan2 580 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) ∧ 𝑘 ∈ ((𝑚 + 1)...𝑛)) → 𝑘 ∈ (ℤ𝑁))
108 0red 10243 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (ℤ𝑁)) → 0 ∈ ℝ)
10967, 23syldan 579 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (ℤ𝑁)) → (𝐺𝑘) ∈ ℝ)
11067, 11syldan 579 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (ℤ𝑁)) → (𝐹𝑘) ∈ ℝ)
111 cvgcmp.6 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (ℤ𝑁)) → 0 ≤ (𝐺𝑘))
112108, 109, 110, 111, 65letrd 10396 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (ℤ𝑁)) → 0 ≤ (𝐹𝑘))
11330, 112sylan 569 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) ∧ 𝑘 ∈ (ℤ𝑁)) → 0 ≤ (𝐹𝑘))
114107, 113syldan 579 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) ∧ 𝑘 ∈ ((𝑚 + 1)...𝑛)) → 0 ≤ (𝐹𝑘))
11546, 47, 106, 114sermono 13040 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → (seq𝑀( + , 𝐹)‘𝑚) ≤ (seq𝑀( + , 𝐹)‘𝑛))
11636, 41, 115abssubge0d 14378 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚))) = ((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚)))
117116breq1d 4796 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → ((abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚))) < 𝑥 ↔ ((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚)) < 𝑥))
11830, 49, 23syl2an 583 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) ∧ 𝑘 ∈ (𝑀...𝑛)) → (𝐺𝑘) ∈ ℝ)
11930, 111sylan 569 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) ∧ 𝑘 ∈ (ℤ𝑁)) → 0 ≤ (𝐺𝑘))
12064, 119syldan 579 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) ∧ 𝑘 ∈ (ℤ‘(𝑚 + 1))) → 0 ≤ (𝐺𝑘))
12160, 120sylan2 580 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) ∧ 𝑘 ∈ ((𝑚 + 1)...𝑛)) → 0 ≤ (𝐺𝑘))
12246, 47, 118, 121sermono 13040 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → (seq𝑀( + , 𝐺)‘𝑚) ≤ (seq𝑀( + , 𝐺)‘𝑛))
12344, 42, 122abssubge0d 14378 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → (abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) = ((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚)))
124123breq1d 4796 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → ((abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥 ↔ ((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚)) < 𝑥))
125105, 117, 1243imtr4d 283 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑚 ∈ (ℤ𝑁) ∧ 𝑛 ∈ (ℤ𝑚))) → ((abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚))) < 𝑥 → (abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥))
126125anassrs 458 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (ℤ𝑁)) ∧ 𝑛 ∈ (ℤ𝑚)) → ((abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚))) < 𝑥 → (abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥))
127126adantld 478 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (ℤ𝑁)) ∧ 𝑛 ∈ (ℤ𝑚)) → (((seq𝑀( + , 𝐹)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚))) < 𝑥) → (abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥))
128127ralimdva 3111 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (ℤ𝑁)) → (∀𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚))) < 𝑥) → ∀𝑛 ∈ (ℤ𝑚)(abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥))
129128reximdva 3165 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → (∃𝑚 ∈ (ℤ𝑁)∀𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚))) < 𝑥) → ∃𝑚 ∈ (ℤ𝑁)∀𝑛 ∈ (ℤ𝑚)(abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥))
13037r19.29uz 14298 . . . . . . 7 ((∀𝑛 ∈ (ℤ𝑁)(seq𝑀( + , 𝐺)‘𝑛) ∈ ℂ ∧ ∃𝑚 ∈ (ℤ𝑁)∀𝑛 ∈ (ℤ𝑚)(abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥) → ∃𝑚 ∈ (ℤ𝑁)∀𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐺)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥))
13129, 129, 130syl6an 663 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → (∃𝑚 ∈ (ℤ𝑁)∀𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚))) < 𝑥) → ∃𝑚 ∈ (ℤ𝑁)∀𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐺)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥)))
132131ralimdva 3111 . . . . 5 (𝜑 → (∀𝑥 ∈ ℝ+𝑚 ∈ (ℤ𝑁)∀𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚))) < 𝑥) → ∀𝑥 ∈ ℝ+𝑚 ∈ (ℤ𝑁)∀𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐺)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥)))
1331, 37cau4 14304 . . . . . 6 (𝑁𝑍 → (∀𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+𝑚 ∈ (ℤ𝑁)∀𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚))) < 𝑥)))
1344, 133syl 17 . . . . 5 (𝜑 → (∀𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+𝑚 ∈ (ℤ𝑁)∀𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚))) < 𝑥)))
1351, 37cau4 14304 . . . . . 6 (𝑁𝑍 → (∀𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐺)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+𝑚 ∈ (ℤ𝑁)∀𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐺)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥)))
1364, 135syl 17 . . . . 5 (𝜑 → (∀𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐺)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+𝑚 ∈ (ℤ𝑁)∀𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐺)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥)))
137132, 134, 1363imtr4d 283 . . . 4 (𝜑 → (∀𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑚))) < 𝑥) → ∀𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐺)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥)))
13820, 137mpd 15 . . 3 (𝜑 → ∀𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐺)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥))
1391uztrn2 11906 . . . . . . . 8 ((𝑚𝑍𝑛 ∈ (ℤ𝑚)) → 𝑛𝑍)
140 simpr 471 . . . . . . . . 9 (((seq𝑀( + , 𝐺)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥) → (abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥)
14125biantrurd 522 . . . . . . . . 9 ((𝜑𝑛𝑍) → ((abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥 ↔ ((seq𝑀( + , 𝐺)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥)))
142140, 141syl5ib 234 . . . . . . . 8 ((𝜑𝑛𝑍) → (((seq𝑀( + , 𝐺)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥) → ((seq𝑀( + , 𝐺)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥)))
143139, 142sylan2 580 . . . . . . 7 ((𝜑 ∧ (𝑚𝑍𝑛 ∈ (ℤ𝑚))) → (((seq𝑀( + , 𝐺)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥) → ((seq𝑀( + , 𝐺)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥)))
144143anassrs 458 . . . . . 6 (((𝜑𝑚𝑍) ∧ 𝑛 ∈ (ℤ𝑚)) → (((seq𝑀( + , 𝐺)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥) → ((seq𝑀( + , 𝐺)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥)))
145144ralimdva 3111 . . . . 5 ((𝜑𝑚𝑍) → (∀𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐺)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥) → ∀𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐺)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥)))
146145reximdva 3165 . . . 4 (𝜑 → (∃𝑚𝑍𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐺)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥) → ∃𝑚𝑍𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐺)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥)))
147146ralimdv 3112 . . 3 (𝜑 → (∀𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐺)‘𝑛) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥) → ∀𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐺)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥)))
148138, 147mpd 15 . 2 (𝜑 → ∀𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ (ℤ𝑚)((seq𝑀( + , 𝐺)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐺)‘𝑛) − (seq𝑀( + , 𝐺)‘𝑚))) < 𝑥))
1491, 3, 148caurcvg2 14616 1 (𝜑 → seq𝑀( + , 𝐺) ∈ dom ⇝ )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1631  wcel 2145  wral 3061  wrex 3062  Vcvv 3351   class class class wbr 4786  cmpt 4863  dom cdm 5249  wf 6027  cfv 6031  (class class class)co 6793  cc 10136  cr 10137  0cc0 10138  1c1 10139   + caddc 10141   < clt 10276  cle 10277  cmin 10468  cz 11579  cuz 11888  +crp 12035  ...cfz 12533  seqcseq 13008  abscabs 14182  cli 14423
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-inf2 8702  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-er 7896  df-pm 8012  df-en 8110  df-dom 8111  df-sdom 8112  df-sup 8504  df-inf 8505  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-3 11282  df-n0 11495  df-z 11580  df-uz 11889  df-rp 12036  df-ico 12386  df-fz 12534  df-fzo 12674  df-fl 12801  df-seq 13009  df-exp 13068  df-cj 14047  df-re 14048  df-im 14049  df-sqrt 14183  df-abs 14184  df-limsup 14410  df-clim 14427  df-rlim 14428
This theorem is referenced by:  cvgcmpce  14757  rpnnen2lem5  15153  aaliou3lem3  24319
  Copyright terms: Public domain W3C validator