The abstract of the Mizar article:

Ordered Rings - Part III

by

Michal Muzalewski, and

Leslaw W. Szczerba

Received October 11, 1990

MML identifier: O_RING_3

[ Mizar article, MML identifier index ]

environ

 vocabulary VECTSP_1, FINSEQ_1, RELAT_1, FUNCT_1, O_RING_1;
 notation XREAL_0, NAT_1, FUNCT_1, FINSEQ_1, STRUCT_0, RLVECT_1, VECTSP_1,
      O_RING_1;
 constructors NAT_1, O_RING_1, XREAL_0, XBOOLE_0;
 clusters VECTSP_1, STRUCT_0, RELSET_1, NAT_1, ZFMISC_1, XBOOLE_0;
 requirements NUMERALS, REAL, SUBSET, ARITHM;


begin
reserve i,j,k,l,m,n for Nat;

reserve R for non empty doubleLoopStr;
reserve x,y for Scalar of R;
reserve f,g,h for FinSequence of the carrier of R;

theorem :: O_RING_3:1
    x is_a_square & y is_a_square
    implies x*y is_a_product_of_squares;

theorem :: O_RING_3:2
    x is_a_product_of_squares & y is_a_square
    implies x*y is_a_product_of_squares;

theorem :: O_RING_3:3
    x is_a_square & y is_a_product_of_squares or
  x is_a_square & y is_an_amalgam_of_squares
    implies x*y is_an_amalgam_of_squares;

theorem :: O_RING_3:4
    x is_a_product_of_squares & y is_a_product_of_squares or
  x is_a_product_of_squares & y is_an_amalgam_of_squares
    implies x*y is_an_amalgam_of_squares;

theorem :: O_RING_3:5
    x is_an_amalgam_of_squares & y is_a_square or
  x is_an_amalgam_of_squares & y is_a_product_of_squares or
  x is_an_amalgam_of_squares & y is_an_amalgam_of_squares
    implies x*y is_an_amalgam_of_squares;

theorem :: O_RING_3:6
    x is_a_square & y is_a_sum_of_squares or
  x is_a_square & y is_a_sum_of_products_of_squares or
  x is_a_square & y is_a_sum_of_amalgams_of_squares or
  x is_a_square & y is_generated_from_squares
    implies x*y is_generated_from_squares;


theorem :: O_RING_3:7
    x is_a_sum_of_squares & y is_a_square or
  x is_a_sum_of_squares & y is_a_sum_of_squares or
  x is_a_sum_of_squares & y is_a_product_of_squares or
  x is_a_sum_of_squares & y is_a_sum_of_products_of_squares or
  x is_a_sum_of_squares & y is_an_amalgam_of_squares or
  x is_a_sum_of_squares & y is_a_sum_of_amalgams_of_squares or
  x is_a_sum_of_squares & y is_generated_from_squares
    implies x*y is_generated_from_squares;

theorem :: O_RING_3:8
    x is_a_product_of_squares & y is_a_sum_of_squares or
  x is_a_product_of_squares & y is_a_sum_of_products_of_squares or
  x is_a_product_of_squares & y is_a_sum_of_amalgams_of_squares or
  x is_a_product_of_squares & y is_generated_from_squares
    implies x*y is_generated_from_squares;


theorem :: O_RING_3:9
    x is_a_sum_of_products_of_squares & y is_a_square or
  x is_a_sum_of_products_of_squares & y is_a_sum_of_squares or
  x is_a_sum_of_products_of_squares & y is_a_product_of_squares or
  x is_a_sum_of_products_of_squares & y is_a_sum_of_products_of_squares or
  x is_a_sum_of_products_of_squares & y is_an_amalgam_of_squares or
  x is_a_sum_of_products_of_squares & y is_a_sum_of_amalgams_of_squares or
  x is_a_sum_of_products_of_squares & y is_generated_from_squares
    implies x*y is_generated_from_squares;

theorem :: O_RING_3:10
    x is_an_amalgam_of_squares & y is_a_sum_of_squares or
  x is_an_amalgam_of_squares & y is_a_sum_of_products_of_squares or
  x is_an_amalgam_of_squares & y is_a_sum_of_amalgams_of_squares or
  x is_an_amalgam_of_squares & y is_generated_from_squares
    implies x*y is_generated_from_squares;

theorem :: O_RING_3:11
    x is_a_sum_of_amalgams_of_squares & y is_a_square or
  x is_a_sum_of_amalgams_of_squares & y is_a_sum_of_squares or
  x is_a_sum_of_amalgams_of_squares & y is_a_product_of_squares or
  x is_a_sum_of_amalgams_of_squares & y is_a_sum_of_products_of_squares or
  x is_a_sum_of_amalgams_of_squares & y is_an_amalgam_of_squares or
  x is_a_sum_of_amalgams_of_squares & y is_a_sum_of_amalgams_of_squares or
  x is_a_sum_of_amalgams_of_squares & y is_generated_from_squares
    implies x*y is_generated_from_squares;

theorem :: O_RING_3:12
    x is_generated_from_squares & y is_a_square or
  x is_generated_from_squares & y is_a_sum_of_squares or
  x is_generated_from_squares & y is_a_product_of_squares or
  x is_generated_from_squares & y is_a_sum_of_products_of_squares or
  x is_generated_from_squares & y is_an_amalgam_of_squares or
  x is_generated_from_squares & y is_a_sum_of_amalgams_of_squares or
  x is_generated_from_squares & y is_generated_from_squares
    implies x*y is_generated_from_squares;