Metamath Proof Explorer

Theorem dvivthlem1

Description: Lemma for dvivth . (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses dvivth.1 ⊢ ( 𝜑 → 𝑀 ∈ ( 𝐴 (,) 𝐵 ) )
dvivth.2 ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐴 (,) 𝐵 ) )
dvivth.3 ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )
dvivth.4 ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
dvivth.5 ⊢ ( 𝜑 → 𝑀 < 𝑁 )
dvivth.6 ⊢ ( 𝜑 → 𝐶 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑁 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑀 ) ) )
dvivth.7 ⊢ 𝐺 = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐶 · 𝑦 ) ) )
Assertion dvivthlem1 ( 𝜑 → ∃ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 )

Proof

Step Hyp Ref Expression
1 dvivth.1 ⊢ ( 𝜑 → 𝑀 ∈ ( 𝐴 (,) 𝐵 ) )
2 dvivth.2 ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐴 (,) 𝐵 ) )
3 dvivth.3 ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )
4 dvivth.4 ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
5 dvivth.5 ⊢ ( 𝜑 → 𝑀 < 𝑁 )
6 dvivth.6 ⊢ ( 𝜑 → 𝐶 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑁 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑀 ) ) )
7 dvivth.7 ⊢ 𝐺 = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐶 · 𝑦 ) ) )
8 ioossre ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
9 8 1 sselid ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
10 8 2 sselid ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
11 9 10 5 ltled ⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
12 cncff ⊢ ( 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
13 3 12 syl ⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
14 13 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
15 dvfre ⊢ ( ( 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℝ ) → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
16 13 8 15 sylancl ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
17 2 4 eleqtrrd ⊢ ( 𝜑 → 𝑁 ∈ dom ( ℝ D 𝐹 ) )
18 16 17 ffvelcdmd ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ∈ ℝ )
19 1 4 eleqtrrd ⊢ ( 𝜑 → 𝑀 ∈ dom ( ℝ D 𝐹 ) )
20 16 19 ffvelcdmd ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ‘ 𝑀 ) ∈ ℝ )
21 iccssre ⊢ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ∈ ℝ ∧ ( ( ℝ D 𝐹 ) ‘ 𝑀 ) ∈ ℝ ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑁 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑀 ) ) ⊆ ℝ )
22 18 20 21 syl2anc ⊢ ( 𝜑 → ( ( ( ℝ D 𝐹 ) ‘ 𝑁 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑀 ) ) ⊆ ℝ )
23 22 6 sseldd ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐶 ∈ ℝ )
25 8 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
26 25 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑦 ∈ ℝ )
27 24 26 remulcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐶 · 𝑦 ) ∈ ℝ )
28 14 27 resubcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ 𝑦 ) − ( 𝐶 · 𝑦 ) ) ∈ ℝ )
29 28 7 fmptd ⊢ ( 𝜑 → 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
30 iccssioo2 ⊢ ( ( 𝑀 ∈ ( 𝐴 (,) 𝐵 ) ∧ 𝑁 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝑀 [,] 𝑁 ) ⊆ ( 𝐴 (,) 𝐵 ) )
31 1 2 30 syl2anc ⊢ ( 𝜑 → ( 𝑀 [,] 𝑁 ) ⊆ ( 𝐴 (,) 𝐵 ) )
32 29 31 fssresd ⊢ ( 𝜑 → ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) : ( 𝑀 [,] 𝑁 ) ⟶ ℝ )
33 ax-resscn ⊢ ℝ ⊆ ℂ
34 33 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
35 fss ⊢ ( ( 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
36 29 33 35 sylancl ⊢ ( 𝜑 → 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
37 7 oveq2i ⊢ ( ℝ D 𝐺 ) = ( ℝ D ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐶 · 𝑦 ) ) ) )
38 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
39 38 a1i ⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
40 14 recnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
41 4 feq2d ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ ↔ ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ ) )
42 16 41 mpbid ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
43 42 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ∈ ℝ )
44 13 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑦 ) ) )
45 44 oveq2d ⊢ ( 𝜑 → ( ℝ D 𝐹 ) = ( ℝ D ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑦 ) ) ) )
46 42 feqmptd ⊢ ( 𝜑 → ( ℝ D 𝐹 ) = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) )
47 45 46 eqtr3d ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) )
48 27 recnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐶 · 𝑦 ) ∈ ℂ )
49 remulcl ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝐶 · 𝑦 ) ∈ ℝ )
50 23 49 sylan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐶 · 𝑦 ) ∈ ℝ )
51 50 recnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐶 · 𝑦 ) ∈ ℂ )
52 23 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝐶 ∈ ℝ )
53 34 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℂ )
54 1cnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 1 ∈ ℂ )
55 39 dvmptid ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ℝ ↦ 𝑦 ) ) = ( 𝑦 ∈ ℝ ↦ 1 ) )
56 23 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
57 39 53 54 55 56 dvmptcmul ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ℝ ↦ ( 𝐶 · 𝑦 ) ) ) = ( 𝑦 ∈ ℝ ↦ ( 𝐶 · 1 ) ) )
58 56 mulridd ⊢ ( 𝜑 → ( 𝐶 · 1 ) = 𝐶 )
59 58 mpteq2dv ⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ ( 𝐶 · 1 ) ) = ( 𝑦 ∈ ℝ ↦ 𝐶 ) )
60 57 59 eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ℝ ↦ ( 𝐶 · 𝑦 ) ) ) = ( 𝑦 ∈ ℝ ↦ 𝐶 ) )
61 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
62 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
63 iooretop ⊢ ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) )
64 63 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) ) )
65 39 51 52 60 25 61 62 64 dvmptres ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐶 · 𝑦 ) ) ) = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐶 ) )
66 39 40 43 47 48 24 65 dvmptsub ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐶 · 𝑦 ) ) ) ) = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) − 𝐶 ) ) )
67 37 66 eqtrid ⊢ ( 𝜑 → ( ℝ D 𝐺 ) = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) − 𝐶 ) ) )
68 67 dmeqd ⊢ ( 𝜑 → dom ( ℝ D 𝐺 ) = dom ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) − 𝐶 ) ) )
69 dmmptg ⊢ ( ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) − 𝐶 ) ∈ V → dom ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) − 𝐶 ) ) = ( 𝐴 (,) 𝐵 ) )
70 ovex ⊢ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) − 𝐶 ) ∈ V
71 70 a1i ⊢ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) − 𝐶 ) ∈ V )
72 69 71 mprg ⊢ dom ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) − 𝐶 ) ) = ( 𝐴 (,) 𝐵 )
73 68 72 eqtrdi ⊢ ( 𝜑 → dom ( ℝ D 𝐺 ) = ( 𝐴 (,) 𝐵 ) )
74 dvcn ⊢ ( ( ( ℝ ⊆ ℂ ∧ 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℝ ) ∧ dom ( ℝ D 𝐺 ) = ( 𝐴 (,) 𝐵 ) ) → 𝐺 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
75 34 36 25 73 74 syl31anc ⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
76 rescncf ⊢ ( ( 𝑀 [,] 𝑁 ) ⊆ ( 𝐴 (,) 𝐵 ) → ( 𝐺 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) → ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℂ ) ) )
77 31 75 76 sylc ⊢ ( 𝜑 → ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℂ ) )
78 cncfcdm ⊢ ( ( ℝ ⊆ ℂ ∧ ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℂ ) ) → ( ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℝ ) ↔ ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) : ( 𝑀 [,] 𝑁 ) ⟶ ℝ ) )
79 33 77 78 sylancr ⊢ ( 𝜑 → ( ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℝ ) ↔ ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) : ( 𝑀 [,] 𝑁 ) ⟶ ℝ ) )
80 32 79 mpbird ⊢ ( 𝜑 → ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℝ ) )
81 9 10 11 80 evthicc ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ∀ 𝑧 ∈ ( 𝑀 [,] 𝑁 ) ( ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ‘ 𝑧 ) ≤ ( ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ‘ 𝑥 ) ∧ ∃ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ∀ 𝑧 ∈ ( 𝑀 [,] 𝑁 ) ( ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ‘ 𝑥 ) ≤ ( ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ‘ 𝑧 ) ) )
82 81 simpld ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ∀ 𝑧 ∈ ( 𝑀 [,] 𝑁 ) ( ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ‘ 𝑧 ) ≤ ( ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ‘ 𝑥 ) )
83 fvres ⊢ ( 𝑧 ∈ ( 𝑀 [,] 𝑁 ) → ( ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
84 fvres ⊢ ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) → ( ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
85 83 84 breqan12rd ⊢ ( ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ∧ 𝑧 ∈ ( 𝑀 [,] 𝑁 ) ) → ( ( ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ‘ 𝑧 ) ≤ ( ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ‘ 𝑥 ) ↔ ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) )
86 85 ralbidva ⊢ ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) → ( ∀ 𝑧 ∈ ( 𝑀 [,] 𝑁 ) ( ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ‘ 𝑧 ) ≤ ( ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ‘ 𝑥 ) ↔ ∀ 𝑧 ∈ ( 𝑀 [,] 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) )
87 86 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( ∀ 𝑧 ∈ ( 𝑀 [,] 𝑁 ) ( ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ‘ 𝑧 ) ≤ ( ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ‘ 𝑥 ) ↔ ∀ 𝑧 ∈ ( 𝑀 [,] 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) )
88 ioossicc ⊢ ( 𝑀 (,) 𝑁 ) ⊆ ( 𝑀 [,] 𝑁 )
89 ssralv ⊢ ( ( 𝑀 (,) 𝑁 ) ⊆ ( 𝑀 [,] 𝑁 ) → ( ∀ 𝑧 ∈ ( 𝑀 [,] 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) → ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) )
90 88 89 ax-mp ⊢ ( ∀ 𝑧 ∈ ( 𝑀 [,] 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) → ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) )
91 87 90 biimtrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( ∀ 𝑧 ∈ ( 𝑀 [,] 𝑁 ) ( ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ‘ 𝑧 ) ≤ ( ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ‘ 𝑥 ) → ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) )
92 31 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
93 42 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℝ )
94 92 93 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℝ )
95 94 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℂ )
96 95 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℂ )
97 56 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝐶 ∈ ℂ )
98 67 fveq1d ⊢ ( 𝜑 → ( ( ℝ D 𝐺 ) ‘ 𝑥 ) = ( ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) − 𝐶 ) ) ‘ 𝑥 ) )
99 98 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( ( ℝ D 𝐺 ) ‘ 𝑥 ) = ( ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) − 𝐶 ) ) ‘ 𝑥 ) )
100 fveq2 ⊢ ( 𝑦 = 𝑥 → ( ( ℝ D 𝐹 ) ‘ 𝑦 ) = ( ( ℝ D 𝐹 ) ‘ 𝑥 ) )
101 100 oveq1d ⊢ ( 𝑦 = 𝑥 → ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) − 𝐶 ) = ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) − 𝐶 ) )
102 eqid ⊢ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) − 𝐶 ) ) = ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) − 𝐶 ) )
103 ovex ⊢ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) − 𝐶 ) ∈ V
104 101 102 103 fvmpt ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ( ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) − 𝐶 ) ) ‘ 𝑥 ) = ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) − 𝐶 ) )
105 92 104 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑦 ) − 𝐶 ) ) ‘ 𝑥 ) = ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) − 𝐶 ) )
106 99 105 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( ( ℝ D 𝐺 ) ‘ 𝑥 ) = ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) − 𝐶 ) )
107 106 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ℝ D 𝐺 ) ‘ 𝑥 ) = ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) − 𝐶 ) )
108 29 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
109 8 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
110 simprl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝑥 ∈ ( 𝑀 (,) 𝑁 ) )
111 88 31 sstrid ⊢ ( 𝜑 → ( 𝑀 (,) 𝑁 ) ⊆ ( 𝐴 (,) 𝐵 ) )
112 111 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( 𝑀 (,) 𝑁 ) ⊆ ( 𝐴 (,) 𝐵 ) )
113 92 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
114 73 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → dom ( ℝ D 𝐺 ) = ( 𝐴 (,) 𝐵 ) )
115 113 114 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝑥 ∈ dom ( ℝ D 𝐺 ) )
116 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) )
117 fveq2 ⊢ ( 𝑧 = 𝑤 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑤 ) )
118 117 breq1d ⊢ ( 𝑧 = 𝑤 → ( ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ↔ ( 𝐺 ‘ 𝑤 ) ≤ ( 𝐺 ‘ 𝑥 ) ) )
119 118 cbvralvw ⊢ ( ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ↔ ∀ 𝑤 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑤 ) ≤ ( 𝐺 ‘ 𝑥 ) )
120 116 119 sylib ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ∀ 𝑤 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑤 ) ≤ ( 𝐺 ‘ 𝑥 ) )
121 108 109 110 112 115 120 dvferm ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ℝ D 𝐺 ) ‘ 𝑥 ) = 0 )
122 107 121 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) − 𝐶 ) = 0 )
123 96 97 122 subeq0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 )
124 123 exp32 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) → ( ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 ) ) )
125 vex ⊢ 𝑥 ∈ V
126 125 elpr ⊢ ( 𝑥 ∈ { 𝑀 , 𝑁 } ↔ ( 𝑥 = 𝑀 ∨ 𝑥 = 𝑁 ) )
127 106 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ℝ D 𝐺 ) ‘ 𝑥 ) = ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) − 𝐶 ) )
128 29 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
129 8 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
130 simprl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝑥 = 𝑀 )
131 eliooord ⊢ ( 𝑀 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 < 𝑀 ∧ 𝑀 < 𝐵 ) )
132 1 131 syl ⊢ ( 𝜑 → ( 𝐴 < 𝑀 ∧ 𝑀 < 𝐵 ) )
133 132 simpld ⊢ ( 𝜑 → 𝐴 < 𝑀 )
134 ne0i ⊢ ( 𝑀 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 (,) 𝐵 ) ≠ ∅ )
135 ndmioo ⊢ ( ¬ ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 (,) 𝐵 ) = ∅ )
136 135 necon1ai ⊢ ( ( 𝐴 (,) 𝐵 ) ≠ ∅ → ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) )
137 1 134 136 3syl ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) )
138 137 simpld ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
139 10 rexrd ⊢ ( 𝜑 → 𝑁 ∈ ℝ* )
140 elioo2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝑁 ∈ ℝ* ) → ( 𝑀 ∈ ( 𝐴 (,) 𝑁 ) ↔ ( 𝑀 ∈ ℝ ∧ 𝐴 < 𝑀 ∧ 𝑀 < 𝑁 ) ) )
141 138 139 140 syl2anc ⊢ ( 𝜑 → ( 𝑀 ∈ ( 𝐴 (,) 𝑁 ) ↔ ( 𝑀 ∈ ℝ ∧ 𝐴 < 𝑀 ∧ 𝑀 < 𝑁 ) ) )
142 9 133 5 141 mpbir3and ⊢ ( 𝜑 → 𝑀 ∈ ( 𝐴 (,) 𝑁 ) )
143 142 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝑀 ∈ ( 𝐴 (,) 𝑁 ) )
144 130 143 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝑥 ∈ ( 𝐴 (,) 𝑁 ) )
145 137 simprd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
146 eliooord ⊢ ( 𝑁 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 < 𝑁 ∧ 𝑁 < 𝐵 ) )
147 2 146 syl ⊢ ( 𝜑 → ( 𝐴 < 𝑁 ∧ 𝑁 < 𝐵 ) )
148 147 simprd ⊢ ( 𝜑 → 𝑁 < 𝐵 )
149 139 145 148 xrltled ⊢ ( 𝜑 → 𝑁 ≤ 𝐵 )
150 iooss2 ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑁 ≤ 𝐵 ) → ( 𝐴 (,) 𝑁 ) ⊆ ( 𝐴 (,) 𝐵 ) )
151 145 149 150 syl2anc ⊢ ( 𝜑 → ( 𝐴 (,) 𝑁 ) ⊆ ( 𝐴 (,) 𝐵 ) )
152 151 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( 𝐴 (,) 𝑁 ) ⊆ ( 𝐴 (,) 𝐵 ) )
153 92 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
154 73 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → dom ( ℝ D 𝐺 ) = ( 𝐴 (,) 𝐵 ) )
155 153 154 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝑥 ∈ dom ( ℝ D 𝐺 ) )
156 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) )
157 156 119 sylib ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ∀ 𝑤 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑤 ) ≤ ( 𝐺 ‘ 𝑥 ) )
158 130 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( 𝑥 (,) 𝑁 ) = ( 𝑀 (,) 𝑁 ) )
159 157 158 raleqtrrdv ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ∀ 𝑤 ∈ ( 𝑥 (,) 𝑁 ) ( 𝐺 ‘ 𝑤 ) ≤ ( 𝐺 ‘ 𝑥 ) )
160 128 129 144 152 155 159 dvferm1 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ℝ D 𝐺 ) ‘ 𝑥 ) ≤ 0 )
161 127 160 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) − 𝐶 ) ≤ 0 )
162 94 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℝ )
163 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝐶 ∈ ℝ )
164 162 163 suble0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) − 𝐶 ) ≤ 0 ↔ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ≤ 𝐶 ) )
165 161 164 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ≤ 𝐶 )
166 elicc2 ⊢ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ∈ ℝ ∧ ( ( ℝ D 𝐹 ) ‘ 𝑀 ) ∈ ℝ ) → ( 𝐶 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑁 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑀 ) ) ↔ ( 𝐶 ∈ ℝ ∧ ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ≤ 𝐶 ∧ 𝐶 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑀 ) ) ) )
167 18 20 166 syl2anc ⊢ ( 𝜑 → ( 𝐶 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑁 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑀 ) ) ↔ ( 𝐶 ∈ ℝ ∧ ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ≤ 𝐶 ∧ 𝐶 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑀 ) ) ) )
168 6 167 mpbid ⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ≤ 𝐶 ∧ 𝐶 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑀 ) ) )
169 168 simp3d ⊢ ( 𝜑 → 𝐶 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑀 ) )
170 169 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝐶 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑀 ) )
171 130 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = ( ( ℝ D 𝐹 ) ‘ 𝑀 ) )
172 170 171 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝐶 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) )
173 162 163 letri3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 ↔ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ≤ 𝐶 ∧ 𝐶 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) )
174 165 172 173 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 )
175 174 exp32 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( 𝑥 = 𝑀 → ( ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 ) ) )
176 simprl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝑥 = 𝑁 )
177 176 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = ( ( ℝ D 𝐹 ) ‘ 𝑁 ) )
178 168 simp2d ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ≤ 𝐶 )
179 178 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ≤ 𝐶 )
180 177 179 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ≤ 𝐶 )
181 29 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
182 8 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
183 9 rexrd ⊢ ( 𝜑 → 𝑀 ∈ ℝ* )
184 elioo2 ⊢ ( ( 𝑀 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑁 ∈ ( 𝑀 (,) 𝐵 ) ↔ ( 𝑁 ∈ ℝ ∧ 𝑀 < 𝑁 ∧ 𝑁 < 𝐵 ) ) )
185 183 145 184 syl2anc ⊢ ( 𝜑 → ( 𝑁 ∈ ( 𝑀 (,) 𝐵 ) ↔ ( 𝑁 ∈ ℝ ∧ 𝑀 < 𝑁 ∧ 𝑁 < 𝐵 ) ) )
186 10 5 148 185 mpbir3and ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑀 (,) 𝐵 ) )
187 186 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝑁 ∈ ( 𝑀 (,) 𝐵 ) )
188 176 187 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝑥 ∈ ( 𝑀 (,) 𝐵 ) )
189 138 183 133 xrltled ⊢ ( 𝜑 → 𝐴 ≤ 𝑀 )
190 iooss1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝑀 ) → ( 𝑀 (,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐵 ) )
191 138 189 190 syl2anc ⊢ ( 𝜑 → ( 𝑀 (,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐵 ) )
192 191 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( 𝑀 (,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐵 ) )
193 92 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
194 73 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → dom ( ℝ D 𝐺 ) = ( 𝐴 (,) 𝐵 ) )
195 193 194 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝑥 ∈ dom ( ℝ D 𝐺 ) )
196 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) )
197 196 119 sylib ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ∀ 𝑤 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑤 ) ≤ ( 𝐺 ‘ 𝑥 ) )
198 176 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( 𝑀 (,) 𝑥 ) = ( 𝑀 (,) 𝑁 ) )
199 197 198 raleqtrrdv ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ∀ 𝑤 ∈ ( 𝑀 (,) 𝑥 ) ( 𝐺 ‘ 𝑤 ) ≤ ( 𝐺 ‘ 𝑥 ) )
200 181 182 188 192 195 199 dvferm2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 0 ≤ ( ( ℝ D 𝐺 ) ‘ 𝑥 ) )
201 106 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ℝ D 𝐺 ) ‘ 𝑥 ) = ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) − 𝐶 ) )
202 200 201 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 0 ≤ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) − 𝐶 ) )
203 94 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℝ )
204 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝐶 ∈ ℝ )
205 203 204 subge0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( 0 ≤ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) − 𝐶 ) ↔ 𝐶 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
206 202 205 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝐶 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) )
207 203 204 letri3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 ↔ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ≤ 𝐶 ∧ 𝐶 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) )
208 180 206 207 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 )
209 208 exp32 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( 𝑥 = 𝑁 → ( ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 ) ) )
210 175 209 jaod ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( ( 𝑥 = 𝑀 ∨ 𝑥 = 𝑁 ) → ( ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 ) ) )
211 126 210 biimtrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( 𝑥 ∈ { 𝑀 , 𝑁 } → ( ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 ) ) )
212 elun ⊢ ( 𝑥 ∈ ( ( 𝑀 (,) 𝑁 ) ∪ { 𝑀 , 𝑁 } ) ↔ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ∨ 𝑥 ∈ { 𝑀 , 𝑁 } ) )
213 prunioo ⊢ ( ( 𝑀 ∈ ℝ* ∧ 𝑁 ∈ ℝ* ∧ 𝑀 ≤ 𝑁 ) → ( ( 𝑀 (,) 𝑁 ) ∪ { 𝑀 , 𝑁 } ) = ( 𝑀 [,] 𝑁 ) )
214 183 139 11 213 syl3anc ⊢ ( 𝜑 → ( ( 𝑀 (,) 𝑁 ) ∪ { 𝑀 , 𝑁 } ) = ( 𝑀 [,] 𝑁 ) )
215 214 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 𝑀 (,) 𝑁 ) ∪ { 𝑀 , 𝑁 } ) ↔ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) )
216 212 215 bitr3id ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ∨ 𝑥 ∈ { 𝑀 , 𝑁 } ) ↔ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) )
217 216 biimpar ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ∨ 𝑥 ∈ { 𝑀 , 𝑁 } ) )
218 124 211 217 mpjaod ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 ) )
219 91 218 syld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( ∀ 𝑧 ∈ ( 𝑀 [,] 𝑁 ) ( ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ‘ 𝑧 ) ≤ ( ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ‘ 𝑥 ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 ) )
220 219 reximdva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ∀ 𝑧 ∈ ( 𝑀 [,] 𝑁 ) ( ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ‘ 𝑧 ) ≤ ( ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ‘ 𝑥 ) → ∃ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 ) )
221 82 220 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 )