Metamath Proof Explorer

Theorem rlimuni

Description: A real function whose domain is unbounded above converges to at most one limit. (Contributed by Mario Carneiro, 8-May-2016)

Ref Expression
Hypotheses rlimuni.1 ⊢ φ → F : A ⟶ ℂ
rlimuni.2 ⊢ φ → sup A ℝ * < = +∞
rlimuni.3 ⊢ φ → F ⇝ℝ B
rlimuni.4 ⊢ φ → F ⇝ℝ C
Assertion rlimuni ⊢ φ → B = C

Proof

Step Hyp Ref Expression
1 rlimuni.1 ⊢ φ → F : A ⟶ ℂ
2 rlimuni.2 ⊢ φ → sup A ℝ * < = +∞
3 rlimuni.3 ⊢ φ → F ⇝ℝ B
4 rlimuni.4 ⊢ φ → F ⇝ℝ C
5 rlimcl ⊢ F ⇝ℝ B → B ∈ ℂ
6 3 5 syl ⊢ φ → B ∈ ℂ
7 6 ad2antrr ⊢ φ ∧ j ∈ ℝ ∧ k ∈ A → B ∈ ℂ
8 rlimcl ⊢ F ⇝ℝ C → C ∈ ℂ
9 4 8 syl ⊢ φ → C ∈ ℂ
10 9 ad2antrr ⊢ φ ∧ j ∈ ℝ ∧ k ∈ A → C ∈ ℂ
11 7 10 subcld ⊢ φ ∧ j ∈ ℝ ∧ k ∈ A → B − C ∈ ℂ
12 11 abscld ⊢ φ ∧ j ∈ ℝ ∧ k ∈ A → B − C ∈ ℝ
13 12 ltnrd ⊢ φ ∧ j ∈ ℝ ∧ k ∈ A → ¬ B − C < B − C
14 1 ffvelcdmda ⊢ φ ∧ k ∈ A → F ⁡ k ∈ ℂ
15 14 adantlr ⊢ φ ∧ j ∈ ℝ ∧ k ∈ A → F ⁡ k ∈ ℂ
16 15 7 abssubd ⊢ φ ∧ j ∈ ℝ ∧ k ∈ A → F ⁡ k − B = B − F ⁡ k
17 16 breq1d ⊢ φ ∧ j ∈ ℝ ∧ k ∈ A → F ⁡ k − B < B − C 2 ↔ B − F ⁡ k < B − C 2
18 17 anbi1d ⊢ φ ∧ j ∈ ℝ ∧ k ∈ A → F ⁡ k − B < B − C 2 ∧ F ⁡ k − C < B − C 2 ↔ B − F ⁡ k < B − C 2 ∧ F ⁡ k − C < B − C 2
19 abs3lem ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ F ⁡ k ∈ ℂ ∧ B − C ∈ ℝ → B − F ⁡ k < B − C 2 ∧ F ⁡ k − C < B − C 2 → B − C < B − C
20 7 10 15 12 19 syl22anc ⊢ φ ∧ j ∈ ℝ ∧ k ∈ A → B − F ⁡ k < B − C 2 ∧ F ⁡ k − C < B − C 2 → B − C < B − C
21 18 20 sylbid ⊢ φ ∧ j ∈ ℝ ∧ k ∈ A → F ⁡ k − B < B − C 2 ∧ F ⁡ k − C < B − C 2 → B − C < B − C
22 21 imim2d ⊢ φ ∧ j ∈ ℝ ∧ k ∈ A → j ≤ k → F ⁡ k − B < B − C 2 ∧ F ⁡ k − C < B − C 2 → j ≤ k → B − C < B − C
23 22 impcomd ⊢ φ ∧ j ∈ ℝ ∧ k ∈ A → j ≤ k ∧ j ≤ k → F ⁡ k − B < B − C 2 ∧ F ⁡ k − C < B − C 2 → B − C < B − C
24 13 23 mtod ⊢ φ ∧ j ∈ ℝ ∧ k ∈ A → ¬ j ≤ k ∧ j ≤ k → F ⁡ k − B < B − C 2 ∧ F ⁡ k − C < B − C 2
25 24 nrexdv ⊢ φ ∧ j ∈ ℝ → ¬ ∃ k ∈ A j ≤ k ∧ j ≤ k → F ⁡ k − B < B − C 2 ∧ F ⁡ k − C < B − C 2
26 r19.29r ⊢ ∃ k ∈ A j ≤ k ∧ ∀ k ∈ A j ≤ k → F ⁡ k − B < B − C 2 ∧ F ⁡ k − C < B − C 2 → ∃ k ∈ A j ≤ k ∧ j ≤ k → F ⁡ k − B < B − C 2 ∧ F ⁡ k − C < B − C 2
27 25 26 nsyl ⊢ φ ∧ j ∈ ℝ → ¬ ∃ k ∈ A j ≤ k ∧ ∀ k ∈ A j ≤ k → F ⁡ k − B < B − C 2 ∧ F ⁡ k − C < B − C 2
28 27 nrexdv ⊢ φ → ¬ ∃ j ∈ ℝ ∃ k ∈ A j ≤ k ∧ ∀ k ∈ A j ≤ k → F ⁡ k − B < B − C 2 ∧ F ⁡ k − C < B − C 2
29 1 fdmd ⊢ φ → dom ⁡ F = A
30 rlimss ⊢ F ⇝ℝ B → dom ⁡ F ⊆ ℝ
31 3 30 syl ⊢ φ → dom ⁡ F ⊆ ℝ
32 29 31 eqsstrrd ⊢ φ → A ⊆ ℝ
33 ressxr ⊢ ℝ ⊆ ℝ *
34 32 33 sstrdi ⊢ φ → A ⊆ ℝ *
35 supxrunb1 ⊢ A ⊆ ℝ * → ∀ j ∈ ℝ ∃ k ∈ A j ≤ k ↔ sup A ℝ * < = +∞
36 34 35 syl ⊢ φ → ∀ j ∈ ℝ ∃ k ∈ A j ≤ k ↔ sup A ℝ * < = +∞
37 2 36 mpbird ⊢ φ → ∀ j ∈ ℝ ∃ k ∈ A j ≤ k
38 r19.29 ⊢ ∀ j ∈ ℝ ∃ k ∈ A j ≤ k ∧ ∃ j ∈ ℝ ∀ k ∈ A j ≤ k → F ⁡ k − B < B − C 2 ∧ F ⁡ k − C < B − C 2 → ∃ j ∈ ℝ ∃ k ∈ A j ≤ k ∧ ∀ k ∈ A j ≤ k → F ⁡ k − B < B − C 2 ∧ F ⁡ k − C < B − C 2
39 38 ex ⊢ ∀ j ∈ ℝ ∃ k ∈ A j ≤ k → ∃ j ∈ ℝ ∀ k ∈ A j ≤ k → F ⁡ k − B < B − C 2 ∧ F ⁡ k − C < B − C 2 → ∃ j ∈ ℝ ∃ k ∈ A j ≤ k ∧ ∀ k ∈ A j ≤ k → F ⁡ k − B < B − C 2 ∧ F ⁡ k − C < B − C 2
40 37 39 syl ⊢ φ → ∃ j ∈ ℝ ∀ k ∈ A j ≤ k → F ⁡ k − B < B − C 2 ∧ F ⁡ k − C < B − C 2 → ∃ j ∈ ℝ ∃ k ∈ A j ≤ k ∧ ∀ k ∈ A j ≤ k → F ⁡ k − B < B − C 2 ∧ F ⁡ k − C < B − C 2
41 28 40 mtod ⊢ φ → ¬ ∃ j ∈ ℝ ∀ k ∈ A j ≤ k → F ⁡ k − B < B − C 2 ∧ F ⁡ k − C < B − C 2
42 1 adantr ⊢ φ ∧ B ≠ C → F : A ⟶ ℂ
43 ffvelcdm ⊢ F : A ⟶ ℂ ∧ k ∈ A → F ⁡ k ∈ ℂ
44 43 ralrimiva ⊢ F : A ⟶ ℂ → ∀ k ∈ A F ⁡ k ∈ ℂ
45 42 44 syl ⊢ φ ∧ B ≠ C → ∀ k ∈ A F ⁡ k ∈ ℂ
46 6 adantr ⊢ φ ∧ B ≠ C → B ∈ ℂ
47 9 adantr ⊢ φ ∧ B ≠ C → C ∈ ℂ
48 46 47 subcld ⊢ φ ∧ B ≠ C → B − C ∈ ℂ
49 simpr ⊢ φ ∧ B ≠ C → B ≠ C
50 46 47 49 subne0d ⊢ φ ∧ B ≠ C → B − C ≠ 0
51 48 50 absrpcld ⊢ φ ∧ B ≠ C → B − C ∈ ℝ +
52 51 rphalfcld ⊢ φ ∧ B ≠ C → B − C 2 ∈ ℝ +
53 42 feqmptd ⊢ φ ∧ B ≠ C → F = k ∈ A ⟼ F ⁡ k
54 3 adantr ⊢ φ ∧ B ≠ C → F ⇝ℝ B
55 53 54 eqbrtrrd ⊢ φ ∧ B ≠ C → k ∈ A ⟼ F ⁡ k ⇝ℝ B
56 45 52 55 rlimi ⊢ φ ∧ B ≠ C → ∃ j ∈ ℝ ∀ k ∈ A j ≤ k → F ⁡ k − B < B − C 2
57 4 adantr ⊢ φ ∧ B ≠ C → F ⇝ℝ C
58 53 57 eqbrtrrd ⊢ φ ∧ B ≠ C → k ∈ A ⟼ F ⁡ k ⇝ℝ C
59 45 52 58 rlimi ⊢ φ ∧ B ≠ C → ∃ j ∈ ℝ ∀ k ∈ A j ≤ k → F ⁡ k − C < B − C 2
60 32 adantr ⊢ φ ∧ B ≠ C → A ⊆ ℝ
61 rexanre ⊢ A ⊆ ℝ → ∃ j ∈ ℝ ∀ k ∈ A j ≤ k → F ⁡ k − B < B − C 2 ∧ F ⁡ k − C < B − C 2 ↔ ∃ j ∈ ℝ ∀ k ∈ A j ≤ k → F ⁡ k − B < B − C 2 ∧ ∃ j ∈ ℝ ∀ k ∈ A j ≤ k → F ⁡ k − C < B − C 2
62 60 61 syl ⊢ φ ∧ B ≠ C → ∃ j ∈ ℝ ∀ k ∈ A j ≤ k → F ⁡ k − B < B − C 2 ∧ F ⁡ k − C < B − C 2 ↔ ∃ j ∈ ℝ ∀ k ∈ A j ≤ k → F ⁡ k − B < B − C 2 ∧ ∃ j ∈ ℝ ∀ k ∈ A j ≤ k → F ⁡ k − C < B − C 2
63 56 59 62 mpbir2and ⊢ φ ∧ B ≠ C → ∃ j ∈ ℝ ∀ k ∈ A j ≤ k → F ⁡ k − B < B − C 2 ∧ F ⁡ k − C < B − C 2
64 63 ex ⊢ φ → B ≠ C → ∃ j ∈ ℝ ∀ k ∈ A j ≤ k → F ⁡ k − B < B − C 2 ∧ F ⁡ k − C < B − C 2
65 64 necon1bd ⊢ φ → ¬ ∃ j ∈ ℝ ∀ k ∈ A j ≤ k → F ⁡ k − B < B − C 2 ∧ F ⁡ k − C < B − C 2 → B = C
66 41 65 mpd ⊢ φ → B = C