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

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

Back to top