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

Theorem ltmnqi 7231
 Description: Ordering property of multiplication for positive fractions. One direction of ltmnqg 7229. (Contributed by Jim Kingdon, 9-Dec-2019.)
Assertion
Ref Expression
ltmnqi ((𝐴 <Q 𝐵𝐶Q) → (𝐶 ·Q 𝐴) <Q (𝐶 ·Q 𝐵))

Proof of Theorem ltmnqi
StepHypRef Expression
1 simpl 108 . 2 ((𝐴 <Q 𝐵𝐶Q) → 𝐴 <Q 𝐵)
2 ltrelnq 7193 . . . 4 <Q ⊆ (Q × Q)
32brel 4595 . . 3 (𝐴 <Q 𝐵 → (𝐴Q𝐵Q))
4 ltmnqg 7229 . . . 4 ((𝐴Q𝐵Q𝐶Q) → (𝐴 <Q 𝐵 ↔ (𝐶 ·Q 𝐴) <Q (𝐶 ·Q 𝐵)))
543expa 1182 . . 3 (((𝐴Q𝐵Q) ∧ 𝐶Q) → (𝐴 <Q 𝐵 ↔ (𝐶 ·Q 𝐴) <Q (𝐶 ·Q 𝐵)))
63, 5sylan 281 . 2 ((𝐴 <Q 𝐵𝐶Q) → (𝐴 <Q 𝐵 ↔ (𝐶 ·Q 𝐴) <Q (𝐶 ·Q 𝐵)))
71, 6mpbid 146 1 ((𝐴 <Q 𝐵𝐶Q) → (𝐶 ·Q 𝐴) <Q (𝐶 ·Q 𝐵))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∈ wcel 1481   class class class wbr 3933  (class class class)co 5778  Qcnq 7108   ·Q cmq 7111
 Copyright terms: Public domain W3C validator