Metamath Proof Explorer

Theorem limcleqr

Description: If the left and the right limits are equal, the limit of the function exits and the three limits coincide. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses limcleqr.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
limcleqr.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
limcleqr.j ⊢ 𝐽 = ( topGen ‘ ran (,) )
limcleqr.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
limcleqr.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
limcleqr.l ⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) limℂ 𝐵 ) )
limcleqr.r ⊢ ( 𝜑 → 𝑅 ∈ ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) limℂ 𝐵 ) )
limcleqr.leqr ⊢ ( 𝜑 → 𝐿 = 𝑅 )
Assertion limcleqr ( 𝜑 → 𝐿 ∈ ( 𝐹 limℂ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 limcleqr.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
2 limcleqr.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
3 limcleqr.j ⊢ 𝐽 = ( topGen ‘ ran (,) )
4 limcleqr.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
5 limcleqr.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
6 limcleqr.l ⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) limℂ 𝐵 ) )
7 limcleqr.r ⊢ ( 𝜑 → 𝑅 ∈ ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) limℂ 𝐵 ) )
8 limcleqr.leqr ⊢ ( 𝜑 → 𝐿 = 𝑅 )
9 limccl ⊢ ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) limℂ 𝐵 ) ⊆ ℂ
10 9 6 sseldi ⊢ ( 𝜑 → 𝐿 ∈ ℂ )
11 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) → 𝑎 ∈ ℝ+ )
12 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) → 𝑏 ∈ ℝ+ )
13 11 12 ifcld ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ∈ ℝ+ )
14 nfv ⊢ Ⅎ 𝑧 ( 𝜑 ∧ 𝑥 ∈ ℝ+ )
15 nfv ⊢ Ⅎ 𝑧 𝑎 ∈ ℝ+
16 14 15 nfan ⊢ Ⅎ 𝑧 ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ )
17 nfra1 ⊢ Ⅎ 𝑧 ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 )
18 16 17 nfan ⊢ Ⅎ 𝑧 ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) )
19 nfv ⊢ Ⅎ 𝑧 𝑏 ∈ ℝ+
20 18 19 nfan ⊢ Ⅎ 𝑧 ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ )
21 nfra1 ⊢ Ⅎ 𝑧 ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 )
22 20 21 nfan ⊢ Ⅎ 𝑧 ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) )
23 simp-6l ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 < 𝐵 ) → 𝜑 )
24 23 3ad2antl1 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝑧 < 𝐵 ) → 𝜑 )
25 simpl2 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝑧 < 𝐵 ) → 𝑧 ∈ 𝐴 )
26 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝑧 < 𝐵 ) → 𝑧 < 𝐵 )
27 mnfxr ⊢ -∞ ∈ ℝ*
28 27 a1i ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 < 𝐵 ) → -∞ ∈ ℝ* )
29 5 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
30 29 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 < 𝐵 ) → 𝐵 ∈ ℝ* )
31 2 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ℝ )
32 31 3adant3 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 < 𝐵 ) → 𝑧 ∈ ℝ )
33 32 mnfltd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 < 𝐵 ) → -∞ < 𝑧 )
34 simp3 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 < 𝐵 ) → 𝑧 < 𝐵 )
35 28 30 32 33 34 eliood ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑧 < 𝐵 ) → 𝑧 ∈ ( -∞ (,) 𝐵 ) )
36 24 25 26 35 syl3anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝑧 < 𝐵 ) → 𝑧 ∈ ( -∞ (,) 𝐵 ) )
37 fvres ⊢ ( 𝑧 ∈ ( -∞ (,) 𝐵 ) → ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
38 37 oveq1d ⊢ ( 𝑧 ∈ ( -∞ (,) 𝐵 ) → ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) = ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) )
39 38 eqcomd ⊢ ( 𝑧 ∈ ( -∞ (,) 𝐵 ) → ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) = ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) )
40 39 fveq2d ⊢ ( 𝑧 ∈ ( -∞ (,) 𝐵 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) = ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) )
41 36 40 syl ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝑧 < 𝐵 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) = ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) )
42 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 < 𝐵 ) → ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) )
43 42 3ad2antl1 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝑧 < 𝐵 ) → ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) )
44 25 36 elind ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝑧 < 𝐵 ) → 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) )
45 43 44 jca ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝑧 < 𝐵 ) → ( ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) )
46 simpl3l ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝑧 < 𝐵 ) → 𝑧 ≠ 𝐵 )
47 11 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 < 𝐵 ) → 𝑎 ∈ ℝ+ )
48 47 3ad2antl1 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝑧 < 𝐵 ) → 𝑎 ∈ ℝ+ )
49 12 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 < 𝐵 ) → 𝑏 ∈ ℝ+ )
50 49 3ad2antl1 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝑧 < 𝐵 ) → 𝑏 ∈ ℝ+ )
51 simpl3r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝑧 < 𝐵 ) → ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) )
52 simpl1 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ∧ 𝑧 ∈ 𝐴 ) ) → 𝜑 )
53 simprr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ∧ 𝑧 ∈ 𝐴 ) ) → 𝑧 ∈ 𝐴 )
54 31 recnd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ℂ )
55 5 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
56 55 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
57 54 56 subcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑧 − 𝐵 ) ∈ ℂ )
58 57 abscld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( abs ‘ ( 𝑧 − 𝐵 ) ) ∈ ℝ )
59 52 53 58 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ∧ 𝑧 ∈ 𝐴 ) ) → ( abs ‘ ( 𝑧 − 𝐵 ) ) ∈ ℝ )
60 rpre ⊢ ( 𝑎 ∈ ℝ+ → 𝑎 ∈ ℝ )
61 60 adantr ⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → 𝑎 ∈ ℝ )
62 rpre ⊢ ( 𝑏 ∈ ℝ+ → 𝑏 ∈ ℝ )
63 62 adantl ⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → 𝑏 ∈ ℝ )
64 61 63 ifcld ⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ∈ ℝ )
65 64 3adant1 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ∈ ℝ )
66 65 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ∧ 𝑧 ∈ 𝐴 ) ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ∈ ℝ )
67 61 3adant1 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → 𝑎 ∈ ℝ )
68 67 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ∧ 𝑧 ∈ 𝐴 ) ) → 𝑎 ∈ ℝ )
69 simprl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ∧ 𝑧 ∈ 𝐴 ) ) → ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) )
70 63 3adant1 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → 𝑏 ∈ ℝ )
71 min1 ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ≤ 𝑎 )
72 67 70 71 syl2anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ≤ 𝑎 )
73 72 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ∧ 𝑧 ∈ 𝐴 ) ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ≤ 𝑎 )
74 59 66 68 69 73 ltletrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ∧ 𝑧 ∈ 𝐴 ) ) → ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 )
75 24 48 50 51 25 74 syl32anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝑧 < 𝐵 ) → ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 )
76 46 75 jca ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝑧 < 𝐵 ) → ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) )
77 rspa ⊢ ( ( ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) → ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) )
78 45 76 77 sylc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝑧 < 𝐵 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 )
79 41 78 eqbrtrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝑧 < 𝐵 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 )
80 simp-6l ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ ¬ 𝑧 < 𝐵 ) → 𝜑 )
81 80 3ad2antl1 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ ¬ 𝑧 < 𝐵 ) → 𝜑 )
82 81 5 syl ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ ¬ 𝑧 < 𝐵 ) → 𝐵 ∈ ℝ )
83 simpl2 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ ¬ 𝑧 < 𝐵 ) → 𝑧 ∈ 𝐴 )
84 81 83 31 syl2anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ ¬ 𝑧 < 𝐵 ) → 𝑧 ∈ ℝ )
85 id ⊢ ( 𝑧 ≠ 𝐵 → 𝑧 ≠ 𝐵 )
86 85 necomd ⊢ ( 𝑧 ≠ 𝐵 → 𝐵 ≠ 𝑧 )
87 86 ad2antrr ⊢ ( ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ∧ ¬ 𝑧 < 𝐵 ) → 𝐵 ≠ 𝑧 )
88 87 3ad2antl3 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ ¬ 𝑧 < 𝐵 ) → 𝐵 ≠ 𝑧 )
89 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ ¬ 𝑧 < 𝐵 ) → ¬ 𝑧 < 𝐵 )
90 82 84 88 89 lttri5d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ ¬ 𝑧 < 𝐵 ) → 𝐵 < 𝑧 )
91 simp-6l ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝐵 < 𝑧 ) → 𝜑 )
92 91 3ad2antl1 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝐵 < 𝑧 ) → 𝜑 )
93 simpl2 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝐵 < 𝑧 ) → 𝑧 ∈ 𝐴 )
94 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝐵 < 𝑧 ) → 𝐵 < 𝑧 )
95 29 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝐵 < 𝑧 ) → 𝐵 ∈ ℝ* )
96 pnfxr ⊢ +∞ ∈ ℝ*
97 96 a1i ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝐵 < 𝑧 ) → +∞ ∈ ℝ* )
98 31 3adant3 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝐵 < 𝑧 ) → 𝑧 ∈ ℝ )
99 simp3 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝐵 < 𝑧 ) → 𝐵 < 𝑧 )
100 98 ltpnfd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝐵 < 𝑧 ) → 𝑧 < +∞ )
101 95 97 98 99 100 eliood ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝐵 < 𝑧 ) → 𝑧 ∈ ( 𝐵 (,) +∞ ) )
102 92 93 94 101 syl3anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝐵 < 𝑧 ) → 𝑧 ∈ ( 𝐵 (,) +∞ ) )
103 fvres ⊢ ( 𝑧 ∈ ( 𝐵 (,) +∞ ) → ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
104 103 eqcomd ⊢ ( 𝑧 ∈ ( 𝐵 (,) +∞ ) → ( 𝐹 ‘ 𝑧 ) = ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) )
105 104 fvoveq1d ⊢ ( 𝑧 ∈ ( 𝐵 (,) +∞ ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) = ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) )
106 102 105 syl ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝐵 < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) = ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) )
107 simpl1r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝐵 < 𝑧 ) → ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) )
108 93 102 elind ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝐵 < 𝑧 ) → 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) )
109 107 108 jca ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝐵 < 𝑧 ) → ( ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) )
110 simpl3l ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝐵 < 𝑧 ) → 𝑧 ≠ 𝐵 )
111 11 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝐵 < 𝑧 ) → 𝑎 ∈ ℝ+ )
112 111 3ad2antl1 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝐵 < 𝑧 ) → 𝑎 ∈ ℝ+ )
113 12 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝐵 < 𝑧 ) → 𝑏 ∈ ℝ+ )
114 113 3ad2antl1 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝐵 < 𝑧 ) → 𝑏 ∈ ℝ+ )
115 simpl3r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝐵 < 𝑧 ) → ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) )
116 70 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ∧ 𝑧 ∈ 𝐴 ) ) → 𝑏 ∈ ℝ )
117 min2 ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ≤ 𝑏 )
118 67 70 117 syl2anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ≤ 𝑏 )
119 118 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ∧ 𝑧 ∈ 𝐴 ) ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ≤ 𝑏 )
120 59 66 116 69 119 ltletrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ∧ 𝑧 ∈ 𝐴 ) ) → ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 )
121 92 112 114 115 93 120 syl32anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝐵 < 𝑧 ) → ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 )
122 110 121 jca ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝐵 < 𝑧 ) → ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) )
123 rspa ⊢ ( ( ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) → ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) )
124 109 122 123 sylc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝐵 < 𝑧 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 )
125 106 124 eqbrtrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ 𝐵 < 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 )
126 90 125 syldan ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) ∧ ¬ 𝑧 < 𝐵 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 )
127 79 126 pm2.61dan ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 )
128 127 3exp ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) → ( 𝑧 ∈ 𝐴 → ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) )
129 22 128 ralrimi ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) → ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) )
130 brimralrspcev ⊢ ( ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ∈ ℝ+ ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) )
131 13 129 130 syl2anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) )
132 fresin ⊢ ( 𝐹 : 𝐴 ⟶ ℂ → ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) : ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ⟶ ℂ )
133 4 132 syl ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) : ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ⟶ ℂ )
134 inss2 ⊢ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ⊆ ( 𝐵 (,) +∞ )
135 ioosscn ⊢ ( 𝐵 (,) +∞ ) ⊆ ℂ
136 134 135 sstri ⊢ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ⊆ ℂ
137 136 a1i ⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ⊆ ℂ )
138 133 137 55 ellimc3 ⊢ ( 𝜑 → ( 𝑅 ∈ ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) limℂ 𝐵 ) ↔ ( 𝑅 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝑅 ) ) < 𝑥 ) ) ) )
139 7 138 mpbid ⊢ ( 𝜑 → ( 𝑅 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝑅 ) ) < 𝑥 ) ) )
140 139 simprd ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝑅 ) ) < 𝑥 ) )
141 140 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑏 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝑅 ) ) < 𝑥 ) )
142 8 oveq2d ⊢ ( 𝜑 → ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) = ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝑅 ) )
143 142 fveq2d ⊢ ( 𝜑 → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) = ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝑅 ) ) )
144 143 breq1d ⊢ ( 𝜑 → ( ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ↔ ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝑅 ) ) < 𝑥 ) )
145 144 imbi2d ⊢ ( 𝜑 → ( ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ↔ ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝑅 ) ) < 𝑥 ) ) )
146 145 rexralbidv ⊢ ( 𝜑 → ( ∃ 𝑏 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ↔ ∃ 𝑏 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝑅 ) ) < 𝑥 ) ) )
147 146 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑏 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ↔ ∃ 𝑏 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝑅 ) ) < 𝑥 ) ) )
148 141 147 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑏 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) )
149 148 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) → ∃ 𝑏 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) )
150 131 149 r19.29a ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) )
151 fresin ⊢ ( 𝐹 : 𝐴 ⟶ ℂ → ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) : ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ⟶ ℂ )
152 4 151 syl ⊢ ( 𝜑 → ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) : ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ⟶ ℂ )
153 inss2 ⊢ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ⊆ ( -∞ (,) 𝐵 )
154 ioossre ⊢ ( -∞ (,) 𝐵 ) ⊆ ℝ
155 153 154 sstri ⊢ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ⊆ ℝ
156 ax-resscn ⊢ ℝ ⊆ ℂ
157 156 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
158 155 157 sstrid ⊢ ( 𝜑 → ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ⊆ ℂ )
159 152 158 55 ellimc3 ⊢ ( 𝜑 → ( 𝐿 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) limℂ 𝐵 ) ↔ ( 𝐿 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑎 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ) )
160 6 159 mpbid ⊢ ( 𝜑 → ( 𝐿 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑎 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) )
161 160 simprd ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑎 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) )
162 161 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑎 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑎 ) → ( abs ‘ ( ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) )
163 150 162 r19.29a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) )
164 163 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) )
165 2 156 sstrdi ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
166 4 165 55 ellimc3 ⊢ ( 𝜑 → ( 𝐿 ∈ ( 𝐹 limℂ 𝐵 ) ↔ ( 𝐿 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐵 ∧ ( abs ‘ ( 𝑧 − 𝐵 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐿 ) ) < 𝑥 ) ) ) )
167 10 164 166 mpbir2and ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐹 limℂ 𝐵 ) )