Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  pitri3or GIF version

Theorem pitri3or 6306
 Description: Trichotomy for positive integers. (Contributed by Jim Kingdon, 21-Sep-2019.)
Assertion
Ref Expression
pitri3or ((A N B N) → (A <N B A = B B <N A))

Proof of Theorem pitri3or
StepHypRef Expression
1 pinn 6293 . . 3 (A NA 𝜔)
2 pinn 6293 . . 3 (B NB 𝜔)
3 nntri3or 6011 . . 3 ((A 𝜔 B 𝜔) → (A B A = B B A))
41, 2, 3syl2an 273 . 2 ((A N B N) → (A B A = B B A))
5 ltpiord 6303 . . 3 ((A N B N) → (A <N BA B))
6 biidd 161 . . 3 ((A N B N) → (A = BA = B))
7 ltpiord 6303 . . . 4 ((B N A N) → (B <N AB A))
87ancoms 255 . . 3 ((A N B N) → (B <N AB A))
95, 6, 83orbi123d 1205 . 2 ((A N B N) → ((A <N B A = B B <N A) ↔ (A B A = B B A)))
104, 9mpbird 156 1 ((A N B N) → (A <N B A = B B <N A))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∨ w3o 883   = wceq 1242   ∈ wcel 1390   class class class wbr 3755  𝜔com 4256  Ncnpi 6256
 Copyright terms: Public domain W3C validator