Reference · Signed rationals

rainbow.math.rational.signed.reciprocal-antitone

Signed rationalssrc/rainbow/math/rational/signed/reciprocal_antitone.clj0 definitions, 3 theorems

B4 of the limit-reciprocal arc: reciprocal reverses order on positives, plus the two reusable order<->subtract-nonneg bridges it needs. signed/nonnegative-subtract-of-at-most : x <= y -> nonnegative (y - x) signed/at-most-of-nonnegative-subtract : nonnegative (a - b) -> b <= a signed/reciprocal-antitone : nonnegative x -> 1<=num(mag(x*x)) -> 1<=num(mag(y*y)) -> x <= y -> reciprocal y <= reciprocal x The antitone proof REUSES the reciprocal-difference identity (b106532): recip x - recip y ~ (recip x * recip y) * (y - x), whose RHS is >= 0 (product of nonnegatives: reciprocal-nonnegative twice + the y-x bridge), so recip x - recip y >= 0, i.e. recip y <= recip x. Everything is done through `0 <= .` (signed at-most zero), since signed/nonnegative-respects-equivalence is absent. Axiom-free; additive; does not touch the LP checker.

Depends onmath.rational.signed.reciprocal-differencemath.rational.signed.reciprocal-nonnegativemath.rational.signed.multiply-ordermath.rational.signed.order-monotonemath.rational.signed.order-transitivitymath.rational.signed.order-respectsmath.rational.signed.unit-lawsmath.rational.signed.recovery-laws

signed/nonnegative-subtract-of-at-most :
  (x y : ℚ)
  (hxy : x ≤ y)
  → signed/nonnegative (y - x)

signed/at-most-of-nonnegative-subtract :
  (a b : ℚ) (h : signed/nonnegative (a - b))
  → b ≤ a

signed/reciprocal-antitone :
  (x y : ℚ) (hx : signed/nonnegative x)
  (hx0 : 1 ≤ nnrat/numerator (signed/magnitude (x · x)))
  (hy0 : 1 ≤ nnrat/numerator (signed/magnitude (y · y)))
  (hxy : x ≤ y)
  → signed/reciprocal y ≤ signed/reciprocal x