Metamath Proof Explorer

Theorem ioodvbdlimc1

Description: A real function with bounded derivative, has a limit at the upper bound of an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019) (Proof shortened by AV, 3-Oct-2020)

Ref Expression
Hypotheses ioodvbdlimc1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
ioodvbdlimc1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
ioodvbdlimc1.f ⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
ioodvbdlimc1.dmdv ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
ioodvbdlimc1.dvbd ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑦 )
Assertion ioodvbdlimc1 ( 𝜑 → ( 𝐹 limℂ 𝐴 ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 ioodvbdlimc1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 ioodvbdlimc1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 ioodvbdlimc1.f ⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
4 ioodvbdlimc1.dmdv ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
5 ioodvbdlimc1.dvbd ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑦 )
6 1 adantr ⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → 𝐴 ∈ ℝ )
7 2 adantr ⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → 𝐵 ∈ ℝ )
8 simpr ⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → 𝐴 < 𝐵 )
9 3 adantr ⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
10 4 adantr ⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
11 5 adantr ⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑦 )
12 2fveq3 ⊢ ( 𝑦 = 𝑥 → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) = ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
13 12 cbvmptv ⊢ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
14 13 rneqi ⊢ ran ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ) = ran ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
15 14 supeq1i ⊢ sup ( ran ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ) , ℝ , < ) = sup ( ran ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) , ℝ , < )
16 eqid ⊢ ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) = ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 )
17 oveq2 ⊢ ( 𝑗 = 𝑘 → ( 1 / 𝑗 ) = ( 1 / 𝑘 ) )
18 17 oveq2d ⊢ ( 𝑗 = 𝑘 → ( 𝐴 + ( 1 / 𝑗 ) ) = ( 𝐴 + ( 1 / 𝑘 ) ) )
19 18 fveq2d ⊢ ( 𝑗 = 𝑘 → ( 𝐹 ‘ ( 𝐴 + ( 1 / 𝑗 ) ) ) = ( 𝐹 ‘ ( 𝐴 + ( 1 / 𝑘 ) ) ) )
20 19 cbvmptv ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ) ↦ ( 𝐹 ‘ ( 𝐴 + ( 1 / 𝑗 ) ) ) ) = ( 𝑘 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ) ↦ ( 𝐹 ‘ ( 𝐴 + ( 1 / 𝑘 ) ) ) )
21 18 cbvmptv ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ) ↦ ( 𝐴 + ( 1 / 𝑗 ) ) ) = ( 𝑘 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ) ↦ ( 𝐴 + ( 1 / 𝑘 ) ) )
22 eqid ⊢ if ( ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ≤ ( ( ⌊ ‘ ( sup ( ran ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ) , ℝ , < ) / ( 𝑥 / 2 ) ) ) + 1 ) , ( ( ⌊ ‘ ( sup ( ran ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ) , ℝ , < ) / ( 𝑥 / 2 ) ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ) = if ( ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ≤ ( ( ⌊ ‘ ( sup ( ran ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ) , ℝ , < ) / ( 𝑥 / 2 ) ) ) + 1 ) , ( ( ⌊ ‘ ( sup ( ran ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ) , ℝ , < ) / ( 𝑥 / 2 ) ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) )
23 biid ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 < 𝐵 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ≤ ( ( ⌊ ‘ ( sup ( ran ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ) , ℝ , < ) / ( 𝑥 / 2 ) ) ) + 1 ) , ( ( ⌊ ‘ ( sup ( ran ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ) , ℝ , < ) / ( 𝑥 / 2 ) ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ) ) ) ∧ ( abs ‘ ( ( ( 𝑗 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ) ↦ ( 𝐹 ‘ ( 𝐴 + ( 1 / 𝑗 ) ) ) ) ‘ 𝑘 ) − ( lim sup ‘ ( 𝑗 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ) ↦ ( 𝐹 ‘ ( 𝐴 + ( 1 / 𝑗 ) ) ) ) ) ) ) < ( 𝑥 / 2 ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < ( 1 / 𝑘 ) ) ↔ ( ( ( ( ( ( 𝜑 ∧ 𝐴 < 𝐵 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ≤ ( ( ⌊ ‘ ( sup ( ran ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ) , ℝ , < ) / ( 𝑥 / 2 ) ) ) + 1 ) , ( ( ⌊ ‘ ( sup ( ran ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ) , ℝ , < ) / ( 𝑥 / 2 ) ) ) + 1 ) , ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ) ) ) ∧ ( abs ‘ ( ( ( 𝑗 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ) ↦ ( 𝐹 ‘ ( 𝐴 + ( 1 / 𝑗 ) ) ) ) ‘ 𝑘 ) − ( lim sup ‘ ( 𝑗 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ) ↦ ( 𝐹 ‘ ( 𝐴 + ( 1 / 𝑗 ) ) ) ) ) ) ) < ( 𝑥 / 2 ) ) ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < ( 1 / 𝑘 ) ) )
24 6 7 8 9 10 11 15 16 20 21 22 23 ioodvbdlimc1lem2 ⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → ( lim sup ‘ ( 𝑗 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 1 / ( 𝐵 − 𝐴 ) ) ) + 1 ) ) ↦ ( 𝐹 ‘ ( 𝐴 + ( 1 / 𝑗 ) ) ) ) ) ∈ ( 𝐹 limℂ 𝐴 ) )
25 24 ne0d ⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → ( 𝐹 limℂ 𝐴 ) ≠ ∅ )
26 ax-resscn ⊢ ℝ ⊆ ℂ
27 26 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
28 3 27 fssd ⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
30 simpr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → 𝐵 ≤ 𝐴 )
31 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → 𝐴 ∈ ℝ* )
33 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → 𝐵 ∈ ℝ* )
35 ioo0 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 (,) 𝐵 ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )
36 32 34 35 syl2anc ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → ( ( 𝐴 (,) 𝐵 ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )
37 30 36 mpbird ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → ( 𝐴 (,) 𝐵 ) = ∅ )
38 37 feq2d ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → ( 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ↔ 𝐹 : ∅ ⟶ ℂ ) )
39 29 38 mpbid ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → 𝐹 : ∅ ⟶ ℂ )
40 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
41 40 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → 𝐴 ∈ ℂ )
42 39 41 limcdm0 ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → ( 𝐹 limℂ 𝐴 ) = ℂ )
43 0cn ⊢ 0 ∈ ℂ
44 43 ne0ii ⊢ ℂ ≠ ∅
45 44 a1i ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → ℂ ≠ ∅ )
46 42 45 eqnetrd ⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → ( 𝐹 limℂ 𝐴 ) ≠ ∅ )
47 25 46 1 2 ltlecasei ⊢ ( 𝜑 → ( 𝐹 limℂ 𝐴 ) ≠ ∅ )