dvivthlem1

	Ref	Expression
Hypotheses	dvivth.1	$⊢ φ \to M \in (A, B)$
	dvivth.2	$⊢ φ \to N \in (A, B)$
	dvivth.3	$⊢ φ \to F : (A, B) \underset{cn}{⟶} ℝ$
	dvivth.4	$⊢ φ \to dom F_{ℝ}^{'} = (A, B)$
	dvivth.5	$⊢ φ \to M < N$
	dvivth.6	$⊢ φ \to C \in [F_{ℝ}^{'} (N), F_{ℝ}^{'} (M)]$
	dvivth.7	$⊢ G = (y \in (A, B) ⟼ F (y) - C y)$
Assertion	dvivthlem1	$⊢ φ \to \exists x \in [M, N] F_{ℝ}^{'} (x) = C$

Proof

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

Metamath Proof Explorer

Theorem dvivthlem1

Proof