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

Proof

Step	Hyp	Ref	Expression
1		iccpartgtprec.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2		iccpartgtprec.p	⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
3	1	nnnn0d	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
4		elnn0uz	⊢ ( 𝑀 ∈ ℕ0 ↔ 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
5	3 4	sylib	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
6		fzpred	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → ( 0 ... 𝑀 ) = ( { 0 } ∪ ( ( 0 + 1 ) ... 𝑀 ) ) )
7	5 6	syl	⊢ ( 𝜑 → ( 0 ... 𝑀 ) = ( { 0 } ∪ ( ( 0 + 1 ) ... 𝑀 ) ) )
8	7	eleq2d	⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ... 𝑀 ) ↔ 𝑖 ∈ ( { 0 } ∪ ( ( 0 + 1 ) ... 𝑀 ) ) ) )
9		elun	⊢ ( 𝑖 ∈ ( { 0 } ∪ ( ( 0 + 1 ) ... 𝑀 ) ) ↔ ( 𝑖 ∈ { 0 } ∨ 𝑖 ∈ ( ( 0 + 1 ) ... 𝑀 ) ) )
10	9	a1i	⊢ ( 𝜑 → ( 𝑖 ∈ ( { 0 } ∪ ( ( 0 + 1 ) ... 𝑀 ) ) ↔ ( 𝑖 ∈ { 0 } ∨ 𝑖 ∈ ( ( 0 + 1 ) ... 𝑀 ) ) ) )
11		velsn	⊢ ( 𝑖 ∈ { 0 } ↔ 𝑖 = 0 )
12	11	a1i	⊢ ( 𝜑 → ( 𝑖 ∈ { 0 } ↔ 𝑖 = 0 ) )
13		0p1e1	⊢ ( 0 + 1 ) = 1
14	13	a1i	⊢ ( 𝜑 → ( 0 + 1 ) = 1 )
15	14	oveq1d	⊢ ( 𝜑 → ( ( 0 + 1 ) ... 𝑀 ) = ( 1 ... 𝑀 ) )
16	15	eleq2d	⊢ ( 𝜑 → ( 𝑖 ∈ ( ( 0 + 1 ) ... 𝑀 ) ↔ 𝑖 ∈ ( 1 ... 𝑀 ) ) )
17	12 16	orbi12d	⊢ ( 𝜑 → ( ( 𝑖 ∈ { 0 } ∨ 𝑖 ∈ ( ( 0 + 1 ) ... 𝑀 ) ) ↔ ( 𝑖 = 0 ∨ 𝑖 ∈ ( 1 ... 𝑀 ) ) ) )
18	8 10 17	3bitrd	⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ... 𝑀 ) ↔ ( 𝑖 = 0 ∨ 𝑖 ∈ ( 1 ... 𝑀 ) ) ) )
19		0elfz	⊢ ( 𝑀 ∈ ℕ0 → 0 ∈ ( 0 ... 𝑀 ) )
20	3 19	syl	⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑀 ) )
21	1 2 20	iccpartxr	⊢ ( 𝜑 → ( 𝑃 ‘ 0 ) ∈ ℝ* )
22	21	xrleidd	⊢ ( 𝜑 → ( 𝑃 ‘ 0 ) ≤ ( 𝑃 ‘ 0 ) )
23		fveq2	⊢ ( 𝑖 = 0 → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ 0 ) )
24	23	breq2d	⊢ ( 𝑖 = 0 → ( ( 𝑃 ‘ 0 ) ≤ ( 𝑃 ‘ 𝑖 ) ↔ ( 𝑃 ‘ 0 ) ≤ ( 𝑃 ‘ 0 ) ) )
25	22 24	imbitrrid	⊢ ( 𝑖 = 0 → ( 𝜑 → ( 𝑃 ‘ 0 ) ≤ ( 𝑃 ‘ 𝑖 ) ) )
26	21	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑃 ‘ 0 ) ∈ ℝ* )
27	1	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝑀 ∈ ℕ )
28	2	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
29		1nn0	⊢ 1 ∈ ℕ0
30	29	a1i	⊢ ( 𝜑 → 1 ∈ ℕ0 )
31		elnn0uz	⊢ ( 1 ∈ ℕ0 ↔ 1 ∈ ( ℤ≥ ‘ 0 ) )
32	30 31	sylib	⊢ ( 𝜑 → 1 ∈ ( ℤ≥ ‘ 0 ) )
33		fzss1	⊢ ( 1 ∈ ( ℤ≥ ‘ 0 ) → ( 1 ... 𝑀 ) ⊆ ( 0 ... 𝑀 ) )
34	32 33	syl	⊢ ( 𝜑 → ( 1 ... 𝑀 ) ⊆ ( 0 ... 𝑀 ) )
35	34	sselda	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
36	27 28 35	iccpartxr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℝ* )
37	1 2	iccpartgtl	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑘 ) )
38		fveq2	⊢ ( 𝑘 = 𝑖 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑖 ) )
39	38	breq2d	⊢ ( 𝑘 = 𝑖 → ( ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑘 ) ↔ ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑖 ) ) )
40	39	rspccv	⊢ ( ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑘 ) → ( 𝑖 ∈ ( 1 ... 𝑀 ) → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑖 ) ) )
41	37 40	syl	⊢ ( 𝜑 → ( 𝑖 ∈ ( 1 ... 𝑀 ) → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑖 ) ) )
42	41	imp	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑖 ) )
43	26 36 42	xrltled	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑃 ‘ 0 ) ≤ ( 𝑃 ‘ 𝑖 ) )
44	43	expcom	⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → ( 𝜑 → ( 𝑃 ‘ 0 ) ≤ ( 𝑃 ‘ 𝑖 ) ) )
45	25 44	jaoi	⊢ ( ( 𝑖 = 0 ∨ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝜑 → ( 𝑃 ‘ 0 ) ≤ ( 𝑃 ‘ 𝑖 ) ) )
46	45	com12	⊢ ( 𝜑 → ( ( 𝑖 = 0 ∨ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑃 ‘ 0 ) ≤ ( 𝑃 ‘ 𝑖 ) ) )
47	18 46	sylbid	⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ... 𝑀 ) → ( 𝑃 ‘ 0 ) ≤ ( 𝑃 ‘ 𝑖 ) ) )
48	47	ralrimiv	⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑃 ‘ 0 ) ≤ ( 𝑃 ‘ 𝑖 ) )