Metamath Proof Explorer


Theorem cvgcmp

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)

Ref Expression
Hypotheses cvgcmp.1 𝑍 = ( ℤ𝑀 )
cvgcmp.2 ( 𝜑𝑁𝑍 )
cvgcmp.3 ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ℝ )
cvgcmp.4 ( ( 𝜑𝑘𝑍 ) → ( 𝐺𝑘 ) ∈ ℝ )
cvgcmp.5 ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
cvgcmp.6 ( ( 𝜑𝑘 ∈ ( ℤ𝑁 ) ) → 0 ≤ ( 𝐺𝑘 ) )
cvgcmp.7 ( ( 𝜑𝑘 ∈ ( ℤ𝑁 ) ) → ( 𝐺𝑘 ) ≤ ( 𝐹𝑘 ) )
Assertion cvgcmp ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ∈ dom ⇝ )

Proof

Step Hyp Ref Expression
1 cvgcmp.1 𝑍 = ( ℤ𝑀 )
2 cvgcmp.2 ( 𝜑𝑁𝑍 )
3 cvgcmp.3 ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ℝ )
4 cvgcmp.4 ( ( 𝜑𝑘𝑍 ) → ( 𝐺𝑘 ) ∈ ℝ )
5 cvgcmp.5 ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
6 cvgcmp.6 ( ( 𝜑𝑘 ∈ ( ℤ𝑁 ) ) → 0 ≤ ( 𝐺𝑘 ) )
7 cvgcmp.7 ( ( 𝜑𝑘 ∈ ( ℤ𝑁 ) ) → ( 𝐺𝑘 ) ≤ ( 𝐹𝑘 ) )
8 seqex seq 𝑀 ( + , 𝐺 ) ∈ V
9 8 a1i ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ∈ V )
10 2 1 eleqtrdi ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
11 eluzel2 ( 𝑁 ∈ ( ℤ𝑀 ) → 𝑀 ∈ ℤ )
12 10 11 syl ( 𝜑𝑀 ∈ ℤ )
13 1 climcau ( ( 𝑀 ∈ ℤ ∧ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) → ∀ 𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ ( ℤ𝑚 ) ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) < 𝑥 )
14 12 5 13 syl2anc ( 𝜑 → ∀ 𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ ( ℤ𝑚 ) ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) < 𝑥 )
15 1 12 3 serfre ( 𝜑 → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℝ )
16 15 ffvelrnda ( ( 𝜑𝑛𝑍 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℝ )
17 16 recnd ( ( 𝜑𝑛𝑍 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℂ )
18 17 ralrimiva ( 𝜑 → ∀ 𝑛𝑍 ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℂ )
19 1 r19.29uz ( ( ∀ 𝑛𝑍 ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℂ ∧ ∃ 𝑚𝑍𝑛 ∈ ( ℤ𝑚 ) ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) < 𝑥 ) → ∃ 𝑚𝑍𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) < 𝑥 ) )
20 19 ex ( ∀ 𝑛𝑍 ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℂ → ( ∃ 𝑚𝑍𝑛 ∈ ( ℤ𝑚 ) ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) < 𝑥 → ∃ 𝑚𝑍𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) < 𝑥 ) ) )
21 18 20 syl ( 𝜑 → ( ∃ 𝑚𝑍𝑛 ∈ ( ℤ𝑚 ) ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) < 𝑥 → ∃ 𝑚𝑍𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) < 𝑥 ) ) )
22 21 ralimdv ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ ( ℤ𝑚 ) ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) < 𝑥 → ∀ 𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) < 𝑥 ) ) )
23 14 22 mpd ( 𝜑 → ∀ 𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) < 𝑥 ) )
24 1 uztrn2 ( ( 𝑁𝑍𝑛 ∈ ( ℤ𝑁 ) ) → 𝑛𝑍 )
25 2 24 sylan ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → 𝑛𝑍 )
26 1 12 4 serfre ( 𝜑 → seq 𝑀 ( + , 𝐺 ) : 𝑍 ⟶ ℝ )
27 26 ffvelrnda ( ( 𝜑𝑛𝑍 ) → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℝ )
28 27 recnd ( ( 𝜑𝑛𝑍 ) → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℂ )
29 25 28 syldan ( ( 𝜑𝑛 ∈ ( ℤ𝑁 ) ) → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℂ )
30 29 ralrimiva ( 𝜑 → ∀ 𝑛 ∈ ( ℤ𝑁 ) ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℂ )
31 30 adantr ( ( 𝜑𝑥 ∈ ℝ+ ) → ∀ 𝑛 ∈ ( ℤ𝑁 ) ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℂ )
32 simpll ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → 𝜑 )
33 32 15 syl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℝ )
34 32 2 syl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → 𝑁𝑍 )
35 simprl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → 𝑚 ∈ ( ℤ𝑁 ) )
36 1 uztrn2 ( ( 𝑁𝑍𝑚 ∈ ( ℤ𝑁 ) ) → 𝑚𝑍 )
37 34 35 36 syl2anc ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → 𝑚𝑍 )
38 33 37 ffvelrnd ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ∈ ℝ )
39 eqid ( ℤ𝑁 ) = ( ℤ𝑁 )
40 39 uztrn2 ( ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) → 𝑛 ∈ ( ℤ𝑁 ) )
41 40 adantl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → 𝑛 ∈ ( ℤ𝑁 ) )
42 34 41 24 syl2anc ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → 𝑛𝑍 )
43 32 42 16 syl2anc ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℝ )
44 32 42 27 syl2anc ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℝ )
45 32 26 syl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → seq 𝑀 ( + , 𝐺 ) : 𝑍 ⟶ ℝ )
46 45 37 ffvelrnd ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ∈ ℝ )
47 44 46 resubcld ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ∈ ℝ )
48 37 1 eleqtrdi ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → 𝑚 ∈ ( ℤ𝑀 ) )
49 simprr ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → 𝑛 ∈ ( ℤ𝑚 ) )
50 elfzuz ( 𝑘 ∈ ( 𝑀 ... 𝑛 ) → 𝑘 ∈ ( ℤ𝑀 ) )
51 50 1 eleqtrrdi ( 𝑘 ∈ ( 𝑀 ... 𝑛 ) → 𝑘𝑍 )
52 fveq2 ( 𝑚 = 𝑘 → ( 𝐹𝑚 ) = ( 𝐹𝑘 ) )
53 fveq2 ( 𝑚 = 𝑘 → ( 𝐺𝑚 ) = ( 𝐺𝑘 ) )
54 52 53 oveq12d ( 𝑚 = 𝑘 → ( ( 𝐹𝑚 ) − ( 𝐺𝑚 ) ) = ( ( 𝐹𝑘 ) − ( 𝐺𝑘 ) ) )
55 eqid ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) − ( 𝐺𝑚 ) ) ) = ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) − ( 𝐺𝑚 ) ) )
56 ovex ( ( 𝐹𝑘 ) − ( 𝐺𝑘 ) ) ∈ V
57 54 55 56 fvmpt ( 𝑘𝑍 → ( ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) − ( 𝐺𝑚 ) ) ) ‘ 𝑘 ) = ( ( 𝐹𝑘 ) − ( 𝐺𝑘 ) ) )
58 57 adantl ( ( 𝜑𝑘𝑍 ) → ( ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) − ( 𝐺𝑚 ) ) ) ‘ 𝑘 ) = ( ( 𝐹𝑘 ) − ( 𝐺𝑘 ) ) )
59 3 4 resubcld ( ( 𝜑𝑘𝑍 ) → ( ( 𝐹𝑘 ) − ( 𝐺𝑘 ) ) ∈ ℝ )
60 58 59 eqeltrd ( ( 𝜑𝑘𝑍 ) → ( ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) − ( 𝐺𝑚 ) ) ) ‘ 𝑘 ) ∈ ℝ )
61 32 51 60 syl2an ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → ( ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) − ( 𝐺𝑚 ) ) ) ‘ 𝑘 ) ∈ ℝ )
62 elfzuz ( 𝑘 ∈ ( ( 𝑚 + 1 ) ... 𝑛 ) → 𝑘 ∈ ( ℤ ‘ ( 𝑚 + 1 ) ) )
63 peano2uz ( 𝑚 ∈ ( ℤ𝑁 ) → ( 𝑚 + 1 ) ∈ ( ℤ𝑁 ) )
64 35 63 syl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → ( 𝑚 + 1 ) ∈ ( ℤ𝑁 ) )
65 39 uztrn2 ( ( ( 𝑚 + 1 ) ∈ ( ℤ𝑁 ) ∧ 𝑘 ∈ ( ℤ ‘ ( 𝑚 + 1 ) ) ) → 𝑘 ∈ ( ℤ𝑁 ) )
66 64 65 sylan ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) ∧ 𝑘 ∈ ( ℤ ‘ ( 𝑚 + 1 ) ) ) → 𝑘 ∈ ( ℤ𝑁 ) )
67 1 uztrn2 ( ( 𝑁𝑍𝑘 ∈ ( ℤ𝑁 ) ) → 𝑘𝑍 )
68 2 67 sylan ( ( 𝜑𝑘 ∈ ( ℤ𝑁 ) ) → 𝑘𝑍 )
69 3 4 subge0d ( ( 𝜑𝑘𝑍 ) → ( 0 ≤ ( ( 𝐹𝑘 ) − ( 𝐺𝑘 ) ) ↔ ( 𝐺𝑘 ) ≤ ( 𝐹𝑘 ) ) )
70 68 69 syldan ( ( 𝜑𝑘 ∈ ( ℤ𝑁 ) ) → ( 0 ≤ ( ( 𝐹𝑘 ) − ( 𝐺𝑘 ) ) ↔ ( 𝐺𝑘 ) ≤ ( 𝐹𝑘 ) ) )
71 7 70 mpbird ( ( 𝜑𝑘 ∈ ( ℤ𝑁 ) ) → 0 ≤ ( ( 𝐹𝑘 ) − ( 𝐺𝑘 ) ) )
72 68 57 syl ( ( 𝜑𝑘 ∈ ( ℤ𝑁 ) ) → ( ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) − ( 𝐺𝑚 ) ) ) ‘ 𝑘 ) = ( ( 𝐹𝑘 ) − ( 𝐺𝑘 ) ) )
73 71 72 breqtrrd ( ( 𝜑𝑘 ∈ ( ℤ𝑁 ) ) → 0 ≤ ( ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) − ( 𝐺𝑚 ) ) ) ‘ 𝑘 ) )
74 32 66 73 syl2an2r ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) ∧ 𝑘 ∈ ( ℤ ‘ ( 𝑚 + 1 ) ) ) → 0 ≤ ( ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) − ( 𝐺𝑚 ) ) ) ‘ 𝑘 ) )
75 62 74 sylan2 ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) ∧ 𝑘 ∈ ( ( 𝑚 + 1 ) ... 𝑛 ) ) → 0 ≤ ( ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) − ( 𝐺𝑚 ) ) ) ‘ 𝑘 ) )
76 48 49 61 75 sermono ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → ( seq 𝑀 ( + , ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) − ( 𝐺𝑚 ) ) ) ) ‘ 𝑚 ) ≤ ( seq 𝑀 ( + , ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) − ( 𝐺𝑚 ) ) ) ) ‘ 𝑛 ) )
77 elfzuz ( 𝑘 ∈ ( 𝑀 ... 𝑚 ) → 𝑘 ∈ ( ℤ𝑀 ) )
78 77 1 eleqtrrdi ( 𝑘 ∈ ( 𝑀 ... 𝑚 ) → 𝑘𝑍 )
79 3 recnd ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ℂ )
80 32 78 79 syl2an ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑚 ) ) → ( 𝐹𝑘 ) ∈ ℂ )
81 4 recnd ( ( 𝜑𝑘𝑍 ) → ( 𝐺𝑘 ) ∈ ℂ )
82 32 78 81 syl2an ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑚 ) ) → ( 𝐺𝑘 ) ∈ ℂ )
83 32 78 58 syl2an ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑚 ) ) → ( ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) − ( 𝐺𝑚 ) ) ) ‘ 𝑘 ) = ( ( 𝐹𝑘 ) − ( 𝐺𝑘 ) ) )
84 48 80 82 83 sersub ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → ( seq 𝑀 ( + , ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) − ( 𝐺𝑚 ) ) ) ) ‘ 𝑚 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) )
85 42 1 eleqtrdi ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → 𝑛 ∈ ( ℤ𝑀 ) )
86 32 51 79 syl2an ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → ( 𝐹𝑘 ) ∈ ℂ )
87 32 51 81 syl2an ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → ( 𝐺𝑘 ) ∈ ℂ )
88 32 51 58 syl2an ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → ( ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) − ( 𝐺𝑚 ) ) ) ‘ 𝑘 ) = ( ( 𝐹𝑘 ) − ( 𝐺𝑘 ) ) )
89 85 86 87 88 sersub ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → ( seq 𝑀 ( + , ( 𝑚𝑍 ↦ ( ( 𝐹𝑚 ) − ( 𝐺𝑚 ) ) ) ) ‘ 𝑛 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) )
90 76 84 89 3brtr3d ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ≤ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) )
91 43 44 resubcld ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) ∈ ℝ )
92 38 46 91 lesubaddd ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → ( ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ≤ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ≤ ( ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) )
93 90 92 mpbid ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ≤ ( ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) )
94 43 recnd ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℂ )
95 44 recnd ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℂ )
96 46 recnd ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ∈ ℂ )
97 94 95 96 subsubd ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) = ( ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) )
98 93 97 breqtrrd ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ≤ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) )
99 38 43 47 98 lesubd ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ≤ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) )
100 43 38 resubcld ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ∈ ℝ )
101 rpre ( 𝑥 ∈ ℝ+𝑥 ∈ ℝ )
102 101 ad2antlr ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → 𝑥 ∈ ℝ )
103 lelttr ( ( ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ∈ ℝ ∧ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ≤ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ∧ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) < 𝑥 ) → ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) < 𝑥 ) )
104 47 100 102 103 syl3anc ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → ( ( ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ≤ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ∧ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) < 𝑥 ) → ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) < 𝑥 ) )
105 99 104 mpand ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → ( ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) < 𝑥 → ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) < 𝑥 ) )
106 32 51 3 syl2an ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → ( 𝐹𝑘 ) ∈ ℝ )
107 62 66 sylan2 ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) ∧ 𝑘 ∈ ( ( 𝑚 + 1 ) ... 𝑛 ) ) → 𝑘 ∈ ( ℤ𝑁 ) )
108 0red ( ( 𝜑𝑘 ∈ ( ℤ𝑁 ) ) → 0 ∈ ℝ )
109 68 4 syldan ( ( 𝜑𝑘 ∈ ( ℤ𝑁 ) ) → ( 𝐺𝑘 ) ∈ ℝ )
110 68 3 syldan ( ( 𝜑𝑘 ∈ ( ℤ𝑁 ) ) → ( 𝐹𝑘 ) ∈ ℝ )
111 108 109 110 6 7 letrd ( ( 𝜑𝑘 ∈ ( ℤ𝑁 ) ) → 0 ≤ ( 𝐹𝑘 ) )
112 32 107 111 syl2an2r ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) ∧ 𝑘 ∈ ( ( 𝑚 + 1 ) ... 𝑛 ) ) → 0 ≤ ( 𝐹𝑘 ) )
113 48 49 106 112 sermono ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ≤ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) )
114 38 43 113 abssubge0d ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) )
115 114 breq1d ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → ( ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) < 𝑥 ↔ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) < 𝑥 ) )
116 32 51 4 syl2an ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → ( 𝐺𝑘 ) ∈ ℝ )
117 32 66 6 syl2an2r ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) ∧ 𝑘 ∈ ( ℤ ‘ ( 𝑚 + 1 ) ) ) → 0 ≤ ( 𝐺𝑘 ) )
118 62 117 sylan2 ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) ∧ 𝑘 ∈ ( ( 𝑚 + 1 ) ... 𝑛 ) ) → 0 ≤ ( 𝐺𝑘 ) )
119 48 49 116 118 sermono ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ≤ ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) )
120 46 44 119 abssubge0d ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) )
121 120 breq1d ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → ( ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ↔ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) < 𝑥 ) )
122 105 115 121 3imtr4d ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ𝑁 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) ) → ( ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) < 𝑥 → ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) )
123 122 anassrs ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( ℤ𝑁 ) ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) → ( ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) < 𝑥 → ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) )
124 123 adantld ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( ℤ𝑁 ) ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) → ( ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) < 𝑥 ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) )
125 124 ralimdva ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( ℤ𝑁 ) ) → ( ∀ 𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) < 𝑥 ) → ∀ 𝑛 ∈ ( ℤ𝑚 ) ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) )
126 125 reximdva ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ∃ 𝑚 ∈ ( ℤ𝑁 ) ∀ 𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) < 𝑥 ) → ∃ 𝑚 ∈ ( ℤ𝑁 ) ∀ 𝑛 ∈ ( ℤ𝑚 ) ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) )
127 39 r19.29uz ( ( ∀ 𝑛 ∈ ( ℤ𝑁 ) ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℂ ∧ ∃ 𝑚 ∈ ( ℤ𝑁 ) ∀ 𝑛 ∈ ( ℤ𝑚 ) ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) → ∃ 𝑚 ∈ ( ℤ𝑁 ) ∀ 𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) )
128 31 126 127 syl6an ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ∃ 𝑚 ∈ ( ℤ𝑁 ) ∀ 𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) < 𝑥 ) → ∃ 𝑚 ∈ ( ℤ𝑁 ) ∀ 𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) ) )
129 128 ralimdva ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+𝑚 ∈ ( ℤ𝑁 ) ∀ 𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ+𝑚 ∈ ( ℤ𝑁 ) ∀ 𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) ) )
130 1 39 cau4 ( 𝑁𝑍 → ( ∀ 𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+𝑚 ∈ ( ℤ𝑁 ) ∀ 𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) < 𝑥 ) ) )
131 2 130 syl ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+𝑚 ∈ ( ℤ𝑁 ) ∀ 𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) < 𝑥 ) ) )
132 1 39 cau4 ( 𝑁𝑍 → ( ∀ 𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+𝑚 ∈ ( ℤ𝑁 ) ∀ 𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) ) )
133 2 132 syl ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+𝑚 ∈ ( ℤ𝑁 ) ∀ 𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) ) )
134 129 131 133 3imtr4d ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) ) )
135 23 134 mpd ( 𝜑 → ∀ 𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) )
136 1 uztrn2 ( ( 𝑚𝑍𝑛 ∈ ( ℤ𝑚 ) ) → 𝑛𝑍 )
137 simpr ( ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 )
138 27 biantrurd ( ( 𝜑𝑛𝑍 ) → ( ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ↔ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℝ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) ) )
139 137 138 syl5ib ( ( 𝜑𝑛𝑍 ) → ( ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) → ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℝ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) ) )
140 136 139 sylan2 ( ( 𝜑 ∧ ( 𝑚𝑍𝑛 ∈ ( ℤ𝑚 ) ) ) → ( ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) → ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℝ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) ) )
141 140 anassrs ( ( ( 𝜑𝑚𝑍 ) ∧ 𝑛 ∈ ( ℤ𝑚 ) ) → ( ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) → ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℝ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) ) )
142 141 ralimdva ( ( 𝜑𝑚𝑍 ) → ( ∀ 𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) → ∀ 𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℝ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) ) )
143 142 reximdva ( 𝜑 → ( ∃ 𝑚𝑍𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) → ∃ 𝑚𝑍𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℝ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) ) )
144 143 ralimdv ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℝ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) ) )
145 135 144 mpd ( 𝜑 → ∀ 𝑥 ∈ ℝ+𝑚𝑍𝑛 ∈ ( ℤ𝑚 ) ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℝ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) ) < 𝑥 ) )
146 1 9 145 caurcvg2 ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ∈ dom ⇝ )