Theorem iccpartipre

Description: If there is a partition, then all intermediate points are real numbers. (Contributed by AV, 11-Jul-2020)

	Ref	Expression
Hypotheses	iccpartgtprec.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	iccpartgtprec.p	⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
	iccpartipre.i	⊢ ( 𝜑 → 𝐼 ∈ ( 1 ..^ 𝑀 ) )
Assertion	iccpartipre	⊢ ( 𝜑 → ( 𝑃 ‘ 𝐼 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		iccpartgtprec.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2		iccpartgtprec.p	⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
3		iccpartipre.i	⊢ ( 𝜑 → 𝐼 ∈ ( 1 ..^ 𝑀 ) )
4		nnz	⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℤ )
5		peano2zm	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 − 1 ) ∈ ℤ )
6		id	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℤ )
7		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
8	7	lem1d	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 − 1 ) ≤ 𝑀 )
9	5 6 8	3jca	⊢ ( 𝑀 ∈ ℤ → ( ( 𝑀 − 1 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( 𝑀 − 1 ) ≤ 𝑀 ) )
10	4 9	syl	⊢ ( 𝑀 ∈ ℕ → ( ( 𝑀 − 1 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( 𝑀 − 1 ) ≤ 𝑀 ) )
11		eluz2	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) ↔ ( ( 𝑀 − 1 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( 𝑀 − 1 ) ≤ 𝑀 ) )
12	10 11	sylibr	⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) )
13	1 12	syl	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) )
14		fzss2	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ ( 𝑀 − 1 ) ) → ( 0 ... ( 𝑀 − 1 ) ) ⊆ ( 0 ... 𝑀 ) )
15	13 14	syl	⊢ ( 𝜑 → ( 0 ... ( 𝑀 − 1 ) ) ⊆ ( 0 ... 𝑀 ) )
16		fzossfz	⊢ ( 1 ..^ 𝑀 ) ⊆ ( 1 ... 𝑀 )
17	16 3	sselid	⊢ ( 𝜑 → 𝐼 ∈ ( 1 ... 𝑀 ) )
18		elfzoelz	⊢ ( 𝐼 ∈ ( 1 ..^ 𝑀 ) → 𝐼 ∈ ℤ )
19	3 18	syl	⊢ ( 𝜑 → 𝐼 ∈ ℤ )
20	1	nnzd	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
21		elfzm1b	⊢ ( ( 𝐼 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐼 ∈ ( 1 ... 𝑀 ) ↔ ( 𝐼 − 1 ) ∈ ( 0 ... ( 𝑀 − 1 ) ) ) )
22	19 20 21	syl2anc	⊢ ( 𝜑 → ( 𝐼 ∈ ( 1 ... 𝑀 ) ↔ ( 𝐼 − 1 ) ∈ ( 0 ... ( 𝑀 − 1 ) ) ) )
23	17 22	mpbid	⊢ ( 𝜑 → ( 𝐼 − 1 ) ∈ ( 0 ... ( 𝑀 − 1 ) ) )
24	15 23	sseldd	⊢ ( 𝜑 → ( 𝐼 − 1 ) ∈ ( 0 ... 𝑀 ) )
25	1 2 24	iccpartxr	⊢ ( 𝜑 → ( 𝑃 ‘ ( 𝐼 − 1 ) ) ∈ ℝ* )
26		1eluzge0	⊢ 1 ∈ ( ℤ≥ ‘ 0 )
27		fzoss1	⊢ ( 1 ∈ ( ℤ≥ ‘ 0 ) → ( 1 ..^ 𝑀 ) ⊆ ( 0 ..^ 𝑀 ) )
28	26 27	mp1i	⊢ ( 𝜑 → ( 1 ..^ 𝑀 ) ⊆ ( 0 ..^ 𝑀 ) )
29		fzossfz	⊢ ( 0 ..^ 𝑀 ) ⊆ ( 0 ... 𝑀 )
30	28 29	sstrdi	⊢ ( 𝜑 → ( 1 ..^ 𝑀 ) ⊆ ( 0 ... 𝑀 ) )
31	30 3	sseldd	⊢ ( 𝜑 → 𝐼 ∈ ( 0 ... 𝑀 ) )
32	1 2 31	iccpartxr	⊢ ( 𝜑 → ( 𝑃 ‘ 𝐼 ) ∈ ℝ* )
33	28 3	sseldd	⊢ ( 𝜑 → 𝐼 ∈ ( 0 ..^ 𝑀 ) )
34		fzofzp1	⊢ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) )
35	33 34	syl	⊢ ( 𝜑 → ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) )
36	1 2 35	iccpartxr	⊢ ( 𝜑 → ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* )
37	1 2 17	iccpartgtprec	⊢ ( 𝜑 → ( 𝑃 ‘ ( 𝐼 − 1 ) ) < ( 𝑃 ‘ 𝐼 ) )
38		iccpartimp	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑃 ∈ ( RePart ‘ 𝑀 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) )
39	1 2 33 38	syl3anc	⊢ ( 𝜑 → ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) )
40	39	simprd	⊢ ( 𝜑 → ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) )
41		xrre2	⊢ ( ( ( ( 𝑃 ‘ ( 𝐼 − 1 ) ) ∈ ℝ* ∧ ( 𝑃 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ) ∧ ( ( 𝑃 ‘ ( 𝐼 − 1 ) ) < ( 𝑃 ‘ 𝐼 ) ∧ ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) → ( 𝑃 ‘ 𝐼 ) ∈ ℝ )
42	25 32 36 37 40 41	syl32anc	⊢ ( 𝜑 → ( 𝑃 ‘ 𝐼 ) ∈ ℝ )