2climnn0 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem 2climnn0 7103

Description: If two sequences converge to each other, they converge to the same limit.

**Hypothesis**
Ref	Expression
2climnn.1	⊢ G ∈ V

**Assertion**
Ref	Expression
2climnn0	⊢ (((A ∈ ℂ ⋀ ∀k ∈ ℕ₀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) ⋀ (∀x ∈ ℝ (0 < x → ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − (F ‘k))) < x)) ⋀ F ⇝ A)) → G ⇝ A)

Distinct variable groups: x,k,j,A j,F,k,x x,G,k,j

**Proof of Theorem 2climnn0**
Step	Hyp	Ref	Expression
1		rehalfclt 6036	. . . . . . 7 ⊢ (y ∈ ℝ → (y / 2) ∈ ℝ)
2		breq2 2628	. . . . . . . . 9 ⊢ (x = (y / 2) → (0 < x ↔ 0 < (y / 2)))
3		opreq12 3976	. . . . . . . . . . . . 13 ⊢ ((x = (y / 2) ⋀ x = (y / 2)) → (x + x) = ((y / 2) + (y / 2)))
4	3	anidms 436	. . . . . . . . . . . 12 ⊢ (x = (y / 2) → (x + x) = ((y / 2) + (y / 2)))
5	4	breq2d 2635	. . . . . . . . . . 11 ⊢ (x = (y / 2) → ((abs ‘((G ‘k) − A)) < (x + x) ↔ (abs ‘((G ‘k) − A)) < ((y / 2) + (y / 2))))
6	5	imbi2d 614	. . . . . . . . . 10 ⊢ (x = (y / 2) → ((j ≤ k → (abs ‘((G ‘k) − A)) < (x + x)) ↔ (j ≤ k → (abs ‘((G ‘k) − A)) < ((y / 2) + (y / 2)))))
7	6	rexralbidv 1685	. . . . . . . . 9 ⊢ (x = (y / 2) → (∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − A)) < (x + x)) ↔ ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − A)) < ((y / 2) + (y / 2)))))
8	2, 7	imbi12d 628	. . . . . . . 8 ⊢ (x = (y / 2) → ((0 < x → ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − A)) < (x + x))) ↔ (0 < (y / 2) → ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − A)) < ((y / 2) + (y / 2))))))
9	8	rcla4v 1876	. . . . . . 7 ⊢ ((y / 2) ∈ ℝ → (∀x ∈ ℝ (0 < x → ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − A)) < (x + x))) → (0 < (y / 2) → ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − A)) < ((y / 2) + (y / 2))))))
10	1, 9	syl 10	. . . . . 6 ⊢ (y ∈ ℝ → (∀x ∈ ℝ (0 < x → ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − A)) < (x + x))) → (0 < (y / 2) → ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − A)) < ((y / 2) + (y / 2))))))
11		0z 6148	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℤ
12		nn0uz 6439	. . . . . . . . . . . . . . . . 17 ⊢ ℕ₀ = (ℤ_≥ ‘0)
13	12	eqimss2i 2115	. . . . . . . . . . . . . . . 16 ⊢ (ℤ_≥ ‘0) ⊆ ℕ₀
14		nn0ssz 6154	. . . . . . . . . . . . . . . 16 ⊢ ℕ₀ ⊆ ℤ
15	11, 13, 14	clmi2 7087	. . . . . . . . . . . . . . 15 ⊢ (((A ∈ ℂ ⋀ F ⇝ A) ⋀ (x ∈ ℝ ⋀ 0 < x)) → ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((F ‘k) − A)) < x))
16	15	adantllr 399	. . . . . . . . . . . . . 14 ⊢ ((((A ∈ ℂ ⋀ ∀k ∈ ℕ₀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) ⋀ F ⇝ A) ⋀ (x ∈ ℝ ⋀ 0 < x)) → ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((F ‘k) − A)) < x))
17	16	anassrs 443	. . . . . . . . . . . . 13 ⊢ (((((A ∈ ℂ ⋀ ∀k ∈ ℕ₀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) ⋀ F ⇝ A) ⋀ x ∈ ℝ) ⋀ 0 < x) → ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((F ‘k) − A)) < x))
18		lt2addt 5655	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((abs ‘((G ‘k) − (F ‘k))) ∈ ℝ ⋀ (abs ‘((F ‘k) − A)) ∈ ℝ) ⋀ (x ∈ ℝ ⋀ x ∈ ℝ)) → (((abs ‘((G ‘k) − (F ‘k))) < x ⋀ (abs ‘((F ‘k) − A)) < x) → ((abs ‘((G ‘k) − (F ‘k))) + (abs ‘((F ‘k) − A))) < (x + x)))
19		subclt 5379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((G ‘k) ∈ ℂ ⋀ (F ‘k) ∈ ℂ) → ((G ‘k) − (F ‘k)) ∈ ℂ)
20	19	ancoms 438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ) → ((G ‘k) − (F ‘k)) ∈ ℂ)
21		absclt 6833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((G ‘k) − (F ‘k)) ∈ ℂ → (abs ‘((G ‘k) − (F ‘k))) ∈ ℝ)
22	20, 21	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ) → (abs ‘((G ‘k) − (F ‘k))) ∈ ℝ)
23	22	adantl 390	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((A ∈ ℂ ⋀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) → (abs ‘((G ‘k) − (F ‘k))) ∈ ℝ)
24		subclt 5379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((F ‘k) ∈ ℂ ⋀ A ∈ ℂ) → ((F ‘k) − A) ∈ ℂ)
25	24	ancoms 438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((A ∈ ℂ ⋀ (F ‘k) ∈ ℂ) → ((F ‘k) − A) ∈ ℂ)
26		absclt 6833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((F ‘k) − A) ∈ ℂ → (abs ‘((F ‘k) − A)) ∈ ℝ)
27	25, 26	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((A ∈ ℂ ⋀ (F ‘k) ∈ ℂ) → (abs ‘((F ‘k) − A)) ∈ ℝ)
28	27	adantrr 397	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((A ∈ ℂ ⋀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) → (abs ‘((F ‘k) − A)) ∈ ℝ)
29	23, 28	jca 288	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((A ∈ ℂ ⋀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) → ((abs ‘((G ‘k) − (F ‘k))) ∈ ℝ ⋀ (abs ‘((F ‘k) − A)) ∈ ℝ))
30	29	adantlr 395	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((A ∈ ℂ ⋀ x ∈ ℝ) ⋀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) → ((abs ‘((G ‘k) − (F ‘k))) ∈ ℝ ⋀ (abs ‘((F ‘k) − A)) ∈ ℝ))
31		pm3.2 283	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (x ∈ ℝ → (x ∈ ℝ → (x ∈ ℝ ⋀ x ∈ ℝ)))
32	31	pm2.43i 64	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (x ∈ ℝ → (x ∈ ℝ ⋀ x ∈ ℝ))
33	32	ad2antlr 407	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((A ∈ ℂ ⋀ x ∈ ℝ) ⋀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) → (x ∈ ℝ ⋀ x ∈ ℝ))
34	18, 30, 33	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((A ∈ ℂ ⋀ x ∈ ℝ) ⋀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) → (((abs ‘((G ‘k) − (F ‘k))) < x ⋀ (abs ‘((F ‘k) − A)) < x) → ((abs ‘((G ‘k) − (F ‘k))) + (abs ‘((F ‘k) − A))) < (x + x)))
35		npncant 5412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((G ‘k) ∈ ℂ ⋀ (F ‘k) ∈ ℂ ⋀ A ∈ ℂ) → (((G ‘k) − (F ‘k)) + ((F ‘k) − A)) = ((G ‘k) − A))
36	35	3com13 840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((A ∈ ℂ ⋀ (F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ) → (((G ‘k) − (F ‘k)) + ((F ‘k) − A)) = ((G ‘k) − A))
37	36	3expb 836	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((A ∈ ℂ ⋀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) → (((G ‘k) − (F ‘k)) + ((F ‘k) − A)) = ((G ‘k) − A))
38	37	fveq2d 3734	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((A ∈ ℂ ⋀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) → (abs ‘(((G ‘k) − (F ‘k)) + ((F ‘k) − A))) = (abs ‘((G ‘k) − A)))
39		abstrit 6898	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((G ‘k) − (F ‘k)) ∈ ℂ ⋀ ((F ‘k) − A) ∈ ℂ) → (abs ‘(((G ‘k) − (F ‘k)) + ((F ‘k) − A))) ≤ ((abs ‘((G ‘k) − (F ‘k))) + (abs ‘((F ‘k) − A))))
40	20	adantl 390	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((A ∈ ℂ ⋀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) → ((G ‘k) − (F ‘k)) ∈ ℂ)
41	25	adantrr 397	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((A ∈ ℂ ⋀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) → ((F ‘k) − A) ∈ ℂ)
42	39, 40, 41	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((A ∈ ℂ ⋀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) → (abs ‘(((G ‘k) − (F ‘k)) + ((F ‘k) − A))) ≤ ((abs ‘((G ‘k) − (F ‘k))) + (abs ‘((F ‘k) − A))))
43	38, 42	eqbrtrrd 2642	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((A ∈ ℂ ⋀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) → (abs ‘((G ‘k) − A)) ≤ ((abs ‘((G ‘k) − (F ‘k))) + (abs ‘((F ‘k) − A))))
44	43	adantlr 395	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((A ∈ ℂ ⋀ x ∈ ℝ) ⋀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) → (abs ‘((G ‘k) − A)) ≤ ((abs ‘((G ‘k) − (F ‘k))) + (abs ‘((F ‘k) − A))))
45		lelttrt 5535	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((abs ‘((G ‘k) − A)) ∈ ℝ ⋀ ((abs ‘((G ‘k) − (F ‘k))) + (abs ‘((F ‘k) − A))) ∈ ℝ ⋀ (x + x) ∈ ℝ) → (((abs ‘((G ‘k) − A)) ≤ ((abs ‘((G ‘k) − (F ‘k))) + (abs ‘((F ‘k) − A))) ⋀ ((abs ‘((G ‘k) − (F ‘k))) + (abs ‘((F ‘k) − A))) < (x + x)) → (abs ‘((G ‘k) − A)) < (x + x)))
46		subclt 5379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((G ‘k) ∈ ℂ ⋀ A ∈ ℂ) → ((G ‘k) − A) ∈ ℂ)
47	46	ancoms 438	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((A ∈ ℂ ⋀ (G ‘k) ∈ ℂ) → ((G ‘k) − A) ∈ ℂ)
48		absclt 6833	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((G ‘k) − A) ∈ ℂ → (abs ‘((G ‘k) − A)) ∈ ℝ)
49	47, 48	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((A ∈ ℂ ⋀ (G ‘k) ∈ ℂ) → (abs ‘((G ‘k) − A)) ∈ ℝ)
50	49	ad2ant2rl 413	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((A ∈ ℂ ⋀ x ∈ ℝ) ⋀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) → (abs ‘((G ‘k) − A)) ∈ ℝ)
51		axaddrcl 5284	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((abs ‘((G ‘k) − (F ‘k))) ∈ ℝ ⋀ (abs ‘((F ‘k) − A)) ∈ ℝ) → ((abs ‘((G ‘k) − (F ‘k))) + (abs ‘((F ‘k) − A))) ∈ ℝ)
52	51, 23, 28	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((A ∈ ℂ ⋀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) → ((abs ‘((G ‘k) − (F ‘k))) + (abs ‘((F ‘k) − A))) ∈ ℝ)
53	52	adantlr 395	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((A ∈ ℂ ⋀ x ∈ ℝ) ⋀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) → ((abs ‘((G ‘k) − (F ‘k))) + (abs ‘((F ‘k) − A))) ∈ ℝ)
54		axaddrcl 5284	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((x ∈ ℝ ⋀ x ∈ ℝ) → (x + x) ∈ ℝ)
55	54	anidms 436	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (x ∈ ℝ → (x + x) ∈ ℝ)
56	55	ad2antlr 407	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((A ∈ ℂ ⋀ x ∈ ℝ) ⋀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) → (x + x) ∈ ℝ)
57	45, 50, 53, 56	syl3anc 860	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((A ∈ ℂ ⋀ x ∈ ℝ) ⋀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) → (((abs ‘((G ‘k) − A)) ≤ ((abs ‘((G ‘k) − (F ‘k))) + (abs ‘((F ‘k) − A))) ⋀ ((abs ‘((G ‘k) − (F ‘k))) + (abs ‘((F ‘k) − A))) < (x + x)) → (abs ‘((G ‘k) − A)) < (x + x)))
58	44, 57	mpand 703	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((A ∈ ℂ ⋀ x ∈ ℝ) ⋀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) → (((abs ‘((G ‘k) − (F ‘k))) + (abs ‘((F ‘k) − A))) < (x + x) → (abs ‘((G ‘k) − A)) < (x + x)))
59	34, 58	syld 27	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((A ∈ ℂ ⋀ x ∈ ℝ) ⋀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) → (((abs ‘((G ‘k) − (F ‘k))) < x ⋀ (abs ‘((F ‘k) − A)) < x) → (abs ‘((G ‘k) − A)) < (x + x)))
60	59	imim2d 25	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((A ∈ ℂ ⋀ x ∈ ℝ) ⋀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) → ((j ≤ k → ((abs ‘((G ‘k) − (F ‘k))) < x ⋀ (abs ‘((F ‘k) − A)) < x)) → (j ≤ k → (abs ‘((G ‘k) − A)) < (x + x))))
61	60	ex 373	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((A ∈ ℂ ⋀ x ∈ ℝ) → (((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ) → ((j ≤ k → ((abs ‘((G ‘k) − (F ‘k))) < x ⋀ (abs ‘((F ‘k) − A)) < x)) → (j ≤ k → (abs ‘((G ‘k) − A)) < (x + x)))))
62	61	r19.20sdv 1713	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((A ∈ ℂ ⋀ x ∈ ℝ) → (∀k ∈ ℕ₀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ) → ∀k ∈ ℕ₀ ((j ≤ k → ((abs ‘((G ‘k) − (F ‘k))) < x ⋀ (abs ‘((F ‘k) − A)) < x)) → (j ≤ k → (abs ‘((G ‘k) − A)) < (x + x)))))
63	62	imp 350	. . . . . . . . . . . . . . . . . . 19 ⊢ (((A ∈ ℂ ⋀ x ∈ ℝ) ⋀ ∀k ∈ ℕ₀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) → ∀k ∈ ℕ₀ ((j ≤ k → ((abs ‘((G ‘k) − (F ‘k))) < x ⋀ (abs ‘((F ‘k) − A)) < x)) → (j ≤ k → (abs ‘((G ‘k) − A)) < (x + x))))
64	63	an1rs 491	. . . . . . . . . . . . . . . . . 18 ⊢ (((A ∈ ℂ ⋀ ∀k ∈ ℕ₀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) ⋀ x ∈ ℝ) → ∀k ∈ ℕ₀ ((j ≤ k → ((abs ‘((G ‘k) − (F ‘k))) < x ⋀ (abs ‘((F ‘k) − A)) < x)) → (j ≤ k → (abs ‘((G ‘k) − A)) < (x + x))))
65		r19.20 1705	. . . . . . . . . . . . . . . . . 18 ⊢ (∀k ∈ ℕ₀ ((j ≤ k → ((abs ‘((G ‘k) − (F ‘k))) < x ⋀ (abs ‘((F ‘k) − A)) < x)) → (j ≤ k → (abs ‘((G ‘k) − A)) < (x + x))) → (∀k ∈ ℕ₀ (j ≤ k → ((abs ‘((G ‘k) − (F ‘k))) < x ⋀ (abs ‘((F ‘k) − A)) < x)) → ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − A)) < (x + x))))
66	64, 65	syl 10	. . . . . . . . . . . . . . . . 17 ⊢ (((A ∈ ℂ ⋀ ∀k ∈ ℕ₀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) ⋀ x ∈ ℝ) → (∀k ∈ ℕ₀ (j ≤ k → ((abs ‘((G ‘k) − (F ‘k))) < x ⋀ (abs ‘((F ‘k) − A)) < x)) → ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − A)) < (x + x))))
67	66	adantlr 395	. . . . . . . . . . . . . . . 16 ⊢ ((((A ∈ ℂ ⋀ ∀k ∈ ℕ₀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) ⋀ F ⇝ A) ⋀ x ∈ ℝ) → (∀k ∈ ℕ₀ (j ≤ k → ((abs ‘((G ‘k) − (F ‘k))) < x ⋀ (abs ‘((F ‘k) − A)) < x)) → ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − A)) < (x + x))))
68	67	adantr 391	. . . . . . . . . . . . . . 15 ⊢ (((((A ∈ ℂ ⋀ ∀k ∈ ℕ₀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) ⋀ F ⇝ A) ⋀ x ∈ ℝ) ⋀ 0 < x) → (∀k ∈ ℕ₀ (j ≤ k → ((abs ‘((G ‘k) − (F ‘k))) < x ⋀ (abs ‘((F ‘k) − A)) < x)) → ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − A)) < (x + x))))
69	68	r19.22sdv 1741	. . . . . . . . . . . . . 14 ⊢ (((((A ∈ ℂ ⋀ ∀k ∈ ℕ₀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) ⋀ F ⇝ A) ⋀ x ∈ ℝ) ⋀ 0 < x) → (∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → ((abs ‘((G ‘k) − (F ‘k))) < x ⋀ (abs ‘((F ‘k) − A)) < x)) → ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − A)) < (x + x))))
70	11, 12	cvganuz 6925	. . . . . . . . . . . . . 14 ⊢ ((∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − (F ‘k))) < x) ⋀ ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((F ‘k) − A)) < x)) ↔ ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → ((abs ‘((G ‘k) − (F ‘k))) < x ⋀ (abs ‘((F ‘k) − A)) < x)))
71	69, 70	syl5ib 206	. . . . . . . . . . . . 13 ⊢ (((((A ∈ ℂ ⋀ ∀k ∈ ℕ₀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) ⋀ F ⇝ A) ⋀ x ∈ ℝ) ⋀ 0 < x) → ((∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − (F ‘k))) < x) ⋀ ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((F ‘k) − A)) < x)) → ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − A)) < (x + x))))
72	17, 71	mpan2d 704	. . . . . . . . . . . 12 ⊢ (((((A ∈ ℂ ⋀ ∀k ∈ ℕ₀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) ⋀ F ⇝ A) ⋀ x ∈ ℝ) ⋀ 0 < x) → (∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − (F ‘k))) < x) → ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − A)) < (x + x))))
73	72	ex 373	. . . . . . . . . . 11 ⊢ ((((A ∈ ℂ ⋀ ∀k ∈ ℕ₀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) ⋀ F ⇝ A) ⋀ x ∈ ℝ) → (0 < x → (∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − (F ‘k))) < x) → ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − A)) < (x + x)))))
74	73	a2d 13	. . . . . . . . . 10 ⊢ ((((A ∈ ℂ ⋀ ∀k ∈ ℕ₀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) ⋀ F ⇝ A) ⋀ x ∈ ℝ) → ((0 < x → ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − (F ‘k))) < x)) → (0 < x → ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − A)) < (x + x)))))
75	74	r19.20dva 1712	. . . . . . . . 9 ⊢ (((A ∈ ℂ ⋀ ∀k ∈ ℕ₀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) ⋀ F ⇝ A) → (∀x ∈ ℝ (0 < x → ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − (F ‘k))) < x)) → ∀x ∈ ℝ (0 < x → ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − A)) < (x + x)))))
76	75	ex 373	. . . . . . . 8 ⊢ ((A ∈ ℂ ⋀ ∀k ∈ ℕ₀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) → (F ⇝ A → (∀x ∈ ℝ (0 < x → ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − (F ‘k))) < x)) → ∀x ∈ ℝ (0 < x → ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − A)) < (x + x))))))
77	76	com23 32	. . . . . . 7 ⊢ ((A ∈ ℂ ⋀ ∀k ∈ ℕ₀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) → (∀x ∈ ℝ (0 < x → ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − (F ‘k))) < x)) → (F ⇝ A → ∀x ∈ ℝ (0 < x → ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − A)) < (x + x))))))
78	77	imp32 363	. . . . . 6 ⊢ (((A ∈ ℂ ⋀ ∀k ∈ ℕ₀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) ⋀ (∀x ∈ ℝ (0 < x → ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − (F ‘k))) < x)) ⋀ F ⇝ A)) → ∀x ∈ ℝ (0 < x → ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − A)) < (x + x))))
79	10, 78	syl5 21	. . . . 5 ⊢ (y ∈ ℝ → (((A ∈ ℂ ⋀ ∀k ∈ ℕ₀ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) ⋀ (∀x ∈ ℝ (0 < x → ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − (F ‘k))) < x)) ⋀ F ⇝ A)) → (0 < (y / 2) → ∃j ∈ ℕ₀ ∀k ∈ ℕ₀ (j ≤ k → (abs ‘((G ‘k) − A)) < ((y / 2) + (y / 2))))))
80		halfpos2t 6039	. . . . . . 7 ⊢ (y ∈ ℝ → (0 < y ↔ 0 < (y / 2)))
81	80	bicomd 523	. . . . . 6 ⊢ (y ∈ ℝ → (0 < (y / 2) ↔ 0 < y))
82		recnt 5325	. . . . . . . . . 10 ⊢ (y ∈ ℝ → y ∈ ℂ)
83		2halvest 6041	. . . . . . . . . 10 ⊢ (y ∈ ℂ → ((y / 2) + (y / 2)) = y)
84	82, 83	syl 10	. . . . . . . . 9 ⊢ (y ∈ ℝ → ((y / 2) + (y / 2)) = y)
85	84	breq2d 2635	. . . . . . . 8 ⊢ (y ∈ ℝ → ((abs ‘((G ‘k) − A)) < ((y / 2) + (y / 2)) ↔ (abs ‘((G ‘k) − A)) < y))
86	85	imbi2d 614	. . . . . . 7 ⊢ (y ∈ ℝ → ((j ≤ k → (abs ‘((G ‘k) − A)) < ((y / 2) + (y / 2))) ↔ (j ≤ k → (abs ‘((G ‘