Metamath Proof Explorer


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 ... 𝑀 ) ( 𝑃𝑖 ) ≤ ( 𝑃𝑀 ) )