iccpartrn

Description: If there is a partition, then all intermediate points and bounds are contained in a closed interval of extended reals. (Contributed by AV, 14-Jul-2020)

	Ref	Expression
Hypotheses	iccpartgtprec.m	$⊢ φ \to M \in ℕ$
	iccpartgtprec.p	$⊢ φ \to P \in RePart (M)$
Assertion	iccpartrn	$⊢ φ \to ran P \subseteq [P (0), P (M)]$

Proof

Step	Hyp	Ref	Expression
1		iccpartgtprec.m	$⊢ φ \to M \in ℕ$
2		iccpartgtprec.p	$⊢ φ \to P \in RePart (M)$
3		iccpart	$⊢ M \in ℕ \to (P \in RePart (M) \leftrightarrow (P \in ({ℝ^{*}}^{(0 \dots M)}) \land \forall i \in (0 ..^M) P (i) < P (i + 1)))$
4	1 3	syl	$⊢ φ \to (P \in RePart (M) \leftrightarrow (P \in ({ℝ^{*}}^{(0 \dots M)}) \land \forall i \in (0 ..^M) P (i) < P (i + 1)))$
5		elmapfn	$⊢ P \in ({ℝ^{*}}^{(0 \dots M)}) \to P Fn (0 \dots M)$
6	5	adantr	$⊢ (P \in ({ℝ^{*}}^{(0 \dots M)}) \land \forall i \in (0 ..^M) P (i) < P (i + 1)) \to P Fn (0 \dots M)$
7	4 6	biimtrdi	$⊢ φ \to (P \in RePart (M) \to P Fn (0 \dots M))$
8	2 7	mpd	$⊢ φ \to P Fn (0 \dots M)$
9		fvelrnb	$⊢ P Fn (0 \dots M) \to (p \in ran P \leftrightarrow \exists i \in (0 \dots M) P (i) = p)$
10	8 9	syl	$⊢ φ \to (p \in ran P \leftrightarrow \exists i \in (0 \dots M) P (i) = p)$
11	1	adantr	$⊢ (φ \land i \in (0 \dots M)) \to M \in ℕ$
12	2	adantr	$⊢ (φ \land i \in (0 \dots M)) \to P \in RePart (M)$
13		simpr	$⊢ (φ \land i \in (0 \dots M)) \to i \in (0 \dots M)$
14	11 12 13	iccpartxr	$⊢ (φ \land i \in (0 \dots M)) \to P (i) \in ℝ^{*}$
15	1 2	iccpartgel	$⊢ φ \to \forall k \in (0 \dots M) P (0) \leq P (k)$
16		fveq2	$⊢ k = i \to P (k) = P (i)$
17	16	breq2d	$⊢ k = i \to (P (0) \leq P (k) \leftrightarrow P (0) \leq P (i))$
18	17	rspcva	$⊢ (i \in (0 \dots M) \land \forall k \in (0 \dots M) P (0) \leq P (k)) \to P (0) \leq P (i)$
19	18	expcom	$⊢ \forall k \in (0 \dots M) P (0) \leq P (k) \to (i \in (0 \dots M) \to P (0) \leq P (i))$
20	15 19	syl	$⊢ φ \to (i \in (0 \dots M) \to P (0) \leq P (i))$
21	20	imp	$⊢ (φ \land i \in (0 \dots M)) \to P (0) \leq P (i)$
22	1 2	iccpartleu	$⊢ φ \to \forall k \in (0 \dots M) P (k) \leq P (M)$
23	16	breq1d	$⊢ k = i \to (P (k) \leq P (M) \leftrightarrow P (i) \leq P (M))$
24	23	rspcva	$⊢ (i \in (0 \dots M) \land \forall k \in (0 \dots M) P (k) \leq P (M)) \to P (i) \leq P (M)$
25	24	expcom	$⊢ \forall k \in (0 \dots M) P (k) \leq P (M) \to (i \in (0 \dots M) \to P (i) \leq P (M))$
26	22 25	syl	$⊢ φ \to (i \in (0 \dots M) \to P (i) \leq P (M))$
27	26	imp	$⊢ (φ \land i \in (0 \dots M)) \to P (i) \leq P (M)$
28		nnnn0	$⊢ M \in ℕ \to M \in ℕ_{0}$
29		0elfz	$⊢ M \in ℕ_{0} \to 0 \in (0 \dots M)$
30	1 28 29	3syl	$⊢ φ \to 0 \in (0 \dots M)$
31	1 2 30	iccpartxr	$⊢ φ \to P (0) \in ℝ^{*}$
32		nn0fz0	$⊢ M \in ℕ_{0} \leftrightarrow M \in (0 \dots M)$
33	28 32	sylib	$⊢ M \in ℕ \to M \in (0 \dots M)$
34	1 33	syl	$⊢ φ \to M \in (0 \dots M)$
35	1 2 34	iccpartxr	$⊢ φ \to P (M) \in ℝ^{*}$
36	31 35	jca	$⊢ φ \to (P (0) \in ℝ^{} \land P (M) \in ℝ^{})$
37	36	adantr	$⊢ (φ \land i \in (0 \dots M)) \to (P (0) \in ℝ^{} \land P (M) \in ℝ^{})$
38		elicc1	$⊢ (P (0) \in ℝ^{} \land P (M) \in ℝ^{}) \to (P (i) \in [P (0), P (M)] \leftrightarrow (P (i) \in ℝ^{*} \land P (0) \leq P (i) \land P (i) \leq P (M)))$
39	37 38	syl	$⊢ (φ \land i \in (0 \dots M)) \to (P (i) \in [P (0), P (M)] \leftrightarrow (P (i) \in ℝ^{*} \land P (0) \leq P (i) \land P (i) \leq P (M)))$
40	14 21 27 39	mpbir3and	$⊢ (φ \land i \in (0 \dots M)) \to P (i) \in [P (0), P (M)]$
41		eleq1	$⊢ P (i) = p \to (P (i) \in [P (0), P (M)] \leftrightarrow p \in [P (0), P (M)])$
42	40 41	syl5ibcom	$⊢ (φ \land i \in (0 \dots M)) \to (P (i) = p \to p \in [P (0), P (M)])$
43	42	rexlimdva	$⊢ φ \to (\exists i \in (0 \dots M) P (i) = p \to p \in [P (0), P (M)])$
44	10 43	sylbid	$⊢ φ \to (p \in ran P \to p \in [P (0), P (M)])$
45	44	ssrdv	$⊢ φ \to ran P \subseteq [P (0), P (M)]$

Metamath Proof Explorer

Theorem iccpartrn

Proof