let n, p, q, k1, k2 be Nat; :: thesis: ( p is prime & q is prime & p <> q & n = p * q & k1, Euler n are_coprime & (k1 * k2) mod (Euler n) = 1 implies for m being Element of NAT st m < n holds
Crypto ((Crypto (m,n,k1)),n,k2) = m )
assume that
A1: p is prime and
A2: q is prime and
A3: p <> q and
A4: n = p * q and
A5: k1, Euler n are_coprime and
A6: (k1 * k2) mod (Euler n) = 1 ; :: thesis: for m being Element of NAT st m < n holds
Crypto ((Crypto (m,n,k1)),n,k2) = m
A7: q > 1 by A2, INT_2:def 4;
A8: p > 1 by A1, INT_2:def 4;
A9: Euler n = (Euler p) * (Euler q) by A1, A2, A3, A4, EULER_1:21, INT_2:30
.= (p - 1) * (Euler q) by A1, EULER_1:20
.= (p - 1) * (q - 1) by A2, EULER_1:20 ;
A10: n > 1 by A4, A8, A7, XREAL_1:161;
A11: ( p <> 0 & q <> 0 ) by A1, A2, INT_2:def 4;
then reconsider p1 = p - 1, q1 = q - 1 as Element of NAT by INT_1:3;
n <> 0 by A4, A11, XCMPLX_1:6;
then A12: Euler n <> 0 by Th42;
( not p1 = 1 or not q1 = 1 ) by A3;
then A13: p1 * q1 <> 1 by NAT_1:15;
A14: k1 <> 0

proof

assume k1 = 0 ; :: thesis: contradiction
then k1 gcd (Euler n) = Euler n by NEWTON:52;
hence contradiction by A5, A9, A13, INT_2:def 3; :: thesis: verum

end;

A15: k2 <> 0 by A6, NAT_D:26;
A16: q > 0 by A2, INT_2:def 4;
let m be Element of NAT ; :: thesis: ( m < n implies Crypto ((Crypto (m,n,k1)),n,k2) = m )
assume A17: m < n ; :: thesis: Crypto ((Crypto (m,n,k1)),n,k2) = m
A18: p > 0 by A1, INT_2:def 4;

now :: thesis: Crypto ((Crypto (m,n,k1)),n,k2) = m

per cases ( m = 0 or m = 1 or ( m <> 0 & m <> 1 ) ) ;

suppose A19: m = 0 ; :: thesis: Crypto ((Crypto (m,n,k1)),n,k2) = m

then m |^ k1 = 0 by A14, NAT_1:14, NEWTON:11;
then (m |^ k1) mod n = 0 by NAT_D:26;
then (Crypto (m,n,k1)) |^ k2 = 0 by A15, NAT_1:14, NEWTON:11;
hence Crypto ((Crypto (m,n,k1)),n,k2) = m by A19, NAT_D:26; :: thesis: verum

end;

suppose A20: m = 1 ; :: thesis: Crypto ((Crypto (m,n,k1)),n,k2) = m

then m |^ k1 = 1 ;
then (m |^ k1) mod n = 1 by A10, NAT_D:14;
then (Crypto (m,n,k1)) |^ k2 = 1 ;
hence Crypto ((Crypto (m,n,k1)),n,k2) = m by A10, A20, NAT_D:14; :: thesis: verum

end;

suppose A21: ( m <> 0 & m <> 1 ) ; :: thesis: Crypto ((Crypto (m,n,k1)),n,k2) = m

A22: for t being Element of NAT holds (m |^ (((t * p1) * q1) + 1)) mod n = m

proof

let t be Element of NAT ; :: thesis: (m |^ (((t * p1) * q1) + 1)) mod n = m

now :: thesis: (m |^ (((t * p1) * q1) + 1)) mod n = m

m |^ ((t * p1) * q1) >= 1 by A21, NAT_1:14, PREPOWER:11;
then (m |^ ((t * p1) * q1)) - 1 >= 1 - 1 by XREAL_1:9;
then reconsider a = (m |^ ((t * p1) * q1)) - 1 as Element of NAT by INT_1:3;
A23: p divides m * a

