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 ⊢φ→supAℝ*<=+∞
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 ⊢φ→supAℝ*<=+∞
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−C2↔B−F⁡k<B−C2
18 17 anbi1d ⊢φ∧j∈ℝ∧k∈A→F⁡k−B<B−C2∧F⁡k−C<B−C2↔B−F⁡k<B−C2∧F⁡k−C<B−C2
19 abs3lem ⊢B∈ℂ∧C∈ℂ∧F⁡k∈ℂ∧B−C∈ℝ→B−F⁡k<B−C2∧F⁡k−C<B−C2→B−C<B−C
20 7 10 15 12 19 syl22anc ⊢φ∧j∈ℝ∧k∈A→B−F⁡k<B−C2∧F⁡k−C<B−C2→B−C<B−C
21 18 20 sylbid ⊢φ∧j∈ℝ∧k∈A→F⁡k−B<B−C2∧F⁡k−C<B−C2→B−C<B−C
22 21 imim2d ⊢φ∧j∈ℝ∧k∈A→j≤k→F⁡k−B<B−C2∧F⁡k−C<B−C2→j≤k→B−C<B−C
23 22 impcomd ⊢φ∧j∈ℝ∧k∈A→j≤k∧j≤k→F⁡k−B<B−C2∧F⁡k−C<B−C2→B−C<B−C
24 13 23 mtod ⊢φ∧j∈ℝ∧k∈A→¬j≤k∧j≤k→F⁡k−B<B−C2∧F⁡k−C<B−C2
25 24 nrexdv ⊢φ∧j∈ℝ→¬∃k∈Aj≤k∧j≤k→F⁡k−B<B−C2∧F⁡k−C<B−C2
26 r19.29r ⊢∃k∈Aj≤k∧∀k∈Aj≤k→F⁡k−B<B−C2∧F⁡k−C<B−C2→∃k∈Aj≤k∧j≤k→F⁡k−B<B−C2∧F⁡k−C<B−C2
27 25 26 nsyl ⊢φ∧j∈ℝ→¬∃k∈Aj≤k∧∀k∈Aj≤k→F⁡k−B<B−C2∧F⁡k−C<B−C2
28 27 nrexdv ⊢φ→¬∃j∈ℝ∃k∈Aj≤k∧∀k∈Aj≤k→F⁡k−B<B−C2∧F⁡k−C<B−C2
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∈Aj≤k↔supAℝ*<=+∞
36 34 35 syl ⊢φ→∀j∈ℝ∃k∈Aj≤k↔supAℝ*<=+∞
37 2 36 mpbird ⊢φ→∀j∈ℝ∃k∈Aj≤k
38 r19.29 ⊢∀j∈ℝ∃k∈Aj≤k∧∃j∈ℝ∀k∈Aj≤k→F⁡k−B<B−C2∧F⁡k−C<B−C2→∃j∈ℝ∃k∈Aj≤k∧∀k∈Aj≤k→F⁡k−B<B−C2∧F⁡k−C<B−C2
39 38 ex ⊢∀j∈ℝ∃k∈Aj≤k→∃j∈ℝ∀k∈Aj≤k→F⁡k−B<B−C2∧F⁡k−C<B−C2→∃j∈ℝ∃k∈Aj≤k∧∀k∈Aj≤k→F⁡k−B<B−C2∧F⁡k−C<B−C2
40 37 39 syl ⊢φ→∃j∈ℝ∀k∈Aj≤k→F⁡k−B<B−C2∧F⁡k−C<B−C2→∃j∈ℝ∃k∈Aj≤k∧∀k∈Aj≤k→F⁡k−B<B−C2∧F⁡k−C<B−C2
41 28 40 mtod ⊢φ→¬∃j∈ℝ∀k∈Aj≤k→F⁡k−B<B−C2∧F⁡k−C<B−C2
42 1 adantr ⊢φ∧B≠C→F:A⟶ℂ
43 ffvelcdm ⊢F:A⟶ℂ∧k∈A→F⁡k∈ℂ
44 43 ralrimiva ⊢F:A⟶ℂ→∀k∈AF⁡k∈ℂ
45 42 44 syl ⊢φ∧B≠C→∀k∈AF⁡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−C2∈ℝ+
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∈Aj≤k→F⁡k−B<B−C2
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∈Aj≤k→F⁡k−C<B−C2
60 32 adantr ⊢φ∧B≠C→A⊆ℝ
61 rexanre ⊢A⊆ℝ→∃j∈ℝ∀k∈Aj≤k→F⁡k−B<B−C2∧F⁡k−C<B−C2↔∃j∈ℝ∀k∈Aj≤k→F⁡k−B<B−C2∧∃j∈ℝ∀k∈Aj≤k→F⁡k−C<B−C2
62 60 61 syl ⊢φ∧B≠C→∃j∈ℝ∀k∈Aj≤k→F⁡k−B<B−C2∧F⁡k−C<B−C2↔∃j∈ℝ∀k∈Aj≤k→F⁡k−B<B−C2∧∃j∈ℝ∀k∈Aj≤k→F⁡k−C<B−C2
63 56 59 62 mpbir2and ⊢φ∧B≠C→∃j∈ℝ∀k∈Aj≤k→F⁡k−B<B−C2∧F⁡k−C<B−C2
64 63 ex ⊢φ→B≠C→∃j∈ℝ∀k∈Aj≤k→F⁡k−B<B−C2∧F⁡k−C<B−C2
65 64 necon1bd ⊢φ→¬∃j∈ℝ∀k∈Aj≤k→F⁡k−B<B−C2∧F⁡k−C<B−C2→B=C
66 41 65 mpd ⊢φ→B=C