Metamath Proof Explorer

Theorem dvgt0lem1

Description: Lemma for dvgt0 and dvlt0 . (Contributed by Mario Carneiro, 19-Feb-2015)

Ref Expression
Hypotheses dvgt0.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
dvgt0.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
dvgt0.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
dvgt0lem.d ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ 𝑆 )
Assertion dvgt0lem1 ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ( ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 dvgt0.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 dvgt0.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 dvgt0.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
4 dvgt0lem.d ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ 𝑆 )
5 iccssxr ⊢ ( 𝐴 [,] 𝐵 ) ⊆ ℝ*
6 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → 𝑋 ∈ ( 𝐴 [,] 𝐵 ) )
7 5 6 sseldi ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → 𝑋 ∈ ℝ* )
8 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → 𝑌 ∈ ( 𝐴 [,] 𝐵 ) )
9 5 8 sseldi ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → 𝑌 ∈ ℝ* )
10 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
11 1 2 10 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
12 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
13 12 6 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → 𝑋 ∈ ℝ )
14 12 8 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → 𝑌 ∈ ℝ )
15 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → 𝑋 < 𝑌 )
16 13 14 15 ltled ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → 𝑋 ≤ 𝑌 )
17 ubicc2 ⊢ ( ( 𝑋 ∈ ℝ* ∧ 𝑌 ∈ ℝ* ∧ 𝑋 ≤ 𝑌 ) → 𝑌 ∈ ( 𝑋 [,] 𝑌 ) )
18 7 9 16 17 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → 𝑌 ∈ ( 𝑋 [,] 𝑌 ) )
19 18 fvresd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ( ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ‘ 𝑌 ) = ( 𝐹 ‘ 𝑌 ) )
20 lbicc2 ⊢ ( ( 𝑋 ∈ ℝ* ∧ 𝑌 ∈ ℝ* ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ∈ ( 𝑋 [,] 𝑌 ) )
21 7 9 16 20 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → 𝑋 ∈ ( 𝑋 [,] 𝑌 ) )
22 21 fvresd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ( ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) )
23 19 22 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ( ( ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ‘ 𝑌 ) − ( ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ‘ 𝑋 ) ) = ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) )
24 23 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ( ( ( ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ‘ 𝑌 ) − ( ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) = ( ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) )
25 iccss2 ⊢ ( ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑋 [,] 𝑌 ) ⊆ ( 𝐴 [,] 𝐵 ) )
26 25 ad2antlr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ( 𝑋 [,] 𝑌 ) ⊆ ( 𝐴 [,] 𝐵 ) )
27 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
28 rescncf ⊢ ( ( 𝑋 [,] 𝑌 ) ⊆ ( 𝐴 [,] 𝐵 ) → ( 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) → ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) ) )
29 26 27 28 sylc ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) )
30 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ 𝑆 )
31 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → 𝐴 ∈ ℝ )
32 31 rexrd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → 𝐴 ∈ ℝ* )
33 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → 𝐵 ∈ ℝ )
34 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵 ) ) )
35 31 33 34 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵 ) ) )
36 6 35 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ( 𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵 ) )
37 36 simp2d ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → 𝐴 ≤ 𝑋 )
38 iooss1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝑋 ) → ( 𝑋 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝑌 ) )
39 32 37 38 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ( 𝑋 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝑌 ) )
40 33 rexrd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → 𝐵 ∈ ℝ* )
41 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑌 ∈ ℝ ∧ 𝐴 ≤ 𝑌 ∧ 𝑌 ≤ 𝐵 ) ) )
42 31 33 41 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ( 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑌 ∈ ℝ ∧ 𝐴 ≤ 𝑌 ∧ 𝑌 ≤ 𝐵 ) ) )
43 8 42 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ( 𝑌 ∈ ℝ ∧ 𝐴 ≤ 𝑌 ∧ 𝑌 ≤ 𝐵 ) )
44 43 simp3d ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → 𝑌 ≤ 𝐵 )
45 iooss2 ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑌 ≤ 𝐵 ) → ( 𝐴 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝐵 ) )
46 40 44 45 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ( 𝐴 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝐵 ) )
47 39 46 sstrd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ( 𝑋 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝐵 ) )
48 30 47 fssresd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ( ( ℝ D 𝐹 ) ↾ ( 𝑋 (,) 𝑌 ) ) : ( 𝑋 (,) 𝑌 ) ⟶ 𝑆 )
49 ax-resscn ⊢ ℝ ⊆ ℂ
50 49 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ℝ ⊆ ℂ )
51 cncff ⊢ ( 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
52 3 51 syl ⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
53 52 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
54 fss ⊢ ( ( 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
55 53 49 54 sylancl ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
56 iccssre ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝑋 [,] 𝑌 ) ⊆ ℝ )
57 13 14 56 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ( 𝑋 [,] 𝑌 ) ⊆ ℝ )
58 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
59 58 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
60 58 59 dvres ⊢ ( ( ( ℝ ⊆ ℂ ∧ 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ ) ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ ℝ ∧ ( 𝑋 [,] 𝑌 ) ⊆ ℝ ) ) → ( ℝ D ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑋 [,] 𝑌 ) ) ) )
61 50 55 12 57 60 syl22anc ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ( ℝ D ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑋 [,] 𝑌 ) ) ) )
62 iccntr ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑋 [,] 𝑌 ) ) = ( 𝑋 (,) 𝑌 ) )
63 13 14 62 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑋 [,] 𝑌 ) ) = ( 𝑋 (,) 𝑌 ) )
64 63 reseq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑋 [,] 𝑌 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( 𝑋 (,) 𝑌 ) ) )
65 61 64 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ( ℝ D ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( 𝑋 (,) 𝑌 ) ) )
66 65 feq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ( ( ℝ D ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ) : ( 𝑋 (,) 𝑌 ) ⟶ 𝑆 ↔ ( ( ℝ D 𝐹 ) ↾ ( 𝑋 (,) 𝑌 ) ) : ( 𝑋 (,) 𝑌 ) ⟶ 𝑆 ) )
67 48 66 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ( ℝ D ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ) : ( 𝑋 (,) 𝑌 ) ⟶ 𝑆 )
68 67 fdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → dom ( ℝ D ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ) = ( 𝑋 (,) 𝑌 ) )
69 13 14 15 29 68 mvth ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ∃ 𝑧 ∈ ( 𝑋 (,) 𝑌 ) ( ( ℝ D ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ) ‘ 𝑧 ) = ( ( ( ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ‘ 𝑌 ) − ( ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) )
70 67 ffvelrnda ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) ∧ 𝑧 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( ℝ D ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ) ‘ 𝑧 ) ∈ 𝑆 )
71 eleq1 ⊢ ( ( ( ℝ D ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ) ‘ 𝑧 ) = ( ( ( ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ‘ 𝑌 ) − ( ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) → ( ( ( ℝ D ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ) ‘ 𝑧 ) ∈ 𝑆 ↔ ( ( ( ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ‘ 𝑌 ) − ( ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) ∈ 𝑆 ) )
72 70 71 syl5ibcom ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) ∧ 𝑧 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( ( ℝ D ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ) ‘ 𝑧 ) = ( ( ( ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ‘ 𝑌 ) − ( ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) → ( ( ( ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ‘ 𝑌 ) − ( ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) ∈ 𝑆 ) )
73 72 rexlimdva ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ( ∃ 𝑧 ∈ ( 𝑋 (,) 𝑌 ) ( ( ℝ D ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ) ‘ 𝑧 ) = ( ( ( ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ‘ 𝑌 ) − ( ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) → ( ( ( ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ‘ 𝑌 ) − ( ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) ∈ 𝑆 ) )
74 69 73 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ( ( ( ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ‘ 𝑌 ) − ( ( 𝐹 ↾ ( 𝑋 [,] 𝑌 ) ) ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) ∈ 𝑆 )
75 24 74 eqeltrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑋 < 𝑌 ) → ( ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) ∈ 𝑆 )