Metamath Proof Explorer

Theorem dvle

Description: If A ( x ) , C ( x ) are differentiable functions and A<_ C` , then for x <_ y , A ( y ) - A ( x ) <_ C ( y ) - C ( x ) ` . (Contributed by Mario Carneiro, 16-May-2016)

Ref Expression
Hypotheses dvle.m ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
dvle.n ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
dvle.a ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℝ ) )
dvle.b ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) )
dvle.c ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐶 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℝ ) )
dvle.d ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ) = ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐷 ) )
dvle.f ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐵 ≤ 𝐷 )
dvle.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑀 [,] 𝑁 ) )
dvle.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑀 [,] 𝑁 ) )
dvle.l ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
dvle.p ⊢ ( 𝑥 = 𝑋 → 𝐴 = 𝑃 )
dvle.q ⊢ ( 𝑥 = 𝑋 → 𝐶 = 𝑄 )
dvle.r ⊢ ( 𝑥 = 𝑌 → 𝐴 = 𝑅 )
dvle.s ⊢ ( 𝑥 = 𝑌 → 𝐶 = 𝑆 )
Assertion dvle ( 𝜑 → ( 𝑅 − 𝑃 ) ≤ ( 𝑆 − 𝑄 ) )

Proof

Step Hyp Ref Expression
1 dvle.m ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
2 dvle.n ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
3 dvle.a ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℝ ) )
4 dvle.b ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) )
5 dvle.c ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐶 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℝ ) )
6 dvle.d ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ) = ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐷 ) )
7 dvle.f ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐵 ≤ 𝐷 )
8 dvle.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑀 [,] 𝑁 ) )
9 dvle.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑀 [,] 𝑁 ) )
10 dvle.l ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
11 dvle.p ⊢ ( 𝑥 = 𝑋 → 𝐴 = 𝑃 )
12 dvle.q ⊢ ( 𝑥 = 𝑋 → 𝐶 = 𝑄 )
13 dvle.r ⊢ ( 𝑥 = 𝑌 → 𝐴 = 𝑅 )
14 dvle.s ⊢ ( 𝑥 = 𝑌 → 𝐶 = 𝑆 )
15 13 eleq1d ⊢ ( 𝑥 = 𝑌 → ( 𝐴 ∈ ℝ ↔ 𝑅 ∈ ℝ ) )
16 cncff ⊢ ( ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℝ ) → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) : ( 𝑀 [,] 𝑁 ) ⟶ ℝ )
17 3 16 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) : ( 𝑀 [,] 𝑁 ) ⟶ ℝ )
18 eqid ⊢ ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) = ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 )
19 18 fmpt ⊢ ( ∀ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) 𝐴 ∈ ℝ ↔ ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) : ( 𝑀 [,] 𝑁 ) ⟶ ℝ )
20 17 19 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) 𝐴 ∈ ℝ )
21 15 20 9 rspcdva ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
22 14 eleq1d ⊢ ( 𝑥 = 𝑌 → ( 𝐶 ∈ ℝ ↔ 𝑆 ∈ ℝ ) )
23 cncff ⊢ ( ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐶 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℝ ) → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐶 ) : ( 𝑀 [,] 𝑁 ) ⟶ ℝ )
24 5 23 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐶 ) : ( 𝑀 [,] 𝑁 ) ⟶ ℝ )
25 eqid ⊢ ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐶 ) = ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐶 )
26 25 fmpt ⊢ ( ∀ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) 𝐶 ∈ ℝ ↔ ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐶 ) : ( 𝑀 [,] 𝑁 ) ⟶ ℝ )
27 24 26 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) 𝐶 ∈ ℝ )
28 22 27 9 rspcdva ⊢ ( 𝜑 → 𝑆 ∈ ℝ )
29 12 eleq1d ⊢ ( 𝑥 = 𝑋 → ( 𝐶 ∈ ℝ ↔ 𝑄 ∈ ℝ ) )
30 29 27 8 rspcdva ⊢ ( 𝜑 → 𝑄 ∈ ℝ )
31 28 30 resubcld ⊢ ( 𝜑 → ( 𝑆 − 𝑄 ) ∈ ℝ )
32 11 eleq1d ⊢ ( 𝑥 = 𝑋 → ( 𝐴 ∈ ℝ ↔ 𝑃 ∈ ℝ ) )
33 32 20 8 rspcdva ⊢ ( 𝜑 → 𝑃 ∈ ℝ )
34 21 recnd ⊢ ( 𝜑 → 𝑅 ∈ ℂ )
35 30 recnd ⊢ ( 𝜑 → 𝑄 ∈ ℂ )
36 28 recnd ⊢ ( 𝜑 → 𝑆 ∈ ℂ )
37 35 36 subcld ⊢ ( 𝜑 → ( 𝑄 − 𝑆 ) ∈ ℂ )
38 34 37 addcomd ⊢ ( 𝜑 → ( 𝑅 + ( 𝑄 − 𝑆 ) ) = ( ( 𝑄 − 𝑆 ) + 𝑅 ) )
39 34 36 35 subsub2d ⊢ ( 𝜑 → ( 𝑅 − ( 𝑆 − 𝑄 ) ) = ( 𝑅 + ( 𝑄 − 𝑆 ) ) )
40 35 36 34 subsubd ⊢ ( 𝜑 → ( 𝑄 − ( 𝑆 − 𝑅 ) ) = ( ( 𝑄 − 𝑆 ) + 𝑅 ) )
41 38 39 40 3eqtr4d ⊢ ( 𝜑 → ( 𝑅 − ( 𝑆 − 𝑄 ) ) = ( 𝑄 − ( 𝑆 − 𝑅 ) ) )
42 28 21 resubcld ⊢ ( 𝜑 → ( 𝑆 − 𝑅 ) ∈ ℝ )
43 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
44 43 subcn ⊢ − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
45 ax-resscn ⊢ ℝ ⊆ ℂ
46 resubcl ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐶 − 𝐴 ) ∈ ℝ )
47 43 44 5 3 45 46 cncfmpt2ss ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ ( 𝐶 − 𝐴 ) ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℝ ) )
48 45 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
49 iccssre ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 [,] 𝑁 ) ⊆ ℝ )
50 1 2 49 syl2anc ⊢ ( 𝜑 → ( 𝑀 [,] 𝑁 ) ⊆ ℝ )
51 24 fvmptelrn ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → 𝐶 ∈ ℝ )
52 17 fvmptelrn ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → 𝐴 ∈ ℝ )
53 51 52 resubcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( 𝐶 − 𝐴 ) ∈ ℝ )
54 53 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( 𝐶 − 𝐴 ) ∈ ℂ )
55 43 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
56 iccntr ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑀 [,] 𝑁 ) ) = ( 𝑀 (,) 𝑁 ) )
57 1 2 56 syl2anc ⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑀 [,] 𝑁 ) ) = ( 𝑀 (,) 𝑁 ) )
58 48 50 54 55 43 57 dvmptntr ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ ( 𝐶 − 𝐴 ) ) ) = ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ ( 𝐶 − 𝐴 ) ) ) )
59 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
60 59 a1i ⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
61 ioossicc ⊢ ( 𝑀 (,) 𝑁 ) ⊆ ( 𝑀 [,] 𝑁 )
62 61 sseli ⊢ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) → 𝑥 ∈ ( 𝑀 [,] 𝑁 ) )
63 51 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → 𝐶 ∈ ℂ )
64 62 63 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐶 ∈ ℂ )
65 lerel ⊢ Rel ≤
66 65 brrelex2i ⊢ ( 𝐵 ≤ 𝐷 → 𝐷 ∈ V )
67 7 66 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐷 ∈ V )
68 52 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → 𝐴 ∈ ℂ )
69 62 68 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐴 ∈ ℂ )
70 65 brrelex1i ⊢ ( 𝐵 ≤ 𝐷 → 𝐵 ∈ V )
71 7 70 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐵 ∈ V )
72 60 64 67 6 69 71 4 dvmptsub ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ ( 𝐶 − 𝐴 ) ) ) = ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ ( 𝐷 − 𝐵 ) ) )
73 58 72 eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ ( 𝐶 − 𝐴 ) ) ) = ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ ( 𝐷 − 𝐵 ) ) )
74 62 51 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐶 ∈ ℝ )
75 74 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℝ )
76 ioossre ⊢ ( 𝑀 (,) 𝑁 ) ⊆ ℝ
77 dvfre ⊢ ( ( ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℝ ∧ ( 𝑀 (,) 𝑁 ) ⊆ ℝ ) → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ) : dom ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ) ⟶ ℝ )
78 75 76 77 sylancl ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ) : dom ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ) ⟶ ℝ )
79 6 dmeqd ⊢ ( 𝜑 → dom ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ) = dom ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐷 ) )
80 67 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) 𝐷 ∈ V )
81 dmmptg ⊢ ( ∀ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) 𝐷 ∈ V → dom ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐷 ) = ( 𝑀 (,) 𝑁 ) )
82 80 81 syl ⊢ ( 𝜑 → dom ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐷 ) = ( 𝑀 (,) 𝑁 ) )
83 79 82 eqtrd ⊢ ( 𝜑 → dom ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ) = ( 𝑀 (,) 𝑁 ) )
84 6 83 feq12d ⊢ ( 𝜑 → ( ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ) : dom ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐶 ) ) ⟶ ℝ ↔ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐷 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℝ ) )
85 78 84 mpbid ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐷 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℝ )
86 85 fvmptelrn ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐷 ∈ ℝ )
87 62 52 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐴 ∈ ℝ )
88 87 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℝ )
89 dvfre ⊢ ( ( ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℝ ∧ ( 𝑀 (,) 𝑁 ) ⊆ ℝ ) → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) : dom ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) ⟶ ℝ )
90 88 76 89 sylancl ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) : dom ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) ⟶ ℝ )
91 4 dmeqd ⊢ ( 𝜑 → dom ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) = dom ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) )
92 71 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) 𝐵 ∈ V )
93 dmmptg ⊢ ( ∀ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) 𝐵 ∈ V → dom ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) = ( 𝑀 (,) 𝑁 ) )
94 92 93 syl ⊢ ( 𝜑 → dom ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) = ( 𝑀 (,) 𝑁 ) )
95 91 94 eqtrd ⊢ ( 𝜑 → dom ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) = ( 𝑀 (,) 𝑁 ) )
96 4 95 feq12d ⊢ ( 𝜑 → ( ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) : dom ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) ⟶ ℝ ↔ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℝ ) )
97 90 96 mpbid ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℝ )
98 97 fvmptelrn ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐵 ∈ ℝ )
99 86 98 resubcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → ( 𝐷 − 𝐵 ) ∈ ℝ )
100 86 98 subge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → ( 0 ≤ ( 𝐷 − 𝐵 ) ↔ 𝐵 ≤ 𝐷 ) )
101 7 100 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 0 ≤ ( 𝐷 − 𝐵 ) )
102 elrege0 ⊢ ( ( 𝐷 − 𝐵 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝐷 − 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 𝐷 − 𝐵 ) ) )
103 99 101 102 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → ( 𝐷 − 𝐵 ) ∈ ( 0 [,) +∞ ) )
104 73 103 fmpt3d ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ ( 𝐶 − 𝐴 ) ) ) : ( 𝑀 (,) 𝑁 ) ⟶ ( 0 [,) +∞ ) )
105 1 2 47 104 8 9 10 dvge0 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ ( 𝐶 − 𝐴 ) ) ‘ 𝑋 ) ≤ ( ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ ( 𝐶 − 𝐴 ) ) ‘ 𝑌 ) )
106 12 11 oveq12d ⊢ ( 𝑥 = 𝑋 → ( 𝐶 − 𝐴 ) = ( 𝑄 − 𝑃 ) )
107 eqid ⊢ ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ ( 𝐶 − 𝐴 ) ) = ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ ( 𝐶 − 𝐴 ) )
108 ovex ⊢ ( 𝐶 − 𝐴 ) ∈ V
109 106 107 108 fvmpt3i ⊢ ( 𝑋 ∈ ( 𝑀 [,] 𝑁 ) → ( ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ ( 𝐶 − 𝐴 ) ) ‘ 𝑋 ) = ( 𝑄 − 𝑃 ) )
110 8 109 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ ( 𝐶 − 𝐴 ) ) ‘ 𝑋 ) = ( 𝑄 − 𝑃 ) )
111 14 13 oveq12d ⊢ ( 𝑥 = 𝑌 → ( 𝐶 − 𝐴 ) = ( 𝑆 − 𝑅 ) )
112 111 107 108 fvmpt3i ⊢ ( 𝑌 ∈ ( 𝑀 [,] 𝑁 ) → ( ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ ( 𝐶 − 𝐴 ) ) ‘ 𝑌 ) = ( 𝑆 − 𝑅 ) )
113 9 112 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ ( 𝐶 − 𝐴 ) ) ‘ 𝑌 ) = ( 𝑆 − 𝑅 ) )
114 105 110 113 3brtr3d ⊢ ( 𝜑 → ( 𝑄 − 𝑃 ) ≤ ( 𝑆 − 𝑅 ) )
115 30 33 42 114 subled ⊢ ( 𝜑 → ( 𝑄 − ( 𝑆 − 𝑅 ) ) ≤ 𝑃 )
116 41 115 eqbrtrd ⊢ ( 𝜑 → ( 𝑅 − ( 𝑆 − 𝑄 ) ) ≤ 𝑃 )
117 21 31 33 116 subled ⊢ ( 𝜑 → ( 𝑅 − 𝑃 ) ≤ ( 𝑆 − 𝑄 ) )