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 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 ⊢ ( 𝜑 → 𝐺 ⇝ 𝐴 )