Proof of Theorem fztri3or
Step | Hyp | Ref
| Expression |
1 | | 3mix1 1151 |
. . 3
⊢ (𝐾 < 𝑀 → (𝐾 < 𝑀 ∨ 𝐾 ∈ (𝑀...𝑁) ∨ 𝑁 < 𝐾)) |
2 | 1 | adantl 275 |
. 2
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝑀) → (𝐾 < 𝑀 ∨ 𝐾 ∈ (𝑀...𝑁) ∨ 𝑁 < 𝐾)) |
3 | | 3mix3 1153 |
. . . 4
⊢ (𝑁 < 𝐾 → (𝐾 < 𝑀 ∨ 𝐾 ∈ (𝑀...𝑁) ∨ 𝑁 < 𝐾)) |
4 | 3 | adantl 275 |
. . 3
⊢ ((((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝐾 < 𝑀) ∧ 𝑁 < 𝐾) → (𝐾 < 𝑀 ∨ 𝐾 ∈ (𝑀...𝑁) ∨ 𝑁 < 𝐾)) |
5 | | simpr 109 |
. . . . . . 7
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝐾 < 𝑀) → ¬ 𝐾 < 𝑀) |
6 | | simpl2 986 |
. . . . . . . . 9
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝐾 < 𝑀) → 𝑀 ∈ ℤ) |
7 | 6 | zred 9291 |
. . . . . . . 8
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝐾 < 𝑀) → 𝑀 ∈ ℝ) |
8 | | simpl1 985 |
. . . . . . . . 9
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝐾 < 𝑀) → 𝐾 ∈ ℤ) |
9 | 8 | zred 9291 |
. . . . . . . 8
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝐾 < 𝑀) → 𝐾 ∈ ℝ) |
10 | 7, 9 | lenltd 7997 |
. . . . . . 7
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝐾 < 𝑀) → (𝑀 ≤ 𝐾 ↔ ¬ 𝐾 < 𝑀)) |
11 | 5, 10 | mpbird 166 |
. . . . . 6
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝐾 < 𝑀) → 𝑀 ≤ 𝐾) |
12 | 11 | adantr 274 |
. . . . 5
⊢ ((((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝐾 < 𝑀) ∧ ¬ 𝑁 < 𝐾) → 𝑀 ≤ 𝐾) |
13 | | simpr 109 |
. . . . . 6
⊢ ((((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝐾 < 𝑀) ∧ ¬ 𝑁 < 𝐾) → ¬ 𝑁 < 𝐾) |
14 | 9 | adantr 274 |
. . . . . . 7
⊢ ((((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝐾 < 𝑀) ∧ ¬ 𝑁 < 𝐾) → 𝐾 ∈ ℝ) |
15 | | simpll3 1023 |
. . . . . . . 8
⊢ ((((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝐾 < 𝑀) ∧ ¬ 𝑁 < 𝐾) → 𝑁 ∈ ℤ) |
16 | 15 | zred 9291 |
. . . . . . 7
⊢ ((((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝐾 < 𝑀) ∧ ¬ 𝑁 < 𝐾) → 𝑁 ∈ ℝ) |
17 | 14, 16 | lenltd 7997 |
. . . . . 6
⊢ ((((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝐾 < 𝑀) ∧ ¬ 𝑁 < 𝐾) → (𝐾 ≤ 𝑁 ↔ ¬ 𝑁 < 𝐾)) |
18 | 13, 17 | mpbird 166 |
. . . . 5
⊢ ((((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝐾 < 𝑀) ∧ ¬ 𝑁 < 𝐾) → 𝐾 ≤ 𝑁) |
19 | | elfz 9924 |
. . . . . . 7
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) |
20 | 19 | adantr 274 |
. . . . . 6
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝐾 < 𝑀) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) |
21 | 20 | adantr 274 |
. . . . 5
⊢ ((((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝐾 < 𝑀) ∧ ¬ 𝑁 < 𝐾) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) |
22 | 12, 18, 21 | mpbir2and 929 |
. . . 4
⊢ ((((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝐾 < 𝑀) ∧ ¬ 𝑁 < 𝐾) → 𝐾 ∈ (𝑀...𝑁)) |
23 | 22 | 3mix2d 1158 |
. . 3
⊢ ((((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝐾 < 𝑀) ∧ ¬ 𝑁 < 𝐾) → (𝐾 < 𝑀 ∨ 𝐾 ∈ (𝑀...𝑁) ∨ 𝑁 < 𝐾)) |
24 | | zdclt 9246 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) →
DECID 𝑁 <
𝐾) |
25 | 24 | ancoms 266 |
. . . . . 6
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
DECID 𝑁 <
𝐾) |
26 | 25 | 3adant2 1001 |
. . . . 5
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
DECID 𝑁 <
𝐾) |
27 | 26 | adantr 274 |
. . . 4
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝐾 < 𝑀) → DECID 𝑁 < 𝐾) |
28 | | df-dc 821 |
. . . 4
⊢
(DECID 𝑁 < 𝐾 ↔ (𝑁 < 𝐾 ∨ ¬ 𝑁 < 𝐾)) |
29 | 27, 28 | sylib 121 |
. . 3
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝐾 < 𝑀) → (𝑁 < 𝐾 ∨ ¬ 𝑁 < 𝐾)) |
30 | 4, 23, 29 | mpjaodan 788 |
. 2
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
𝐾 < 𝑀) → (𝐾 < 𝑀 ∨ 𝐾 ∈ (𝑀...𝑁) ∨ 𝑁 < 𝐾)) |
31 | | zdclt 9246 |
. . . 4
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ) →
DECID 𝐾 <
𝑀) |
32 | 31 | 3adant3 1002 |
. . 3
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
DECID 𝐾 <
𝑀) |
33 | | df-dc 821 |
. . 3
⊢
(DECID 𝐾 < 𝑀 ↔ (𝐾 < 𝑀 ∨ ¬ 𝐾 < 𝑀)) |
34 | 32, 33 | sylib 121 |
. 2
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 < 𝑀 ∨ ¬ 𝐾 < 𝑀)) |
35 | 2, 30, 34 | mpjaodan 788 |
1
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 < 𝑀 ∨ 𝐾 ∈ (𝑀...𝑁) ∨ 𝑁 < 𝐾)) |