proof

now :: thesis: p divides m * a

per cases ( m gcd p = 1 or m gcd p <> 1 ) ;

suppose m gcd p = 1 ; :: thesis: p divides m * a

then A24: m,p are_coprime by INT_2:def 3;
((m |^ (t * q1)) |^ (p1 + 1)) mod p = (m |^ (t * q1)) mod p by A1, EULER_2:19;
then (((m |^ (t * q1)) |^ p1) * (m |^ (t * q1))) mod p = (m |^ (t * q1)) mod p by NEWTON:6;
then ((m |^ (t * q1)) |^ p1) mod p = 1 by A8, A21, A24, Th11, EULER_2:17;
then (m |^ ((t * q1) * p1)) mod p = 1 by NEWTON:9;
then m |^ ((t * p1) * q1) = (p * ((m |^ ((t * p1) * q1)) div p)) + 1 by A18, NAT_D:2;
then p divides a ;
hence p divides m * a by NAT_D:9; :: thesis: verum

end;

suppose m gcd p <> 1 ; :: thesis: p divides m * a

then not m,p are_coprime by INT_2:def 3;
then m gcd p = p by A1, Th2;
then p divides m by NAT_D:def 5;
hence p divides m * a by NAT_D:9; :: thesis: verum

end;

end;

end;

hence p divides m * a ; :: thesis: verum

end;

q divides m * a

proof

now :: thesis: q divides m * a

per cases ( m gcd q = 1 or m gcd q <> 1 ) ;

suppose m gcd q = 1 ; :: thesis: q divides m * a

then A25: m,q are_coprime by INT_2:def 3;
((m |^ (t * p1)) |^ (q1 + 1)) mod q = (m |^ (t * p1)) mod q by A2, EULER_2:19;
then (((m |^ (t * p1)) |^ q1) * (m |^ (t * p1))) mod q = (m |^ (t * p1)) mod q by NEWTON:6;
then ((m |^ (t * p1)) |^ q1) mod q = 1 by A7, A21, A25, Th11, EULER_2:17;
then (m |^ ((t * p1) * q1)) mod q = 1 by NEWTON:9;
then m |^ ((t * p1) * q1) = (q * ((m |^ ((t * p1) * q1)) div q)) + 1 by A16, NAT_D:2;
then q divides a ;
hence q divides m * a by NAT_D:9; :: thesis: verum

end;

suppose m gcd q <> 1 ; :: thesis: q divides m * a

then not m,q are_coprime by INT_2:def 3;
then m gcd q = q by A2, Th2;
then q divides m by NAT_D:def 5;
hence q divides m * a by NAT_D:9; :: thesis: verum

end;

end;

end;

hence q divides m * a ; :: thesis: verum

end;

then p * q divides m * a by A1, A2, A3, A23, Th4, INT_2:30;
then consider k being Nat such that
A26: m * a = (p * q) * k by NAT_D:def 3;
m * ((m |^ ((t * p1) * q1)) - 1) = (m * (m |^ ((t * p1) * q1))) - (m * 1)
.= (m |^ (((t * p1) * q1) + 1)) - m by NEWTON:6 ;
then (m |^ (((t * p1) * q1) + 1)) - (m - m) = (n * k) + m by A4, A26, XCMPLX_1:37;
hence (m |^ (((t * p1) * q1) + 1)) mod n = m by A17, NAT_D:def 2; :: thesis: verum

end;

hence (m |^ (((t * p1) * q1) + 1)) mod n = m ; :: thesis: verum

end;

reconsider t = (k1 * k2) div (Euler n) as Element of NAT ;
k1 * k2 = ((p1 * q1) * t) + 1 by A6, A12, A9, NAT_D:2
.= ((t * p1) * q1) + 1 ;
then (m |^ (k1 * k2)) mod n = m by A22;
then ((m |^ k1) |^ k2) mod n = m by NEWTON:9;
hence Crypto ((Crypto (m,n,k1)),n,k2) = m by EULER_2:22; :: thesis: verum

end;

end;

end;

hence Crypto ((Crypto (m,n,k1)),n,k2) = m ; :: thesis: verum