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

Proof

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