let V, A be set ; for a, b being Element of V
for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) holds
<*(PP_and ((less (A,b,a)),(gcd_inv (V,A,a,b,x0,y0)))),(SC_assignment ((subtraction (A,a,b)),a)),(gcd_inv (V,A,a,b,x0,y0))*> is SFHT of (ND (V,A))
let a, b be Element of V; for x0, y0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & a <> b & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) holds
<*(PP_and ((less (A,b,a)),(gcd_inv (V,A,a,b,x0,y0)))),(SC_assignment ((subtraction (A,a,b)),a)),(gcd_inv (V,A,a,b,x0,y0))*> is SFHT of (ND (V,A))
let x0, y0 be Nat; ( not V is empty & A is_without_nonatomicND_wrt V & a <> b & A is complex-containing & ( for d being TypeSCNominativeData of V,A holds a is_complex_on d ) & ( for d being TypeSCNominativeData of V,A holds b is_complex_on d ) implies <*(PP_and ((less (A,b,a)),(gcd_inv (V,A,a,b,x0,y0)))),(SC_assignment ((subtraction (A,a,b)),a)),(gcd_inv (V,A,a,b,x0,y0))*> is SFHT of (ND (V,A)) )
assume that
A1:
not V is empty
and
A2:
A is_without_nonatomicND_wrt V
and
A3:
a <> b
and
A4:
A is complex-containing
and
A5:
for d being TypeSCNominativeData of V,A holds a is_complex_on d
and
A6:
for d being TypeSCNominativeData of V,A holds b is_complex_on d
; <*(PP_and ((less (A,b,a)),(gcd_inv (V,A,a,b,x0,y0)))),(SC_assignment ((subtraction (A,a,b)),a)),(gcd_inv (V,A,a,b,x0,y0))*> is SFHT of (ND (V,A))
set i = gcd_inv (V,A,a,b,x0,y0);
set l = less (A,b,a);
set D = subtraction (A,a,b);
set Da = denaming (V,A,a);
set Db = denaming (V,A,b);
set f = SC_assignment ((subtraction (A,a,b)),a);
set p = PP_and ((less (A,b,a)),(gcd_inv (V,A,a,b,x0,y0)));
set S = SC_Psuperpos ((gcd_inv (V,A,a,b,x0,y0)),(subtraction (A,a,b)),a);
A7:
<*(SC_Psuperpos ((gcd_inv (V,A,a,b,x0,y0)),(subtraction (A,a,b)),a)),(SC_assignment ((subtraction (A,a,b)),a)),(gcd_inv (V,A,a,b,x0,y0))*> is SFHT of (ND (V,A))
by NOMIN_3:29;
for d being TypeSCNominativeData of V,A st d in dom (PP_and ((less (A,b,a)),(gcd_inv (V,A,a,b,x0,y0)))) & (PP_and ((less (A,b,a)),(gcd_inv (V,A,a,b,x0,y0)))) . d = TRUE & d in dom (SC_assignment ((subtraction (A,a,b)),a)) & (SC_assignment ((subtraction (A,a,b)),a)) . d in dom (gcd_inv (V,A,a,b,x0,y0)) holds
(gcd_inv (V,A,a,b,x0,y0)) . ((SC_assignment ((subtraction (A,a,b)),a)) . d) = TRUE
proof
let d be
TypeSCNominativeData of
V,
A;
( d in dom (PP_and ((less (A,b,a)),(gcd_inv (V,A,a,b,x0,y0)))) & (PP_and ((less (A,b,a)),(gcd_inv (V,A,a,b,x0,y0)))) . d = TRUE & d in dom (SC_assignment ((subtraction (A,a,b)),a)) & (SC_assignment ((subtraction (A,a,b)),a)) . d in dom (gcd_inv (V,A,a,b,x0,y0)) implies (gcd_inv (V,A,a,b,x0,y0)) . ((SC_assignment ((subtraction (A,a,b)),a)) . d) = TRUE )
assume that A8:
d in dom (PP_and ((less (A,b,a)),(gcd_inv (V,A,a,b,x0,y0))))
and A9:
(PP_and ((less (A,b,a)),(gcd_inv (V,A,a,b,x0,y0)))) . d = TRUE
and A10:
d in dom (SC_assignment ((subtraction (A,a,b)),a))
and A11:
(SC_assignment ((subtraction (A,a,b)),a)) . d in dom (gcd_inv (V,A,a,b,x0,y0))
;
(gcd_inv (V,A,a,b,x0,y0)) . ((SC_assignment ((subtraction (A,a,b)),a)) . d) = TRUE
A12:
dom (SC_assignment ((subtraction (A,a,b)),a)) = dom (subtraction (A,a,b))
by NOMIN_2:def 7;
A13:
dom (SC_Psuperpos ((gcd_inv (V,A,a,b,x0,y0)),(subtraction (A,a,b)),a)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((subtraction (A,a,b)) . d),a) in dom (gcd_inv (V,A,a,b,x0,y0)) & d in dom (subtraction (A,a,b)) ) }
by NOMIN_2:def 11;
A14:
dom (denaming (V,A,a)) = { d where d is NonatomicND of V,A : a in dom d }
by NOMIN_1:def 18;
A15:
dom (denaming (V,A,b)) = { d where d is NonatomicND of V,A : b in dom d }
by NOMIN_1:def 18;
A16:
d in dom (less (A,b,a))
by A8, A9, PARTPR_1:23;
A17:
dom ((less A) * <:(denaming (V,A,b)),(denaming (V,A,a)):>) c= dom <:(denaming (V,A,b)),(denaming (V,A,a)):>
by RELAT_1:25;
A18:
dom <:(denaming (V,A,b)),(denaming (V,A,a)):> = (dom (denaming (V,A,b))) /\ (dom (denaming (V,A,a)))
by FUNCT_3:def 7;
then A19:
d in dom (denaming (V,A,a))
by A16, A17, XBOOLE_0:def 4;
then consider da being
NonatomicND of
V,
A such that A20:
d = da
and A21:
a in dom da
by A14;
A22:
d in dom (denaming (V,A,b))
by A16, A17, A18, XBOOLE_0:def 4;
then consider db being
NonatomicND of
V,
A such that A23:
d = db
and A24:
b in dom db
by A15;
reconsider L =
local_overlapping (
V,
A,
da,
((subtraction (A,a,b)) . da),
a) as
Function ;
dom (gcd_inv (V,A,a,b,x0,y0)) = ND (
V,
A)
by Def28;
then A25:
L in dom (gcd_inv (V,A,a,b,x0,y0))
;
A26:
rng (subtraction (A,a,b)) c= rng (subtraction A)
by RELAT_1:26;
A27:
rng (subtraction (A,a,b)) c= A
by A26, XBOOLE_1:1;
reconsider L =
L as
NonatomicND of
V,
A by NOMIN_2:9;
A28:
gcd_inv_pred V,
A,
a,
b,
x0,
y0,
L
proof
take
L
;
NOMIN_4:def 27 ( L = L & a in dom L & b in dom L & ex x, y being Nat st
( x = L . a & y = L . b & x gcd y = x0 gcd y0 ) )
thus
L = L
;
( a in dom L & b in dom L & ex x, y being Nat st
( x = L . a & y = L . b & x gcd y = x0 gcd y0 ) )
(
d in dom (gcd_inv (V,A,a,b,x0,y0)) &
(gcd_inv (V,A,a,b,x0,y0)) . d = TRUE )
by A8, A9, PARTPR_1:23;
then
gcd_inv_pred V,
A,
a,
b,
x0,
y0,
d
by Def28;
then consider d1 being
NonatomicND of
V,
A such that A29:
d = d1
and
a in dom d1
and
b in dom d1
and A30:
ex
x,
y being
Nat st
(
x = d1 . a &
y = d1 . b &
x gcd y = x0 gcd y0 )
;
consider x,
y being
Nat such that A31:
x = d1 . a
and A32:
y = d1 . b
and A33:
x gcd y = x0 gcd y0
by A30;
(subtraction (A,a,b)) . d in rng (subtraction (A,a,b))
by A10, A12, FUNCT_1:def 3;
then reconsider Dd =
(subtraction (A,a,b)) . d as
TypeSCNominativeData of
V,
A by A27, NOMIN_1:def 6;
A34:
L . a = Dd
by A1, A20, NOMIN_2:10;
A35:
<:(denaming (V,A,b)),(denaming (V,A,a)):> . d = [((denaming (V,A,b)) . d),((denaming (V,A,a)) . d)]
by A16, A17, FUNCT_3:def 7;
A36:
(
(denaming (V,A,a)) . d = denaming (
a,
da) &
(denaming (V,A,b)) . d = denaming (
b,
db) )
by A20, A23, A19, A22, NOMIN_1:def 18;
(
a is_complex_on d &
b is_complex_on d )
by A5, A6;
then consider x1,
y1 being
Complex such that A37:
x1 = denaming (
a,
da)
and A38:
y1 = denaming (
b,
db)
and A39:
subtraction (
(denaming (a,da)),
(denaming (b,db)))
= x1 - y1
by A36, Def14;
A40:
x1 = x
by A20, A21, A29, A31, A37, NOMIN_1:def 12;
A41:
y1 = y
by A23, A24, A29, A32, A38, NOMIN_1:def 12;
A42:
not
da in A
by A2, Th3;
A43:
not
naming (
V,
A,
a,
((subtraction (A,a,b)) . da))
in A
by A2, Th3;
Dd = (subtraction (A,a,b)) . d
;
then A44:
L . b = da . b
by A1, A3, A20, A23, A24, A42, A43, NOMIN_2:12;
A45:
denaming (
a,
da)
in COMPLEX
by A37, XCMPLX_0:def 2;
A46:
denaming (
b,
db)
in COMPLEX
by A38, XCMPLX_0:def 2;
A47:
dom (local_overlapping (V,A,da,Dd,a)) = dom da
by A1, A20, A21, A42, A43, NOMIN_2:14;
hence
a in dom L
by A20, A21;
( b in dom L & ex x, y being Nat st
( x = L . a & y = L . b & x gcd y = x0 gcd y0 ) )
thus
b in dom L
by A20, A23, A24, A47;
ex x, y being Nat st
( x = L . a & y = L . b & x gcd y = x0 gcd y0 )
A48:
(less (A,b,a)) . d = TRUE
by A8, A9, PARTPR_1:23;
d in dom (less (A,b,a))
by A8, A9, PARTPR_1:23;
then
(less (A,b,a)) . d = (less A) . (
((denaming (V,A,b)) . d),
((denaming (V,A,a)) . d))
by A35, FUNCT_1:12;
then
(denaming (V,A,b)) . d less_pred (denaming (V,A,a)) . d
by A4, A36, A45, A46, A48, Def12;
then
x - y in NAT
by A36, A37, A38, A40, A41, INT_1:5;
then reconsider z =
x - y as
Nat ;
take
z
;
ex y being Nat st
( z = L . a & y = L . b & z gcd y = x0 gcd y0 )
take
y
;
( z = L . a & y = L . b & z gcd y = x0 gcd y0 )
dom <:(denaming (V,A,a)),(denaming (V,A,b)):> = (dom (denaming (V,A,a))) /\ (dom (denaming (V,A,b)))
by FUNCT_3:def 7;
then A49:
d in dom <:(denaming (V,A,a)),(denaming (V,A,b)):>
by A19, A22, XBOOLE_0:def 4;
then
<:(denaming (V,A,a)),(denaming (V,A,b)):> . d = [((denaming (V,A,a)) . d),((denaming (V,A,b)) . d)]
by FUNCT_3:def 7;
then (subtraction (A,a,b)) . d =
(subtraction A) . (
(denaming (a,da)),
(denaming (b,db)))
by A36, A49, FUNCT_1:13
.=
subtraction (
(denaming (a,da)),
(denaming (b,db)))
by A4, A45, A46, Def15
;
hence
z = L . a
by A20, A21, A29, A31, A34, A37, A39, A41, NOMIN_1:def 12;
( y = L . b & z gcd y = x0 gcd y0 )
thus
y = L . b
by A20, A23, A24, A38, A41, A44, NOMIN_1:def 12;
z gcd y = x0 gcd y0
(x - (1 * y)) gcd y = x gcd y
by NEWTON02:5;
hence
z gcd y = x0 gcd y0
by A33;
verum
end;
A50:
d in dom (SC_Psuperpos ((gcd_inv (V,A,a,b,x0,y0)),(subtraction (A,a,b)),a))
by A10, A12, A13, A20, A25;
then (SC_Psuperpos ((gcd_inv (V,A,a,b,x0,y0)),(subtraction (A,a,b)),a)) . d =
(gcd_inv (V,A,a,b,x0,y0)) . L
by A20, NOMIN_2:35
.=
TRUE
by A25, A28, Def28
;
hence
(gcd_inv (V,A,a,b,x0,y0)) . ((SC_assignment ((subtraction (A,a,b)),a)) . d) = TRUE
by A7, A10, A11, A50, NOMIN_3:11;
verum
end;
hence
<*(PP_and ((less (A,b,a)),(gcd_inv (V,A,a,b,x0,y0)))),(SC_assignment ((subtraction (A,a,b)),a)),(gcd_inv (V,A,a,b,x0,y0))*> is SFHT of (ND (V,A))
by NOMIN_3:28; verum