iccpartgtprec

Description: If there is a partition, then all intermediate points and the upper bound are strictly greater than the preceeding intermediate points or lower bound. (Contributed by AV, 11-Jul-2020)

	Ref	Expression
Hypotheses	iccpartgtprec.m	$⊢ φ \to M \in ℕ$
	iccpartgtprec.p	$⊢ φ \to P \in RePart (M)$
	iccpartgtprec.i	$⊢ φ \to I \in (1 \dots M)$
Assertion	iccpartgtprec	$⊢ φ \to P (I - 1) < P (I)$

Proof

Step	Hyp	Ref	Expression
1		iccpartgtprec.m	$⊢ φ \to M \in ℕ$
2		iccpartgtprec.p	$⊢ φ \to P \in RePart (M)$
3		iccpartgtprec.i	$⊢ φ \to I \in (1 \dots M)$
4	1	nnzd	$⊢ φ \to M \in ℤ$
5		fzval3	$⊢ M \in ℤ \to (1 \dots M) = (1 ..^M + 1)$
6	5	eleq2d	$⊢ M \in ℤ \to (I \in (1 \dots M) \leftrightarrow I \in (1 ..^M + 1))$
7	4 6	syl	$⊢ φ \to (I \in (1 \dots M) \leftrightarrow I \in (1 ..^M + 1))$
8	3 7	mpbid	$⊢ φ \to I \in (1 ..^M + 1)$
9	1	nncnd	$⊢ φ \to M \in ℂ$
10		pncan1	$⊢ M \in ℂ \to M + 1 - 1 = M$
11	9 10	syl	$⊢ φ \to M + 1 - 1 = M$
12	11	eqcomd	$⊢ φ \to M = M + 1 - 1$
13	12	oveq2d	$⊢ φ \to (0 ..^M) = (0 ..^M + 1 - 1)$
14	13	eleq2d	$⊢ φ \to (I - 1 \in (0 ..^M) \leftrightarrow I - 1 \in (0 ..^M + 1 - 1))$
15	3	elfzelzd	$⊢ φ \to I \in ℤ$
16	4	peano2zd	$⊢ φ \to M + 1 \in ℤ$
17		elfzom1b	$⊢ (I \in ℤ \land M + 1 \in ℤ) \to (I \in (1 ..^M + 1) \leftrightarrow I - 1 \in (0 ..^M + 1 - 1))$
18	15 16 17	syl2anc	$⊢ φ \to (I \in (1 ..^M + 1) \leftrightarrow I - 1 \in (0 ..^M + 1 - 1))$
19	14 18	bitr4d	$⊢ φ \to (I - 1 \in (0 ..^M) \leftrightarrow I \in (1 ..^M + 1))$
20	8 19	mpbird	$⊢ φ \to I - 1 \in (0 ..^M)$
21		iccpartimp	$⊢ (M \in ℕ \land P \in RePart (M) \land I - 1 \in (0 ..^M)) \to (P \in ({ℝ^{*}}^{(0 \dots M)}) \land P (I - 1) < P (I - 1 + 1))$
22	1 2 20 21	syl3anc	$⊢ φ \to (P \in ({ℝ^{*}}^{(0 \dots M)}) \land P (I - 1) < P (I - 1 + 1))$
23	22	simprd	$⊢ φ \to P (I - 1) < P (I - 1 + 1)$
24	15	zcnd	$⊢ φ \to I \in ℂ$
25		npcan1	$⊢ I \in ℂ \to I - 1 + 1 = I$
26	24 25	syl	$⊢ φ \to I - 1 + 1 = I$
27	26	eqcomd	$⊢ φ \to I = I - 1 + 1$
28	27	fveq2d	$⊢ φ \to P (I) = P (I - 1 + 1)$
29	23 28	breqtrrd	$⊢ φ \to P (I - 1) < P (I)$

Metamath Proof Explorer

Theorem iccpartgtprec

Proof