Theorem 2clim 15569

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.)

Hypotheses

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

Assertion

Ref	Expression
2clim	⊢ (𝜑 → 𝐺 ⇝ 𝐴)

Distinct variable groups:   𝑗,𝑘,𝐴   𝑥,𝑗,𝐹,𝑘   𝑗,𝐺,𝑥   𝑗,𝑀   𝜑,𝑗,𝑘   𝑗,𝑍,𝑘,𝑥   𝑘,𝐺

Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)   𝑀(𝑥,𝑘)   𝑉(𝑥,𝑗,𝑘)

Proof of Theorem 2clim

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		2clim.6	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < 𝑥)
2		rphalfcl 13050	. . . . . 6 ⊢ (𝑦 ∈ ℝ+ → (𝑦 / 2) ∈ ℝ+)
3		breq2 5156	. . . . . . . 8 ⊢ (𝑥 = (𝑦 / 2) → ((abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < 𝑥 ↔ (abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < (𝑦 / 2)))
4	3	rexralbidv 3210	. . . . . . 7 ⊢ (𝑥 = (𝑦 / 2) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < 𝑥 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < (𝑦 / 2)))
5	4	rspccva 3606	. . . . . 6 ⊢ ((∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < 𝑥 ∧ (𝑦 / 2) ∈ ℝ+) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < (𝑦 / 2))
6	1, 2, 5	syl2an 594	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < (𝑦 / 2))
7		2clim.1	. . . . . 6 ⊢ 𝑍 = (ℤ≥‘𝑀)
8		2clim.2	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℤ)
9	8	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝑀 ∈ ℤ)
10	2	adantl 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑦 / 2) ∈ ℝ+)
11		eqidd 2726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐹‘𝑘))
12		2clim.7	. . . . . . 7 ⊢ (𝜑 → 𝐹 ⇝ 𝐴)
13	12	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝐹 ⇝ 𝐴)
14	7, 9, 10, 11, 13	climi 15507	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < (𝑦 / 2)))
15	7	rexanuz2 15349	. . . . 5 ⊢ (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < (𝑦 / 2) ∧ ((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < (𝑦 / 2))) ↔ (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < (𝑦 / 2) ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < (𝑦 / 2))))
16	6, 14, 15	sylanbrc 581	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < (𝑦 / 2) ∧ ((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < (𝑦 / 2))))
17	7	uztrn2 12888	. . . . . . . 8 ⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍)
18		an12 643	. . . . . . . . 9 ⊢ (((abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < (𝑦 / 2) ∧ ((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < (𝑦 / 2))) ↔ ((𝐹‘𝑘) ∈ ℂ ∧ ((abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < (𝑦 / 2) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < (𝑦 / 2))))
19		simprr 771	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ (𝐹‘𝑘) ∈ ℂ)) → (𝐹‘𝑘) ∈ ℂ)
20		2clim.5	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℂ)
21	20	ad2ant2r 745	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ (𝐹‘𝑘) ∈ ℂ)) → (𝐺‘𝑘) ∈ ℂ)
22	19, 21	abssubd 15453	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ (𝐹‘𝑘) ∈ ℂ)) → (abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) = (abs‘((𝐺‘𝑘) − (𝐹‘𝑘))))
23	22	breq1d 5162	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ (𝐹‘𝑘) ∈ ℂ)) → ((abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < (𝑦 / 2) ↔ (abs‘((𝐺‘𝑘) − (𝐹‘𝑘))) < (𝑦 / 2)))
24	23	anbi1d 629	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ (𝐹‘𝑘) ∈ ℂ)) → (((abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < (𝑦 / 2) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < (𝑦 / 2)) ↔ ((abs‘((𝐺‘𝑘) − (𝐹‘𝑘))) < (𝑦 / 2) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < (𝑦 / 2))))
25		climcl 15496	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ⇝ 𝐴 → 𝐴 ∈ ℂ)
26	12, 25	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ∈ ℂ)
27	26	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ (𝐹‘𝑘) ∈ ℂ)) → 𝐴 ∈ ℂ)
28		rpre 13031	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ)
29	28	ad2antlr 725	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ (𝐹‘𝑘) ∈ ℂ)) → 𝑦 ∈ ℝ)
30		abs3lem 15338	. . . . . . . . . . . . 13 ⊢ ((((𝐺‘𝑘) ∈ ℂ ∧ 𝐴 ∈ ℂ) ∧ ((𝐹‘𝑘) ∈ ℂ ∧ 𝑦 ∈ ℝ)) → (((abs‘((𝐺‘𝑘) − (𝐹‘𝑘))) < (𝑦 / 2) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < (𝑦 / 2)) → (abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦))
31	21, 27, 19, 29, 30	syl22anc 837	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ (𝐹‘𝑘) ∈ ℂ)) → (((abs‘((𝐺‘𝑘) − (𝐹‘𝑘))) < (𝑦 / 2) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < (𝑦 / 2)) → (abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦))
32	24, 31	sylbid 239	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ (𝐹‘𝑘) ∈ ℂ)) → (((abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < (𝑦 / 2) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < (𝑦 / 2)) → (abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦))
33	32	anassrs 466	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) ∧ (𝐹‘𝑘) ∈ ℂ) → (((abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < (𝑦 / 2) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < (𝑦 / 2)) → (abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦))
34	33	expimpd 452	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → (((𝐹‘𝑘) ∈ ℂ ∧ ((abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < (𝑦 / 2) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < (𝑦 / 2))) → (abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦))
35	18, 34	biimtrid 241	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → (((abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < (𝑦 / 2) ∧ ((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < (𝑦 / 2))) → (abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦))
36	17, 35	sylan2 591	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (((abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < (𝑦 / 2) ∧ ((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < (𝑦 / 2))) → (abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦))
37	36	anassrs 466	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < (𝑦 / 2) ∧ ((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < (𝑦 / 2))) → (abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦))
38	37	ralimdva 3156	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)((abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < (𝑦 / 2) ∧ ((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < (𝑦 / 2))) → ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦))
39	38	reximdva 3157	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < (𝑦 / 2) ∧ ((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < (𝑦 / 2))) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦))
40	16, 39	mpd 15	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦)
41	40	ralrimiva 3135	. 2 ⊢ (𝜑 → ∀𝑦 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦)
42		2clim.3	. . 3 ⊢ (𝜑 → 𝐺 ∈ 𝑉)
43		eqidd 2726	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (𝐺‘𝑘))
44	7, 8, 42, 43, 26, 20	clim2c 15502	. 2 ⊢ (𝜑 → (𝐺 ⇝ 𝐴 ↔ ∀𝑦 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐺‘𝑘) − 𝐴)) < 𝑦))
45	41, 44	mpbird 256	1 ⊢ (𝜑 → 𝐺 ⇝ 𝐴)

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1533   ∈ wcel 2098  ∀wral 3050  ∃wrex 3059   class class class wbr 5152  ‘cfv 6553  (class class class)co 7423  ℂcc 11152  ℝcr 11153   < clt 11294   − cmin 11490   / cdiv 11917  2c2 12314  ℤcz 12605  ℤ_≥cuz 12869  ℝ⁺crp 13023  abscabs 15234   ⇝ cli 15481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5303  ax-nul 5310  ax-pow 5368  ax-pr 5432  ax-un 7745  ax-cnex 11210  ax-resscn 11211  ax-1cn 11212  ax-icn 11213  ax-addcl 11214  ax-addrcl 11215  ax-mulcl 11216  ax-mulrcl 11217  ax-mulcom 11218  ax-addass 11219  ax-mulass 11220  ax-distr 11221  ax-i2m1 11222  ax-1ne0 11223  ax-1rid 11224  ax-rnegex 11225  ax-rrecex 11226  ax-cnre 11227  ax-pre-lttri 11228  ax-pre-lttrn 11229  ax-pre-ltadd 11230  ax-pre-mulgt0 11231  ax-pre-sup 11232

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4325  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5579  df-eprel 5585  df-po 5593  df-so 5594  df-fr 5636  df-we 5638  df-xp 5687  df-rel 5688  df-cnv 5689  df-co 5690  df-dm 5691  df-rn 5692  df-res 5693  df-ima 5694  df-pred 6311  df-ord 6378  df-on 6379  df-lim 6380  df-suc 6381  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7379  df-ov 7426  df-oprab 7427  df-mpo 7428  df-om 7876  df-2nd 8003  df-frecs 8295  df-wrecs 8326  df-recs 8400  df-rdg 8439  df-er 8733  df-en 8974  df-dom 8975  df-sdom 8976  df-sup 9481  df-pnf 11296  df-mnf 11297  df-xr 11298  df-ltxr 11299  df-le 11300  df-sub 11492  df-neg 11493  df-div 11918  df-nn 12260  df-2 12322  df-3 12323  df-n0 12520  df-z 12606  df-uz 12870  df-rp 13024  df-seq 14017  df-exp 14077  df-cj 15099  df-re 15100  df-im 15101  df-sqrt 15235  df-abs 15236  df-clim 15485

This theorem is referenced by:  mertens  15885