iccpartltu

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

	Ref	Expression
Hypotheses	iccpartgtprec.m	$⊢ φ \to M \in ℕ$
	iccpartgtprec.p	$⊢ φ \to P \in RePart (M)$
Assertion	iccpartltu	$⊢ φ \to \forall i \in (0 ..^M) P (i) < P (M)$

Proof

Step	Hyp	Ref	Expression
1		iccpartgtprec.m	$⊢ φ \to M \in ℕ$
2		iccpartgtprec.p	$⊢ φ \to P \in RePart (M)$
3		0zd	$⊢ M \in ℕ \to 0 \in ℤ$
4		nnz	$⊢ M \in ℕ \to M \in ℤ$
5		nngt0	$⊢ M \in ℕ \to 0 < M$
6	3 4 5	3jca	$⊢ M \in ℕ \to (0 \in ℤ \land M \in ℤ \land 0 < M)$
7	1 6	syl	$⊢ φ \to (0 \in ℤ \land M \in ℤ \land 0 < M)$
8		fzopred	$⊢ (0 \in ℤ \land M \in ℤ \land 0 < M) \to (0 ..^M) = \{0\} \cup (0 + 1 ..^M)$
9	7 8	syl	$⊢ φ \to (0 ..^M) = \{0\} \cup (0 + 1 ..^M)$
10		0p1e1	$⊢ 0 + 1 = 1$
11	10	a1i	$⊢ φ \to 0 + 1 = 1$
12	11	oveq1d	$⊢ φ \to (0 + 1 ..^M) = (1 ..^M)$
13	12	uneq2d	$⊢ φ \to \{0\} \cup (0 + 1 ..^M) = \{0\} \cup (1 ..^M)$
14	9 13	eqtrd	$⊢ φ \to (0 ..^M) = \{0\} \cup (1 ..^M)$
15	14	eleq2d	$⊢ φ \to (i \in (0 ..^M) \leftrightarrow i \in (\{0\} \cup (1 ..^M)))$
16		elun	$⊢ i \in (\{0\} \cup (1 ..^M)) \leftrightarrow (i \in \{0\} \lor i \in (1 ..^M))$
17		elsni	$⊢ i \in \{0\} \to i = 0$
18		fveq2	$⊢ i = 0 \to P (i) = P (0)$
19	18	adantr	$⊢ (i = 0 \land φ) \to P (i) = P (0)$
20	1 2	iccpartlt	$⊢ φ \to P (0) < P (M)$
21	20	adantl	$⊢ (i = 0 \land φ) \to P (0) < P (M)$
22	19 21	eqbrtrd	$⊢ (i = 0 \land φ) \to P (i) < P (M)$
23	22	ex	$⊢ i = 0 \to (φ \to P (i) < P (M))$
24	17 23	syl	$⊢ i \in \{0\} \to (φ \to P (i) < P (M))$
25		fveq2	$⊢ k = i \to P (k) = P (i)$
26	25	breq1d	$⊢ k = i \to (P (k) < P (M) \leftrightarrow P (i) < P (M))$
27	26	rspccv	$⊢ \forall k \in (1 ..^M) P (k) < P (M) \to (i \in (1 ..^M) \to P (i) < P (M))$
28	1 2	iccpartiltu	$⊢ φ \to \forall k \in (1 ..^M) P (k) < P (M)$
29	27 28	syl11	$⊢ i \in (1 ..^M) \to (φ \to P (i) < P (M))$
30	24 29	jaoi	$⊢ (i \in \{0\} \lor i \in (1 ..^M)) \to (φ \to P (i) < P (M))$
31	30	com12	$⊢ φ \to ((i \in \{0\} \lor i \in (1 ..^M)) \to P (i) < P (M))$
32	16 31	biimtrid	$⊢ φ \to (i \in (\{0\} \cup (1 ..^M)) \to P (i) < P (M))$
33	15 32	sylbid	$⊢ φ \to (i \in (0 ..^M) \to P (i) < P (M))$
34	33	ralrimiv	$⊢ φ \to \forall i \in (0 ..^M) P (i) < P (M)$

Metamath Proof Explorer

Theorem iccpartltu

Proof