Grace/Cumulus/Int/OrderMul.g17

Open in Workbench Download source

Imports

Order

Declarations

Source

1-- Multiplication and the order of the integers: signs of products,2-- cancellation, and squares3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Int.OrderMul9import Order1011theorem integerLe.mul_nonneg (x y : Integer)12  requires first : 0 ≤ x13  requires second : 0 ≤ y14  shows 0 ≤ x * y15proof16  have xNonnegative := integerLe.zero_iff.forward with first17  have yNonnegative := integerLe.zero_iff.forward with second18  apply integerLe.zero_iff.backward19  exact IntegerNonnegative.mul with xNonnegative, yNonnegative2021theorem integerLess.mul_positive (x y : Integer)22  requires first : 0 < x23  requires second : 0 < y24  shows 0 < x * y25proof26  have xPositive := integerLess.zero_iff_positive.forward with first27  have yPositive := integerLess.zero_iff_positive.forward with second28  apply integerLess.zero_iff_positive.backward29  exact IntegerPositive.mul with xPositive, yPositive3031theorem integerLe.mul_left (x y k : Integer)32  requires nonnegative : 0 ≤ k33  requires below : x ≤ y34  shows k * x ≤ k * y35proof36  have difference := integerLe.sub_nonneg_iff.forward with below37  have product := integerLe.mul_nonneg with nonnegative, difference38  have shape : k * y - k * x = k * (y - x) by ring39  apply integerLe.sub_nonneg_iff.backward40  rw shape41  exact product4243theorem integerLe.mul_right (x y k : Integer)44  requires nonnegative : 0 ≤ k45  requires below : x ≤ y46  shows x * k ≤ y * k47proof48  have scaled := integerLe.mul_left with nonnegative, below49  have left : k * x = x * k by ring50  have right : k * y = y * k by ring51  rw [left, right] at scaled52  exact scaled5354theorem integerLess.mul_left (x y k : Integer)55  requires positive : 0 < k56  requires below : x < y57  shows k * x < k * y58proof59  have difference := integerLess.sub_positive_iff.forward with below60  have product := integerLess.mul_positive with positive, difference61  have shape : k * y - k * x = k * (y - x) by ring62  apply integerLess.sub_positive_iff.backward63  rw shape64  exact product6566theorem integerLess.mul_right (x y k : Integer)67  requires positive : 0 < k68  requires below : x < y69  shows x * k < y * k70proof71  have scaled := integerLess.mul_left with positive, below72  have left : k * x = x * k by ring73  have right : k * y = y * k by ring74  rw [left, right] at scaled75  exact scaled7677theorem integerLe.mul (a b c d : Integer)78  requires aNonnegative : 0 ≤ a79  requires first : a ≤ b80  requires cNonnegative : 0 ≤ c81  requires second : c ≤ d82  shows a * c ≤ b * d83proof84  have dNonnegative := integerLe.transitive with cNonnegative, second85  have left := integerLe.mul_left at c, d, a with aNonnegative, second86  have right := integerLe.mul_right at a, b, d with dNonnegative, first87  exact integerLe.transitive with left, right8889theorem integerLe.mul_nonpos (x y : Integer)90  requires nonpositive : x ≤ 091  requires nonnegative : 0 ≤ y92  shows x * y ≤ 093proof94  have negated := integerLe.neg_nonneg_iff.backward with nonpositive95  have product := integerLe.mul_nonneg with negated, nonnegative96  have shape : (-x) * y = -(x * y) by ring97  rw shape at product98  exact integerLe.neg_nonneg_iff.forward with product99100theorem integerLe.mul_nonpos_right (x y : Integer)101  requires nonnegative : 0 ≤ x102  requires nonpositive : y ≤ 0103  shows x * y ≤ 0104proof105  have swapped := integerLe.mul_nonpos with nonpositive, nonnegative106  have shape : y * x = x * y by ring107  rw shape at swapped108  exact swapped109110theorem integerLe.mul_nonpos_nonpos (x y : Integer)111  requires first : x ≤ 0112  requires second : y ≤ 0113  shows 0 ≤ x * y114proof115  have xNegated := integerLe.neg_nonneg_iff.backward with first116  have yNegated := integerLe.neg_nonneg_iff.backward with second117  have product := integerLe.mul_nonneg with xNegated, yNegated118  have shape : (-x) * (-y) = x * y by ring119  rw shape at product120  exact product121122theorem integerLess.mul_negative (x y : Integer)123  requires positive : 0 < x124  requires negative : y < 0125  shows x * y < 0126proof127  have negated := integerLess.neg.forward with negative128  have zero : -integerZero = 0129    ring130  rw zero at negated131  have product := integerLess.mul_positive with positive, negated132  have shape : x * (-y) = -(x * y) by ring133  rw shape at product134  have flipped := integerLess.neg at x * y, integerZero135  rw zero at flipped136  exact flipped.backward with product137138theorem integerLess.mul_negative_negative (x y : Integer)139  requires first : x < 0140  requires second : y < 0141  shows 0 < x * y142proof143  have zero : -integerZero = 0 by ring144  have xNegated := integerLess.neg.forward with first145  have yNegated := integerLess.neg.forward with second146  rw zero at xNegated147  rw zero at yNegated148  have product := integerLess.mul_positive with xNegated, yNegated149  have shape : (-x) * (-y) = x * y by ring150  rw shape at product151  exact product152153theorem integerLe.square_nonneg (x : Integer)154  shows 0 ≤ x * x155proof156  have split := integerLe.cases_sign at x157  cases split with nonnegative | nonpositive158  . exact integerLe.mul_nonneg with nonnegative, nonnegative159  . exact integerLe.mul_nonpos_nonpos with nonpositive, nonpositive160161theorem integerMulValue.eq_zero (x y : Integer)162  requires zero : x * y = 0163  shows x = 0 ∨ y = 0164proof165  have xNat := integerNatAbs.natural at x166  have yNat := integerNatAbs.natural at y167  have magnitudes := integerNatAbs.mul at x, y168  rw zero at magnitudes169  have vanish := integerNatAbs.zero170  rw vanish at magnitudes171  symm at magnitudes172  have split := mul.eq_zero_iff.forward with magnitudes173  cases split with xZero | yZero174  . left175    exact integerNatAbs.zero_iff.forward with xZero176  . right177    exact integerNatAbs.zero_iff.forward with yZero178179theorem integerMulValue.eq_zero_iff (x y : Integer)180  shows x * y = 0 ↔ x = 0 ∨ y = 0181proof182  constructor183  . intro zero184    exact integerMulValue.eq_zero with zero185  . intro split186    cases split with xZero | yZero187    . rw xZero188      ring189    . rw yZero190      ring191192theorem integerMulValue.nonzero (x y : Integer)193  requires first : x ≠ 0194  requires second : y ≠ 0195  shows x * y ≠ 0196proof197  intro zero198  have split := integerMulValue.eq_zero with zero199  cases split with xZero | yZero200  . exact first with xZero201  . exact second with yZero202203theorem integerMulValue.square_eq_zero (x : Integer)204  requires zero : x * x = 0205  shows x = 0206proof207  have split := integerMulValue.eq_zero with zero208  cases split with first | second209  . exact first210  . exact second211212theorem integerMulValue.square_eq_zero_iff (x : Integer)213  shows x * x = 0 ↔ x = 0214proof215  constructor216  . intro zero217    exact integerMulValue.square_eq_zero with zero218  . intro zero219    rw zero220    ring221222theorem integerLess.square_positive (x : Integer)223  requires nonzero : x ≠ 0224  shows 0 < x * x225proof226  have nonnegative := integerLe.square_nonneg at x227  have distinct : 0 ≠ x * x228    intro zero229    symm at zero230    have same := integerMulValue.square_eq_zero with zero231    exact nonzero with same232  exact integerLess.of_le_ne with nonnegative, distinct233234theorem integerMulValue.left_cancel (x y k : Integer)235  requires nonzero : k ≠ 0236  requires same : k * x = k * y237  shows x = y238proof239  have product : k * (x - y) = 0240    have shape : k * (x - y) = k * x - k * y by ring241    rw [shape, same]242    ring243  have split := integerMulValue.eq_zero with product244  cases split with kZero | difference245  . exfalso246    exact nonzero with kZero247  . linear_combination difference248249theorem integerMulValue.right_cancel (x y k : Integer)250  requires nonzero : k ≠ 0251  requires same : x * k = y * k252  shows x = y253proof254  have left : x * k = k * x by ring255  have right : y * k = k * y by ring256  rw [left, right] at same257  exact integerMulValue.left_cancel with nonzero, same258259theorem integerLe.mul_left_cancel (x y k : Integer)260  requires positive : 0 < k261  requires below : k * x ≤ k * y262  shows x ≤ y263proof264  apply integerLe.of_not_less265  intro above266  have scaled := integerLess.mul_left at y, x, k with positive, above267  exact integerLe.not_less with below, scaled268269theorem integerLe.mul_right_cancel (x y k : Integer)270  requires positive : 0 < k271  requires below : x * k ≤ y * k272  shows x ≤ y273proof274  have left : x * k = k * x by ring275  have right : y * k = k * y by ring276  rw [left, right] at below277  exact integerLe.mul_left_cancel with positive, below278279theorem integerLess.mul_left_cancel (x y k : Integer)280  requires positive : 0 < k281  requires below : k * x < k * y282  shows x < y283proof284  apply integerLess.of_not_le285  intro above286  have weak := integerLess.implies_le with positive287  have scaled := integerLe.mul_left at y, x, k with weak, above288  exact integerLess.not_le with below, scaled289290theorem integerLess.mul_right_cancel (x y k : Integer)291  requires positive : 0 < k292  requires below : x * k < y * k293  shows x < y294proof295  have left : x * k = k * x by ring296  have right : y * k = k * y by ring297  rw [left, right] at below298  exact integerLess.mul_left_cancel with positive, below299300theorem integerLe.sum_squares_eq_zero (x y : Integer)301  requires zero : x * x + y * y = 0302  shows x = 0 ∧ y = 0303proof304  have xSquare := integerLe.square_nonneg at x305  have ySquare := integerLe.square_nonneg at y306  have xZero : x * x = 0307    have upper : x * x ≤ 0308      have shape : x * x = 0 - y * y by linear_combination zero309      rw shape310      have flipped := integerLe.neg_nonneg_iff.forward at y * y311      have negShape : -(y * y) = 0 - y * y by ring312      rw negShape at flipped313      have negated := integerLe.neg.forward with ySquare314      have zeroNeg : -integerZero = 0 by ring315      rw [zeroNeg, negShape] at negated316      exact negated317    exact integerLe.antisymmetric with upper, xSquare318  have yZero : y * y = 0 by linear_combination zero - xZero319  constructor320  . exact integerMulValue.square_eq_zero with xZero321  . exact integerMulValue.square_eq_zero with yZero322323theorem integerLe.le_square (x : Integer)324  shows x ≤ x * x325proof326  have split := integerLe.cases_sign at x327  cases split with nonnegative | nonpositive328  . have cases := integerLe.cases with nonnegative329    cases cases with positive | zero330    . have one := integerLess.one_le_of_positive with positive331      have scaled :=332        integerLe.mul_left at integerOne, x, x with nonnegative, one333      have unit : x * 1 = x by ring334      rw unit at scaled335      exact scaled336    . rw ← zero337      have vanish : integerZero * 0 = 0 by ring338      rw vanish339      exact integerLe.reflexive with *340  . have square := integerLe.square_nonneg at x341    exact integerLe.transitive with nonpositive, square342343theorem integerLess.of_one_le (x : Integer)344  requires one : 1 ≤ x345  shows 0 < x346proof347  unfold integerLess348  have shape : integerZero + 1 = integerOne by ring349  rw shape350  exact one351352theorem integerLess.positive_iff_one_le (x : Integer)353  shows 0 < x ↔ 1 ≤ x354proof355  constructor356  . intro positive357    exact integerLess.one_le_of_positive with positive358  . intro one359    exact integerLess.of_one_le with one360