dvivth

Description: Darboux' theorem, or the intermediate value theorem for derivatives. A differentiable function's derivative satisfies the intermediate value property, even though it may not be continuous (so that ivthicc does not directly apply). (Contributed by Mario Carneiro, 24-Feb-2015)

	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)$
Assertion	dvivth	$⊢ φ \to [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)] \subseteq ran F_{ℝ}^{'}$

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	1	adantr	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to M \in (A, B)$
6	2	adantr	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to N \in (A, B)$
7		cncff	$⊢ F : (A, B) \underset{cn}{⟶} ℝ \to F : (A, B) ⟶ ℝ$
8	3 7	syl	$⊢ φ \to F : (A, B) ⟶ ℝ$
9	8	ffvelrnda	$⊢ (φ \land w \in (A, B)) \to F (w) \in ℝ$
10	9	renegcld	$⊢ (φ \land w \in (A, B)) \to - F (w) \in ℝ$
11	10	fmpttd	$⊢ φ \to (w \in (A, B) ⟼ - F (w)) : (A, B) ⟶ ℝ$
12		ax-resscn	$⊢ ℝ \subseteq ℂ$
13		ssid	$⊢ ℂ \subseteq ℂ$
14		cncfss	$⊢ (ℝ \subseteq ℂ \land ℂ \subseteq ℂ) \to (A, B) \underset{cn}{⟶} ℝ \subseteq (A, B) \underset{cn}{⟶} ℂ$
15	12 13 14	mp2an	$⊢ (A, B) \underset{cn}{⟶} ℝ \subseteq (A, B) \underset{cn}{⟶} ℂ$
16	15 3	sseldi	$⊢ φ \to F : (A, B) \underset{cn}{⟶} ℂ$
17		eqid	$⊢ (w \in (A, B) ⟼ - F (w)) = (w \in (A, B) ⟼ - F (w))$
18	17	negfcncf	$⊢ F : (A, B) \underset{cn}{⟶} ℂ \to (w \in (A, B) ⟼ - F (w)) : (A, B) \underset{cn}{⟶} ℂ$
19	16 18	syl	$⊢ φ \to (w \in (A, B) ⟼ - F (w)) : (A, B) \underset{cn}{⟶} ℂ$
20		cncffvrn	$⊢ (ℝ \subseteq ℂ \land (w \in (A, B) ⟼ - F (w)) : (A, B) \underset{cn}{⟶} ℂ) \to ((w \in (A, B) ⟼ - F (w)) : (A, B) \underset{cn}{⟶} ℝ \leftrightarrow (w \in (A, B) ⟼ - F (w)) : (A, B) ⟶ ℝ)$
21	12 19 20	sylancr	$⊢ φ \to ((w \in (A, B) ⟼ - F (w)) : (A, B) \underset{cn}{⟶} ℝ \leftrightarrow (w \in (A, B) ⟼ - F (w)) : (A, B) ⟶ ℝ)$
22	11 21	mpbird	$⊢ φ \to (w \in (A, B) ⟼ - F (w)) : (A, B) \underset{cn}{⟶} ℝ$
23	22	adantr	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to (w \in (A, B) ⟼ - F (w)) : (A, B) \underset{cn}{⟶} ℝ$
24		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
25	24	a1i	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to ℝ \in \{ℝ, ℂ\}$
26	8	adantr	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to F : (A, B) ⟶ ℝ$
27	26	ffvelrnda	$⊢ ((φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \land w \in (A, B)) \to F (w) \in ℝ$
28	27	recnd	$⊢ ((φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \land w \in (A, B)) \to F (w) \in ℂ$
29		fvexd	$⊢ ((φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \land w \in (A, B)) \to F_{ℝ}^{'} (w) \in V$
30	26	feqmptd	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to F = (w \in (A, B) ⟼ F (w))$
31	30	oveq2d	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to ℝ D F = \frac{d (w \in (A, B)⟼ F (w))}{d_{ℝ} w}$
32		ioossre	$⊢ (A, B) \subseteq ℝ$
33		dvfre	$⊢ (F : (A, B) ⟶ ℝ \land (A, B) \subseteq ℝ) \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$
34	8 32 33	sylancl	$⊢ φ \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$
35	4	feq2d	$⊢ φ \to (F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ \leftrightarrow F_{ℝ}^{'} : (A, B) ⟶ ℝ)$
36	34 35	mpbid	$⊢ φ \to F_{ℝ}^{'} : (A, B) ⟶ ℝ$
37	36	adantr	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to F_{ℝ}^{'} : (A, B) ⟶ ℝ$
38	37	feqmptd	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to ℝ D F = (w \in (A, B) ⟼ F_{ℝ}^{'} (w))$
39	31 38	eqtr3d	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to \frac{d (w \in (A, B)⟼ F (w))}{d_{ℝ} w} = (w \in (A, B) ⟼ F_{ℝ}^{'} (w))$
40	25 28 29 39	dvmptneg	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to \frac{d (w \in (A, B)⟼ - F (w))}{d_{ℝ} w} = (w \in (A, B) ⟼ - F_{ℝ}^{'} (w))$
41	40	dmeqd	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to dom \frac{d (w \in (A, B)⟼ - F (w))}{d_{ℝ} w} = dom (w \in (A, B) ⟼ - F_{ℝ}^{'} (w))$
42		dmmptg	$⊢ \forall w \in (A, B) - F_{ℝ}^{'} (w) \in V \to dom (w \in (A, B) ⟼ - F_{ℝ}^{'} (w)) = (A, B)$
43		negex	$⊢ - F_{ℝ}^{'} (w) \in V$
44	43	a1i	$⊢ w \in (A, B) \to - F_{ℝ}^{'} (w) \in V$
45	42 44	mprg	$⊢ dom (w \in (A, B) ⟼ - F_{ℝ}^{'} (w)) = (A, B)$
46	41 45	eqtrdi	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to dom \frac{d (w \in (A, B)⟼ - F (w))}{d_{ℝ} w} = (A, B)$
47		simprl	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to M < N$
48		simprr	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)]$
49	36 1	ffvelrnd	$⊢ φ \to F_{ℝ}^{'} (M) \in ℝ$
50	49	adantr	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to F_{ℝ}^{'} (M) \in ℝ$
51	2 4	eleqtrrd	$⊢ φ \to N \in dom F_{ℝ}^{'}$
52	34 51	ffvelrnd	$⊢ φ \to F_{ℝ}^{'} (N) \in ℝ$
53	52	adantr	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to F_{ℝ}^{'} (N) \in ℝ$
54		iccssre	$⊢ (F_{ℝ}^{'} (M) \in ℝ \land F_{ℝ}^{'} (N) \in ℝ) \to [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)] \subseteq ℝ$
55	49 52 54	syl2anc	$⊢ φ \to [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)] \subseteq ℝ$
56	55	adantr	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)] \subseteq ℝ$
57	56 48	sseldd	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to x \in ℝ$
58		iccneg	$⊢ (F_{ℝ}^{'} (M) \in ℝ \land F_{ℝ}^{'} (N) \in ℝ \land x \in ℝ) \to (x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)] \leftrightarrow - x \in [- F_{ℝ}^{'} (N), - F_{ℝ}^{'} (M)])$
59	50 53 57 58	syl3anc	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to (x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)] \leftrightarrow - x \in [- F_{ℝ}^{'} (N), - F_{ℝ}^{'} (M)])$
60	48 59	mpbid	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to - x \in [- F_{ℝ}^{'} (N), - F_{ℝ}^{'} (M)]$
61	40	fveq1d	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to \frac{d (w \in (A, B)⟼ - F (w))}{d_{ℝ} w} (N) = (w \in (A, B) ⟼ - F_{ℝ}^{'} (w)) (N)$
62		fveq2	$⊢ w = N \to F_{ℝ}^{'} (w) = F_{ℝ}^{'} (N)$
63	62	negeqd	$⊢ w = N \to - F_{ℝ}^{'} (w) = - F_{ℝ}^{'} (N)$
64		eqid	$⊢ (w \in (A, B) ⟼ - F_{ℝ}^{'} (w)) = (w \in (A, B) ⟼ - F_{ℝ}^{'} (w))$
65		negex	$⊢ - F_{ℝ}^{'} (N) \in V$
66	63 64 65	fvmpt	$⊢ N \in (A, B) \to (w \in (A, B) ⟼ - F_{ℝ}^{'} (w)) (N) = - F_{ℝ}^{'} (N)$
67	6 66	syl	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to (w \in (A, B) ⟼ - F_{ℝ}^{'} (w)) (N) = - F_{ℝ}^{'} (N)$
68	61 67	eqtrd	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to \frac{d (w \in (A, B)⟼ - F (w))}{d_{ℝ} w} (N) = - F_{ℝ}^{'} (N)$
69	40	fveq1d	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to \frac{d (w \in (A, B)⟼ - F (w))}{d_{ℝ} w} (M) = (w \in (A, B) ⟼ - F_{ℝ}^{'} (w)) (M)$
70		fveq2	$⊢ w = M \to F_{ℝ}^{'} (w) = F_{ℝ}^{'} (M)$
71	70	negeqd	$⊢ w = M \to - F_{ℝ}^{'} (w) = - F_{ℝ}^{'} (M)$
72		negex	$⊢ - F_{ℝ}^{'} (M) \in V$
73	71 64 72	fvmpt	$⊢ M \in (A, B) \to (w \in (A, B) ⟼ - F_{ℝ}^{'} (w)) (M) = - F_{ℝ}^{'} (M)$
74	5 73	syl	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to (w \in (A, B) ⟼ - F_{ℝ}^{'} (w)) (M) = - F_{ℝ}^{'} (M)$
75	69 74	eqtrd	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to \frac{d (w \in (A, B)⟼ - F (w))}{d_{ℝ} w} (M) = - F_{ℝ}^{'} (M)$
76	68 75	oveq12d	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to [\frac{d (w \in (A, B)⟼ - F (w))}{d_{ℝ} w} (N), \frac{d (w \in (A, B)⟼ - F (w))}{d_{ℝ} w} (M)] = [- F_{ℝ}^{'} (N), - F_{ℝ}^{'} (M)]$
77	60 76	eleqtrrd	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to - x \in [\frac{d (w \in (A, B)⟼ - F (w))}{d_{ℝ} w} (N), \frac{d (w \in (A, B)⟼ - F (w))}{d_{ℝ} w} (M)]$
78		eqid	$⊢ (y \in (A, B) ⟼ (w \in (A, B) ⟼ - F (w)) (y) - (- x) y) = (y \in (A, B) ⟼ (w \in (A, B) ⟼ - F (w)) (y) - (- x) y)$
79	5 6 23 46 47 77 78	dvivthlem2	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to - x \in ran \frac{d (w \in (A, B)⟼ - F (w))}{d_{ℝ} w}$
80	40	rneqd	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to ran \frac{d (w \in (A, B)⟼ - F (w))}{d_{ℝ} w} = ran (w \in (A, B) ⟼ - F_{ℝ}^{'} (w))$
81	79 80	eleqtrd	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to - x \in ran (w \in (A, B) ⟼ - F_{ℝ}^{'} (w))$
82		negex	$⊢ - x \in V$
83	64	elrnmpt	$⊢ - x \in V \to (- x \in ran (w \in (A, B) ⟼ - F_{ℝ}^{'} (w)) \leftrightarrow \exists w \in (A, B) - x = - F_{ℝ}^{'} (w))$
84	82 83	ax-mp	$⊢ - x \in ran (w \in (A, B) ⟼ - F_{ℝ}^{'} (w)) \leftrightarrow \exists w \in (A, B) - x = - F_{ℝ}^{'} (w)$
85	81 84	sylib	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to \exists w \in (A, B) - x = - F_{ℝ}^{'} (w)$
86	57	recnd	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to x \in ℂ$
87	86	adantr	$⊢ ((φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \land w \in (A, B)) \to x \in ℂ$
88	25 28 29 39	dvmptcl	$⊢ ((φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \land w \in (A, B)) \to F_{ℝ}^{'} (w) \in ℂ$
89	87 88	neg11ad	$⊢ ((φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \land w \in (A, B)) \to (- x = - F_{ℝ}^{'} (w) \leftrightarrow x = F_{ℝ}^{'} (w))$
90		eqcom	$⊢ x = F_{ℝ}^{'} (w) \leftrightarrow F_{ℝ}^{'} (w) = x$
91	89 90	bitrdi	$⊢ ((φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \land w \in (A, B)) \to (- x = - F_{ℝ}^{'} (w) \leftrightarrow F_{ℝ}^{'} (w) = x)$
92	91	rexbidva	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to (\exists w \in (A, B) - x = - F_{ℝ}^{'} (w) \leftrightarrow \exists w \in (A, B) F_{ℝ}^{'} (w) = x)$
93	85 92	mpbid	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to \exists w \in (A, B) F_{ℝ}^{'} (w) = x$
94	37	ffnd	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to F_{ℝ}^{'} Fn (A, B)$
95		fvelrnb	$⊢ F_{ℝ}^{'} Fn (A, B) \to (x \in ran F_{ℝ}^{'} \leftrightarrow \exists w \in (A, B) F_{ℝ}^{'} (w) = x)$
96	94 95	syl	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to (x \in ran F_{ℝ}^{'} \leftrightarrow \exists w \in (A, B) F_{ℝ}^{'} (w) = x)$
97	93 96	mpbird	$⊢ (φ \land (M < N \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to x \in ran F_{ℝ}^{'}$
98	97	expr	$⊢ (φ \land M < N) \to (x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)] \to x \in ran F_{ℝ}^{'})$
99	98	ssrdv	$⊢ (φ \land M < N) \to [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)] \subseteq ran F_{ℝ}^{'}$
100		fveq2	$⊢ M = N \to F_{ℝ}^{'} (M) = F_{ℝ}^{'} (N)$
101	100	oveq1d	$⊢ M = N \to [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)] = [F_{ℝ}^{'} (N), F_{ℝ}^{'} (N)]$
102	52	rexrd	$⊢ φ \to F_{ℝ}^{'} (N) \in ℝ^{*}$
103		iccid	$⊢ F_{ℝ}^{'} (N) \in ℝ^{*} \to [F_{ℝ}^{'} (N), F_{ℝ}^{'} (N)] = \{F_{ℝ}^{'} (N)\}$
104	102 103	syl	$⊢ φ \to [F_{ℝ}^{'} (N), F_{ℝ}^{'} (N)] = \{F_{ℝ}^{'} (N)\}$
105	101 104	sylan9eqr	$⊢ (φ \land M = N) \to [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)] = \{F_{ℝ}^{'} (N)\}$
106	34	ffnd	$⊢ φ \to F_{ℝ}^{'} Fn dom F_{ℝ}^{'}$
107		fnfvelrn	$⊢ (F_{ℝ}^{'} Fn dom F_{ℝ}^{'} \land N \in dom F_{ℝ}^{'}) \to F_{ℝ}^{'} (N) \in ran F_{ℝ}^{'}$
108	106 51 107	syl2anc	$⊢ φ \to F_{ℝ}^{'} (N) \in ran F_{ℝ}^{'}$
109	108	snssd	$⊢ φ \to \{F_{ℝ}^{'} (N)\} \subseteq ran F_{ℝ}^{'}$
110	109	adantr	$⊢ (φ \land M = N) \to \{F_{ℝ}^{'} (N)\} \subseteq ran F_{ℝ}^{'}$
111	105 110	eqsstrd	$⊢ (φ \land M = N) \to [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)] \subseteq ran F_{ℝ}^{'}$
112	2	adantr	$⊢ (φ \land (N < M \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to N \in (A, B)$
113	1	adantr	$⊢ (φ \land (N < M \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to M \in (A, B)$
114	3	adantr	$⊢ (φ \land (N < M \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to F : (A, B) \underset{cn}{⟶} ℝ$
115	4	adantr	$⊢ (φ \land (N < M \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to dom F_{ℝ}^{'} = (A, B)$
116		simprl	$⊢ (φ \land (N < M \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to N < M$
117		simprr	$⊢ (φ \land (N < M \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)]$
118		eqid	$⊢ (y \in (A, B) ⟼ F (y) - x y) = (y \in (A, B) ⟼ F (y) - x y)$
119	112 113 114 115 116 117 118	dvivthlem2	$⊢ (φ \land (N < M \land x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)])) \to x \in ran F_{ℝ}^{'}$
120	119	expr	$⊢ (φ \land N < M) \to (x \in [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)] \to x \in ran F_{ℝ}^{'})$
121	120	ssrdv	$⊢ (φ \land N < M) \to [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)] \subseteq ran F_{ℝ}^{'}$
122	32 1	sseldi	$⊢ φ \to M \in ℝ$
123	32 2	sseldi	$⊢ φ \to N \in ℝ$
124	122 123	lttri4d	$⊢ φ \to (M < N \lor M = N \lor N < M)$
125	99 111 121 124	mpjao3dan	$⊢ φ \to [F_{ℝ}^{'} (M), F_{ℝ}^{'} (N)] \subseteq ran F_{ℝ}^{'}$

Metamath Proof Explorer

Theorem dvivth

Proof