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

Theorem pitric 6419
 Description: Trichotomy for positive integers. (Contributed by Jim Kingdon, 21-Sep-2019.)
Assertion
Ref Expression
pitric ((𝐴N𝐵N) → (𝐴 <N 𝐵 ↔ ¬ (𝐴 = 𝐵𝐵 <N 𝐴)))

Proof of Theorem pitric
StepHypRef Expression
1 pinn 6407 . . 3 (𝐴N𝐴 ∈ ω)
2 pinn 6407 . . 3 (𝐵N𝐵 ∈ ω)
3 nntri2 6073 . . 3 ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴𝐵 ↔ ¬ (𝐴 = 𝐵𝐵𝐴)))
41, 2, 3syl2an 273 . 2 ((𝐴N𝐵N) → (𝐴𝐵 ↔ ¬ (𝐴 = 𝐵𝐵𝐴)))
5 ltpiord 6417 . 2 ((𝐴N𝐵N) → (𝐴 <N 𝐵𝐴𝐵))
6 ltpiord 6417 . . . . 5 ((𝐵N𝐴N) → (𝐵 <N 𝐴𝐵𝐴))
76ancoms 255 . . . 4 ((𝐴N𝐵N) → (𝐵 <N 𝐴𝐵𝐴))
87orbi2d 704 . . 3 ((𝐴N𝐵N) → ((𝐴 = 𝐵𝐵 <N 𝐴) ↔ (𝐴 = 𝐵𝐵𝐴)))
98notbid 592 . 2 ((𝐴N𝐵N) → (¬ (𝐴 = 𝐵𝐵 <N 𝐴) ↔ ¬ (𝐴 = 𝐵𝐵𝐴)))
104, 5, 93bitr4d 209 1 ((𝐴N𝐵N) → (𝐴 <N 𝐵 ↔ ¬ (𝐴 = 𝐵𝐵 <N 𝐴)))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 629   = wceq 1243   ∈ wcel 1393   class class class wbr 3764  ωcom 4313  Ncnpi 6370
 Copyright terms: Public domain W3C validator