Metamath Proof Explorer

Theorem iccpartrn

Description: If there is a partition, then all intermediate points and bounds are contained in a closed interval of extended reals. (Contributed by AV, 14-Jul-2020)

Ref Expression
Hypotheses iccpartgtprec.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
iccpartgtprec.p ⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
Assertion iccpartrn ( 𝜑 → ran 𝑃 ⊆ ( ( 𝑃 ‘ 0 ) [,] ( 𝑃 ‘ 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 iccpartgtprec.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 iccpartgtprec.p ⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
3 iccpart ⊢ ( 𝑀 ∈ ℕ → ( 𝑃 ∈ ( RePart ‘ 𝑀 ) ↔ ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) )
4 1 3 syl ⊢ ( 𝜑 → ( 𝑃 ∈ ( RePart ‘ 𝑀 ) ↔ ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) )
5 elmapfn ⊢ ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) → 𝑃 Fn ( 0 ... 𝑀 ) )
6 5 adantr ⊢ ( ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) → 𝑃 Fn ( 0 ... 𝑀 ) )
7 4 6 biimtrdi ⊢ ( 𝜑 → ( 𝑃 ∈ ( RePart ‘ 𝑀 ) → 𝑃 Fn ( 0 ... 𝑀 ) ) )
8 2 7 mpd ⊢ ( 𝜑 → 𝑃 Fn ( 0 ... 𝑀 ) )
9 fvelrnb ⊢ ( 𝑃 Fn ( 0 ... 𝑀 ) → ( 𝑝 ∈ ran 𝑃 ↔ ∃ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑃 ‘ 𝑖 ) = 𝑝 ) )
10 8 9 syl ⊢ ( 𝜑 → ( 𝑝 ∈ ran 𝑃 ↔ ∃ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑃 ‘ 𝑖 ) = 𝑝 ) )
11 1 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → 𝑀 ∈ ℕ )
12 2 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
13 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
14 11 12 13 iccpartxr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ℝ* )
15 1 2 iccpartgel ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑃 ‘ 0 ) ≤ ( 𝑃 ‘ 𝑘 ) )
16 fveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑖 ) )
17 16 breq2d ⊢ ( 𝑘 = 𝑖 → ( ( 𝑃 ‘ 0 ) ≤ ( 𝑃 ‘ 𝑘 ) ↔ ( 𝑃 ‘ 0 ) ≤ ( 𝑃 ‘ 𝑖 ) ) )
18 17 rspcva ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑃 ‘ 0 ) ≤ ( 𝑃 ‘ 𝑘 ) ) → ( 𝑃 ‘ 0 ) ≤ ( 𝑃 ‘ 𝑖 ) )
19 18 expcom ⊢ ( ∀ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑃 ‘ 0 ) ≤ ( 𝑃 ‘ 𝑘 ) → ( 𝑖 ∈ ( 0 ... 𝑀 ) → ( 𝑃 ‘ 0 ) ≤ ( 𝑃 ‘ 𝑖 ) ) )
20 15 19 syl ⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ... 𝑀 ) → ( 𝑃 ‘ 0 ) ≤ ( 𝑃 ‘ 𝑖 ) ) )
21 20 imp ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑃 ‘ 0 ) ≤ ( 𝑃 ‘ 𝑖 ) )
22 1 2 iccpartleu ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑃 ‘ 𝑘 ) ≤ ( 𝑃 ‘ 𝑀 ) )
23 16 breq1d ⊢ ( 𝑘 = 𝑖 → ( ( 𝑃 ‘ 𝑘 ) ≤ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑃 ‘ 𝑖 ) ≤ ( 𝑃 ‘ 𝑀 ) ) )
24 23 rspcva ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑃 ‘ 𝑘 ) ≤ ( 𝑃 ‘ 𝑀 ) ) → ( 𝑃 ‘ 𝑖 ) ≤ ( 𝑃 ‘ 𝑀 ) )
25 24 expcom ⊢ ( ∀ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑃 ‘ 𝑘 ) ≤ ( 𝑃 ‘ 𝑀 ) → ( 𝑖 ∈ ( 0 ... 𝑀 ) → ( 𝑃 ‘ 𝑖 ) ≤ ( 𝑃 ‘ 𝑀 ) ) )
26 22 25 syl ⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ... 𝑀 ) → ( 𝑃 ‘ 𝑖 ) ≤ ( 𝑃 ‘ 𝑀 ) ) )
27 26 imp ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑃 ‘ 𝑖 ) ≤ ( 𝑃 ‘ 𝑀 ) )
28 nnnn0 ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℕ0 )
29 0elfz ⊢ ( 𝑀 ∈ ℕ0 → 0 ∈ ( 0 ... 𝑀 ) )
30 1 28 29 3syl ⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑀 ) )
31 1 2 30 iccpartxr ⊢ ( 𝜑 → ( 𝑃 ‘ 0 ) ∈ ℝ* )
32 nn0fz0 ⊢ ( 𝑀 ∈ ℕ0 ↔ 𝑀 ∈ ( 0 ... 𝑀 ) )
33 28 32 sylib ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ( 0 ... 𝑀 ) )
34 1 33 syl ⊢ ( 𝜑 → 𝑀 ∈ ( 0 ... 𝑀 ) )
35 1 2 34 iccpartxr ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑀 ) ∈ ℝ* )
36 31 35 jca ⊢ ( 𝜑 → ( ( 𝑃 ‘ 0 ) ∈ ℝ* ∧ ( 𝑃 ‘ 𝑀 ) ∈ ℝ* ) )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑃 ‘ 0 ) ∈ ℝ* ∧ ( 𝑃 ‘ 𝑀 ) ∈ ℝ* ) )
38 elicc1 ⊢ ( ( ( 𝑃 ‘ 0 ) ∈ ℝ* ∧ ( 𝑃 ‘ 𝑀 ) ∈ ℝ* ) → ( ( 𝑃 ‘ 𝑖 ) ∈ ( ( 𝑃 ‘ 0 ) [,] ( 𝑃 ‘ 𝑀 ) ) ↔ ( ( 𝑃 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝑃 ‘ 0 ) ≤ ( 𝑃 ‘ 𝑖 ) ∧ ( 𝑃 ‘ 𝑖 ) ≤ ( 𝑃 ‘ 𝑀 ) ) ) )
39 37 38 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑃 ‘ 𝑖 ) ∈ ( ( 𝑃 ‘ 0 ) [,] ( 𝑃 ‘ 𝑀 ) ) ↔ ( ( 𝑃 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝑃 ‘ 0 ) ≤ ( 𝑃 ‘ 𝑖 ) ∧ ( 𝑃 ‘ 𝑖 ) ≤ ( 𝑃 ‘ 𝑀 ) ) ) )
40 14 21 27 39 mpbir3and ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑃 ‘ 𝑖 ) ∈ ( ( 𝑃 ‘ 0 ) [,] ( 𝑃 ‘ 𝑀 ) ) )
41 eleq1 ⊢ ( ( 𝑃 ‘ 𝑖 ) = 𝑝 → ( ( 𝑃 ‘ 𝑖 ) ∈ ( ( 𝑃 ‘ 0 ) [,] ( 𝑃 ‘ 𝑀 ) ) ↔ 𝑝 ∈ ( ( 𝑃 ‘ 0 ) [,] ( 𝑃 ‘ 𝑀 ) ) ) )
42 40 41 syl5ibcom ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑃 ‘ 𝑖 ) = 𝑝 → 𝑝 ∈ ( ( 𝑃 ‘ 0 ) [,] ( 𝑃 ‘ 𝑀 ) ) ) )
43 42 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑃 ‘ 𝑖 ) = 𝑝 → 𝑝 ∈ ( ( 𝑃 ‘ 0 ) [,] ( 𝑃 ‘ 𝑀 ) ) ) )
44 10 43 sylbid ⊢ ( 𝜑 → ( 𝑝 ∈ ran 𝑃 → 𝑝 ∈ ( ( 𝑃 ‘ 0 ) [,] ( 𝑃 ‘ 𝑀 ) ) ) )
45 44 ssrdv ⊢ ( 𝜑 → ran 𝑃 ⊆ ( ( 𝑃 ‘ 0 ) [,] ( 𝑃 ‘ 𝑀 ) ) )