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 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
rlimuni.2 ⊢ ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = +∞ )
rlimuni.3 ⊢ ( 𝜑 → 𝐹 ⇝𝑟 𝐵 )
rlimuni.4 ⊢ ( 𝜑 → 𝐹 ⇝𝑟 𝐶 )
Assertion rlimuni ( 𝜑 → 𝐵 = 𝐶 )

Proof

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