Proof of Theorem nltle2tri
Step | Hyp | Ref
| Expression |
1 | | xrltletr 12305 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶)) |
2 | | id 22 |
. . . . . . . . . 10
⊢ (((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶)) |
3 | 2 | impcom 398 |
. . . . . . . . 9
⊢ (((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) ∧ ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶)) → 𝐴 < 𝐶) |
4 | | xrltnle 10446 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐴 < 𝐶 ↔ ¬ 𝐶 ≤ 𝐴)) |
5 | 4 | 3adant2 1122 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → (𝐴 < 𝐶 ↔ ¬ 𝐶 ≤ 𝐴)) |
6 | 5 | biimpd 221 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → (𝐴 < 𝐶 → ¬ 𝐶 ≤ 𝐴)) |
7 | 6 | imp 397 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 < 𝐶) → ¬ 𝐶 ≤ 𝐴) |
8 | 7 | olcd 863 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ 𝐴 < 𝐶) → (¬ (𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) ∨ ¬ 𝐶 ≤ 𝐴)) |
9 | 8 | expcom 404 |
. . . . . . . . 9
⊢ (𝐴 < 𝐶 → ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (¬ (𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) ∨ ¬ 𝐶 ≤ 𝐴))) |
10 | 3, 9 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) ∧ ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶)) → ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (¬ (𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) ∨ ¬ 𝐶 ≤ 𝐴))) |
11 | 10 | ex 403 |
. . . . . . 7
⊢ ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → (((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶) → ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (¬ (𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) ∨ ¬ 𝐶 ≤ 𝐴)))) |
12 | 11 | com23 86 |
. . . . . 6
⊢ ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶) → (¬ (𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) ∨ ¬ 𝐶 ≤ 𝐴)))) |
13 | 12 | impd 400 |
. . . . 5
⊢ ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶)) → (¬ (𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) ∨ ¬ 𝐶 ≤ 𝐴))) |
14 | | id 22 |
. . . . . . 7
⊢ (¬
(𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → ¬ (𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶)) |
15 | 14 | orcd 862 |
. . . . . 6
⊢ (¬
(𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → (¬ (𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) ∨ ¬ 𝐶 ≤ 𝐴)) |
16 | 15 | a1d 25 |
. . . . 5
⊢ (¬
(𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶)) → (¬ (𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) ∨ ¬ 𝐶 ≤ 𝐴))) |
17 | 13, 16 | pm2.61i 177 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶)) → (¬ (𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) ∨ ¬ 𝐶 ≤ 𝐴)) |
18 | | df-3an 1073 |
. . . . . 6
⊢ ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴) ↔ ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) ∧ 𝐶 ≤ 𝐴)) |
19 | 18 | notbii 312 |
. . . . 5
⊢ (¬
(𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴) ↔ ¬ ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) ∧ 𝐶 ≤ 𝐴)) |
20 | | ianor 967 |
. . . . 5
⊢ (¬
((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) ∧ 𝐶 ≤ 𝐴) ↔ (¬ (𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) ∨ ¬ 𝐶 ≤ 𝐴)) |
21 | 19, 20 | bitri 267 |
. . . 4
⊢ (¬
(𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴) ↔ (¬ (𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) ∨ ¬ 𝐶 ≤ 𝐴)) |
22 | 17, 21 | sylibr 226 |
. . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) ∧ ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶)) → ¬ (𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴)) |
23 | 22 | ex 403 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → (((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶) → ¬ (𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴))) |
24 | 1, 23 | mpd 15 |
1
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ*) → ¬ (𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴)) |