Metamath Proof Explorer


Theorem 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 syl5bi ( ( ( 𝜑𝑦 ∈ ℝ+ ) ∧ 𝑘𝑍 ) → ( ( ( 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 ( 𝜑𝐺𝐴 )