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 𝐴 ) ≠ ∅ )