iccpartleu

Description: If there is a partition, then all intermediate points and the lower and the upper bound are less than or equal to 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	iccpartleu	$⊢ φ \to \forall i \in (0 \dots M) P (i) \leq P (M)$

Proof

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

Metamath Proof Explorer

Theorem iccpartleu

Proof