Theorem 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	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	iccpartgtprec.p	⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
Assertion	iccpartleu	⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑃 ‘ 𝑖 ) ≤ ( 𝑃 ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		iccpartgtprec.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2		iccpartgtprec.p	⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
3		nnnn0	⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℕ0 )
4		elnn0uz	⊢ ( 𝑀 ∈ ℕ0 ↔ 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
5	3 4	sylib	⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
6	1 5	syl	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
7		fzisfzounsn	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → ( 0 ... 𝑀 ) = ( ( 0 ..^ 𝑀 ) ∪ { 𝑀 } ) )
8	6 7	syl	⊢ ( 𝜑 → ( 0 ... 𝑀 ) = ( ( 0 ..^ 𝑀 ) ∪ { 𝑀 } ) )
9	8	eleq2d	⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ... 𝑀 ) ↔ 𝑖 ∈ ( ( 0 ..^ 𝑀 ) ∪ { 𝑀 } ) ) )
10		elun	⊢ ( 𝑖 ∈ ( ( 0 ..^ 𝑀 ) ∪ { 𝑀 } ) ↔ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∨ 𝑖 ∈ { 𝑀 } ) )
11	10	a1i	⊢ ( 𝜑 → ( 𝑖 ∈ ( ( 0 ..^ 𝑀 ) ∪ { 𝑀 } ) ↔ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∨ 𝑖 ∈ { 𝑀 } ) ) )
12		velsn	⊢ ( 𝑖 ∈ { 𝑀 } ↔ 𝑖 = 𝑀 )
13	12	a1i	⊢ ( 𝜑 → ( 𝑖 ∈ { 𝑀 } ↔ 𝑖 = 𝑀 ) )
14	13	orbi2d	⊢ ( 𝜑 → ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∨ 𝑖 ∈ { 𝑀 } ) ↔ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∨ 𝑖 = 𝑀 ) ) )
15	9 11 14	3bitrd	⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ... 𝑀 ) ↔ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∨ 𝑖 = 𝑀 ) ) )
16	1	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑀 ∈ ℕ )
17	2	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
18		fzossfz	⊢ ( 0 ..^ 𝑀 ) ⊆ ( 0 ... 𝑀 )
19	18	a1i	⊢ ( 𝜑 → ( 0 ..^ 𝑀 ) ⊆ ( 0 ... 𝑀 ) )
20	19	sselda	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
21	16 17 20	iccpartxr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℝ* )
22		nn0fz0	⊢ ( 𝑀 ∈ ℕ0 ↔ 𝑀 ∈ ( 0 ... 𝑀 ) )
23	3 22	sylib	⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ( 0 ... 𝑀 ) )
24	1 23	syl	⊢ ( 𝜑 → 𝑀 ∈ ( 0 ... 𝑀 ) )
25	1 2 24	iccpartxr	⊢ ( 𝜑 → ( 𝑃 ‘ 𝑀 ) ∈ ℝ* )
26	25	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑃 ‘ 𝑀 ) ∈ ℝ* )
27	1 2	iccpartltu	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑘 ) < ( 𝑃 ‘ 𝑀 ) )
28		fveq2	⊢ ( 𝑘 = 𝑖 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑖 ) )
29	28	breq1d	⊢ ( 𝑘 = 𝑖 → ( ( 𝑃 ‘ 𝑘 ) < ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
30	29	rspccv	⊢ ( ∀ 𝑘 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑘 ) < ( 𝑃 ‘ 𝑀 ) → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
31	27 30	syl	⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
32	31	imp	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) )
33	21 26 32	xrltled	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑃 ‘ 𝑖 ) ≤ ( 𝑃 ‘ 𝑀 ) )
34	33	expcom	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝜑 → ( 𝑃 ‘ 𝑖 ) ≤ ( 𝑃 ‘ 𝑀 ) ) )
35		fveq2	⊢ ( 𝑖 = 𝑀 → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑀 ) )
36	35	adantr	⊢ ( ( 𝑖 = 𝑀 ∧ 𝜑 ) → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑀 ) )
37	25	xrleidd	⊢ ( 𝜑 → ( 𝑃 ‘ 𝑀 ) ≤ ( 𝑃 ‘ 𝑀 ) )
38	37	adantl	⊢ ( ( 𝑖 = 𝑀 ∧ 𝜑 ) → ( 𝑃 ‘ 𝑀 ) ≤ ( 𝑃 ‘ 𝑀 ) )
39	36 38	eqbrtrd	⊢ ( ( 𝑖 = 𝑀 ∧ 𝜑 ) → ( 𝑃 ‘ 𝑖 ) ≤ ( 𝑃 ‘ 𝑀 ) )
40	39	ex	⊢ ( 𝑖 = 𝑀 → ( 𝜑 → ( 𝑃 ‘ 𝑖 ) ≤ ( 𝑃 ‘ 𝑀 ) ) )
41	34 40	jaoi	⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∨ 𝑖 = 𝑀 ) → ( 𝜑 → ( 𝑃 ‘ 𝑖 ) ≤ ( 𝑃 ‘ 𝑀 ) ) )
42	41	com12	⊢ ( 𝜑 → ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∨ 𝑖 = 𝑀 ) → ( 𝑃 ‘ 𝑖 ) ≤ ( 𝑃 ‘ 𝑀 ) ) )
43	15 42	sylbid	⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ... 𝑀 ) → ( 𝑃 ‘ 𝑖 ) ≤ ( 𝑃 ‘ 𝑀 ) ) )
44	43	ralrimiv	⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑃 ‘ 𝑖 ) ≤ ( 𝑃 ‘ 𝑀 ) )