Proof of Theorem metakunt18
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | metakunt18.2 | . . . . . 6
⊢ (𝜑 → 𝐼 ∈ ℕ) | 
| 2 | 1 | nnred 12281 | . . . . 5
⊢ (𝜑 → 𝐼 ∈ ℝ) | 
| 3 | 2 | ltm1d 12200 | . . . 4
⊢ (𝜑 → (𝐼 − 1) < 𝐼) | 
| 4 |  | fzdisj 13591 | . . . 4
⊢ ((𝐼 − 1) < 𝐼 → ((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅) | 
| 5 | 3, 4 | syl 17 | . . 3
⊢ (𝜑 → ((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅) | 
| 6 |  | metakunt18.1 | . . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 7 | 6 | nnzd 12640 | . . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 8 |  | fzsn 13606 | . . . . . . 7
⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀}) | 
| 9 | 7, 8 | syl 17 | . . . . . 6
⊢ (𝜑 → (𝑀...𝑀) = {𝑀}) | 
| 10 | 9 | eqcomd 2743 | . . . . 5
⊢ (𝜑 → {𝑀} = (𝑀...𝑀)) | 
| 11 | 10 | ineq2d 4220 | . . . 4
⊢ (𝜑 → ((1...(𝐼 − 1)) ∩ {𝑀}) = ((1...(𝐼 − 1)) ∩ (𝑀...𝑀))) | 
| 12 |  | metakunt18.3 | . . . . . 6
⊢ (𝜑 → 𝐼 ≤ 𝑀) | 
| 13 | 1 | nnzd 12640 | . . . . . . 7
⊢ (𝜑 → 𝐼 ∈ ℤ) | 
| 14 |  | zlem1lt 12669 | . . . . . . 7
⊢ ((𝐼 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝐼 ≤ 𝑀 ↔ (𝐼 − 1) < 𝑀)) | 
| 15 | 13, 7, 14 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (𝐼 ≤ 𝑀 ↔ (𝐼 − 1) < 𝑀)) | 
| 16 | 12, 15 | mpbid 232 | . . . . 5
⊢ (𝜑 → (𝐼 − 1) < 𝑀) | 
| 17 |  | fzdisj 13591 | . . . . 5
⊢ ((𝐼 − 1) < 𝑀 → ((1...(𝐼 − 1)) ∩ (𝑀...𝑀)) = ∅) | 
| 18 | 16, 17 | syl 17 | . . . 4
⊢ (𝜑 → ((1...(𝐼 − 1)) ∩ (𝑀...𝑀)) = ∅) | 
| 19 | 11, 18 | eqtrd 2777 | . . 3
⊢ (𝜑 → ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅) | 
| 20 | 10 | ineq2d 4220 | . . . 4
⊢ (𝜑 → ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ((𝐼...(𝑀 − 1)) ∩ (𝑀...𝑀))) | 
| 21 | 6 | nnred 12281 | . . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℝ) | 
| 22 | 21 | ltm1d 12200 | . . . . 5
⊢ (𝜑 → (𝑀 − 1) < 𝑀) | 
| 23 |  | fzdisj 13591 | . . . . 5
⊢ ((𝑀 − 1) < 𝑀 → ((𝐼...(𝑀 − 1)) ∩ (𝑀...𝑀)) = ∅) | 
| 24 | 22, 23 | syl 17 | . . . 4
⊢ (𝜑 → ((𝐼...(𝑀 − 1)) ∩ (𝑀...𝑀)) = ∅) | 
| 25 | 20, 24 | eqtrd 2777 | . . 3
⊢ (𝜑 → ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅) | 
| 26 | 5, 19, 25 | 3jca 1129 | . 2
⊢ (𝜑 → (((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅ ∧ ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅ ∧ ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅)) | 
| 27 |  | incom 4209 | . . . . 5
⊢ ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (1...(𝑀 − 𝐼))) = ((1...(𝑀 − 𝐼)) ∩ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) | 
| 28 | 27 | a1i 11 | . . . 4
⊢ (𝜑 → ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (1...(𝑀 − 𝐼))) = ((1...(𝑀 − 𝐼)) ∩ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)))) | 
| 29 | 21, 2 | resubcld 11691 | . . . . . 6
⊢ (𝜑 → (𝑀 − 𝐼) ∈ ℝ) | 
| 30 | 29 | ltp1d 12198 | . . . . 5
⊢ (𝜑 → (𝑀 − 𝐼) < ((𝑀 − 𝐼) + 1)) | 
| 31 |  | fzdisj 13591 | . . . . 5
⊢ ((𝑀 − 𝐼) < ((𝑀 − 𝐼) + 1) → ((1...(𝑀 − 𝐼)) ∩ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) = ∅) | 
| 32 | 30, 31 | syl 17 | . . . 4
⊢ (𝜑 → ((1...(𝑀 − 𝐼)) ∩ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) = ∅) | 
| 33 | 28, 32 | eqtrd 2777 | . . 3
⊢ (𝜑 → ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (1...(𝑀 − 𝐼))) = ∅) | 
| 34 | 10 | ineq2d 4220 | . . . 4
⊢ (𝜑 → ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ {𝑀}) = ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (𝑀...𝑀))) | 
| 35 |  | fzdisj 13591 | . . . . 5
⊢ ((𝑀 − 1) < 𝑀 → ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (𝑀...𝑀)) = ∅) | 
| 36 | 22, 35 | syl 17 | . . . 4
⊢ (𝜑 → ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (𝑀...𝑀)) = ∅) | 
| 37 | 34, 36 | eqtrd 2777 | . . 3
⊢ (𝜑 → ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ {𝑀}) = ∅) | 
| 38 | 10 | ineq2d 4220 | . . . 4
⊢ (𝜑 → ((1...(𝑀 − 𝐼)) ∩ {𝑀}) = ((1...(𝑀 − 𝐼)) ∩ (𝑀...𝑀))) | 
| 39 | 1 | nnrpd 13075 | . . . . . 6
⊢ (𝜑 → 𝐼 ∈
ℝ+) | 
| 40 | 21, 39 | ltsubrpd 13109 | . . . . 5
⊢ (𝜑 → (𝑀 − 𝐼) < 𝑀) | 
| 41 |  | fzdisj 13591 | . . . . 5
⊢ ((𝑀 − 𝐼) < 𝑀 → ((1...(𝑀 − 𝐼)) ∩ (𝑀...𝑀)) = ∅) | 
| 42 | 40, 41 | syl 17 | . . . 4
⊢ (𝜑 → ((1...(𝑀 − 𝐼)) ∩ (𝑀...𝑀)) = ∅) | 
| 43 | 38, 42 | eqtrd 2777 | . . 3
⊢ (𝜑 → ((1...(𝑀 − 𝐼)) ∩ {𝑀}) = ∅) | 
| 44 | 33, 37, 43 | 3jca 1129 | . 2
⊢ (𝜑 → (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (1...(𝑀 − 𝐼))) = ∅ ∧ ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ {𝑀}) = ∅ ∧ ((1...(𝑀 − 𝐼)) ∩ {𝑀}) = ∅)) | 
| 45 | 26, 44 | jca 511 | 1
⊢ (𝜑 → ((((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅ ∧ ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅ ∧ ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅) ∧ (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (1...(𝑀 − 𝐼))) = ∅ ∧ ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ {𝑀}) = ∅ ∧ ((1...(𝑀 − 𝐼)) ∩ {𝑀}) = ∅))) |