let F be non empty right_complementable almost_left_invertible right-distributive left-distributive well-unital left_unital add-associative right_zeroed commutative doubleLoopStr ; :: thesis: F is gcd-like
let x, y be Element of F; :: according to GCD_1:def 11 :: thesis: ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) )
now :: thesis: ( ( x <> 0. F & y <> 0. F & ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) ) ) or ( x = 0. F & ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) ) ) or ( y = 0. F & ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) ) ) )
per cases ( ( x <> 0. F & y <> 0. F ) or x = 0. F or y = 0. F ) ;
case A1: ( x <> 0. F & y <> 0. F ) ; :: thesis: ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) )
A2: for zz being Element of F st zz divides x & zz divides y holds
zz divides 1_ F
proof
let zz be Element of F; :: thesis: ( zz divides x & zz divides y implies zz divides 1_ F )
assume that
A3: zz divides x and
zz divides y ; :: thesis: zz divides 1_ F
now :: thesis: ( ( zz <> 0. F & zz divides 1_ F ) or ( zz = 0. F & ( zz divides x implies zz divides 1_ F ) ) )
per cases ( zz <> 0. F or zz = 0. F ) ;
case A4: zz = 0. F ; :: thesis: ( zz divides x implies zz divides 1_ F )
assume zz divides x ; :: thesis: zz divides 1_ F
then ex d being Element of F st zz * d = x ;
hence zz divides 1_ F by A1, A4; :: thesis: verum
end;
end;
end;
hence zz divides 1_ F by A3; :: thesis: verum
end;
y = (1_ F) * y ;
then A5: 1_ F divides y ;
x = (1_ F) * x ;
then 1_ F divides x ;
hence ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) ) by A5, A2; :: thesis: verum
end;
case A6: x = 0. F ; :: thesis: ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) )
y * (0. F) = 0. F ;
then A7: y divides 0. F ;
for z being Element of F st z divides 0. F & z divides y holds
z divides y ;
hence ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) ) by A6, A7; :: thesis: verum
end;
case A8: y = 0. F ; :: thesis: ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) )
x * (0. F) = 0. F ;
then A9: x divides 0. F ;
for z being Element of F st z divides x & z divides 0. F holds
z divides x ;
hence ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) ) by A8, A9; :: thesis: verum
end;
end;
end;
hence ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) ) ; :: thesis: verum