ser1f0 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem ser1f0 7126

Description: If an infinite series converges, its underlying sequence converges to zero. Warning: The HTML proof page is 1/2 megabyte in size.

**Hypotheses**
Ref	Expression
ser1f0.1	⊢ F:ℕ–→ℂ
ser1f0.2	⊢ A ∈ ℂ
ser1f0.3	⊢ ( + seq₁F) ⇝ A

**Assertion**
Ref	Expression
ser1f0	⊢ F ⇝ 0

**Proof of Theorem ser1f0**
Step	Hyp	Ref	Expression
1		0cn 5320	. . 3 ⊢ 0 ∈ ℂ
2		inss2 2227	. . . . . . 7 ⊢ (ℤ ∩ (ℤ_≥ ‘2)) ⊆ (ℤ_≥ ‘2)
3		1z 6126	. . . . . . . . . . 11 ⊢ 1 ∈ ℤ
4	3	eluz1 6374	. . . . . . . . . 10 ⊢ (2 ∈ (ℤ_≥ ‘1) ↔ (2 ∈ ℤ ⋀ 1 ≤ 2))
5		2z 6127	. . . . . . . . . 10 ⊢ 2 ∈ ℤ
6		1re 5427	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
7		2re 5946	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ
8		1lt2 5995	. . . . . . . . . . 11 ⊢ 1 < 2
9	6, 7, 8	ltlei 5574	. . . . . . . . . 10 ⊢ 1 ≤ 2
10	4, 5, 9	mpbir2an 729	. . . . . . . . 9 ⊢ 2 ∈ (ℤ_≥ ‘1)
11		uzss 6383	. . . . . . . . 9 ⊢ (2 ∈ (ℤ_≥ ‘1) → (ℤ_≥ ‘2) ⊆ (ℤ_≥ ‘1))
12	10, 11	ax-mp 7	. . . . . . . 8 ⊢ (ℤ_≥ ‘2) ⊆ (ℤ_≥ ‘1)
13		nnuz 6391	. . . . . . . 8 ⊢ ℕ = (ℤ_≥ ‘1)
14	12, 13	sseqtr4 2090	. . . . . . 7 ⊢ (ℤ_≥ ‘2) ⊆ ℕ
15	2, 14	sstri 2069	. . . . . 6 ⊢ (ℤ ∩ (ℤ_≥ ‘2)) ⊆ ℕ
16	15	sseli 2061	. . . . 5 ⊢ (k ∈ (ℤ ∩ (ℤ_≥ ‘2)) → k ∈ ℕ)
17		ser1f0.1	. . . . . 6 ⊢ F:ℕ–→ℂ
18	17	ffvelrni 3817	. . . . 5 ⊢ (k ∈ ℕ → (F ‘k) ∈ ℂ)
19	16, 18	syl 10	. . . 4 ⊢ (k ∈ (ℤ ∩ (ℤ_≥ ‘2)) → (F ‘k) ∈ ℂ)
20	19	rgen 1695	. . 3 ⊢ ∀k ∈ (ℤ ∩ (ℤ_≥ ‘2))(F ‘k) ∈ ℂ
21		uzssz 6382	. . . 4 ⊢ (ℤ_≥ ‘2) ⊆ ℤ
22		ssid 2076	. . . 4 ⊢ ℤ ⊆ ℤ
23		ssid 2076	. . . 4 ⊢ (ℤ_≥ ‘2) ⊆ (ℤ_≥ ‘2)
24		nnex 5901	. . . . 5 ⊢ ℕ ∈ V
25		fex 3654	. . . . 5 ⊢ ((F:ℕ–→ℂ ⋀ ℕ ∈ V) → F ∈ V)
26	17, 24, 25	mp2an 696	. . . 4 ⊢ F ∈ V
27	5, 21, 22, 5, 23, 21, 26	clm4 7038	. . 3 ⊢ ((0 ∈ ℂ ⋀ ∀k ∈ (ℤ ∩ (ℤ_≥ ‘2))(F ‘k) ∈ ℂ) → (F ⇝ 0 ↔ ∀x ∈ ℝ (0 < x → ∃j ∈ ℤ ∀k ∈ (ℤ_≥ ‘2)(j ≤ k → (abs ‘((F ‘k) − 0)) < x))))
28	1, 20, 27	mp2an 696	. 2 ⊢ (F ⇝ 0 ↔ ∀x ∈ ℝ (0 < x → ∃j ∈ ℤ ∀k ∈ (ℤ_≥ ‘2)(j ≤ k → (abs ‘((F ‘k) − 0)) < x)))
29		ser1f0.2	. . . . . 6 ⊢ A ∈ ℂ
30		ser1f0.3	. . . . . 6 ⊢ ( + seq₁F) ⇝ A
31		0z 6113	. . . . . . 7 ⊢ 0 ∈ ℤ
32		uzssz 6382	. . . . . . 7 ⊢ (ℤ_≥ ‘0) ⊆ ℤ
33	31, 32, 22	clmi2 7045	. . . . . 6 ⊢ (((A ∈ ℂ ⋀ ( + seq₁F) ⇝ A) ⋀ ((x / 2) ∈ ℝ ⋀ 0 < (x / 2))) → ∃m ∈ ℤ ∀n ∈ ℤ (m ≤ n → (abs ‘((( + seq₁F) ‘n) − A)) < (x / 2)))
34	29, 30, 33	mpanl12 707	. . . . 5 ⊢ (((x / 2) ∈ ℝ ⋀ 0 < (x / 2)) → ∃m ∈ ℤ ∀n ∈ ℤ (m ≤ n → (abs ‘((( + seq₁F) ‘n) − A)) < (x / 2)))
35		rehalfclt 6001	. . . . . 6 ⊢ (x ∈ ℝ → (x / 2) ∈ ℝ)
36	35	adantr 389	. . . . 5 ⊢ ((x ∈ ℝ ⋀ 0 < x) → (x / 2) ∈ ℝ)
37		halfpos2t 6004	. . . . . 6 ⊢ (x ∈ ℝ → (0 < x ↔ 0 < (x / 2)))
38	37	biimpa 416	. . . . 5 ⊢ ((x ∈ ℝ ⋀ 0 < x) → 0 < (x / 2))
39	34, 36, 38	sylanc 471	. . . 4 ⊢ ((x ∈ ℝ ⋀ 0 < x) → ∃m ∈ ℤ ∀n ∈ ℤ (m ≤ n → (abs ‘((( + seq₁F) ‘n) − A)) < (x / 2)))
40		breq1 2618	. . . . . . . . . . 11 ⊢ (j = (m + 1) → (j ≤ k ↔ (m + 1) ≤ k))
41	40	imbi1d 612	. . . . . . . . . 10 ⊢ (j = (m + 1) → ((j ≤ k → (abs ‘((F ‘k) − 0)) < x) ↔ ((m + 1) ≤ k → (abs ‘((F ‘k) − 0)) < x)))
42	41	ralbidv 1660	. . . . . . . . 9 ⊢ (j = (m + 1) → (∀k ∈ (ℤ_≥ ‘2)(j ≤ k → (abs ‘((F ‘k) − 0)) < x) ↔ ∀k ∈ (ℤ_≥ ‘2)((m + 1) ≤ k → (abs ‘((F ‘k) − 0)) < x)))
43	42	rcla4ev 1873	. . . . . . . 8 ⊢ (((m + 1) ∈ ℤ ⋀ ∀k ∈ (ℤ_≥ ‘2)((m + 1) ≤ k → (abs ‘((F ‘k) − 0)) < x)) → ∃j ∈ ℤ ∀k ∈ (ℤ_≥ ‘2)(j ≤ k → (abs ‘((F ‘k) − 0)) < x))
44		peano2z 6133	. . . . . . . . 9 ⊢ (m ∈ ℤ → (m + 1) ∈ ℤ)
45	44	ad2antrl 406	. . . . . . . 8 ⊢ ((x ∈ ℝ ⋀ (m ∈ ℤ ⋀ ∀n ∈ ℤ (m ≤ n → (abs ‘((( + seq₁F) ‘n) − A)) < (x / 2)))) → (m + 1) ∈ ℤ)
46		p1let 5793	. . . . . . . . . . . . . . . . . . 19 ⊢ ((m ∈ ℝ ⋀ k ∈ ℝ ⋀ (m + 1) ≤ k) → m ≤ k)
47	46	3expia 834	. . . . . . . . . . . . . . . . . 18 ⊢ ((m ∈ ℝ ⋀ k ∈ ℝ) → ((m + 1) ≤ k → m ≤ k))
48		zret 6106	. . . . . . . . . . . . . . . . . 18 ⊢ (m ∈ ℤ → m ∈ ℝ)
49		zret 6106	. . . . . . . . . . . . . . . . . 18 ⊢ (k ∈ ℤ → k ∈ ℝ)
50	47, 48, 49	syl2an 454	. . . . . . . . . . . . . . . . 17 ⊢ ((m ∈ ℤ ⋀ k ∈ ℤ) → ((m + 1) ≤ k → m ≤ k))
51	50	ancoms 436	. . . . . . . . . . . . . . . 16 ⊢ ((k ∈ ℤ ⋀ m ∈ ℤ) → ((m + 1) ≤ k → m ≤ k))
52	51	adantrr 395	. . . . . . . . . . . . . . 15 ⊢ ((k ∈ ℤ ⋀ (m ∈ ℤ ⋀ ∀n ∈ ℤ (m ≤ n → (abs ‘((( + seq₁F) ‘n) − A)) < (x / 2)))) → ((m + 1) ≤ k → m ≤ k))
53		breq2 2619	. . . . . . . . . . . . . . . . . 18 ⊢ (n = k → (m ≤ n ↔ m ≤ k))
54		fveq2 3726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (n = k → (( + seq₁F) ‘n) = (( + seq₁F) ‘k))
55	54	opreq1d 3977	. . . . . . . . . . . . . . . . . . . 20 ⊢ (n = k → ((( + seq₁F) ‘n) − A) = ((( + seq₁F) ‘k) − A))
56	55	fveq2d 3730	. . . . . . . . . . . . . . . . . . 19 ⊢ (n = k → (abs ‘((( + seq₁F) ‘n) − A)) = (abs ‘((( + seq₁F) ‘k) − A)))
57	56	breq1d 2625	. . . . . . . . . . . . . . . . . 18 ⊢ (n = k → ((abs ‘((( + seq₁F) ‘n) − A)) < (x / 2) ↔ (abs ‘((( + seq₁F) ‘k) − A)) < (x / 2)))
58	53, 57	imbi12d 625	. . . . . . . . . . . . . . . . 17 ⊢ (n = k → ((m ≤ n → (abs ‘((( + seq₁F) ‘n) − A)) < (x / 2)) ↔ (m ≤ k → (abs ‘((( + seq₁F) ‘k) − A)) < (x / 2))))
59	58	rcla4va 1871	. . . . . . . . . . . . . . . 16 ⊢ ((k ∈ ℤ ⋀ ∀n ∈ ℤ (m ≤ n → (abs ‘((( + seq₁F) ‘n) − A)) < (x / 2))) → (m ≤ k → (abs ‘((( + seq₁F) ‘k) − A)) < (x / 2)))
60	59	adantrl 394	. . . . . . . . . . . . . . 15 ⊢ ((k ∈ ℤ ⋀ (m ∈ ℤ ⋀ ∀n ∈ ℤ (m ≤ n → (abs ‘((( + seq₁F) ‘n) − A)) < (x / 2)))) → (m ≤ k → (abs ‘((( + seq₁F) ‘k) − A)) < (x / 2)))
61	52, 60	syld 27	. . . . . . . . . . . . . 14 ⊢ ((k ∈ ℤ ⋀ (m ∈ ℤ ⋀ ∀n ∈ ℤ (m ≤ n → (abs ‘((( + seq₁F) ‘n) − A)) < (x / 2)))) → ((m + 1) ≤ k → (abs ‘((( + seq₁F) ‘k) − A)) < (x / 2)))
62		leaddsubt 5627	. . . . . . . . . . . . . . . . . . 19 ⊢ ((m ∈ ℝ ⋀ 1 ∈ ℝ ⋀ k ∈ ℝ) → ((m + 1) ≤ k ↔ m ≤ (k − 1)))
63	6, 62	mp3an2 902	. . . . . . . . . . . . . . . . . 18 ⊢ ((m ∈ ℝ ⋀ k ∈ ℝ) → ((m + 1) ≤ k ↔ m ≤ (k − 1)))
64	63, 48, 49	syl2an 454	. . . . . . . . . . . . . . . . 17 ⊢ ((m ∈ ℤ ⋀ k ∈ ℤ) → ((m + 1) ≤ k ↔ m ≤ (k − 1)))
65	64	ancoms 436	. . . . . . . . . . . . . . . 16 ⊢ ((k ∈ ℤ ⋀ m ∈ ℤ) → ((m + 1) ≤ k ↔ m ≤ (k − 1)))
66	65	adantrr 395	. . . . . . . . . . . . . . 15 ⊢ ((k ∈ ℤ ⋀ (m ∈ ℤ ⋀ ∀n ∈ ℤ (m ≤ n → (abs ‘((( + seq₁F) ‘n) − A)) < (x / 2)))) → ((m + 1) ≤ k ↔ m ≤ (k − 1)))
67		peano2zm 6136	. . . . . . . . . . . . . . . . . 18 ⊢ (k ∈ ℤ → (k − 1) ∈ ℤ)
68		breq2 2619	. . . . . . . . . . . . . . . . . . . 20 ⊢ (n = (k − 1) → (m ≤ n ↔ m ≤ (k − 1)))
69		fveq2 3726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (n = (k − 1) → (( + seq₁F) ‘n) = (( + seq₁F) ‘(k − 1)))
70	69	opreq1d 3977	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (n = (k − 1) → ((( + seq₁F) ‘n) − A) = ((( + seq₁F) ‘(k − 1)) − A))
71	70	fveq2d 3730	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (n = (k − 1) → (abs ‘((( + seq₁F) ‘n) − A)) = (abs ‘((( + seq₁F) ‘(k − 1)) − A)))
72	71	breq1d 2625	. . . . . . . . . . . . . . . . . . . 20 ⊢ (n = (k − 1) → ((abs ‘((( + seq₁F) ‘n) − A)) < (x / 2) ↔ (abs ‘((( + seq₁F) ‘(k − 1)) − A)) < (x / 2)))
73	68, 72	imbi12d 625	. . . . . . . . . . . . . . . . . . 19 ⊢ (n = (k − 1) → ((m ≤ n → (abs ‘((( + seq₁F) ‘n) − A)) < (x / 2)) ↔ (m ≤ (k − 1) → (abs ‘((( + seq₁F) ‘(k − 1)) − A)) < (x / 2))))
74	73	rcla4v 1869	. . . . . . . . . . . . . . . . . 18 ⊢ ((k − 1) ∈ ℤ → (∀n ∈ ℤ (m ≤ n → (abs ‘((( + seq₁F) ‘n) − A)) < (x / 2)) → (m ≤ (k − 1) → (abs ‘((( + seq₁F) ‘(k − 1)) − A)) < (x / 2))))
75	67, 74	syl 10	. . . . . . . . . . . . . . . . 17 ⊢ (k ∈ ℤ → (∀n ∈ ℤ (m ≤ n → (abs ‘((( + seq₁F) ‘n) − A)) < (x / 2)) → (m ≤ (k − 1) → (abs ‘((( + seq₁F) ‘(k − 1)) − A)) < (x / 2))))
76	75	imp 350	. . . . . . . . . . . . . . . 16 ⊢ ((k ∈ ℤ ⋀ ∀n ∈ ℤ (m ≤ n → (abs ‘((( + seq₁F) ‘n) − A)) < (x / 2))) → (m ≤ (k − 1) → (abs ‘((( + seq₁F) ‘(k − 1)) − A)) < (x / 2)))
77	76	adantrl 394	. . . . . . . . . . . . . . 15 ⊢ ((k ∈ ℤ ⋀ (m ∈ ℤ ⋀ ∀n ∈ ℤ (m ≤ n → (abs ‘((( + seq₁F) ‘n) − A)) < (x / 2)))) → (m ≤ (k − 1) → (abs ‘((( + seq₁F) ‘(k − 1)) − A)) < (x / 2)))
78	66, 77	sylbid 203	. . . . . . . . . . . . . 14 ⊢ ((k ∈ ℤ ⋀ (m ∈ ℤ ⋀ ∀n ∈ ℤ (m ≤ n → (abs ‘((( + seq₁F) ‘n) − A)) < (x / 2)))) → ((m + 1) ≤ k → (abs ‘((( + seq₁F) ‘(k − 1)) − A)) < (x / 2)))
79	61, 78	jcad 599	. . . . . . . . . . . . 13 ⊢ ((k ∈ ℤ ⋀ (m ∈ ℤ ⋀ ∀n ∈ ℤ (m ≤ n → (abs ‘((( + seq₁F) ‘n) − A)) < (x / 2)))) → ((m + 1) ≤ k → ((abs ‘((( + seq₁F) ‘k) − A)) < (x / 2) ⋀ (abs ‘((( + seq₁F) ‘(k − 1)) − A)) < (x / 2))))
80	79	ad2ant2rl 411	. . . . . . . . . . . 12 ⊢ (((k ∈ ℤ ⋀ 2 ≤ k) ⋀ (x ∈ ℝ ⋀ (m ∈ ℤ ⋀ ∀n ∈ ℤ (m ≤ n → (abs ‘((( + seq₁F) ‘n) − A)) < (x / 2))))) → ((m + 1) ≤ k → ((abs ‘((( + seq₁F) ‘k) − A)) < (x / 2) ⋀ (abs ‘((( + seq₁F) ‘(k − 1)) − A)) < (x / 2))))
81		lt2addt 5637	. . . . . . . . . . . . . . . . 17 ⊢ ((((abs ‘((( + seq₁F) ‘k) − A)) ∈ ℝ ⋀ (abs ‘((( + seq₁F) ‘(k − 1)) − A)) ∈ ℝ) ⋀ ((x / 2) ∈ ℝ ⋀ (x / 2) ∈ ℝ)) → (((abs ‘((( + seq₁F) ‘k) − A)) < (x / 2) ⋀ (abs ‘((( + seq₁F) ‘(k − 1)) − A)) < (x / 2)) → ((abs ‘((( + seq₁F) ‘k) − A)) + (abs ‘((( + seq₁F) ‘(k − 1)) − A))) < ((x / 2) + (x / 2))))
82	17	ser1cl1 6287	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (k ∈ ℕ → (( + seq₁F) ‘k) ∈ ℂ)
83		subclt 5359	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((( + seq₁F) ‘k) ∈ ℂ ⋀ A ∈ ℂ) → ((( + seq₁F) ‘k) − A) ∈ ℂ)
84	29, 83	mpan2 695	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((( + seq₁F) ‘k) ∈ ℂ → ((( + seq₁F) ‘k) − A) ∈ ℂ)
85	82, 84	syl 10	. . . . . . . . . . . . . . . . . . . 20 ⊢ (k ∈ ℕ → ((( + seq₁F) ‘k) − A) ∈ ℂ)
86		absclt 6788	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((( + seq₁F) ‘k) − A) ∈ ℂ → (abs ‘((( + seq₁F) ‘k) − A)) ∈ ℝ)
87	85, 86	syl 10	. . . . . . . . . . . . . . . . . . 19 ⊢ (k ∈ ℕ → (abs ‘((( + seq₁F) ‘k) − A)) ∈ ℝ)
88	87	adantr 389	. . . . . . . . . . . . . . . . . 18 ⊢ ((k ∈ ℕ ⋀ 1 < k) → (abs ‘((( + seq₁F) ‘k) − A)) ∈ ℝ)
89		1nn 5902	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ ℕ
90		nnsubt 5924	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 ∈ ℕ ⋀ k ∈ ℕ) → (1 < k ↔ (k − 1) ∈ ℕ))
91	89, 90	mpan 694	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (k ∈ ℕ → (1 < k ↔ (k − 1) ∈ ℕ))
92	91	biimpa 416	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((k ∈ ℕ ⋀ 1 < k) → (k − 1) ∈ ℕ)
93	17	ser1cl1 6287	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((k − 1) ∈ ℕ → (( + seq₁F) ‘(k − 1)) ∈ ℂ)
94	92, 93	syl 10	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((k ∈ ℕ ⋀ 1 < k) → (( + seq₁F) ‘(k − 1)) ∈ ℂ)
95		subclt 5359	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((( + seq₁F) ‘(k − 1)) ∈ ℂ ⋀ A ∈ ℂ) → ((( + seq₁F) ‘(k − 1)) − A) ∈ ℂ)
96	29, 95	mpan2 695	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((( + seq₁F) ‘(k − 1)) ∈ ℂ → ((( + seq₁F) ‘(k − 1)) − A) ∈ ℂ)
97	94, 96	syl 10	. . . . . . . . . . . . . . . . . . 19 ⊢ ((k ∈ ℕ ⋀ 1 < k) → ((( + seq₁F) ‘(k − 1)) − A) ∈ ℂ)
98		absclt 6788	. . . . . . . . . . . . . . . . . . 19 ⊢ (((( + seq₁F) ‘(k − 1)) − A) ∈ ℂ → (abs ‘((( + seq₁F) ‘(k − 1)) − A)) ∈ ℝ)
99	97, 98	syl 10	. . . . . . . . . . . . . . . . . 18 ⊢ ((k ∈ ℕ ⋀ 1 < k) → (abs ‘((( + seq₁F) ‘(k − 1)) − A)) ∈ ℝ)
100	88, 99	jca 288	. . . . . . . . . . . . . . . . 17 ⊢ ((k ∈ ℕ ⋀ 1 < k) → ((abs ‘((( + seq₁F) ‘k) − A)) ∈ ℝ ⋀ (abs ‘((( + seq₁F) ‘(k − 1)) − A)) ∈ ℝ))
101	35, 35	jca 288	. . . . . . . . . . . . . . . . 17 ⊢ (x ∈ ℝ → ((x / 2) ∈ ℝ ⋀ (x / 2) ∈ ℝ))
102	81, 100, 101	syl2an 454	. . . . . . . . . . . . . . . 16 ⊢ (((k ∈ ℕ ⋀ 1 < k) ⋀ x ∈ ℝ) → (((abs ‘((( + seq₁F) ‘k) − A)) < (x / 2) ⋀ (abs ‘((( + seq₁F) ‘(k − 1)) − A)) < (x / 2)) → ((abs ‘((( + seq₁F) ‘k) − A)) + (abs ‘((( + seq₁F) ‘(k − 1)) − A))) < ((x / 2) + (x / 2))))
103		abssubt 6852	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((( + seq₁F) ‘(k − 1)) ∈ ℂ ⋀ A ∈ ℂ) → (abs ‘((( + seq₁F) ‘(k − 1)) − A)) = (abs ‘(A − (( + seq₁F) ‘(k − 1)))))
104	29, 103	mpan2 695	. . . . . . . . . . . . . . . . . . 19 ⊢ ((( + seq₁F) ‘(k − 1)) ∈ ℂ → (abs ‘((( + seq₁F) ‘(k − 1)) − A)) = (abs ‘(A − (( + seq₁F) ‘(k − 1)))))
105	94, 104	syl 10	. . . . . . . . . . . . . . . . . 18 ⊢ ((k ∈ ℕ ⋀ 1 < k) → (abs ‘((( + seq₁F) ‘(k − 1)) − A)) = (abs ‘(A − (( + seq₁F) ‘(k − 1)))))
106	105	opreq2d 3978	. . . . . . . . . . . . . . . . 17 ⊢ ((k ∈ ℕ ⋀ 1 < k) → ((abs ‘((( + seq₁F) ‘k) − A)) + (abs ‘((( + seq₁F) ‘(k − 1)) − A))) = ((abs ‘((( + seq₁F) ‘k) − A)) + (abs ‘(A − (( + seq₁F) ‘(k − 1))))))
107		recnt 5305	. . . . . . . . . . . . . . . . . 18 ⊢ (x ∈ ℝ → x ∈ ℂ)
108		2halvest 6006	. . . . . . . . . . . . . . . . . 18 ⊢ (x ∈ ℂ → ((x / 2) + (x / 2)) = x)
109	107, 108	syl 10	. . . . . . . . . . . . . . . . 17 ⊢ (x ∈ ℝ → ((x / 2) + (x / 2)) = x)
110	106, 109	breqan12d 2628	. . . . . . . . . . . . . . . 16 ⊢ (((k ∈ ℕ ⋀ 1 < k) ⋀ x ∈ ℝ) → (((abs ‘((( + seq₁F) ‘k) − A)) + (abs ‘((( + seq₁F) ‘(k − 1)) − A))) < ((x / 2) + (x / 2)) ↔ ((abs ‘((( + seq₁F) ‘k) − A)) + (abs ‘(A − (( + seq₁F) ‘(k − 1))))) < x))
111	102, 110	sylibd 202	. . . . . . . . . . . . . . 15 ⊢ (((k ∈ ℕ ⋀ 1 < k) ⋀ x ∈ ℝ) → (((abs ‘((( + seq₁F) ‘k) − A)) < (x / 2) ⋀ (abs ‘((( + seq₁F) ‘(k − 1)) − A)) < (x / 2)) → ((abs ‘((( + seq₁F) ‘k) − A)) + (abs ‘(A − (( + seq₁F) ‘(k − 1))))) < x))
112		abstrit 6855	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((( + seq₁F) ‘k) − A) ∈ ℂ ⋀ (A − (( + seq₁F) ‘(k − 1))) ∈ ℂ) → (abs ‘(((( + seq₁F) ‘k) − A) + (A − (( + seq₁F) ‘(k − 1))))) ≤ ((abs ‘((( + seq₁F) ‘k) − A)) + (abs ‘(A − (( + seq₁F) ‘(k − 1))))))
113	85	adantr 389	. . . . . . . . . . . . . . . . . . 19 ⊢ ((k ∈ ℕ ⋀ 1 < k) → ((( + seq₁F) ‘k) − A) ∈ ℂ)
114		subclt 5359	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((A ∈ ℂ ⋀ (( + seq₁F) ‘(k − 1)) ∈ ℂ) → (A − (( + seq₁F) ‘(k − 1))) ∈ ℂ)
115	29, 114	mpan 694	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((( + seq₁F) ‘(k − 1)) ∈ ℂ → (A − (( + seq₁F) ‘(k − 1))) ∈ ℂ)
116	94, 115	syl 10	. . . . . . . . . . . . . . . . . . 19 ⊢ ((k ∈ ℕ ⋀ 1 < k) → (A − (( + seq₁F) ‘(k − 1))) ∈ ℂ)
117	112, 113, 116	sylanc 471	. . . . . . . . . . . . . . . . . 18 ⊢ ((k ∈ ℕ ⋀ 1 < k) → (abs ‘(((( + seq₁F) ‘k) − A) + (A − (( + seq₁F) ‘(k − 1))))) ≤ ((abs ‘((( + seq₁F) ‘k) − A)) + (abs ‘(A − (( + seq₁F) ‘(k − 1))))))
118	117	adantr 389	. . . . . . . . . . . . . . . . 17 ⊢ (((k ∈ ℕ ⋀ 1 < k) ⋀ x ∈ ℝ) → (abs ‘(((( + seq₁F) ‘k) − A) + (A − (( + seq₁F) ‘(k − 1))))) ≤ ((abs ‘((( + seq₁F) ‘k) − A)) + (abs ‘(A − (( + seq₁F) ‘(k − 1))))))
119		lelttrt 5516	. . . . . . . . . . . . . . . . . 18 ⊢ (((abs ‘(((( + seq₁F) ‘k) − A) + (A − (( + seq₁F) ‘(k − 1))))) ∈ ℝ ⋀ ((abs ‘((( + seq₁F) ‘k) − A)) + (abs ‘(A − (( + seq₁F) ‘(k − 1))))) ∈ ℝ ⋀ x ∈ ℝ) → (((abs ‘(((( + seq₁F) ‘k) − A) + (A − (( + seq₁F) ‘(k − 1))))) ≤ ((abs ‘((( + seq₁F) ‘k) − A)) + (abs ‘(A − (( + seq₁F) ‘(k − 1))))) ⋀ ((abs ‘((( + seq₁F) ‘k) − A)) + (abs ‘(A − (( + seq₁F) ‘(k − 1))))) < x) → (abs ‘(((( + seq₁F) ‘k) − A) + (A − (( + seq₁F) ‘(k − 1))))) < x))
120		axaddcl 5263	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((( + seq₁F) ‘k) − A) ∈ ℂ ⋀ (A − (( + seq₁F) ‘(k − 1))) ∈ ℂ) → (((( + seq₁F) ‘k) − A) + (A − (( + seq₁F) ‘(k − 1)))) ∈ ℂ)
121	120, 113, 116	sylanc 471	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((k ∈ ℕ ⋀ 1 < k) → (((( + seq₁F) ‘k) − A) + (A − (( + seq₁F) ‘(k − 1)))) ∈ ℂ)
122		absclt 6788	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((( + seq₁F) ‘k) − A) + (A − (( + seq₁F) ‘(k − 1)))) ∈ ℂ → (abs ‘(((( + seq₁F) ‘k) − A) + (A − (( + seq₁F) ‘(k − 1))))) ∈ ℝ)
123	121, 122	syl 10	. . . . . . . . . . . . . . . . . . 19 ⊢ ((k ∈ ℕ ⋀ 1 < k) → (abs ‘(((( + seq₁F) ‘k) − A) + (A − (( + seq₁F) ‘(k − 1))))) ∈ ℝ)
124	123	adantr 389	. . . . . . . . . . . . . . . . . 18 ⊢ (((k ∈ ℕ ⋀ 1 < k) ⋀ x ∈ ℝ) → (abs ‘(((( + seq₁F) ‘k) − A) + (A − (( + seq₁F) ‘(k − 1))))) ∈ ℝ)
125		axaddrcl 5264	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((abs ‘((( + seq₁F) ‘k) − A)) ∈ ℝ ⋀ (abs ‘(A − (( + seq₁F) ‘(k − 1)))) ∈ ℝ) → ((abs ‘((( + seq₁F) ‘k) − A)) + (abs ‘(A − (( + seq₁F) ‘(k − 1))))) ∈ ℝ)
126		absclt 6788	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((A − (( + seq₁F) ‘(k − 1))) ∈ ℂ → (abs ‘(A − (( + seq₁F) ‘(k − 1)))) ∈ ℝ)
127	116, 126	syl 10	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((k ∈ ℕ ⋀ 1 < k) → (abs ‘(A − (( + seq₁F) ‘(k − 1)))) ∈ ℝ)
128	125, 88, 127	sylanc 471	. . . . . . . . . . . . . . . . . . 19 ⊢ ((k ∈ ℕ ⋀ 1 < k) → ((abs ‘((( + seq₁F) ‘k) − A)) + (abs ‘(A − (( + seq₁F) ‘(k − 1))))) ∈ ℝ)
129	128	adantr 389	. . . . . . . . . . . . . . . . . 18 ⊢ (((k ∈ ℕ ⋀ 1 < k) ⋀ x ∈ ℝ) → ((abs ‘((( + seq₁F) ‘k) − A)) + (abs ‘(A − (( + seq₁F) ‘(k − 1))))) ∈ ℝ)
130		pm3.27 323	. . . . . . . . . . . . . . . . . 18 ⊢ (((k ∈ ℕ ⋀ 1 < k) ⋀ x ∈ ℝ) → x ∈ ℝ)
131	119, 124, 129, 130	syl3anc 857	. . . . . . . . . . . . . . . . 17 ⊢ (((k ∈ ℕ ⋀ 1 < k) ⋀ x ∈ ℝ) → (((abs ‘(((( + seq₁F) ‘k) − A) + (A − (( + seq₁F) ‘(k − 1))))) ≤ ((abs ‘((( + seq₁F) ‘k) − A)) + (abs ‘(A − (( + seq₁F) ‘(k − 1))))) ⋀ ((abs ‘((( + seq₁F) ‘k) − A)) + (abs ‘(A − (( + seq₁F) ‘(k − 1))))) < x) → (abs ‘(((( + seq₁F) ‘k) − A) + (A − (( + seq₁F) ‘(k − 1))))) < x))
132	118, 131	mpand 700	. . . . . . . . . . . . . . . 16 ⊢ (((k ∈ ℕ ⋀ 1 < k) ⋀ x ∈ ℝ) → (((abs ‘((( + seq₁F) ‘k) − A)) + (abs ‘(A − (( + seq₁F) ‘(k − 1))))) < x → (abs ‘(((( + seq₁F) ‘k) − A) + (A − (( + seq₁F) ‘(k − 1))))) < x))
133		addex 5309	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ + ∈ V
134	133, 26	seq1m1 6276	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((k ∈ ℕ ⋀ 1 < k) → (( + seq₁F) ‘k) = ((( + seq₁F) ‘(k − 1)) + (F ‘k)))
135	134	eqcomd 1477	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((k ∈ ℕ ⋀ 1 < k) → ((( + seq₁F) ‘(k − 1)) + (F ‘k)) = (( + seq₁F) ‘k))
136		subaddt 5367	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((( + seq₁F) ‘k) ∈ ℂ ⋀ (( + seq₁F) ‘(k − 1)) ∈ ℂ ⋀ (F ‘k) ∈ ℂ) → (((( + seq₁F) ‘k) − (( + seq₁F) ‘(k − 1))) = (F ‘k) ↔ ((( + seq₁F) ‘(k − 1)) + (F ‘k)) = (( + seq₁F) ‘k)))
137	82	adantr 389	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((k ∈ ℕ ⋀ 1 < k) → (( + seq₁F) ‘k) ∈ ℂ)
138	18	adantr 389	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((k ∈ ℕ ⋀ 1 < k) → (F ‘k) ∈ ℂ)
139	136, 137, 94, 138	syl3anc 857	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((k ∈ ℕ ⋀ 1 < k) → (((( + seq₁F) ‘k) − (( + seq₁F) ‘(k − 1))) = (F ‘k) ↔ ((( + seq₁F) ‘(k − 1)) + (F ‘k)) = (( + seq₁F) ‘k)))
140	135, 139	mpbird 196	. . . . . . . . . . . . . . . . . . 19 ⊢ ((k ∈ ℕ ⋀ 1 < k) → ((( + seq₁F) ‘k) − (( + seq₁F) ‘(k − 1))) = (F ‘k))
141		npncant 5392	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((( + seq₁F) ‘k) ∈ ℂ ⋀ A ∈ ℂ ⋀ (( + seq₁F) ‘(k − 1)) ∈ ℂ) → (((( + seq₁F) ‘k) − A) + (A − (( + seq₁F) ‘(k − 1)))) = ((( + seq₁F) ‘k) − (( + seq₁F) ‘(k − 1))))
142	29, 141	mp3an2 902	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((( + seq₁F) ‘k) ∈ ℂ ⋀ (( + seq₁F) ‘(k − 1)) ∈ ℂ) → (((( + seq₁F) ‘k) − A) + (A − (( + seq₁F) ‘(k − 1)))) = ((( + seq₁F) ‘k) − (( + seq₁F) ‘(k − 1))))
143	142, 137, 94	sylanc 471	. . . . . . . . . . . . . . . . . . 19 ⊢ ((k ∈ ℕ ⋀ 1 < k) → (((( + seq₁F) ‘k) − A) + (A − (( + seq₁F) ‘(k − 1)))) = ((( + seq₁F) ‘k) − (( + seq₁F) ‘(k − 1))))
144		subid1t 5388	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((F ‘k) ∈ ℂ → ((F ‘k) − 0) = (F ‘k))
145	18, 144	syl 10	. . . . . . . . . . . . . . . . . . . 20 ⊢ (k ∈ ℕ → ((F ‘k) − 0) = (F ‘k))
146	145	adantr 389	. . . . . . . . . . . . . . . . . . 19 ⊢ ((k ∈ ℕ ⋀ 1 < k) → ((F ‘k) − 0) = (F ‘k))
147	140, 143, 146	3eqtr4d 1514	. . . . . . . . . . . . . . . . . 18 ⊢ ((k ∈ ℕ ⋀ 1 < k) → (((( + seq₁F) ‘k) − A) + (A − (( + seq₁F) ‘(k − 1)))) = ((F ‘k) − 0))
148	147	fveq2d 3730	. . . . . . . . . . . . . . . . 17 ⊢ ((k ∈ ℕ ⋀ 1 < k) → (abs ‘(((( + seq₁F) ‘k) − A) + (A − (( + seq₁F) ‘(k − 1))))) = (abs ‘((F ‘k) − 0)))
149		equid 1124	. . . . . . . . . . . . . . . . . 18 ⊢ x = x
150	149	a1i 8	. . . . . . . . . . . . . . . . 17 ⊢ (x ∈ ℝ → x = x)
151	148, 150	breqan12d 2628	. . . . . . . . . . . . . . . 16 ⊢ (((k ∈ ℕ ⋀ 1 < k) ⋀ x ∈ ℝ) → ((abs ‘(((( + seq₁F) ‘k) − A) + (A − (( + seq₁F) ‘(k − 1))))) < x ↔ (abs ‘((F ‘k) − 0)) < x))
152	132, 151	sylibd 202	. . . . . . . . . . . . . . 15 ⊢ (((k ∈ ℕ ⋀ 1 < k) ⋀ x ∈ ℝ) → (((abs ‘((( + seq₁F) ‘k) − A)) + (abs ‘(A − (( + seq₁F) ‘(k − 1))))) < x → (abs ‘((F ‘k) − 0)) < x))
153	111, 152	syld 27	. . . . . . . . . . . . . 14 ⊢ (((k ∈ ℕ ⋀ 1 < k) ⋀ x ∈ ℝ) → (((abs ‘((( + seq₁F) ‘k) − A)) < (x / 2) ⋀ (abs ‘((( + seq₁F) ‘(k − 1)) − A)) < (x / 2)) → (abs ‘((F ‘k) − 0)) < x))
154		zltp1let 6148	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℤ ⋀ k ∈ ℤ) → (1 < k ↔ (1 + 1) ≤ k))
155	3, 154	mpan 694	. . . . . . . . . . . . . . . . . . 19 ⊢ (k ∈ ℤ → (1 < k ↔ (1 + 1) ≤ k))
156		df-2 5937	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 = (1 + 1)
157	156	breq1i 2622	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 ≤ k ↔ (1 + 1) ≤ k)
158	155, 157	syl6bbr 537	. . . . . . . . . . . . . . . . . 18 ⊢ (k ∈ ℤ → (1 < k ↔ 2 ≤ k))
159		ltlet 5513	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℝ ⋀ k ∈ ℝ) → (1 < k → 1 ≤ k))
160	6, 159	mpan 694	. . . . . . . . . . . . . . . . . . 19 ⊢ (k ∈ ℝ → (1 < k → 1 ≤ k))
161	49, 160	syl 10	. . . . . . . . . . . . . . . . . 18 ⊢ (k ∈ ℤ → (1 < k → 1 ≤ k))
162	158, 161	sylbird 205	. . . . . . . . . . . . . . . . 17 ⊢ (k ∈ ℤ → (2 ≤ k → 1 ≤ k))
163	162	imdistani 443	. . . . . . . . . . . . . . . 16 ⊢ ((k ∈ ℤ ⋀ 2 ≤ k) → (k ∈ ℤ ⋀ 1 ≤ k))
164		elnnz1 6122	. . . . . . . . . . . . . . . 16 ⊢ (k ∈ ℕ ↔ (k ∈ ℤ ⋀ 1 ≤ k))
165	163, 164	sylibr 200	. . . . . . . . . . . . . . 15 ⊢ ((k ∈ ℤ ⋀ 2 ≤ k) → k ∈ ℕ)
166	158	biimpar 417	. . . . . . . . . . . . . . 15 ⊢ ((k ∈ ℤ ⋀ 2 ≤ k) → 1 < k)
167	165, 166	jca 288	. . . . . . . . . . . . . 14 ⊢ ((k ∈ ℤ ⋀ 2 ≤ k) → (k ∈ ℕ ⋀ 1 < k))
168	153, 167	sylan 448	. . . . . . . . . . . . 13 ⊢ (((k ∈ ℤ ⋀ 2 ≤ k) ⋀ x ∈ ℝ) → (((abs ‘((( + seq₁F) ‘k) − A)) < (x / 2) ⋀ (abs ‘((( + seq₁F) ‘(k − 1)) − A)) < (x / 2)) → (abs ‘((F ‘k) − 0)) < x))
169	168	adantrr 395	. . . . . . . . . . . 12 ⊢ (((k ∈ ℤ ⋀ 2 ≤ k) ⋀ (x ∈ ℝ ⋀ (m ∈ ℤ ⋀ ∀n ∈ ℤ (m ≤ n → (abs ‘((( + seq₁F) ‘n) − A)) < (x / 2))))) → (((abs ‘((( + seq₁F) ‘k) − A)) < (x / 2) ⋀ (abs ‘((( + seq₁F) ‘(k − 1)) − A)) < (x / 2)) → (abs ‘((F ‘k) − 0)) < x))
170	80, 169	syld 27	. . . . . . . . . . 11 ⊢ (((k ∈ ℤ ⋀ 2 ≤ k) ⋀ (x ∈ ℝ ⋀ (m ∈ ℤ ⋀ ∀n ∈ ℤ (m ≤ n → (abs ‘((( + seq₁F) ‘n) − A)) < (x / 2))))) → ((m + 1) ≤ k → (abs ‘((F ‘k) − 0)) < x))
171	170	expcom 374	. . . . . . . . . 10 ⊢ ((x ∈ ℝ ⋀ (m ∈ ℤ ⋀ ∀n ∈ ℤ (m ≤ n → (abs ‘((( + seq₁F) ‘n) − A)) < (x / 2)))) → ((k ∈ ℤ ⋀ 2 ≤ k) → ((m + 1) ≤ k → (abs ‘((F ‘k) − 0)) < x)))
172	5	eluz1 6374	. . . . . . . . . 10 ⊢ (k ∈ (ℤ_≥ ‘2) ↔ (k ∈ ℤ ⋀ 2 ≤ k))
173	171, 172	syl5ib 206	. . . . . . . . 9 ⊢ ((x ∈ ℝ ⋀ (m ∈ ℤ ⋀ ∀n ∈ ℤ (m ≤ n → (abs ‘((( + seq₁F) ‘n) − A)) < (x / 2)))) → (k ∈ (ℤ_≥ ‘2) → ((m + 1) ≤ k → (abs ‘((F ‘k) − 0)) < x)))
174	173	r19.21aiv 1710	. . . . . . . 8 ⊢ ((x ∈ ℝ ⋀ (m ∈ ℤ ⋀ ∀n ∈ ℤ (m ≤ n → (abs ‘((( + seq₁F) ‘n) − A)) < (x / 2)))) → ∀k ∈ (ℤ_≥ ‘2)((m + 1) ≤ k → (abs ‘((F ‘k) − 0)) < x))
175	43, 45, 174	sylanc 471	. . . . . . 7 ⊢ ((x ∈ ℝ ⋀ (m ∈ ℤ ⋀ ∀n ∈ ℤ (m ≤ n → (abs ‘((( + seq₁F) ‘n) − A)) < (x / 2)))) → ∃j ∈ ℤ ∀k ∈ (ℤ_≥ ‘2)(j ≤ k → (abs ‘((F ‘k) − 0)) < x))
176	175	exp32 377	. . . . . 6 ⊢ (x ∈ ℝ → (m ∈ ℤ → (∀n ∈ ℤ (m ≤ n → (abs ‘((( + seq₁F) ‘n) − A)) < (x / 2)) → ∃j ∈ ℤ ∀k ∈ (ℤ_≥ ‘2)(j ≤ k → (abs ‘((F ‘k) − 0)) < x))))
177	176	r19.23adv 1743	. . . . 5 ⊢ (x ∈ ℝ → (∃m ∈ ℤ ∀n ∈ ℤ (m ≤ n → (abs ‘((( + seq₁F) ‘n) − A)) < (x / 2)) → ∃j ∈ ℤ ∀k ∈ (ℤ_≥ ‘2)(j ≤ k → (abs ‘((F ‘k) − 0)) < x)))
178	177	adantr 389	. . . 4 ⊢ ((x ∈ ℝ ⋀ 0 < x) → (&e