let d, e be Nat; :: thesis: for p being Prime st p > 2 & d gcd p = 1 & e gcd p = 1 holds

Lege (((d ^2) * e),p) = Lege (e,p)

let p be Prime; :: thesis: ( p > 2 & d gcd p = 1 & e gcd p = 1 implies Lege (((d ^2) * e),p) = Lege (e,p) )

assume that

A1: p > 2 and

A2: d gcd p = 1 and

A3: e gcd p = 1 ; :: thesis: Lege (((d ^2) * e),p) = Lege (e,p)

reconsider d2 = d ^2 , e = e as Element of NAT by ORDINAL1:def 12;

set fp = <*d2,e*>;

reconsider fp = <*d2,e*> as FinSequence of NAT by FINSEQ_2:13;

not p divides d by A2, Lm3;

then d mod p <> 0 by INT_1:62;

then A4: Lege ((d ^2),p) = 1 by Th26;

reconsider p = p as prime Element of NAT by ORDINAL1:def 12;

for k being Nat st k in dom fp holds

(fp . k) gcd p = 1

A6: len fr = len fp and

A7: for k being Nat st k in dom fr holds

fr . k = Lege ((fp . k),p) and

A8: Lege ((Product fp),p) = Product fr by A1, Th34;

A9: len fr = 2 by A6, FINSEQ_1:44;

then 2 in dom fr by FINSEQ_3:25;

then fr . 2 = Lege ((fp . 2),p) by A7;

then A10: fr . 2 = Lege (e,p) by FINSEQ_1:44;

fr . 1 = Lege ((fp . 1),p) by A7, A9, FINSEQ_3:25;

then fr . 1 = Lege ((d ^2),p) by FINSEQ_1:44;

then fr = <*1,(Lege (e,p))*> by A4, A9, A10, FINSEQ_1:44;

then Product fr = 1 * (Lege (e,p)) by RVSUM_1:99;

hence Lege (((d ^2) * e),p) = Lege (e,p) by A8, RVSUM_1:99; :: thesis: verum

Lege (((d ^2) * e),p) = Lege (e,p)

let p be Prime; :: thesis: ( p > 2 & d gcd p = 1 & e gcd p = 1 implies Lege (((d ^2) * e),p) = Lege (e,p) )

assume that

A1: p > 2 and

A2: d gcd p = 1 and

A3: e gcd p = 1 ; :: thesis: Lege (((d ^2) * e),p) = Lege (e,p)

reconsider d2 = d ^2 , e = e as Element of NAT by ORDINAL1:def 12;

set fp = <*d2,e*>;

reconsider fp = <*d2,e*> as FinSequence of NAT by FINSEQ_2:13;

not p divides d by A2, Lm3;

then d mod p <> 0 by INT_1:62;

then A4: Lege ((d ^2),p) = 1 by Th26;

reconsider p = p as prime Element of NAT by ORDINAL1:def 12;

for k being Nat st k in dom fp holds

(fp . k) gcd p = 1

proof

then consider fr being FinSequence of INT such that
let k be Nat; :: thesis: ( k in dom fp implies (fp . k) gcd p = 1 )

assume k in dom fp ; :: thesis: (fp . k) gcd p = 1

then k in Seg (len fp) by FINSEQ_1:def 3;

then A5: k in Seg 2 by FINSEQ_1:44;

end;assume k in dom fp ; :: thesis: (fp . k) gcd p = 1

then k in Seg (len fp) by FINSEQ_1:def 3;

then A5: k in Seg 2 by FINSEQ_1:44;

A6: len fr = len fp and

A7: for k being Nat st k in dom fr holds

fr . k = Lege ((fp . k),p) and

A8: Lege ((Product fp),p) = Product fr by A1, Th34;

A9: len fr = 2 by A6, FINSEQ_1:44;

then 2 in dom fr by FINSEQ_3:25;

then fr . 2 = Lege ((fp . 2),p) by A7;

then A10: fr . 2 = Lege (e,p) by FINSEQ_1:44;

fr . 1 = Lege ((fp . 1),p) by A7, A9, FINSEQ_3:25;

then fr . 1 = Lege ((d ^2),p) by FINSEQ_1:44;

then fr = <*1,(Lege (e,p))*> by A4, A9, A10, FINSEQ_1:44;

then Product fr = 1 * (Lege (e,p)) by RVSUM_1:99;

hence Lege (((d ^2) * e),p) = Lege (e,p) by A8, RVSUM_1:99; :: thesis: verum