Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Ordered Rings - Part II

by
Michal Muzalewski, and
Leslaw W. Szczerba

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;
```