**Description:** 'Less than' is not symmetric. (Contributed by NM, 8-Jan-2002)

Ref | Expression | ||
---|---|---|---|

Assertion | ltnsym | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 → ¬ 𝐵 < 𝐴 ) ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | axlttri | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 < 𝐴 ) ) ) | |

2 | pm2.46 | ⊢ ( ¬ ( 𝐴 = 𝐵 ∨ 𝐵 < 𝐴 ) → ¬ 𝐵 < 𝐴 ) | |

3 | 1 2 | syl6bi | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 → ¬ 𝐵 < 𝐴 ) ) |