This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ¬ ( 𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴 ) )

Proof

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