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		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
62	61	tgioo2	⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
63		iooretop	⊢ ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) )
64	63	a1i	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ ( topGen ‘ ran (,) ) )
65	39 51 52 60 25 62 61 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	syl6bi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( ∀ 𝑧 ∈ ( 𝑀 [,] 𝑁 ) ( ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ‘ 𝑧 ) ≤ ( ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ‘ 𝑥 ) → ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) )
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	158	raleqdv	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ∀ 𝑤 ∈ ( 𝑥 (,) 𝑁 ) ( 𝐺 ‘ 𝑤 ) ≤ ( 𝐺 ‘ 𝑥 ) ↔ ∀ 𝑤 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑤 ) ≤ ( 𝐺 ‘ 𝑥 ) ) )
160	157 159	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ∀ 𝑤 ∈ ( 𝑥 (,) 𝑁 ) ( 𝐺 ‘ 𝑤 ) ≤ ( 𝐺 ‘ 𝑥 ) )
161	128 129 144 152 155 160	dvferm1	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ℝ D 𝐺 ) ‘ 𝑥 ) ≤ 0 )
162	127 161	eqbrtrrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) − 𝐶 ) ≤ 0 )
163	94	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℝ )
164	23	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝐶 ∈ ℝ )
165	163 164	suble0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) − 𝐶 ) ≤ 0 ↔ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ≤ 𝐶 ) )
166	162 165	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ≤ 𝐶 )
167		elicc2	⊢ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ∈ ℝ ∧ ( ( ℝ D 𝐹 ) ‘ 𝑀 ) ∈ ℝ ) → ( 𝐶 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑁 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑀 ) ) ↔ ( 𝐶 ∈ ℝ ∧ ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ≤ 𝐶 ∧ 𝐶 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑀 ) ) ) )
168	18 20 167	syl2anc	⊢ ( 𝜑 → ( 𝐶 ∈ ( ( ( ℝ D 𝐹 ) ‘ 𝑁 ) [,] ( ( ℝ D 𝐹 ) ‘ 𝑀 ) ) ↔ ( 𝐶 ∈ ℝ ∧ ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ≤ 𝐶 ∧ 𝐶 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑀 ) ) ) )
169	6 168	mpbid	⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ≤ 𝐶 ∧ 𝐶 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑀 ) ) )
170	169	simp3d	⊢ ( 𝜑 → 𝐶 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑀 ) )
171	170	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝐶 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑀 ) )
172	130	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = ( ( ℝ D 𝐹 ) ‘ 𝑀 ) )
173	171 172	breqtrrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝐶 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) )
174	163 164	letri3d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 ↔ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ≤ 𝐶 ∧ 𝐶 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) )
175	166 173 174	mpbir2and	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑀 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 )
176	175	exp32	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( 𝑥 = 𝑀 → ( ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 ) ) )
177		simprl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝑥 = 𝑁 )
178	177	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = ( ( ℝ D 𝐹 ) ‘ 𝑁 ) )
179	169	simp2d	⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ≤ 𝐶 )
180	179	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑁 ) ≤ 𝐶 )
181	178 180	eqbrtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ≤ 𝐶 )
182	29	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝐺 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
183	8	a1i	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
184	9	rexrd	⊢ ( 𝜑 → 𝑀 ∈ ℝ* )
185		elioo2	⊢ ( ( 𝑀 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑁 ∈ ( 𝑀 (,) 𝐵 ) ↔ ( 𝑁 ∈ ℝ ∧ 𝑀 < 𝑁 ∧ 𝑁 < 𝐵 ) ) )
186	184 145 185	syl2anc	⊢ ( 𝜑 → ( 𝑁 ∈ ( 𝑀 (,) 𝐵 ) ↔ ( 𝑁 ∈ ℝ ∧ 𝑀 < 𝑁 ∧ 𝑁 < 𝐵 ) ) )
187	10 5 148 186	mpbir3and	⊢ ( 𝜑 → 𝑁 ∈ ( 𝑀 (,) 𝐵 ) )
188	187	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝑁 ∈ ( 𝑀 (,) 𝐵 ) )
189	177 188	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝑥 ∈ ( 𝑀 (,) 𝐵 ) )
190	138 184 133	xrltled	⊢ ( 𝜑 → 𝐴 ≤ 𝑀 )
191		iooss1	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝑀 ) → ( 𝑀 (,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐵 ) )
192	138 190 191	syl2anc	⊢ ( 𝜑 → ( 𝑀 (,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐵 ) )
193	192	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( 𝑀 (,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐵 ) )
194	92	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
195	73	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → dom ( ℝ D 𝐺 ) = ( 𝐴 (,) 𝐵 ) )
196	194 195	eleqtrrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝑥 ∈ dom ( ℝ D 𝐺 ) )
197		simprr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) )
198	197 119	sylib	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ∀ 𝑤 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑤 ) ≤ ( 𝐺 ‘ 𝑥 ) )
199	177	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( 𝑀 (,) 𝑥 ) = ( 𝑀 (,) 𝑁 ) )
200	199	raleqdv	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ∀ 𝑤 ∈ ( 𝑀 (,) 𝑥 ) ( 𝐺 ‘ 𝑤 ) ≤ ( 𝐺 ‘ 𝑥 ) ↔ ∀ 𝑤 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑤 ) ≤ ( 𝐺 ‘ 𝑥 ) ) )
201	198 200	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ∀ 𝑤 ∈ ( 𝑀 (,) 𝑥 ) ( 𝐺 ‘ 𝑤 ) ≤ ( 𝐺 ‘ 𝑥 ) )
202	182 183 189 193 196 201	dvferm2	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 0 ≤ ( ( ℝ D 𝐺 ) ‘ 𝑥 ) )
203	106	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ℝ D 𝐺 ) ‘ 𝑥 ) = ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) − 𝐶 ) )
204	202 203	breqtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 0 ≤ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) − 𝐶 ) )
205	94	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℝ )
206	23	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝐶 ∈ ℝ )
207	205 206	subge0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( 0 ≤ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) − 𝐶 ) ↔ 𝐶 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
208	204 207	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → 𝐶 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) )
209	205 206	letri3d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 ↔ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ≤ 𝐶 ∧ 𝐶 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) )
210	181 208 209	mpbir2and	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) ∧ ( 𝑥 = 𝑁 ∧ ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 )
211	210	exp32	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( 𝑥 = 𝑁 → ( ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 ) ) )
212	176 211	jaod	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( ( 𝑥 = 𝑀 ∨ 𝑥 = 𝑁 ) → ( ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 ) ) )
213	126 212	biimtrid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( 𝑥 ∈ { 𝑀 , 𝑁 } → ( ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 ) ) )
214		elun	⊢ ( 𝑥 ∈ ( ( 𝑀 (,) 𝑁 ) ∪ { 𝑀 , 𝑁 } ) ↔ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ∨ 𝑥 ∈ { 𝑀 , 𝑁 } ) )
215		prunioo	⊢ ( ( 𝑀 ∈ ℝ* ∧ 𝑁 ∈ ℝ* ∧ 𝑀 ≤ 𝑁 ) → ( ( 𝑀 (,) 𝑁 ) ∪ { 𝑀 , 𝑁 } ) = ( 𝑀 [,] 𝑁 ) )
216	184 139 11 215	syl3anc	⊢ ( 𝜑 → ( ( 𝑀 (,) 𝑁 ) ∪ { 𝑀 , 𝑁 } ) = ( 𝑀 [,] 𝑁 ) )
217	216	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 𝑀 (,) 𝑁 ) ∪ { 𝑀 , 𝑁 } ) ↔ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) )
218	214 217	bitr3id	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ∨ 𝑥 ∈ { 𝑀 , 𝑁 } ) ↔ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) )
219	218	biimpar	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ∨ 𝑥 ∈ { 𝑀 , 𝑁 } ) )
220	124 213 219	mpjaod	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( ∀ 𝑧 ∈ ( 𝑀 (,) 𝑁 ) ( 𝐺 ‘ 𝑧 ) ≤ ( 𝐺 ‘ 𝑥 ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 ) )
221	91 220	syld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( ∀ 𝑧 ∈ ( 𝑀 [,] 𝑁 ) ( ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ‘ 𝑧 ) ≤ ( ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ‘ 𝑥 ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 ) )
222	221	reximdva	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ∀ 𝑧 ∈ ( 𝑀 [,] 𝑁 ) ( ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ‘ 𝑧 ) ≤ ( ( 𝐺 ↾ ( 𝑀 [,] 𝑁 ) ) ‘ 𝑥 ) → ∃ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 ) )
223	82 222	mpd	⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 𝐶 )