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

Proof

Step	Hyp	Ref	Expression
1		iccpartgtprec.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2		iccpartgtprec.p	⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
3		0zd	⊢ ( 𝑀 ∈ ℕ → 0 ∈ ℤ )
4		nnz	⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℤ )
5		nngt0	⊢ ( 𝑀 ∈ ℕ → 0 < 𝑀 )
6	3 4 5	3jca	⊢ ( 𝑀 ∈ ℕ → ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀 ) )
7	1 6	syl	⊢ ( 𝜑 → ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀 ) )
8		fzopred	⊢ ( ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀 ) → ( 0 ..^ 𝑀 ) = ( { 0 } ∪ ( ( 0 + 1 ) ..^ 𝑀 ) ) )
9	7 8	syl	⊢ ( 𝜑 → ( 0 ..^ 𝑀 ) = ( { 0 } ∪ ( ( 0 + 1 ) ..^ 𝑀 ) ) )
10		0p1e1	⊢ ( 0 + 1 ) = 1
11	10	a1i	⊢ ( 𝜑 → ( 0 + 1 ) = 1 )
12	11	oveq1d	⊢ ( 𝜑 → ( ( 0 + 1 ) ..^ 𝑀 ) = ( 1 ..^ 𝑀 ) )
13	12	uneq2d	⊢ ( 𝜑 → ( { 0 } ∪ ( ( 0 + 1 ) ..^ 𝑀 ) ) = ( { 0 } ∪ ( 1 ..^ 𝑀 ) ) )
14	9 13	eqtrd	⊢ ( 𝜑 → ( 0 ..^ 𝑀 ) = ( { 0 } ∪ ( 1 ..^ 𝑀 ) ) )
15	14	eleq2d	⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↔ 𝑖 ∈ ( { 0 } ∪ ( 1 ..^ 𝑀 ) ) ) )
16		elun	⊢ ( 𝑖 ∈ ( { 0 } ∪ ( 1 ..^ 𝑀 ) ) ↔ ( 𝑖 ∈ { 0 } ∨ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) )
17		elsni	⊢ ( 𝑖 ∈ { 0 } → 𝑖 = 0 )
18		fveq2	⊢ ( 𝑖 = 0 → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ 0 ) )
19	18	adantr	⊢ ( ( 𝑖 = 0 ∧ 𝜑 ) → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ 0 ) )
20	1 2	iccpartlt	⊢ ( 𝜑 → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑀 ) )
21	20	adantl	⊢ ( ( 𝑖 = 0 ∧ 𝜑 ) → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑀 ) )
22	19 21	eqbrtrd	⊢ ( ( 𝑖 = 0 ∧ 𝜑 ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) )
23	22	ex	⊢ ( 𝑖 = 0 → ( 𝜑 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
24	17 23	syl	⊢ ( 𝑖 ∈ { 0 } → ( 𝜑 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
25		fveq2	⊢ ( 𝑘 = 𝑖 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑖 ) )
26	25	breq1d	⊢ ( 𝑘 = 𝑖 → ( ( 𝑃 ‘ 𝑘 ) < ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
27	26	rspccv	⊢ ( ∀ 𝑘 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 𝑘 ) < ( 𝑃 ‘ 𝑀 ) → ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
28	1 2	iccpartiltu	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 𝑘 ) < ( 𝑃 ‘ 𝑀 ) )
29	27 28	syl11	⊢ ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → ( 𝜑 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
30	24 29	jaoi	⊢ ( ( 𝑖 ∈ { 0 } ∨ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → ( 𝜑 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
31	30	com12	⊢ ( 𝜑 → ( ( 𝑖 ∈ { 0 } ∨ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
32	16 31	syl5bi	⊢ ( 𝜑 → ( 𝑖 ∈ ( { 0 } ∪ ( 1 ..^ 𝑀 ) ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
33	15 32	sylbid	⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
34	33	ralrimiv	⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) )