This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 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 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ) ) → ( 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 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ) ) → ( 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 imbitrid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( ( 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 ⇝ )