The abstract of the Mizar article:

Ordered Rings - Part II

by

Michal Muzalewski, and

Leslaw W. Szczerba

Received October 11, 1990

MML identifier: O_RING_2

[ 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_2:1
    x is_a_square & y is_a_square or
  x is_a_sum_of_squares & y is_a_square
    implies x+y is_a_sum_of_squares;

theorem :: O_RING_2:2
    x is_a_sum_of_products_of_squares & y is_a_square or
  x is_a_sum_of_products_of_squares & y is_a_product_of_squares
    implies x+y is_a_sum_of_products_of_squares;

theorem :: O_RING_2:3
    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 or
  x is_a_sum_of_amalgams_of_squares & y is_a_square 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_an_amalgam_of_squares
    implies x+y is_a_sum_of_amalgams_of_squares;

theorem :: O_RING_2:4
    x is_a_square & y is_a_sum_of_squares or
  x is_a_square & y is_a_product_of_squares or
  x is_a_square & y is_a_sum_of_products_of_squares or
  x is_a_square & y is_an_amalgam_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_2:5
    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_2:6
    x is_a_product_of_squares & y is_a_square or
  x is_a_product_of_squares & y is_a_sum_of_squares or
  x is_a_product_of_squares & y is_a_product_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_an_amalgam_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_2:7
    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_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_2:8
    x is_an_amalgam_of_squares & y is_a_square or
  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_2:9
    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_sum_of_products_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_2:10
    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;