iccpartipre

Description: If there is a partition, then all intermediate points are real numbers. (Contributed by AV, 11-Jul-2020)

	Ref	Expression
Hypotheses	iccpartgtprec.m	$⊢ φ \to M \in ℕ$
	iccpartgtprec.p	$⊢ φ \to P \in RePart (M)$
	iccpartipre.i	$⊢ φ \to I \in (1 ..^M)$
Assertion	iccpartipre	$⊢ φ \to P (I) \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		iccpartgtprec.m	$⊢ φ \to M \in ℕ$
2		iccpartgtprec.p	$⊢ φ \to P \in RePart (M)$
3		iccpartipre.i	$⊢ φ \to I \in (1 ..^M)$
4		nnz	$⊢ M \in ℕ \to M \in ℤ$
5		peano2zm	$⊢ M \in ℤ \to M - 1 \in ℤ$
6		id	$⊢ M \in ℤ \to M \in ℤ$
7		zre	$⊢ M \in ℤ \to M \in ℝ$
8	7	lem1d	$⊢ M \in ℤ \to M - 1 \leq M$
9	5 6 8	3jca	$⊢ M \in ℤ \to (M - 1 \in ℤ \land M \in ℤ \land M - 1 \leq M)$
10	4 9	syl	$⊢ M \in ℕ \to (M - 1 \in ℤ \land M \in ℤ \land M - 1 \leq M)$
11		eluz2	$⊢ M \in ℤ_{\geq (M - 1)} \leftrightarrow (M - 1 \in ℤ \land M \in ℤ \land M - 1 \leq M)$
12	10 11	sylibr	$⊢ M \in ℕ \to M \in ℤ_{\geq (M - 1)}$
13	1 12	syl	$⊢ φ \to M \in ℤ_{\geq (M - 1)}$
14		fzss2	$⊢ M \in ℤ_{\geq (M - 1)} \to (0 \dots M - 1) \subseteq (0 \dots M)$
15	13 14	syl	$⊢ φ \to (0 \dots M - 1) \subseteq (0 \dots M)$
16		fzossfz	$⊢ (1 ..^M) \subseteq (1 \dots M)$
17	16 3	sselid	$⊢ φ \to I \in (1 \dots M)$
18		elfzoelz	$⊢ I \in (1 ..^M) \to I \in ℤ$
19	3 18	syl	$⊢ φ \to I \in ℤ$
20	1	nnzd	$⊢ φ \to M \in ℤ$
21		elfzm1b	$⊢ (I \in ℤ \land M \in ℤ) \to (I \in (1 \dots M) \leftrightarrow I - 1 \in (0 \dots M - 1))$
22	19 20 21	syl2anc	$⊢ φ \to (I \in (1 \dots M) \leftrightarrow I - 1 \in (0 \dots M - 1))$
23	17 22	mpbid	$⊢ φ \to I - 1 \in (0 \dots M - 1)$
24	15 23	sseldd	$⊢ φ \to I - 1 \in (0 \dots M)$
25	1 2 24	iccpartxr	$⊢ φ \to P (I - 1) \in ℝ^{*}$
26		1eluzge0	$⊢ 1 \in ℤ_{\geq 0}$
27		fzoss1	$⊢ 1 \in ℤ_{\geq 0} \to (1 ..^M) \subseteq (0 ..^M)$
28	26 27	mp1i	$⊢ φ \to (1 ..^M) \subseteq (0 ..^M)$
29		fzossfz	$⊢ (0 ..^M) \subseteq (0 \dots M)$
30	28 29	sstrdi	$⊢ φ \to (1 ..^M) \subseteq (0 \dots M)$
31	30 3	sseldd	$⊢ φ \to I \in (0 \dots M)$
32	1 2 31	iccpartxr	$⊢ φ \to P (I) \in ℝ^{*}$
33	28 3	sseldd	$⊢ φ \to I \in (0 ..^M)$
34		fzofzp1	$⊢ I \in (0 ..^M) \to I + 1 \in (0 \dots M)$
35	33 34	syl	$⊢ φ \to I + 1 \in (0 \dots M)$
36	1 2 35	iccpartxr	$⊢ φ \to P (I + 1) \in ℝ^{*}$
37	1 2 17	iccpartgtprec	$⊢ φ \to P (I - 1) < P (I)$
38		iccpartimp	$⊢ (M \in ℕ \land P \in RePart (M) \land I \in (0 ..^M)) \to (P \in ({ℝ^{*}}^{(0 \dots M)}) \land P (I) < P (I + 1))$
39	1 2 33 38	syl3anc	$⊢ φ \to (P \in ({ℝ^{*}}^{(0 \dots M)}) \land P (I) < P (I + 1))$
40	39	simprd	$⊢ φ \to P (I) < P (I + 1)$
41		xrre2	$⊢ ((P (I - 1) \in ℝ^{} \land P (I) \in ℝ^{} \land P (I + 1) \in ℝ^{*}) \land (P (I - 1) < P (I) \land P (I) < P (I + 1))) \to P (I) \in ℝ$
42	25 32 36 37 40 41	syl32anc	$⊢ φ \to P (I) \in ℝ$

Metamath Proof Explorer

Theorem iccpartipre

Proof