Proof of Theorem elfzonelfzo
Step | Hyp | Ref
| Expression |
1 | | elfzo2 9160 |
. . 3
⊢ (𝐾 ∈ (𝑀..^𝑅) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑅 ∈ ℤ ∧ 𝐾 < 𝑅)) |
2 | | simpr 108 |
. . . . . 6
⊢ ((((𝐾 ∈
(ℤ≥‘𝑀) ∧ 𝑅 ∈ ℤ ∧ 𝐾 < 𝑅) ∧ ¬ 𝐾 ∈ (𝑀..^𝑁)) ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℤ) |
3 | | eluzelz 8628 |
. . . . . . . 8
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → 𝐾 ∈ ℤ) |
4 | 3 | 3ad2ant1 959 |
. . . . . . 7
⊢ ((𝐾 ∈
(ℤ≥‘𝑀) ∧ 𝑅 ∈ ℤ ∧ 𝐾 < 𝑅) → 𝐾 ∈ ℤ) |
5 | 4 | ad2antrr 471 |
. . . . . 6
⊢ ((((𝐾 ∈
(ℤ≥‘𝑀) ∧ 𝑅 ∈ ℤ ∧ 𝐾 < 𝑅) ∧ ¬ 𝐾 ∈ (𝑀..^𝑁)) ∧ 𝑁 ∈ ℤ) → 𝐾 ∈ ℤ) |
6 | 3 | adantr 270 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ) → 𝐾 ∈ ℤ) |
7 | | eluzel2 8624 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
8 | 7 | adantr 270 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℤ) |
9 | | simpr 108 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℤ) |
10 | | elfzo 9159 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀..^𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁))) |
11 | 6, 8, 9, 10 | syl3anc 1169 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀..^𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁))) |
12 | | eluzle 8631 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝐾) |
13 | 12 | adantr 270 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ) → 𝑀 ≤ 𝐾) |
14 | 13 | biantrurd 299 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ) → (𝐾 < 𝑁 ↔ (𝑀 ≤ 𝐾 ∧ 𝐾 < 𝑁))) |
15 | 11, 14 | bitr4d 189 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀..^𝑁) ↔ 𝐾 < 𝑁)) |
16 | 15 | notbid 624 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ) → (¬ 𝐾 ∈ (𝑀..^𝑁) ↔ ¬ 𝐾 < 𝑁)) |
17 | 9 | zred 8469 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℝ) |
18 | 6 | zred 8469 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ) → 𝐾 ∈ ℝ) |
19 | 17, 18 | lenltd 7227 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ 𝐾 ↔ ¬ 𝐾 < 𝑁)) |
20 | 16, 19 | bitr4d 189 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ) → (¬ 𝐾 ∈ (𝑀..^𝑁) ↔ 𝑁 ≤ 𝐾)) |
21 | 20 | biimpd 142 |
. . . . . . . . . 10
⊢ ((𝐾 ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ) → (¬ 𝐾 ∈ (𝑀..^𝑁) → 𝑁 ≤ 𝐾)) |
22 | 21 | ex 113 |
. . . . . . . . 9
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → (𝑁 ∈ ℤ → (¬ 𝐾 ∈ (𝑀..^𝑁) → 𝑁 ≤ 𝐾))) |
23 | 22 | com23 77 |
. . . . . . . 8
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → (¬ 𝐾 ∈ (𝑀..^𝑁) → (𝑁 ∈ ℤ → 𝑁 ≤ 𝐾))) |
24 | 23 | 3ad2ant1 959 |
. . . . . . 7
⊢ ((𝐾 ∈
(ℤ≥‘𝑀) ∧ 𝑅 ∈ ℤ ∧ 𝐾 < 𝑅) → (¬ 𝐾 ∈ (𝑀..^𝑁) → (𝑁 ∈ ℤ → 𝑁 ≤ 𝐾))) |
25 | 24 | imp31 252 |
. . . . . 6
⊢ ((((𝐾 ∈
(ℤ≥‘𝑀) ∧ 𝑅 ∈ ℤ ∧ 𝐾 < 𝑅) ∧ ¬ 𝐾 ∈ (𝑀..^𝑁)) ∧ 𝑁 ∈ ℤ) → 𝑁 ≤ 𝐾) |
26 | | eluz2 8625 |
. . . . . 6
⊢ (𝐾 ∈
(ℤ≥‘𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ≤ 𝐾)) |
27 | 2, 5, 25, 26 | syl3anbrc 1122 |
. . . . 5
⊢ ((((𝐾 ∈
(ℤ≥‘𝑀) ∧ 𝑅 ∈ ℤ ∧ 𝐾 < 𝑅) ∧ ¬ 𝐾 ∈ (𝑀..^𝑁)) ∧ 𝑁 ∈ ℤ) → 𝐾 ∈ (ℤ≥‘𝑁)) |
28 | | simpll2 978 |
. . . . 5
⊢ ((((𝐾 ∈
(ℤ≥‘𝑀) ∧ 𝑅 ∈ ℤ ∧ 𝐾 < 𝑅) ∧ ¬ 𝐾 ∈ (𝑀..^𝑁)) ∧ 𝑁 ∈ ℤ) → 𝑅 ∈ ℤ) |
29 | | simpll3 979 |
. . . . 5
⊢ ((((𝐾 ∈
(ℤ≥‘𝑀) ∧ 𝑅 ∈ ℤ ∧ 𝐾 < 𝑅) ∧ ¬ 𝐾 ∈ (𝑀..^𝑁)) ∧ 𝑁 ∈ ℤ) → 𝐾 < 𝑅) |
30 | | elfzo2 9160 |
. . . . 5
⊢ (𝐾 ∈ (𝑁..^𝑅) ↔ (𝐾 ∈ (ℤ≥‘𝑁) ∧ 𝑅 ∈ ℤ ∧ 𝐾 < 𝑅)) |
31 | 27, 28, 29, 30 | syl3anbrc 1122 |
. . . 4
⊢ ((((𝐾 ∈
(ℤ≥‘𝑀) ∧ 𝑅 ∈ ℤ ∧ 𝐾 < 𝑅) ∧ ¬ 𝐾 ∈ (𝑀..^𝑁)) ∧ 𝑁 ∈ ℤ) → 𝐾 ∈ (𝑁..^𝑅)) |
32 | 31 | ex 113 |
. . 3
⊢ (((𝐾 ∈
(ℤ≥‘𝑀) ∧ 𝑅 ∈ ℤ ∧ 𝐾 < 𝑅) ∧ ¬ 𝐾 ∈ (𝑀..^𝑁)) → (𝑁 ∈ ℤ → 𝐾 ∈ (𝑁..^𝑅))) |
33 | 1, 32 | sylanb 278 |
. 2
⊢ ((𝐾 ∈ (𝑀..^𝑅) ∧ ¬ 𝐾 ∈ (𝑀..^𝑁)) → (𝑁 ∈ ℤ → 𝐾 ∈ (𝑁..^𝑅))) |
34 | 33 | com12 30 |
1
⊢ (𝑁 ∈ ℤ → ((𝐾 ∈ (𝑀..^𝑅) ∧ ¬ 𝐾 ∈ (𝑀..^𝑁)) → 𝐾 ∈ (𝑁..^𝑅))) |