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