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

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

Proof of Theorem ltnnnq
StepHypRef Expression
1 simpl 106 . . 3 ((𝐴N𝐵N) → 𝐴N)
2 1pi 6470 . . . 4 1𝑜N
32a1i 9 . . 3 ((𝐴N𝐵N) → 1𝑜N)
4 simpr 107 . . 3 ((𝐴N𝐵N) → 𝐵N)
5 ordpipqqs 6529 . . 3 (((𝐴N ∧ 1𝑜N) ∧ (𝐵N ∧ 1𝑜N)) → ([⟨𝐴, 1𝑜⟩] ~Q <Q [⟨𝐵, 1𝑜⟩] ~Q ↔ (𝐴 ·N 1𝑜) <N (1𝑜 ·N 𝐵)))
61, 3, 4, 3, 5syl22anc 1147 . 2 ((𝐴N𝐵N) → ([⟨𝐴, 1𝑜⟩] ~Q <Q [⟨𝐵, 1𝑜⟩] ~Q ↔ (𝐴 ·N 1𝑜) <N (1𝑜 ·N 𝐵)))
7 mulidpi 6473 . . . 4 (𝐴N → (𝐴 ·N 1𝑜) = 𝐴)
81, 7syl 14 . . 3 ((𝐴N𝐵N) → (𝐴 ·N 1𝑜) = 𝐴)
9 mulcompig 6486 . . . . 5 ((1𝑜N𝐵N) → (1𝑜 ·N 𝐵) = (𝐵 ·N 1𝑜))
102, 4, 9sylancr 399 . . . 4 ((𝐴N𝐵N) → (1𝑜 ·N 𝐵) = (𝐵 ·N 1𝑜))
11 mulidpi 6473 . . . . 5 (𝐵N → (𝐵 ·N 1𝑜) = 𝐵)
124, 11syl 14 . . . 4 ((𝐴N𝐵N) → (𝐵 ·N 1𝑜) = 𝐵)
1310, 12eqtrd 2088 . . 3 ((𝐴N𝐵N) → (1𝑜 ·N 𝐵) = 𝐵)
148, 13breq12d 3804 . 2 ((𝐴N𝐵N) → ((𝐴 ·N 1𝑜) <N (1𝑜 ·N 𝐵) ↔ 𝐴 <N 𝐵))
156, 14bitr2d 182 1 ((𝐴N𝐵N) → (𝐴 <N 𝐵 ↔ [⟨𝐴, 1𝑜⟩] ~Q <Q [⟨𝐵, 1𝑜⟩] ~Q ))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ↔ wb 102   = wceq 1259   ∈ wcel 1409  ⟨cop 3405   class class class wbr 3791  (class class class)co 5539  1𝑜c1o 6024  [cec 6134  Ncnpi 6427   ·N cmi 6429
 Copyright terms: Public domain W3C validator