Metamath Proof Explorer

Theorem iccpartgtl

Description: If there is a partition, then all intermediate points and the upper bound are strictly greater than the lower bound. (Contributed by AV, 14-Jul-2020)

Ref Expression
Hypotheses iccpartgtprec.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
iccpartgtprec.p ⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
Assertion iccpartgtl ( 𝜑 → ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑖 ) )

Proof

Step Hyp Ref Expression
1 iccpartgtprec.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 iccpartgtprec.p ⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
3 elnnuz ⊢ ( 𝑀 ∈ ℕ ↔ 𝑀 ∈ ( ℤ≥ ‘ 1 ) )
4 1 3 sylib ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 1 ) )
5 fzisfzounsn ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 1 ) → ( 1 ... 𝑀 ) = ( ( 1 ..^ 𝑀 ) ∪ { 𝑀 } ) )
6 4 5 syl ⊢ ( 𝜑 → ( 1 ... 𝑀 ) = ( ( 1 ..^ 𝑀 ) ∪ { 𝑀 } ) )
7 6 eleq2d ⊢ ( 𝜑 → ( 𝑖 ∈ ( 1 ... 𝑀 ) ↔ 𝑖 ∈ ( ( 1 ..^ 𝑀 ) ∪ { 𝑀 } ) ) )
8 elun ⊢ ( 𝑖 ∈ ( ( 1 ..^ 𝑀 ) ∪ { 𝑀 } ) ↔ ( 𝑖 ∈ ( 1 ..^ 𝑀 ) ∨ 𝑖 ∈ { 𝑀 } ) )
9 8 a1i ⊢ ( 𝜑 → ( 𝑖 ∈ ( ( 1 ..^ 𝑀 ) ∪ { 𝑀 } ) ↔ ( 𝑖 ∈ ( 1 ..^ 𝑀 ) ∨ 𝑖 ∈ { 𝑀 } ) ) )
10 velsn ⊢ ( 𝑖 ∈ { 𝑀 } ↔ 𝑖 = 𝑀 )
11 10 a1i ⊢ ( 𝜑 → ( 𝑖 ∈ { 𝑀 } ↔ 𝑖 = 𝑀 ) )
12 11 orbi2d ⊢ ( 𝜑 → ( ( 𝑖 ∈ ( 1 ..^ 𝑀 ) ∨ 𝑖 ∈ { 𝑀 } ) ↔ ( 𝑖 ∈ ( 1 ..^ 𝑀 ) ∨ 𝑖 = 𝑀 ) ) )
13 7 9 12 3bitrd ⊢ ( 𝜑 → ( 𝑖 ∈ ( 1 ... 𝑀 ) ↔ ( 𝑖 ∈ ( 1 ..^ 𝑀 ) ∨ 𝑖 = 𝑀 ) ) )
14 fveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑖 ) )
15 14 breq2d ⊢ ( 𝑘 = 𝑖 → ( ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑘 ) ↔ ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑖 ) ) )
16 15 rspccv ⊢ ( ∀ 𝑘 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑘 ) → ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑖 ) ) )
17 1 2 iccpartigtl ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑘 ) )
18 16 17 syl11 ⊢ ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → ( 𝜑 → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑖 ) ) )
19 1 2 iccpartlt ⊢ ( 𝜑 → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑀 ) )
20 19 adantl ⊢ ( ( 𝑖 = 𝑀 ∧ 𝜑 ) → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑀 ) )
21 fveq2 ⊢ ( 𝑖 = 𝑀 → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑀 ) )
22 21 adantr ⊢ ( ( 𝑖 = 𝑀 ∧ 𝜑 ) → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑀 ) )
23 20 22 breqtrrd ⊢ ( ( 𝑖 = 𝑀 ∧ 𝜑 ) → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑖 ) )
24 23 ex ⊢ ( 𝑖 = 𝑀 → ( 𝜑 → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑖 ) ) )
25 18 24 jaoi ⊢ ( ( 𝑖 ∈ ( 1 ..^ 𝑀 ) ∨ 𝑖 = 𝑀 ) → ( 𝜑 → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑖 ) ) )
26 25 com12 ⊢ ( 𝜑 → ( ( 𝑖 ∈ ( 1 ..^ 𝑀 ) ∨ 𝑖 = 𝑀 ) → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑖 ) ) )
27 13 26 sylbid ⊢ ( 𝜑 → ( 𝑖 ∈ ( 1 ... 𝑀 ) → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑖 ) ) )
28 27 ralrimiv ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑖 ) )