Metamath Proof Explorer

Theorem nltle2tri

Description: Negated extended trichotomy law for 'less than' and 'less than or equal to'. (Contributed by AV, 18-Jul-2020)

Ref Expression
Assertion nltle2tri ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → ¬ A < B ∧ B ≤ C ∧ C ≤ A

Proof

Step Hyp Ref Expression
1 xrltletr ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → A < B ∧ B ≤ C → A < C
2 id ⊢ A < B ∧ B ≤ C → A < C → A < B ∧ B ≤ C → A < C
3 2 impcom ⊢ A < B ∧ B ≤ C ∧ A < B ∧ B ≤ C → A < C → A < C
4 xrltnle ⊢ A ∈ ℝ * ∧ C ∈ ℝ * → A < C ↔ ¬ C ≤ A
5 4 3adant2 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → A < C ↔ ¬ C ≤ A
6 5 biimpd ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → A < C → ¬ C ≤ A
7 6 imp ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A < C → ¬ C ≤ A
8 7 olcd ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A < C → ¬ A < B ∧ B ≤ C ∨ ¬ C ≤ A
9 8 expcom ⊢ A < C → A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → ¬ A < B ∧ B ≤ C ∨ ¬ C ≤ A
10 3 9 syl ⊢ A < B ∧ B ≤ C ∧ A < B ∧ B ≤ C → A < C → A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → ¬ A < B ∧ B ≤ C ∨ ¬ C ≤ A
11 10 ex ⊢ A < B ∧ B ≤ C → A < B ∧ B ≤ C → A < C → A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → ¬ A < B ∧ B ≤ C ∨ ¬ C ≤ A
12 11 com23 ⊢ A < B ∧ B ≤ C → A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → A < B ∧ B ≤ C → A < C → ¬ A < B ∧ B ≤ C ∨ ¬ C ≤ A
13 12 impd ⊢ A < B ∧ B ≤ C → A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A < B ∧ B ≤ C → A < C → ¬ A < B ∧ B ≤ C ∨ ¬ C ≤ A
14 id ⊢ ¬ A < B ∧ B ≤ C → ¬ A < B ∧ B ≤ C
15 14 orcd ⊢ ¬ A < B ∧ B ≤ C → ¬ A < B ∧ B ≤ C ∨ ¬ C ≤ A
16 15 a1d ⊢ ¬ A < B ∧ B ≤ C → A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A < B ∧ B ≤ C → A < C → ¬ A < B ∧ B ≤ C ∨ ¬ C ≤ A
17 13 16 pm2.61i ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A < B ∧ B ≤ C → A < C → ¬ A < B ∧ B ≤ C ∨ ¬ C ≤ A
18 df-3an ⊢ A < B ∧ B ≤ C ∧ C ≤ A ↔ A < B ∧ B ≤ C ∧ C ≤ A
19 18 notbii ⊢ ¬ A < B ∧ B ≤ C ∧ C ≤ A ↔ ¬ A < B ∧ B ≤ C ∧ C ≤ A
20 ianor ⊢ ¬ A < B ∧ B ≤ C ∧ C ≤ A ↔ ¬ A < B ∧ B ≤ C ∨ ¬ C ≤ A
21 19 20 bitri ⊢ ¬ A < B ∧ B ≤ C ∧ C ≤ A ↔ ¬ A < B ∧ B ≤ C ∨ ¬ C ≤ A
22 17 21 sylibr ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A < B ∧ B ≤ C → A < C → ¬ A < B ∧ B ≤ C ∧ C ≤ A
23 22 ex ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → A < B ∧ B ≤ C → A < C → ¬ A < B ∧ B ≤ C ∧ C ≤ A
24 1 23 mpd ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → ¬ A < B ∧ B ≤ C ∧ C ≤ A