2clim

Description: If two sequences converge to each other, they converge to the same limit. (Contributed by NM, 24-Dec-2005) (Proof shortened by Mario Carneiro, 31-Jan-2014)

	Ref	Expression
Hypotheses	2clim.1	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
	2clim.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	2clim.3	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
	2clim.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
	2clim.6	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) < 𝑥 )
	2clim.7	⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
Assertion	2clim	⊢ ( 𝜑 → 𝐺 ⇝ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		2clim.1	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
2		2clim.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		2clim.3	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
4		2clim.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
5		2clim.6	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) < 𝑥 )
6		2clim.7	⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
7		rphalfcl	⊢ ( 𝑦 ∈ ℝ⁺ → ( 𝑦 / 2 ) ∈ ℝ⁺ )
8		breq2	⊢ ( 𝑥 = ( 𝑦 / 2 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) < ( 𝑦 / 2 ) ) )
9	8	rexralbidv	⊢ ( 𝑥 = ( 𝑦 / 2 ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) < 𝑥 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) < ( 𝑦 / 2 ) ) )
10	9	rspccva	⊢ ( ( ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) < 𝑥 ∧ ( 𝑦 / 2 ) ∈ ℝ⁺ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) < ( 𝑦 / 2 ) )
11	5 7 10	syl2an	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) < ( 𝑦 / 2 ) )
12	2	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → 𝑀 ∈ ℤ )
13	7	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → ( 𝑦 / 2 ) ∈ ℝ⁺ )
14		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
15	6	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → 𝐹 ⇝ 𝐴 )
16	1 12 13 14 15	climi	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( 𝑦 / 2 ) ) )
17	1	rexanuz2	⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) < ( 𝑦 / 2 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( 𝑦 / 2 ) ) ) ↔ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) < ( 𝑦 / 2 ) ∧ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( 𝑦 / 2 ) ) ) )
18	11 16 17	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) < ( 𝑦 / 2 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( 𝑦 / 2 ) ) ) )
19	1	uztrn2	⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
20		an12	⊢ ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) < ( 𝑦 / 2 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( 𝑦 / 2 ) ) ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) < ( 𝑦 / 2 ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( 𝑦 / 2 ) ) ) )
21		simprr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑘 ∈ 𝑍 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
22	4	ad2ant2r	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑘 ∈ 𝑍 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
23	21 22	abssubd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑘 ∈ 𝑍 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑘 ) ) ) )
24	23	breq1d	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑘 ∈ 𝑍 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) < ( 𝑦 / 2 ) ↔ ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑘 ) ) ) < ( 𝑦 / 2 ) ) )
25	24	anbi1d	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑘 ∈ 𝑍 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) → ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) < ( 𝑦 / 2 ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( 𝑦 / 2 ) ) ↔ ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑘 ) ) ) < ( 𝑦 / 2 ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( 𝑦 / 2 ) ) ) )
26		climcl	⊢ ( 𝐹 ⇝ 𝐴 → 𝐴 ∈ ℂ )
27	6 26	syl	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
28	27	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑘 ∈ 𝑍 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) → 𝐴 ∈ ℂ )
29		rpre	⊢ ( 𝑦 ∈ ℝ⁺ → 𝑦 ∈ ℝ )
30	29	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑘 ∈ 𝑍 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) → 𝑦 ∈ ℝ )
31		abs3lem	⊢ ( ( ( ( 𝐺 ‘ 𝑘 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ 𝑦 ∈ ℝ ) ) → ( ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑘 ) ) ) < ( 𝑦 / 2 ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( 𝑦 / 2 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) )
32	22 28 21 30 31	syl22anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑘 ∈ 𝑍 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) → ( ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑘 ) ) ) < ( 𝑦 / 2 ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( 𝑦 / 2 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) )
33	25 32	sylbid	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑘 ∈ 𝑍 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) → ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) < ( 𝑦 / 2 ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( 𝑦 / 2 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) )
34	33	anassrs	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) < ( 𝑦 / 2 ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( 𝑦 / 2 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) )
35	34	expimpd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) < ( 𝑦 / 2 ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( 𝑦 / 2 ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) )
36	20 35	biimtrid	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) < ( 𝑦 / 2 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( 𝑦 / 2 ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) )
37	19 36	sylan2	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ) ) → ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) < ( 𝑦 / 2 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( 𝑦 / 2 ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) )
38	37	anassrs	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ) → ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) < ( 𝑦 / 2 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( 𝑦 / 2 ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) )
39	38	ralimdva	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) < ( 𝑦 / 2 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( 𝑦 / 2 ) ) ) → ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) )
40	39	reximdva	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐺 ‘ 𝑘 ) ) ) < ( 𝑦 / 2 ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( 𝑦 / 2 ) ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) )
41	18 40	mpd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 )
42	41	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 )
43		eqidd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
44	1 2 3 43 27 4	clim2c	⊢ ( 𝜑 → ( 𝐺 ⇝ 𝐴 ↔ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) )
45	42 44	mpbird	⊢ ( 𝜑 → 𝐺 ⇝ 𝐴 )

Metamath Proof Explorer

Theorem 2clim

Proof