Grace/Cumulus/Algebra/OrderedField/Core.g17

Open in Workbench Download source

Imports

Defs

Declarations

Source

1-- Core ordered-field theory2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Algebra.OrderedField.Core8import Defs910theorem IsOrderedField.field (A add zero neg mul one inv lt : Set)11  requires h : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)12  shows IsFieldWithInverse(A, add, zero, neg, mul, one, inv)13proof14  simp [IsOrderedField]1516theorem IsOrderedField.strict_linear_order (A add zero neg mul one inv lt : Set)17  requires h : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)18  shows StrictLinearOrder(A, lt)19proof20  simp [IsOrderedField]2122theorem IsOrderedField.add_strict_mono (A add zero neg mul one inv lt : Set)23  requires h : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)24  shows AddStrictMono(A, add, lt)25proof26  simp [IsOrderedField]2728theorem IsOrderedField.mul_positive (A add zero neg mul one inv lt : Set)29  requires h : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)30  shows MulPositive(A, mul, zero, lt)31proof32  simp [IsOrderedField]3334theorem IsOrderedField.comm_ring (A add zero neg mul one inv lt : Set)35  requires h : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)36  shows IsCommRing(A, add, zero, neg, mul, one)37proof38  have field := IsOrderedField.field with h39  exact IsFieldWithInverse.comm_ring with field4041theorem IsOrderedField.order (A add zero neg mul one inv lt : Set)42  requires h : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)43  shows StrictOrder(A, lt)44proof45  have linear := IsOrderedField.strict_linear_order with h46  exact StrictLinearOrder.strict with linear4748theorem IsOrderedField.connected (A add zero neg mul one inv lt : Set)49  requires h : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)50  shows ConnectedOn(A, lt)51proof52  have linear := IsOrderedField.strict_linear_order with h53  exact StrictLinearOrder.connected with linear5455theorem IsOrderedField.nontrivial (A add zero neg mul one inv lt : Set)56  requires h : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)57  shows Nontrivial(A, zero, one)58proof59  have field := IsOrderedField.field with h60  exact IsFieldWithInverse.nontrivial with field6162theorem IsOrderedField.add_right (A add zero neg mul one inv lt x y z : Set)63  requires h : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)64  requires hx : x ∈ A65  requires hy : y ∈ A66  requires hz : z ∈ A67  requires hxy : relates(lt, x, y)68  shows relates(lt, call2(add, x, z), call2(add, y, z))69proof70  exact IsOrderedField.add_strict_mono with h, x, hx, y, hy, z, hz, hxy7172theorem IsOrderedField.add_left (A add zero neg mul one inv lt x y z : Set)73  requires field : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)74  requires xInA : x ∈ A75  requires yInA : y ∈ A76  requires zInA : z ∈ A77  requires less : relates(lt, x, y)78  shows relates(lt, call2(add, z, x), call2(add, z, y))79proof80  have translated := IsOrderedField.add_right with field, xInA, yInA, zInA, less81  have ring := IsOrderedField.comm_ring with field82  have commutative := IsCommRing.add_commutative with ring83  have left := commutative with x, xInA, z, zInA84  have right := commutative with y, yInA, z, zInA85  rwa [left, right] at translated8687theorem IsOrderedField.add (A add zero neg mul one inv lt x y z w : Set)88  requires field : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)89  requires xInA : x ∈ A90  requires yInA : y ∈ A91  requires zInA : z ∈ A92  requires wInA : w ∈ A93  requires xy : relates(lt, x, y)94  requires zw : relates(lt, z, w)95  shows relates(lt, call2(add, x, z), call2(add, y, w))96proof97  have commRing := IsOrderedField.comm_ring with field98  have ring := IsCommRing.ring with commRing99  have xzInA := IsRing.add_closed with ring, xInA, zInA100  have yzInA := IsRing.add_closed with ring, yInA, zInA101  have ywInA := IsRing.add_closed with ring, yInA, wInA102  have first := IsOrderedField.add_right with field, xInA, yInA, zInA, xy103  have second := IsOrderedField.add_left with field, zInA, wInA, yInA, zw104  have order := IsOrderedField.order with field105  have transitive := StrictOrder.transitive with order106  exact transitive with107    call2(add, x, z), xzInA,108    call2(add, y, z), yzInA,109    call2(add, y, w), ywInA, first, second110111theorem IsOrderedField.transitive (A add zero neg mul one inv lt x y z : Set)112  requires field : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)113  requires xInA : x ∈ A114  requires yInA : y ∈ A115  requires zInA : z ∈ A116  requires xy : relates(lt, x, y)117  requires yz : relates(lt, y, z)118  shows relates(lt, x, z)119proof120  have order := IsOrderedField.order with field121  have transitive := StrictOrder.transitive with order122  exact transitive with x, xInA, y, yInA, z, zInA, xy, yz123124theorem IsOrderedField.irreflexive (A add zero neg mul one inv lt x : Set)125  requires field : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)126  requires xInA : x ∈ A127  shows ¬relates(lt, x, x)128proof129  have order := IsOrderedField.order with field130  have irreflexive := StrictOrder.irreflexive with order131  exact irreflexive with x, xInA132133theorem IsOrderedField.add_right_iff (A add zero neg mul one inv lt x y z : Set)134  requires field : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)135  requires xInA : x ∈ A136  requires yInA : y ∈ A137  requires zInA : z ∈ A138  shows relates(lt, call2(add, x, z), call2(add, y, z)) ↔139    relates(lt, x, y)140proof141  have commRing := IsOrderedField.comm_ring with field142  have ring := IsCommRing.ring with commRing143  have negZInA := IsRing.neg_closed with ring, zInA144  have xzInA := IsRing.add_closed with ring, xInA, zInA145  have yzInA := IsRing.add_closed with ring, yInA, zInA146  have associative := IsRing.add_associative with ring147  have inverseZ := IsRing.add_inverse_right with ring, zInA148  have identityX := IsRing.add_right_identity with ring, xInA149  have identityY := IsRing.add_right_identity with ring, yInA150  constructor151  . intro translated152    have cancelled := IsOrderedField.add_right with field, xzInA, yzInA, negZInA, translated153    have associateX := Associative.law with associative, xInA, zInA, negZInA154    have associateY := Associative.law with associative, yInA, zInA, negZInA155    rwa [associateX, associateY, inverseZ, identityX, identityY] at cancelled156  . intro less157    exact IsOrderedField.add_right with field, xInA, yInA, zInA, less158159theorem IsOrderedField.add_left_iff (A add zero neg mul one inv lt x y z : Set)160  requires field : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)161  requires xInA : x ∈ A162  requires yInA : y ∈ A163  requires zInA : z ∈ A164  shows relates(lt, call2(add, z, x), call2(add, z, y)) ↔165    relates(lt, x, y)166proof167  have ring := IsOrderedField.comm_ring with field168  have commutative := IsCommRing.add_commutative with ring169  have left := commutative with z, zInA, x, xInA170  have right := commutative with z, zInA, y, yInA171  rw [left, right]172  exact IsOrderedField.add_right_iff with field, xInA, yInA, zInA173174theorem IsOrderedField.positive_sum (A add zero neg mul one inv lt x y : Set)175  requires field : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)176  requires xInA : x ∈ A177  requires yInA : y ∈ A178  requires positiveX : relates(lt, zero, x)179  requires positiveY : relates(lt, zero, y)180  shows relates(lt, zero, call2(add, x, y))181proof182  have commRing := IsOrderedField.comm_ring with field183  have ring := IsCommRing.ring with commRing184  have zeroInA := IsRing.zero_in_carrier with ring185  have sumInA := IsRing.add_closed with ring, xInA, yInA186  have xLessSum := IsOrderedField.add_left with field, zeroInA, yInA, xInA, positiveY187  have identityX := IsRing.add_right_identity with ring, xInA188  rw identityX at xLessSum189  exact IsOrderedField.transitive with field, zeroInA, xInA, sumInA, positiveX, xLessSum190191theorem IsOrderedField.ne_of_less (A add zero neg mul one inv lt x y : Set)192  requires field : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)193  requires xInA : x ∈ A194  requires yInA : y ∈ A195  requires less : relates(lt, x, y)196  shows x ≠ y197proof198  intro equal199  rw equal at less200  exact IsOrderedField.irreflexive with field, yInA, less201202theorem IsOrderedField.positive_neg_of_negative (A add zero neg mul one inv lt x : Set)203  requires field : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)204  requires xInA : x ∈ A205  requires negative : relates(lt, x, zero)206  shows relates(lt, zero, neg(x))207proof208  have commRing := IsOrderedField.comm_ring with field209  have ring := IsCommRing.ring with commRing210  have zeroInA := IsRing.zero_in_carrier with ring211  have negXInA := IsRing.neg_closed with ring, xInA212  have translated := IsOrderedField.add_right with field, xInA, zeroInA, negXInA, negative213  have inverse := IsRing.add_inverse_right with ring, xInA214  have identity := IsRing.add_left_identity with ring, negXInA215  rwa [inverse, identity] at translated216217theorem IsOrderedField.negative_neg_of_positive (A add zero neg mul one inv lt x : Set)218  requires field : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)219  requires xInA : x ∈ A220  requires positive : relates(lt, zero, x)221  shows relates(lt, neg(x), zero)222proof223  have commRing := IsOrderedField.comm_ring with field224  have ring := IsCommRing.ring with commRing225  have zeroInA := IsRing.zero_in_carrier with ring226  have negXInA := IsRing.neg_closed with ring, xInA227  have translated := IsOrderedField.add_right with field, zeroInA, xInA, negXInA, positive228  have identity := IsRing.add_left_identity with ring, negXInA229  have inverse := IsRing.add_inverse_right with ring, xInA230  rwa [identity, inverse] at translated231232theorem IsOrderedField.neg_reverses (A add zero neg mul one inv lt x y : Set)233  requires field : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)234  requires xInA : x ∈ A235  requires yInA : y ∈ A236  requires less : relates(lt, x, y)237  shows relates(lt, neg(y), neg(x))238proof239  have commRing := IsOrderedField.comm_ring with field240  have ring := IsCommRing.ring with commRing241  have zeroInA := IsRing.zero_in_carrier with ring242  have negXInA := IsRing.neg_closed with ring, xInA243  have negYInA := IsRing.neg_closed with ring, yInA244  have differencePositive := IsOrderedField.add_right with field, xInA, yInA, negXInA, less245  have inverseX := IsRing.add_inverse_right with ring, xInA246  rw inverseX at differencePositive247  have commutative := IsCommRing.add_commutative with commRing248  have differenceCommutes := commutative with y, yInA, neg(x), negXInA249  rw differenceCommutes at differencePositive250  have inverseY := IsRing.add_inverse_left with ring, yInA251  have translated : relates(lt,252      call2(add, neg(y), y),253      call2(add, neg(x), y))254    rwa inverseY255  have cancellation := IsOrderedField.add_right_iff with field, negYInA, negXInA, yInA256  exact cancellation.forward with translated257258theorem IsOrderedField.sign_cases (A add zero neg mul one inv lt x : Set)259  requires field : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)260  requires xInA : x ∈ A261  shows x = zero ∨ relates(lt, x, zero) ∨ relates(lt, zero, x)262proof263  have commRing := IsOrderedField.comm_ring with field264  have ring := IsCommRing.ring with commRing265  have zeroInA := IsRing.zero_in_carrier with ring266  have equalityCases : x = zero ∨ x ≠ zero by tauto267  cases equalityCases with equal | unequal268  . left269    exact equal270  . have connected := IsOrderedField.connected at271      A, add, zero, neg, mul, one, inv, lt with field272    have signs := connected with x, xInA, zero, zeroInA, unequal273    cases signs with negative | positive274    . right275      left276      exact negative277    . right278      right279      exact positive280281theorem LessEqualBy.reflexive (A lt x : Set)282  requires xInA : x ∈ A283  shows LessEqualBy(A, lt, x, x)284proof285  unfold LessEqualBy286  refine ⟨xInA, xInA, _⟩287  left288  rfl289290theorem LessEqualBy.of_less (A lt x y : Set)291  requires xInA : x ∈ A292  requires yInA : y ∈ A293  requires less : relates(lt, x, y)294  shows LessEqualBy(A, lt, x, y)295proof296  unfold LessEqualBy297  refine ⟨xInA, yInA, _⟩298  right299  exact less300301theorem LessEqualBy.transitive (A add zero neg mul one inv lt x y z : Set)302  requires field : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)303  requires xy : LessEqualBy(A, lt, x, y)304  requires yz : LessEqualBy(A, lt, y, z)305  shows LessEqualBy(A, lt, x, z)306proof307  rcases xy with ⟨xInA, yInA, xyOrder⟩308  rcases yz with ⟨yInAAgain, zInA, yzOrder⟩309  unfold LessEqualBy310  refine ⟨xInA, zInA, _⟩311  cases xyOrder with equalXY | lessXY312  . rw equalXY313    exact yzOrder314  . cases yzOrder with equalYZ | lessYZ315    . rw ← equalYZ316      right317      exact lessXY318    . right319      exact IsOrderedField.transitive with field, xInA, yInA, zInA, lessXY,320        lessYZ321322theorem LessEqualBy.add (A add zero neg mul one inv lt x y z w : Set)323  requires field : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)324  requires xy : LessEqualBy(A, lt, x, y)325  requires zw : LessEqualBy(A, lt, z, w)326  shows LessEqualBy(A, lt, call2(add, x, z), call2(add, y, w))327proof328  rcases xy with ⟨xInA, yInA, xyOrder⟩329  rcases zw with ⟨zInA, wInA, zwOrder⟩330  have commRing := IsOrderedField.comm_ring with field331  have ring := IsCommRing.ring with commRing332  have xzInA := IsRing.add_closed with ring, xInA, zInA333  have ywInA := IsRing.add_closed with ring, yInA, wInA334  unfold LessEqualBy335  refine ⟨xzInA, ywInA, _⟩336  cases xyOrder with equalXY | lessXY337  . cases zwOrder with equalZW | lessZW338    . left339      cc340    . right341      rw equalXY342      exact IsOrderedField.add_left with field, zInA, wInA, yInA, lessZW343  . cases zwOrder with equalZW | lessZW344    . right345      rw equalZW346      exact IsOrderedField.add_right with field, xInA, yInA, wInA, lessXY347    . right348      have yzInA := IsRing.add_closed with ring, yInA, zInA349      have first := IsOrderedField.add_right with field, xInA, yInA, zInA,350        lessXY351      have second := IsOrderedField.add_left with field, zInA, wInA, yInA,352        lessZW353      exact IsOrderedField.transitive with field, xzInA, yzInA, ywInA, first, second354355theorem AbsoluteValue.function (A zero neg lt abs : Set)356  requires absolute : AbsoluteValue(A, zero, neg, lt, abs)357  shows abs : A → A358proof359  rcases absolute with ⟨function, atZero, branches⟩360  exact function361362theorem AbsoluteValue.closed (A zero neg lt abs x : Set)363  requires absolute : AbsoluteValue(A, zero, neg, lt, abs)364  requires xInA : x ∈ A365  shows abs(x) ∈ A366proof367  have function := AbsoluteValue.function with absolute368  exact FunctionBetween.apply_closed with function, xInA369370theorem AbsoluteValue.zero (A zero neg lt abs : Set)371  requires absolute : AbsoluteValue(A, zero, neg, lt, abs)372  shows abs(zero) = zero373proof374  rcases absolute with ⟨function, atZero, branches⟩375  exact atZero376377theorem AbsoluteValue.of_positive (A zero neg lt abs x : Set)378  requires absolute : AbsoluteValue(A, zero, neg, lt, abs)379  requires xInA : x ∈ A380  requires positive : relates(lt, zero, x)381  shows abs(x) = x382proof383  rcases absolute with ⟨function, atZero, branches⟩384  obtain ⟨positiveBranch, negativeBranch⟩ := branches with x, xInA385  exact positiveBranch with positive386387theorem AbsoluteValue.of_negative (A zero neg lt abs x : Set)388  requires absolute : AbsoluteValue(A, zero, neg, lt, abs)389  requires xInA : x ∈ A390  requires negative : relates(lt, x, zero)391  shows abs(x) = neg(x)392proof393  rcases absolute with ⟨function, atZero, branches⟩394  obtain ⟨positiveBranch, negativeBranch⟩ := branches with x, xInA395  exact negativeBranch with negative396397theorem AbsoluteValue.nonnegative (A add zero neg mul one inv lt abs x : Set)398  requires field : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)399  requires absolute : AbsoluteValue(A, zero, neg, lt, abs)400  requires xInA : x ∈ A401  shows LessEqualBy(A, lt, zero, abs(x))402proof403  have commRing := IsOrderedField.comm_ring with field404  have ring := IsCommRing.ring with commRing405  have zeroInA := IsRing.zero_in_carrier with ring406  have absoluteInA := AbsoluteValue.closed with absolute, xInA407  unfold LessEqualBy408  refine ⟨zeroInA, absoluteInA, _⟩409  have signs := IsOrderedField.sign_cases with field, xInA410  cases signs with equal | nonzero411  . left412    have atZero := AbsoluteValue.zero with absolute413    cc414  . cases nonzero with negative | positive415    . right416      have positiveNeg := IsOrderedField.positive_neg_of_negative with field, xInA, negative417      have shape := AbsoluteValue.of_negative with absolute, xInA, negative418      rwa shape419    . right420      have shape := AbsoluteValue.of_positive with absolute, xInA, positive421      rwa shape422423theorem AbsoluteValue.positive_of_ne (A add zero neg mul one inv lt abs x : Set)424  requires field : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)425  requires absolute : AbsoluteValue(A, zero, neg, lt, abs)426  requires xInA : x ∈ A427  requires nonzero : x ≠ zero428  shows relates(lt, zero, abs(x))429proof430  have signs := IsOrderedField.sign_cases with field, xInA431  cases signs with equal | nonzeroSign432  . exfalso433    exact nonzero with equal434  . cases nonzeroSign with negative | positive435    . have positiveNeg := IsOrderedField.positive_neg_of_negative at436        A, add, zero, neg, mul, one, inv, lt, x with437          field, xInA, negative438      have shape := AbsoluteValue.of_negative with absolute, xInA, negative439      rwa shape440    . have shape := AbsoluteValue.of_positive at441        A, zero, neg, lt, abs, x with absolute, xInA, positive442      rwa shape443444theorem AbsoluteValue.eq_zero_iff (A add zero neg mul one inv lt abs x : Set)445  requires field : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)446  requires absolute : AbsoluteValue(A, zero, neg, lt, abs)447  requires xInA : x ∈ A448  shows abs(x) = zero ↔ x = zero449proof450  have commRing := IsOrderedField.comm_ring with field451  have ring := IsCommRing.ring with commRing452  have zeroInA := IsRing.zero_in_carrier with ring453  constructor454  . intro absoluteZero455    have signs := IsOrderedField.sign_cases with field, xInA456    cases signs with equal | nonzero457    . exact equal458    . cases nonzero with negative | positive459      . have shape := AbsoluteValue.of_negative at460          A, zero, neg, lt, abs, x with absolute, xInA, negative461        have negXInA := IsRing.neg_closed with ring, xInA462        have positiveNeg := IsOrderedField.positive_neg_of_negative with field, xInA, negative463        rw shape at absoluteZero464        rw absoluteZero at positiveNeg465        exfalso466        exact IsOrderedField.irreflexive with field, zeroInA, positiveNeg467      . have shape := AbsoluteValue.of_positive at468          A, zero, neg, lt, abs, x with absolute, xInA, positive469        rwa shape at absoluteZero470  . intro equal471    rw equal472    exact AbsoluteValue.zero with absolute473474theorem AbsoluteValue.upper (A add zero neg mul one inv lt abs x : Set)475  requires field : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)476  requires absolute : AbsoluteValue(A, zero, neg, lt, abs)477  requires xInA : x ∈ A478  shows LessEqualBy(A, lt, x, abs(x))479proof480  have commRing := IsOrderedField.comm_ring with field481  have ring := IsCommRing.ring with commRing482  have zeroInA := IsRing.zero_in_carrier with ring483  have absoluteInA := AbsoluteValue.closed with absolute, xInA484  unfold LessEqualBy485  refine ⟨xInA, absoluteInA, _⟩486  have signs := IsOrderedField.sign_cases with field, xInA487  cases signs with equal | nonzero488  . left489    have atZero := AbsoluteValue.zero with absolute490    cc491  . cases nonzero with negative | positive492    . right493      have positiveNeg := IsOrderedField.positive_neg_of_negative with field, xInA, negative494      have negXInA := IsRing.neg_closed with ring, xInA495      have strict := IsOrderedField.transitive with field, xInA, zeroInA, negXInA, negative, positiveNeg496      have shape := AbsoluteValue.of_negative with absolute, xInA, negative497      rwa shape498    . left499      have shape := AbsoluteValue.of_positive with absolute, xInA, positive500      cc501502theorem AbsoluteValue.upper_neg (A add zero neg mul one inv lt abs x : Set)503  requires field : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)504  requires absolute : AbsoluteValue(A, zero, neg, lt, abs)505  requires xInA : x ∈ A506  shows LessEqualBy(A, lt, neg(x), abs(x))507proof508  have commRing := IsOrderedField.comm_ring with field509  have ring := IsCommRing.ring with commRing510  have additive := IsRing.additive with ring511  have group := IsAbelianGroup.group with additive512  have zeroInA := IsRing.zero_in_carrier with ring513  have negXInA := IsRing.neg_closed with ring, xInA514  have absoluteInA := AbsoluteValue.closed with absolute, xInA515  unfold LessEqualBy516  refine ⟨negXInA, absoluteInA, _⟩517  have signs := IsOrderedField.sign_cases with field, xInA518  cases signs with equal | nonzero519  . left520    have negZero := IsGroup.inverse_unit with group521    have atZero := AbsoluteValue.zero with absolute522    cc523  . cases nonzero with negative | positive524    . left525      have shape := AbsoluteValue.of_negative with absolute, xInA, negative526      cc527    . right528      have negativeNeg := IsOrderedField.negative_neg_of_positive with field, xInA, positive529      have strict := IsOrderedField.transitive with field, negXInA, zeroInA, xInA, negativeNeg, positive530      have shape := AbsoluteValue.of_positive with absolute, xInA, positive531      rwa shape532533theorem AbsoluteValue.neg (A add zero neg mul one inv lt abs x : Set)534  requires field : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)535  requires absolute : AbsoluteValue(A, zero, neg, lt, abs)536  requires xInA : x ∈ A537  shows abs(neg(x)) = abs(x)538proof539  have commRing := IsOrderedField.comm_ring with field540  have ring := IsCommRing.ring with commRing541  have additive := IsRing.additive with ring542  have group := IsAbelianGroup.group with additive543  have negXInA := IsRing.neg_closed with ring, xInA544  have involutive := IsGroup.inverse_involutive with group, xInA545  have signs := IsOrderedField.sign_cases with field, xInA546  cases signs with equal | nonzero547  . have negZero := IsGroup.inverse_unit with group548    have atZero := AbsoluteValue.zero with absolute549    cc550  . cases nonzero with negative | positive551    . have positiveNeg := IsOrderedField.positive_neg_of_negative at552        A, add, zero, neg, mul, one, inv, lt, x with553          field, xInA, negative554      have left := AbsoluteValue.of_positive with absolute, negXInA, positiveNeg555      have right := AbsoluteValue.of_negative with absolute, xInA, negative556      cc557    . have negativeNeg := IsOrderedField.negative_neg_of_positive at558        A, add, zero, neg, mul, one, inv, lt, x with559          field, xInA, positive560      have left := AbsoluteValue.of_negative with absolute, negXInA, negativeNeg561      have right := AbsoluteValue.of_positive with absolute, xInA, positive562      cc563564-- Absolute value is multiplicative in every ordered field.  Splitting on565-- the signs of the factors leaves only the positive-product law and the566-- familiar sign rules for multiplication.567theorem AbsoluteValue.mul (A add zero neg mul one inv lt abs x y : Set)568  requires field : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)569  requires absolute : AbsoluteValue(A, zero, neg, lt, abs)570  requires xInA : x ∈ A571  requires yInA : y ∈ A572  shows abs(call2(mul, x, y)) =573    call2(mul, abs(x), abs(y))574proof575  have commRing := IsOrderedField.comm_ring with field576  have ring := IsCommRing.ring with commRing577  have positiveMul := IsOrderedField.mul_positive with field578  have productInA := IsRing.mul_closed with ring, xInA, yInA579  have absXInA := AbsoluteValue.closed with absolute, xInA580  have absYInA := AbsoluteValue.closed with absolute, yInA581  have signsX := IsOrderedField.sign_cases with field, xInA582  cases signsX with xZero | xNonzero583  . have zeroProduct := IsRing.zero_mul at584      A, add, zero, neg, mul, one, y with ring, yInA585    have zeroTimesAbs := IsRing.zero_mul with ring, absYInA586    have absZero := AbsoluteValue.zero with absolute587    rw xZero588    cc589  . cases xNonzero with xNegative | xPositive590    . have negXInA := IsRing.neg_closed at591        A, add, zero, neg, mul, one, x with ring, xInA592      have negXPositive := IsOrderedField.positive_neg_of_negative with field, xInA, xNegative593      have absX := AbsoluteValue.of_negative with absolute, xInA, xNegative594      have signsY := IsOrderedField.sign_cases with field, yInA595      cases signsY with yZero | yNonzero596      . have productZero := IsRing.mul_zero at597          A, add, zero, neg, mul, one, x with ring, xInA598        have absTimesZero := IsRing.mul_zero with ring, absXInA599        have absZero := AbsoluteValue.zero with absolute600        rw yZero601        cc602      . cases yNonzero with yNegative | yPositive603        . have negYInA := IsRing.neg_closed at604            A, add, zero, neg, mul, one, y with ring, yInA605          have negYPositive := IsOrderedField.positive_neg_of_negative with field, yInA, yNegative606          have positiveProduct := positiveMul with607            neg(x), negXInA, neg(y), negYInA,608            negXPositive, negYPositive609          have signsCancel := IsCommRing.neg_mul_neg with commRing, xInA, yInA610          rw signsCancel at positiveProduct611          have absProduct := AbsoluteValue.of_positive with absolute, productInA, positiveProduct612          have absY := AbsoluteValue.of_negative with absolute, yInA, yNegative613          cc614        . have positiveProduct := positiveMul with615            neg(x), negXInA, y, yInA, negXPositive, yPositive616          have negProduct := IsRing.neg_mul with ring, xInA, yInA617          have absNegProduct := AbsoluteValue.neg with field, absolute, productInA618          have positiveProductInA := IsRing.mul_closed with ring, negXInA, yInA619          have absPositiveProduct := AbsoluteValue.of_positive with620            absolute, positiveProductInA, positiveProduct621          have absY := AbsoluteValue.of_positive with absolute, yInA, yPositive622          cc623    . have absX := AbsoluteValue.of_positive at624        A, zero, neg, lt, abs, x with absolute, xInA, xPositive625      have signsY := IsOrderedField.sign_cases with field, yInA626      cases signsY with yZero | yNonzero627      . have productZero := IsRing.mul_zero at628          A, add, zero, neg, mul, one, x with ring, xInA629        have xTimesZero := IsRing.mul_zero with ring, xInA630        have absZero := AbsoluteValue.zero with absolute631        rw yZero632        cc633      . cases yNonzero with yNegative | yPositive634        . have negYInA := IsRing.neg_closed at635            A, add, zero, neg, mul, one, y with ring, yInA636          have negYPositive := IsOrderedField.positive_neg_of_negative with field, yInA, yNegative637          have positiveProduct := positiveMul with638            x, xInA, neg(y), negYInA, xPositive, negYPositive639          have negProduct := IsCommRing.mul_neg with commRing, xInA, yInA640          have absNegProduct := AbsoluteValue.neg with field, absolute, productInA641          have positiveProductInA := IsRing.mul_closed with ring, xInA, negYInA642          have absPositiveProduct := AbsoluteValue.of_positive with643            absolute, positiveProductInA, positiveProduct644          have absY := AbsoluteValue.of_negative with absolute, yInA, yNegative645          cc646        . have positiveProduct := positiveMul with647            x, xInA, y, yInA, xPositive, yPositive648          have absProduct := AbsoluteValue.of_positive with absolute, productInA, positiveProduct649          have absY := AbsoluteValue.of_positive with absolute, yInA, yPositive650          cc651652theorem AbsoluteValue.triangle (A add zero neg mul one inv lt abs x y : Set)653  requires field : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)654  requires absolute : AbsoluteValue(A, zero, neg, lt, abs)655  requires xInA : x ∈ A656  requires yInA : y ∈ A657  shows LessEqualBy(A, lt,658    abs(call2(add, x, y)),659    call2(add, abs(x), abs(y)))660proof661  have commRing := IsOrderedField.comm_ring with field662  have ring := IsCommRing.ring with commRing663  have additive := IsRing.additive with ring664  have group := IsAbelianGroup.group with additive665  have sumInA := IsRing.add_closed with ring, xInA, yInA666  have upperX := AbsoluteValue.upper with field, absolute, xInA667  have upperY := AbsoluteValue.upper with field, absolute, yInA668  have sumUpper := LessEqualBy.add with field, upperX, upperY669  have upperNegX := AbsoluteValue.upper_neg with field, absolute, xInA670  have upperNegY := AbsoluteValue.upper_neg with field, absolute, yInA671  have negSumUpper := LessEqualBy.add with field, upperNegX, upperNegY672  have negSum := IsAbelianGroup.inverse_op with additive, xInA, yInA673  rw ← negSum at negSumUpper674  have signs := IsOrderedField.sign_cases with field, sumInA675  cases signs with equal | nonzero676  . have shape := AbsoluteValue.zero with absolute677    rw equal at sumUpper678    rwa [equal, shape]679  . cases nonzero with negative | positive680    . have shape := AbsoluteValue.of_negative at681        A, zero, neg, lt, abs, call2(add, x, y) with682          absolute, sumInA, negative683      rwa shape684    . have shape := AbsoluteValue.of_positive at685        A, zero, neg, lt, abs, call2(add, x, y) with686          absolute, sumInA, positive687      rwa shape688689theorem IsOrderedField.positive_one (A add zero neg mul one inv lt : Set)690  requires field : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)691  shows relates(lt, zero, one)692proof693  have ordinaryField := IsOrderedField.field with field694  have commRing := IsOrderedField.comm_ring with field695  have ring := IsCommRing.ring with commRing696  have zeroInA := IsRing.zero_in_carrier with ring697  have oneInA := IsFieldWithInverse.one_in_carrier with ordinaryField698  have nontrivial := IsOrderedField.nontrivial with field699  have distinct := Nontrivial.distinct with nontrivial700  have signs := IsOrderedField.sign_cases with field, oneInA701  cases signs with equal | nonzero702  . exfalso703    apply distinct704    cc705  . cases nonzero with negative | positive706    . have negOneInA := IsRing.neg_closed at707        A, add, zero, neg, mul, one, one with ring, oneInA708      have positiveNegOne := IsOrderedField.positive_neg_of_negative with field, oneInA, negative709      have positiveMul := IsOrderedField.mul_positive with field710      have positiveSquare := positiveMul with711        neg(one), negOneInA, neg(one), negOneInA,712        positiveNegOne, positiveNegOne713      have square := IsCommRing.neg_mul_neg with commRing, oneInA, oneInA714      have monoid := IsRing.multiplicative with ring715      have oneMulOne := IsMonoid.left_identity with monoid, oneInA716      rwa [square, oneMulOne] at positiveSquare717    . exact positive718719theorem IsOrderedField.positive_inverse (A add zero neg mul one inv lt x : Set)720  requires field : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)721  requires xInA : x ∈ A722  requires positive : relates(lt, zero, x)723  shows relates(lt, zero, inv(x))724proof725  have ordinaryField := IsOrderedField.field with field726  have commRing := IsOrderedField.comm_ring with field727  have ring := IsCommRing.ring with commRing728  have zeroInA := IsRing.zero_in_carrier with ring729  have oneInA := IsFieldWithInverse.one_in_carrier with ordinaryField730  have inverseInA := IsFieldWithInverse.inverse_closed with ordinaryField, xInA731  have zeroNeX := IsOrderedField.ne_of_less with field, zeroInA, xInA, positive732  have nonzero : x ≠ zero733    intro equal734    apply zeroNeX735    cc736  have product := IsFieldWithInverse.inverse_right with ordinaryField, xInA,737    nonzero738  have signs := IsOrderedField.sign_cases with field, inverseInA739  cases signs with equal | nonzeroSign740  . have zeroProduct := IsRing.mul_zero at741      A, add, zero, neg, mul, one, x with ring, xInA742    have nontrivial := IsOrderedField.nontrivial with field743    have distinct := Nontrivial.distinct with nontrivial744    exfalso745    apply distinct746    cc747  . cases nonzeroSign with negative | inversePositive748    . have negInverseInA := IsRing.neg_closed at749        A, add, zero, neg, mul, one, inv(x) with ring, inverseInA750      have positiveNegInverse := IsOrderedField.positive_neg_of_negative with field, inverseInA, negative751      have positiveMul := IsOrderedField.mul_positive with field752      have positiveNegativeOne := positiveMul with753        x, xInA, neg(inv(x)), negInverseInA,754        positive, positiveNegInverse755      have negProduct := IsCommRing.mul_neg with commRing, xInA, inverseInA756      have onePositive := IsOrderedField.positive_one with field757      have negativeNegativeOne := IsOrderedField.negative_neg_of_positive with field, oneInA, onePositive758      rw [negProduct, product] at positiveNegativeOne759      have negOneInA := IsRing.neg_closed with ring, oneInA760      have cycle := IsOrderedField.transitive with761        field, negOneInA, zeroInA, negOneInA, negativeNegativeOne, positiveNegativeOne762      exfalso763      exact IsOrderedField.irreflexive with field, negOneInA, cycle764    . exact inversePositive765766theorem IsOrderedField.half_closed (A add zero neg mul one inv lt x : Set)767  requires field : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)768  requires xInA : x ∈ A769  shows fieldHalf(add, mul, one, inv, x) ∈ A770proof771  have ordinaryField := IsOrderedField.field with field772  have commRing := IsOrderedField.comm_ring with field773  have ring := IsCommRing.ring with commRing774  have oneInA := IsFieldWithInverse.one_in_carrier with ordinaryField775  have twoInA := IsRing.add_closed with ring, oneInA, oneInA776  have inverseTwoInA := IsFieldWithInverse.inverse_closed with ordinaryField,777    twoInA778  unfold fieldHalf779  exact IsRing.mul_closed with ring, inverseTwoInA, xInA780781theorem IsOrderedField.half_positive (A add zero neg mul one inv lt x : Set)782  requires field : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)783  requires xInA : x ∈ A784  requires positive : relates(lt, zero, x)785  shows relates(lt, zero, fieldHalf(add, mul, one, inv, x))786proof787  have ordinaryField := IsOrderedField.field with field788  have commRing := IsOrderedField.comm_ring with field789  have ring := IsCommRing.ring with commRing790  have oneInA := IsFieldWithInverse.one_in_carrier with ordinaryField791  have onePositive := IsOrderedField.positive_one with field792  have twoInA := IsRing.add_closed with ring, oneInA, oneInA793  have twoPositive := IsOrderedField.positive_sum with field, oneInA, oneInA, onePositive, onePositive794  have inverseTwoInA := IsFieldWithInverse.inverse_closed with ordinaryField,795    twoInA796  have inverseTwoPositive := IsOrderedField.positive_inverse with field, twoInA, twoPositive797  have positiveMul := IsOrderedField.mul_positive with field798  unfold fieldHalf799  exact positiveMul with800    inv(call2(add, one, one)), inverseTwoInA, x, xInA,801    inverseTwoPositive, positive802803theorem IsOrderedField.half_add_self (A add zero neg mul one inv lt x : Set)804  requires field : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)805  requires xInA : x ∈ A806  shows call2(add,807    fieldHalf(add, mul, one, inv, x),808    fieldHalf(add, mul, one, inv, x)) = x809proof810  have ordinaryField := IsOrderedField.field with field811  have commRing := IsOrderedField.comm_ring with field812  have ring := IsCommRing.ring with commRing813  have monoid := IsRing.multiplicative with ring814  have oneInA := IsFieldWithInverse.one_in_carrier with ordinaryField815  have twoInA := IsRing.add_closed with ring, oneInA, oneInA816  have onePositive := IsOrderedField.positive_one with field817  have twoPositive := IsOrderedField.positive_sum with field, oneInA, oneInA, onePositive, onePositive818  have zeroInA := IsRing.zero_in_carrier with ring819  have zeroNeTwo := IsOrderedField.ne_of_less with field, zeroInA, twoInA, twoPositive820  have twoNonzero : call2(add, one, one) ≠ zero821    intro equal822    apply zeroNeTwo823    cc824  have inverseTwoInA := IsFieldWithInverse.inverse_closed with ordinaryField,825    twoInA826  have inverseTwo := IsFieldWithInverse.inverse_right with ordinaryField,827    twoInA, twoNonzero828  have halfInA := IsOrderedField.half_closed with field, xInA829  have distributive := IsRing.distributive with ring830  have laws := distributive with one, oneInA, one, oneInA,831    fieldHalf(add, mul, one, inv, x), halfInA832  rcases laws with ⟨leftLaw, twoTimesHalf⟩833  have oneTimesHalf := IsMonoid.left_identity with monoid, halfInA834  rw oneTimesHalf at twoTimesHalf835  unfold fieldHalf at twoTimesHalf836  have associative := IsMonoid.associative with monoid837  have reassociate := Associative.law with associative, twoInA, inverseTwoInA, xInA838  have oneTimesX := IsMonoid.left_identity with monoid, xInA839  unfold fieldHalf840  cc841842theorem IsOrderedField.positive_product (A add zero neg mul one inv lt x y : Set)843  requires h : IsOrderedField(A, add, zero, neg, mul, one, inv, lt)844  requires hx : x ∈ A845  requires hy : y ∈ A846  requires positiveX : relates(lt, zero, x)847  requires positiveY : relates(lt, zero, y)848  shows relates(lt, zero, call2(mul, x, y))849proof850  have positive := IsOrderedField.mul_positive with h851  exact positive with x, hx, y, hy, positiveX, positiveY852