Reference · Signed rationals

rainbow.math.rational.signed.product-radius-positive

Signed rationalssrc/rainbow/math/rational/signed/product_radius_positive.clj0 definitions, 1 theorems

Second sub-proof of the limit-product modulus assembly: the magnitude of the radius base V = (1+|L|)+|M| has a positive numerator, so nnrat/make-succ-of-positive-numerator and analysis/nnrat-radius-cancel apply to it. Axiom-free; additive. analysis/product-radius-numerator-positive : forall L M, nat/at-most (succ zero) (nnrat/numerator (signed/magnitude (sadd (sadd one (abs L)) (abs M)))) Chain: 1<=V (signed, via add-monotone + add-zero-right) -> rewrite V ~ from-nnrat(mag V) (from-nnrat-magnitude + product-radius-nonneg) -> 1 <= from-nnrat(mag V) [signed/one =def= from-nnrat nnrat/one] -> nnrat/at-most nnrat/one (mag V) (from-nnrat-at-most-reverse) -> base-at-most (at-most-to-cross) -> den(mag) <= num(mag) (rewrite the *1 factors) -> 1 <= den(mag) (witness) -> 1 <= num(mag) (nat at-most transitive).

Depends onmath.rational.signed.product-radius-nonnegmath.rational.signed.magnitudemath.rational.nnrat.order-equivalencemath.rational.signed.geometric-bridgemath.rational.signed.vector-sup-trianglemath.rational.signed.distance-triangle

analysis/product-radius-numerator-positive :
  (L M : ℚ)
  → 1 ≤ nnrat/numerator (signed/magnitude (1 + signed/absolute L + signed/absolute M))