let p, q, n, k1, k2 be Nat; :: thesis: ( p is prime & q is prime & p <> q & n = p * q & k1, Euler n are_relative_prime & (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 A1: ( p is prime & q is prime & p <> q & n = p * q & k1, Euler n are_relative_prime & (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
let m be Element of NAT ; :: thesis: ( m < n implies Crypto (Crypto m,n,k1),n,k2 = m )
assume A2: m < n ; :: thesis: Crypto (Crypto m,n,k1),n,k2 = m
A3: ( p <> 0 & q <> 0 ) by A1, INT_2:def 5;
then reconsider p1 = p - 1, q1 = q - 1 as Element of NAT by Lm3, INT_1:16;
A4: ( p > 1 & q > 1 ) by A1, INT_2:def 5;
A5: n <> 0 by A1, A3, XCMPLX_1:6;
A6: ( p > 0 & q > 0 ) by A1, INT_2:def 5;
Euler n <> 0 by A5, Th45;
then A7: Euler n > 0 ;
A8: Euler n = (Euler p) * (Euler q) by A1, A4, EULER_1:22, INT_2:47
.= (p - 1) * (Euler q) by A1, EULER_1:21
.= (p - 1) * (q - 1) by A1, EULER_1:21 ;
( not p1 = 1 or not q1 = 1 ) by A1;
then A9: p1 * q1 <> 1 by NAT_1:15;
A10: k1 <> 0
proof
assume k1 = 0 ; :: thesis: contradiction
then k1 gcd (Euler n) = Euler n by NEWTON:65;
hence contradiction by A1, A8, A9, INT_2:def 4; :: thesis: verum
end;
A11: k2 <> 0 by A1, NAT_D:26;
A12: n > 1 by A1, A4, XREAL_1:163;
now
per cases ( m = 0 or m = 1 or ( m <> 0 & m <> 1 ) ) ;
suppose A13: m = 0 ; :: thesis: Crypto (Crypto m,n,k1),n,k2 = m
then m |^ k1 = 0 by A10, NAT_1:14, NEWTON:16;
then (m |^ k1) mod n = 0 by NAT_D:26;
then (Crypto m,n,k1) |^ k2 = 0 by A11, NAT_1:14, NEWTON:16;
hence Crypto (Crypto m,n,k1),n,k2 = m by A13, NAT_D:26; :: thesis: verum
end;
suppose A14: m = 1 ; :: thesis: Crypto (Crypto m,n,k1),n,k2 = m
then m |^ k1 = 1 by NEWTON:15;
then (m |^ k1) mod n = 1 by A12, NAT_D:14;
then (Crypto m,n,k1) |^ k2 = 1 by NEWTON:15;
hence Crypto (Crypto m,n,k1),n,k2 = m by A12, A14, NAT_D:14; :: thesis: verum
end;
suppose A15: ( m <> 0 & m <> 1 ) ; :: thesis: Crypto (Crypto m,n,k1),n,k2 = m
A16: 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
m |^ ((t * p1) * q1) >= 1 by A15, NAT_1:14, PREPOWER:19;
then (m |^ ((t * p1) * q1)) - 1 >= 1 - 1 by XREAL_1:11;
then reconsider a = (m |^ ((t * p1) * q1)) - 1 as Element of NAT by INT_1:16;
A17: q divides m * a
proof
now
per cases ( m gcd q = 1 or m gcd q <> 1 ) ;
suppose m gcd q = 1 ; :: thesis: q divides m * a
then A18: m,q are_relative_prime by INT_2:def 4;
m |^ (t * p1) <> 0 by A15, PREPOWER:12;
then ((m |^ (t * p1)) |^ (q1 + 1)) mod q = (m |^ (t * p1)) mod q by A1, A15, A18, EULER_2:32, EULER_2:34;
then (((m |^ (t * p1)) |^ q1) * (m |^ (t * p1))) mod q = (m |^ (t * p1)) mod q by NEWTON:11;
then ((m |^ (t * p1)) |^ q1) mod q = 1 by A4, A15, A18, Th11, EULER_2:32;
then (m |^ ((t * p1) * q1)) mod q = 1 by NEWTON:14;
then m |^ ((t * p1) * q1) = (q * ((m |^ ((t * p1) * q1)) div q)) + 1 by A6, NAT_D:2;
then q divides a by NAT_D:def 3;
hence q divides m * a by NAT_D:9; :: thesis: verum
end;
end;
end;
hence q divides m * a ; :: thesis: verum
end;
p divides m * a
proof
now
per cases ( m gcd p = 1 or m gcd p <> 1 ) ;
suppose m gcd p = 1 ; :: thesis: p divides m * a
then A19: m,p are_relative_prime by INT_2:def 4;
m |^ (t * q1) <> 0 by A15, PREPOWER:12;
then ((m |^ (t * q1)) |^ (p1 + 1)) mod p = (m |^ (t * q1)) mod p by A1, A15, A19, EULER_2:32, EULER_2:34;
then (((m |^ (t * q1)) |^ p1) * (m |^ (t * q1))) mod p = (m |^ (t * q1)) mod p by NEWTON:11;
then ((m |^ (t * q1)) |^ p1) mod p = 1 by A4, A15, A19, Th11, EULER_2:32;
then (m |^ ((t * q1) * p1)) mod p = 1 by NEWTON:14;
then m |^ ((t * p1) * q1) = (p * ((m |^ ((t * p1) * q1)) div p)) + 1 by A6, NAT_D:2;
then p divides a by NAT_D:def 3;
hence p divides m * a by NAT_D:9; :: thesis: verum
end;
end;
end;
hence p divides m * a ; :: thesis: verum
end;
then p * q divides m * a by A1, A17, Th4, INT_2:47;
then consider k being Nat such that
A20: 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:11 ;
then (m |^ (((t * p1) * q1) + 1)) - (m - m) = (n * k) + m by A1, A20, XCMPLX_1:37;
hence (m |^ (((t * p1) * q1) + 1)) mod n = m by A2, 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 A1, A7, A8, NAT_D:2
.= ((t * p1) * q1) + 1 ;
then (m |^ (k1 * k2)) mod n = m by A16;
then ((m |^ k1) |^ k2) mod n = m by NEWTON:14;
hence Crypto (Crypto m,n,k1),n,k2 = m by Th12; :: thesis: verum
end;
end;
end;
hence Crypto (Crypto m,n,k1),n,k2 = m ; :: thesis: verum