let m be CR_Sequence; :: thesis: for i being natural number st i in dom m holds
for mm being Integer st mm = (Product m) / (m . i) holds
mm,m . i are_relative_prime
let i be natural number ; :: thesis: ( i in dom m implies for mm being Integer st mm = (Product m) / (m . i) holds
mm,m . i are_relative_prime )
assume AS1:
i in dom m
; :: thesis: for mm being Integer st mm = (Product m) / (m . i) holds
mm,m . i are_relative_prime
let mm be Integer; :: thesis: ( mm = (Product m) / (m . i) implies mm,m . i are_relative_prime )
assume AS2:
mm = (Product m) / (m . i)
; :: thesis: mm,m . i are_relative_prime
set k = mm gcd (m . i);
defpred S1[ Nat] means for m being CR_Sequence st len m = $1 holds
for i being natural number st i in dom m holds
for mm being Integer st mm = (Product m) / (m . i) holds
mm,m . i are_relative_prime ;
then A:
S1[ 0 ]
;
B:
now let k be
Element of
NAT ;
:: thesis: ( S1[k] implies S1[k + 1] )assume B1:
S1[
k]
;
:: thesis: S1[k + 1]now let m be
CR_Sequence;
:: thesis: ( len m = k + 1 implies for i' being natural number st i' in dom m holds
for mm being Integer st mm = (Product m) / (m . i') holds
b5,b3 . b4 are_relative_prime )assume A:
len m = k + 1
;
:: thesis: for i' being natural number st i' in dom m holds
for mm being Integer st mm = (Product m) / (m . i') holds
b5,b3 . b4 are_relative_prime let i' be
natural number ;
:: thesis: ( i' in dom m implies for mm being Integer st mm = (Product m) / (m . i') holds
b4,b2 . b3 are_relative_prime )assume B:
i' in dom m
;
:: thesis: for mm being Integer st mm = (Product m) / (m . i') holds
b4,b2 . b3 are_relative_prime reconsider i =
i' as
Element of
NAT by ORDINAL1:def 13;
let mm be
Integer;
:: thesis: ( mm = (Product m) / (m . i') implies b3,b1 . b2 are_relative_prime )assume M:
mm = (Product m) / (m . i')
;
:: thesis: b3,b1 . b2 are_relative_prime set m1 =
m | k;
C4:
i in Seg (k + 1)
by A, B, FINSEQ_1:def 3;
then C5:
( 1
<= i &
i <= k + 1 )
by FINSEQ_1:3;
Y:
len (m | k) = k
by A, FINSEQ_1:80, NAT_1:11;
1
<= k + 1
by NAT_1:11;
then
k + 1
in Seg (k + 1)
;
then G:
k + 1
in dom m
by A, FINSEQ_1:def 3;
F:
(m | k) ^ <*(m . (k + 1))*> =
m | (k + 1)
by A, th67
.=
m
by A, FINSEQ_1:79
;
per cases
( k > 0 or k = 0 )
;
suppose
k > 0
;
:: thesis: b3,b1 . b2 are_relative_prime then reconsider m1 =
m | k as
CR_Sequence by A, CRsub, NAT_1:11;
per cases
( i in dom m1 or not i in dom m1 )
;
suppose E:
i in dom m1
;
:: thesis: b3,b1 . b2 are_relative_prime then E1:
m1 . i = m . i
by FUNCT_1:70;
reconsider mm1 =
(Product m1) / (m1 . i) as
Integer by E, prodint;
i in Seg k
by E, Y, FINSEQ_1:def 3;
then
( 1
<= i &
i <= k )
by FINSEQ_1:3;
then E2:
i <> k + 1
by NAT_1:13;
X:
m . i,
m . (k + 1) are_relative_prime
by E2, B, G, DefCR;
mm1,
m . i are_relative_prime
by E1, E, Y, B1;
then E3:
(m . i) gcd (mm1 * (m . (k + 1))) =
(m . i) gcd (m . (k + 1))
by thgcd2
.=
1
by X, INT_2:def 4
;
mm1 * (m . (k + 1)) =
((Product m1) * (m . (k + 1))) * ((m . i) " )
by E1
.=
mm
by F, M, RVSUM_1:126
;
hence
mm,
m . i' are_relative_prime
by E3, INT_2:def 4;
:: thesis: verum end; suppose
not
i in dom m1
;
:: thesis: b3,b1 . b2 are_relative_prime then
not
i in Seg k
by Y, FINSEQ_1:def 3;
then
( not 1
<= i or not
i <= k )
;
then
not
i < k + 1
by C4, FINSEQ_1:3, NAT_1:13;
then D0:
i = k + 1
by C5, XXREAL_0:1;
m . (k + 1) in rng m
by G, FUNCT_1:12;
then D1:
m . (k + 1) > 0
by PARTFUN3:def 1;
defpred S2[
Nat]
means ( $1
<= len m1 implies for
s being
Element of
NAT st
s = $1 holds
Product (m1 | s),
m . (k + 1) are_relative_prime );
m1 | 0 is
empty
;
then Q1:
S2[
0 ]
by RVSUM_1:124, WSIERP_1:14;
Q2:
now let j be
Element of
NAT ;
:: thesis: ( 0 <= j & j < len m1 & S2[j] implies S2[j + 1] )assume Q3:
(
0 <= j &
j < len m1 )
;
:: thesis: ( S2[j] implies S2[j + 1] )assume Q4:
S2[
j]
;
:: thesis: S2[j + 1]now assume Q8:
j + 1
<= len m1
;
:: thesis: S2[j + 1]then
j + 1
<= k
by A, FINSEQ_1:80, NAT_1:11;
then Q5:
j + 1
<> k + 1
by NAT_1:13;
Q7:
0 + 1
<= j + 1
by XREAL_1:8;
j + 1
<= len m
by A, Y, Q3, XREAL_1:10;
then
j + 1
in Seg (len m)
by Q7;
then Q6:
j + 1
in dom m
by FINSEQ_1:def 3;
j + 1
in Seg (len m1)
by Q7, Q8;
then Q9:
j + 1
in dom m1
by FINSEQ_1:def 3;
now let s be
Element of
NAT ;
:: thesis: ( s = j + 1 implies Product (m1 | s),m . (k + 1) are_relative_prime )assume QX:
s = j + 1
;
:: thesis: Product (m1 | s),m . (k + 1) are_relative_prime reconsider s' =
j as
Element of
NAT ;
X:
m . (j + 1),
m . (k + 1) are_relative_prime
by DefCR, Q5, G, Q6;
j <= j + 1
by NAT_1:11;
then
Product (m1 | s'),
m . (k + 1) are_relative_prime
by Q4, Q8, XXREAL_0:2;
then QQ:
((Product (m1 | s')) * (m . (j + 1))) gcd (m . (k + 1)) =
(m . (j + 1)) gcd (m . (k + 1))
by thgcd2
.=
1
by X, INT_2:def 4
;
Q10:
m1 . (j + 1) = m . (j + 1)
by Q9, FUNCT_1:70;
(m1 | s') ^ <*(m1 . s)*> = m1 | s
by QX, Q8, th67;
then
(Product (m1 | s)) gcd (m . (k + 1)) = 1
by QX, QQ, Q10, RVSUM_1:126;
hence
Product (m1 | s),
m . (k + 1) are_relative_prime
by INT_2:def 4;
:: thesis: verum end; hence
S2[
j + 1]
;
:: thesis: verum end; hence
S2[
j + 1]
;
:: thesis: verum end; Q3:
for
j being
Element of
NAT st
0 <= j &
j <= len m1 holds
S2[
j]
from POLYNOM2:sch 4(Q1, Q2);
D2:
m1 | (len m1) = m1
by FINSEQ_1:79;
mm =
((Product m1) * (m . (k + 1))) * ((m . (k + 1)) " )
by M, D0, F, RVSUM_1:126
.=
(Product m1) * ((m . (k + 1)) * ((m . (k + 1)) " ))
.=
(Product m1) * 1
by D1, XCMPLX_0:def 7
;
hence
mm,
m . i' are_relative_prime
by D2, Q3, D0;
:: thesis: verum end; end; end; hence
S1[
k + 1]
;
:: thesis: verum end;
I:
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A, B);
consider l being Element of NAT such that
H:
len m = l
;
thus
mm,m . i are_relative_prime
by I, H, AS1, AS2; :: thesis: verum