Proof of Theorem elfzomelpfzo
Step | Hyp | Ref
| Expression |
1 | | zsubcl 12107 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑀 − 𝐿) ∈ ℤ) |
2 | 1 | ad2ant2rl 749 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → (𝑀 − 𝐿) ∈ ℤ) |
3 | | simpl 486 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈
ℤ) |
4 | 3 | adantr 484 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → 𝑀 ∈
ℤ) |
5 | 2, 4 | 2thd 268 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → ((𝑀 − 𝐿) ∈ ℤ ↔ 𝑀 ∈ ℤ)) |
6 | | simpl 486 |
. . . . . . 7
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → 𝐾 ∈
ℤ) |
7 | 6 | adantl 485 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → 𝐾 ∈
ℤ) |
8 | | zaddcl 12105 |
. . . . . . 7
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝐾 + 𝐿) ∈ ℤ) |
9 | 8 | adantl 485 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → (𝐾 + 𝐿) ∈ ℤ) |
10 | 7, 9 | 2thd 268 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → (𝐾 ∈ ℤ ↔ (𝐾 + 𝐿) ∈ ℤ)) |
11 | | zre 12068 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
12 | 11 | adantr 484 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈
ℝ) |
13 | 12 | adantr 484 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → 𝑀 ∈
ℝ) |
14 | | zre 12068 |
. . . . . . . 8
⊢ (𝐿 ∈ ℤ → 𝐿 ∈
ℝ) |
15 | 14 | adantl 485 |
. . . . . . 7
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → 𝐿 ∈
ℝ) |
16 | 15 | adantl 485 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → 𝐿 ∈
ℝ) |
17 | | zre 12068 |
. . . . . . . 8
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℝ) |
18 | 17 | adantr 484 |
. . . . . . 7
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → 𝐾 ∈
ℝ) |
19 | 18 | adantl 485 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → 𝐾 ∈
ℝ) |
20 | 13, 16, 19 | lesubaddd 11317 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → ((𝑀 − 𝐿) ≤ 𝐾 ↔ 𝑀 ≤ (𝐾 + 𝐿))) |
21 | 5, 10, 20 | 3anbi123d 1437 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ)) →
(((𝑀 − 𝐿) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ (𝑀 − 𝐿) ≤ 𝐾) ↔ (𝑀 ∈ ℤ ∧ (𝐾 + 𝐿) ∈ ℤ ∧ 𝑀 ≤ (𝐾 + 𝐿)))) |
22 | | eluz2 12332 |
. . . 4
⊢ (𝐾 ∈
(ℤ≥‘(𝑀 − 𝐿)) ↔ ((𝑀 − 𝐿) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ (𝑀 − 𝐿) ≤ 𝐾)) |
23 | | eluz2 12332 |
. . . 4
⊢ ((𝐾 + 𝐿) ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝐾 + 𝐿) ∈ ℤ ∧ 𝑀 ≤ (𝐾 + 𝐿))) |
24 | 21, 22, 23 | 3bitr4g 317 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → (𝐾 ∈
(ℤ≥‘(𝑀 − 𝐿)) ↔ (𝐾 + 𝐿) ∈ (ℤ≥‘𝑀))) |
25 | | zsubcl 12107 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑁 − 𝐿) ∈ ℤ) |
26 | 25 | ad2ant2l 746 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → (𝑁 − 𝐿) ∈ ℤ) |
27 | | simplr 769 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → 𝑁 ∈
ℤ) |
28 | 26, 27 | 2thd 268 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → ((𝑁 − 𝐿) ∈ ℤ ↔ 𝑁 ∈ ℤ)) |
29 | | zre 12068 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
30 | 29 | adantl 485 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈
ℝ) |
31 | 30 | adantr 484 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → 𝑁 ∈
ℝ) |
32 | 19, 16, 31 | ltaddsubd 11320 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → ((𝐾 + 𝐿) < 𝑁 ↔ 𝐾 < (𝑁 − 𝐿))) |
33 | 32 | bicomd 226 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → (𝐾 < (𝑁 − 𝐿) ↔ (𝐾 + 𝐿) < 𝑁)) |
34 | 24, 28, 33 | 3anbi123d 1437 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → ((𝐾 ∈
(ℤ≥‘(𝑀 − 𝐿)) ∧ (𝑁 − 𝐿) ∈ ℤ ∧ 𝐾 < (𝑁 − 𝐿)) ↔ ((𝐾 + 𝐿) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ (𝐾 + 𝐿) < 𝑁))) |
35 | | elfzo2 13134 |
. 2
⊢ (𝐾 ∈ ((𝑀 − 𝐿)..^(𝑁 − 𝐿)) ↔ (𝐾 ∈ (ℤ≥‘(𝑀 − 𝐿)) ∧ (𝑁 − 𝐿) ∈ ℤ ∧ 𝐾 < (𝑁 − 𝐿))) |
36 | | elfzo2 13134 |
. 2
⊢ ((𝐾 + 𝐿) ∈ (𝑀..^𝑁) ↔ ((𝐾 + 𝐿) ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ (𝐾 + 𝐿) < 𝑁)) |
37 | 34, 35, 36 | 3bitr4g 317 |
1
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → (𝐾 ∈ ((𝑀 − 𝐿)..^(𝑁 − 𝐿)) ↔ (𝐾 + 𝐿) ∈ (𝑀..^𝑁))) |