Metamath Proof Explorer

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 ⊢ φ → M ∈ ℕ
iccpartgtprec.p ⊢ φ → P ∈ RePart ⁡ M
Assertion iccpartltu ⊢ φ → ∀ i ∈ 0 ..^ M P ⁡ i < P ⁡ M

Proof

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