Proof of Theorem metakunt18
Step | Hyp | Ref
| Expression |
1 | | metakunt18.2 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ ℕ) |
2 | 1 | nnred 11674 |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ ℝ) |
3 | 2 | ltm1d 11595 |
. . . 4
⊢ (𝜑 → (𝐼 − 1) < 𝐼) |
4 | | fzdisj 12968 |
. . . 4
⊢ ((𝐼 − 1) < 𝐼 → ((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅) |
5 | 3, 4 | syl 17 |
. . 3
⊢ (𝜑 → ((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅) |
6 | | metakunt18.1 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℕ) |
7 | 6 | nnzd 12110 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℤ) |
8 | | fzsn 12983 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀}) |
9 | 7, 8 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑀...𝑀) = {𝑀}) |
10 | 9 | eqcomd 2765 |
. . . . 5
⊢ (𝜑 → {𝑀} = (𝑀...𝑀)) |
11 | 10 | ineq2d 4113 |
. . . 4
⊢ (𝜑 → ((1...(𝐼 − 1)) ∩ {𝑀}) = ((1...(𝐼 − 1)) ∩ (𝑀...𝑀))) |
12 | | metakunt18.3 |
. . . . . 6
⊢ (𝜑 → 𝐼 ≤ 𝑀) |
13 | 1 | nnzd 12110 |
. . . . . . 7
⊢ (𝜑 → 𝐼 ∈ ℤ) |
14 | | zlem1lt 12058 |
. . . . . . 7
⊢ ((𝐼 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝐼 ≤ 𝑀 ↔ (𝐼 − 1) < 𝑀)) |
15 | 13, 7, 14 | syl2anc 588 |
. . . . . 6
⊢ (𝜑 → (𝐼 ≤ 𝑀 ↔ (𝐼 − 1) < 𝑀)) |
16 | 12, 15 | mpbid 235 |
. . . . 5
⊢ (𝜑 → (𝐼 − 1) < 𝑀) |
17 | | fzdisj 12968 |
. . . . 5
⊢ ((𝐼 − 1) < 𝑀 → ((1...(𝐼 − 1)) ∩ (𝑀...𝑀)) = ∅) |
18 | 16, 17 | syl 17 |
. . . 4
⊢ (𝜑 → ((1...(𝐼 − 1)) ∩ (𝑀...𝑀)) = ∅) |
19 | 11, 18 | eqtrd 2794 |
. . 3
⊢ (𝜑 → ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅) |
20 | 10 | ineq2d 4113 |
. . . 4
⊢ (𝜑 → ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ((𝐼...(𝑀 − 1)) ∩ (𝑀...𝑀))) |
21 | 6 | nnred 11674 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℝ) |
22 | 21 | ltm1d 11595 |
. . . . 5
⊢ (𝜑 → (𝑀 − 1) < 𝑀) |
23 | | fzdisj 12968 |
. . . . 5
⊢ ((𝑀 − 1) < 𝑀 → ((𝐼...(𝑀 − 1)) ∩ (𝑀...𝑀)) = ∅) |
24 | 22, 23 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝐼...(𝑀 − 1)) ∩ (𝑀...𝑀)) = ∅) |
25 | 20, 24 | eqtrd 2794 |
. . 3
⊢ (𝜑 → ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅) |
26 | 5, 19, 25 | 3jca 1126 |
. 2
⊢ (𝜑 → (((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅ ∧ ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅ ∧ ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅)) |
27 | | incom 4102 |
. . . . 5
⊢ ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (1...(𝑀 − 𝐼))) = ((1...(𝑀 − 𝐼)) ∩ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) |
28 | 27 | a1i 11 |
. . . 4
⊢ (𝜑 → ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (1...(𝑀 − 𝐼))) = ((1...(𝑀 − 𝐼)) ∩ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)))) |
29 | 21, 2 | resubcld 11091 |
. . . . . 6
⊢ (𝜑 → (𝑀 − 𝐼) ∈ ℝ) |
30 | 29 | ltp1d 11593 |
. . . . 5
⊢ (𝜑 → (𝑀 − 𝐼) < ((𝑀 − 𝐼) + 1)) |
31 | | fzdisj 12968 |
. . . . 5
⊢ ((𝑀 − 𝐼) < ((𝑀 − 𝐼) + 1) → ((1...(𝑀 − 𝐼)) ∩ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) = ∅) |
32 | 30, 31 | syl 17 |
. . . 4
⊢ (𝜑 → ((1...(𝑀 − 𝐼)) ∩ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) = ∅) |
33 | 28, 32 | eqtrd 2794 |
. . 3
⊢ (𝜑 → ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (1...(𝑀 − 𝐼))) = ∅) |
34 | 10 | ineq2d 4113 |
. . . 4
⊢ (𝜑 → ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ {𝑀}) = ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (𝑀...𝑀))) |
35 | | fzdisj 12968 |
. . . . 5
⊢ ((𝑀 − 1) < 𝑀 → ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (𝑀...𝑀)) = ∅) |
36 | 22, 35 | syl 17 |
. . . 4
⊢ (𝜑 → ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (𝑀...𝑀)) = ∅) |
37 | 34, 36 | eqtrd 2794 |
. . 3
⊢ (𝜑 → ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ {𝑀}) = ∅) |
38 | 10 | ineq2d 4113 |
. . . 4
⊢ (𝜑 → ((1...(𝑀 − 𝐼)) ∩ {𝑀}) = ((1...(𝑀 − 𝐼)) ∩ (𝑀...𝑀))) |
39 | 1 | nnrpd 12455 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈
ℝ+) |
40 | 21, 39 | ltsubrpd 12489 |
. . . . 5
⊢ (𝜑 → (𝑀 − 𝐼) < 𝑀) |
41 | | fzdisj 12968 |
. . . . 5
⊢ ((𝑀 − 𝐼) < 𝑀 → ((1...(𝑀 − 𝐼)) ∩ (𝑀...𝑀)) = ∅) |
42 | 40, 41 | syl 17 |
. . . 4
⊢ (𝜑 → ((1...(𝑀 − 𝐼)) ∩ (𝑀...𝑀)) = ∅) |
43 | 38, 42 | eqtrd 2794 |
. . 3
⊢ (𝜑 → ((1...(𝑀 − 𝐼)) ∩ {𝑀}) = ∅) |
44 | 33, 37, 43 | 3jca 1126 |
. 2
⊢ (𝜑 → (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (1...(𝑀 − 𝐼))) = ∅ ∧ ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ {𝑀}) = ∅ ∧ ((1...(𝑀 − 𝐼)) ∩ {𝑀}) = ∅)) |
45 | 26, 44 | jca 516 |
1
⊢ (𝜑 → ((((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅ ∧ ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅ ∧ ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅) ∧ (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (1...(𝑀 − 𝐼))) = ∅ ∧ ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ {𝑀}) = ∅ ∧ ((1...(𝑀 − 𝐼)) ∩ {𝑀}) = ∅))) |