let n be Nat; ( n mod 11 = 1 & n mod 2 = 1 implies n mod 22 = 1 )
assume A2:
( n mod 11 = 1 & n mod 2 = 1 )
; n mod 22 = 1
then A3:
( 11 divides n - 1 & 2 divides n - 1 )
by PEPIN:8;
a0:
n is odd
by A2, NAT_2:22;
then
2 * 11 divides n - 1
by INT_2:30, XPRIMES1:2, XPRIMES1:11, A3, PEPIN:4;
then B1:
(n - 1) mod 22 = 0
by a0, PEPIN:6;
then
(n - 1) mod 22 < 22 - 1
;
then
((n - 1) + 1) mod 22 = ((n - 1) mod 22) + 1
by a0, NAT_D:70;
hence
n mod 22 = 1
by B1; verum