iccpartgel

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

	Ref	Expression
Hypotheses	iccpartgtprec.m	$⊢ φ \to M \in ℕ$
	iccpartgtprec.p	$⊢ φ \to P \in RePart (M)$
Assertion	iccpartgel	$⊢ φ \to \forall i \in (0 \dots M) P (0) \leq P (i)$

Proof

Step	Hyp	Ref	Expression
1		iccpartgtprec.m	$⊢ φ \to M \in ℕ$
2		iccpartgtprec.p	$⊢ φ \to P \in RePart (M)$
3	1	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
4		elnn0uz	$⊢ M \in ℕ_{0} \leftrightarrow M \in ℤ_{\geq 0}$
5	3 4	sylib	$⊢ φ \to M \in ℤ_{\geq 0}$
6		fzpred	$⊢ M \in ℤ_{\geq 0} \to (0 \dots M) = \{0\} \cup (0 + 1 \dots M)$
7	5 6	syl	$⊢ φ \to (0 \dots M) = \{0\} \cup (0 + 1 \dots M)$
8	7	eleq2d	$⊢ φ \to (i \in (0 \dots M) \leftrightarrow i \in (\{0\} \cup (0 + 1 \dots M)))$
9		elun	$⊢ i \in (\{0\} \cup (0 + 1 \dots M)) \leftrightarrow (i \in \{0\} \lor i \in (0 + 1 \dots M))$
10	9	a1i	$⊢ φ \to (i \in (\{0\} \cup (0 + 1 \dots M)) \leftrightarrow (i \in \{0\} \lor i \in (0 + 1 \dots M)))$
11		velsn	$⊢ i \in \{0\} \leftrightarrow i = 0$
12	11	a1i	$⊢ φ \to (i \in \{0\} \leftrightarrow i = 0)$
13		0p1e1	$⊢ 0 + 1 = 1$
14	13	a1i	$⊢ φ \to 0 + 1 = 1$
15	14	oveq1d	$⊢ φ \to (0 + 1 \dots M) = (1 \dots M)$
16	15	eleq2d	$⊢ φ \to (i \in (0 + 1 \dots M) \leftrightarrow i \in (1 \dots M))$
17	12 16	orbi12d	$⊢ φ \to ((i \in \{0\} \lor i \in (0 + 1 \dots M)) \leftrightarrow (i = 0 \lor i \in (1 \dots M)))$
18	8 10 17	3bitrd	$⊢ φ \to (i \in (0 \dots M) \leftrightarrow (i = 0 \lor i \in (1 \dots M)))$
19		0elfz	$⊢ M \in ℕ_{0} \to 0 \in (0 \dots M)$
20	3 19	syl	$⊢ φ \to 0 \in (0 \dots M)$
21	1 2 20	iccpartxr	$⊢ φ \to P (0) \in ℝ^{*}$
22	21	xrleidd	$⊢ φ \to P (0) \leq P (0)$
23		fveq2	$⊢ i = 0 \to P (i) = P (0)$
24	23	breq2d	$⊢ i = 0 \to (P (0) \leq P (i) \leftrightarrow P (0) \leq P (0))$
25	22 24	syl5ibr	$⊢ i = 0 \to (φ \to P (0) \leq P (i))$
26	21	adantr	$⊢ (φ \land i \in (1 \dots M)) \to P (0) \in ℝ^{*}$
27	1	adantr	$⊢ (φ \land i \in (1 \dots M)) \to M \in ℕ$
28	2	adantr	$⊢ (φ \land i \in (1 \dots M)) \to P \in RePart (M)$
29		1nn0	$⊢ 1 \in ℕ_{0}$
30	29	a1i	$⊢ φ \to 1 \in ℕ_{0}$
31		elnn0uz	$⊢ 1 \in ℕ_{0} \leftrightarrow 1 \in ℤ_{\geq 0}$
32	30 31	sylib	$⊢ φ \to 1 \in ℤ_{\geq 0}$
33		fzss1	$⊢ 1 \in ℤ_{\geq 0} \to (1 \dots M) \subseteq (0 \dots M)$
34	32 33	syl	$⊢ φ \to (1 \dots M) \subseteq (0 \dots M)$
35	34	sselda	$⊢ (φ \land i \in (1 \dots M)) \to i \in (0 \dots M)$
36	27 28 35	iccpartxr	$⊢ (φ \land i \in (1 \dots M)) \to P (i) \in ℝ^{*}$
37	1 2	iccpartgtl	$⊢ φ \to \forall k \in (1 \dots M) P (0) < P (k)$
38		fveq2	$⊢ k = i \to P (k) = P (i)$
39	38	breq2d	$⊢ k = i \to (P (0) < P (k) \leftrightarrow P (0) < P (i))$
40	39	rspccv	$⊢ \forall k \in (1 \dots M) P (0) < P (k) \to (i \in (1 \dots M) \to P (0) < P (i))$
41	37 40	syl	$⊢ φ \to (i \in (1 \dots M) \to P (0) < P (i))$
42	41	imp	$⊢ (φ \land i \in (1 \dots M)) \to P (0) < P (i)$
43	26 36 42	xrltled	$⊢ (φ \land i \in (1 \dots M)) \to P (0) \leq P (i)$
44	43	expcom	$⊢ i \in (1 \dots M) \to (φ \to P (0) \leq P (i))$
45	25 44	jaoi	$⊢ (i = 0 \lor i \in (1 \dots M)) \to (φ \to P (0) \leq P (i))$
46	45	com12	$⊢ φ \to ((i = 0 \lor i \in (1 \dots M)) \to P (0) \leq P (i))$
47	18 46	sylbid	$⊢ φ \to (i \in (0 \dots M) \to P (0) \leq P (i))$
48	47	ralrimiv	$⊢ φ \to \forall i \in (0 \dots M) P (0) \leq P (i)$

Metamath Proof Explorer

Theorem iccpartgel

Proof