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

Theorem ltnnnq 7238
 Description: Ordering of positive integers via
Assertion
Ref Expression
ltnnnq ((𝐴N𝐵N) → (𝐴 <N 𝐵 ↔ [⟨𝐴, 1o⟩] ~Q <Q [⟨𝐵, 1o⟩] ~Q ))

Proof of Theorem ltnnnq
StepHypRef Expression
1 simpl 108 . . 3 ((𝐴N𝐵N) → 𝐴N)
2 1pi 7130 . . . 4 1oN
32a1i 9 . . 3 ((𝐴N𝐵N) → 1oN)
4 simpr 109 . . 3 ((𝐴N𝐵N) → 𝐵N)
5 ordpipqqs 7189 . . 3 (((𝐴N ∧ 1oN) ∧ (𝐵N ∧ 1oN)) → ([⟨𝐴, 1o⟩] ~Q <Q [⟨𝐵, 1o⟩] ~Q ↔ (𝐴 ·N 1o) <N (1o ·N 𝐵)))
61, 3, 4, 3, 5syl22anc 1217 . 2 ((𝐴N𝐵N) → ([⟨𝐴, 1o⟩] ~Q <Q [⟨𝐵, 1o⟩] ~Q ↔ (𝐴 ·N 1o) <N (1o ·N 𝐵)))
7 mulidpi 7133 . . . 4 (𝐴N → (𝐴 ·N 1o) = 𝐴)
81, 7syl 14 . . 3 ((𝐴N𝐵N) → (𝐴 ·N 1o) = 𝐴)
9 mulcompig 7146 . . . . 5 ((1oN𝐵N) → (1o ·N 𝐵) = (𝐵 ·N 1o))
102, 4, 9sylancr 410 . . . 4 ((𝐴N𝐵N) → (1o ·N 𝐵) = (𝐵 ·N 1o))
11 mulidpi 7133 . . . . 5 (𝐵N → (𝐵 ·N 1o) = 𝐵)
124, 11syl 14 . . . 4 ((𝐴N𝐵N) → (𝐵 ·N 1o) = 𝐵)
1310, 12eqtrd 2172 . . 3 ((𝐴N𝐵N) → (1o ·N 𝐵) = 𝐵)
148, 13breq12d 3942 . 2 ((𝐴N𝐵N) → ((𝐴 ·N 1o) <N (1o ·N 𝐵) ↔ 𝐴 <N 𝐵))
156, 14bitr2d 188 1 ((𝐴N𝐵N) → (𝐴 <N 𝐵 ↔ [⟨𝐴, 1o⟩] ~Q <Q [⟨𝐵, 1o⟩] ~Q ))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1331   ∈ wcel 1480  ⟨cop 3530   class class class wbr 3929  (class class class)co 5774  1oc1o 6306  [cec 6427  Ncnpi 7087   ·N cmi 7089
 Copyright terms: Public domain W3C validator