let k be Nat; :: thesis: ( k >= 1 implies (30 * k) + 7 is not_representable_by_sum_or_difference_of_two_primes )
assume AA: k >= 1 ; :: thesis: (30 * k) + 7 is not_representable_by_sum_or_difference_of_two_primes
assume not (30 * k) + 7 is not_representable_by_sum_or_difference_of_two_primes ; :: thesis: contradiction
then consider p, q being Prime such that
A1: ( (30 * k) + 7 = p + q or (30 * k) + 7 = p - q ) ;
( p is even or q is even ) by A1, Lemma30kOdd;

per cases then ( q = 2 or p = 2 ) by INT_2:def 4, ABIAN:def 1;

suppose S1: q = 2 ; :: thesis: contradiction

per cases ( (30 * k) + 7 = p + q or (30 * k) + 7 = p - q ) by A1;

suppose ss: (30 * k) + 7 = p + q ; :: thesis: contradiction

then p = 5 * ((6 * k) + 1) by S1;
then 5 divides p ;
then p = 5 by INT_2:def 4;
then k = 0 by S1, ss;
hence contradiction by AA; :: thesis: verum

end;

suppose ss: (30 * k) + 7 = p - q ; :: thesis: contradiction

then p = 3 * ((10 * k) + 3) by S1;
then 3 divides p ;
then s0: p = 3 by INT_2:def 4;
10 * k >= 10 * 1 by AA, XREAL_1:66;
then (10 * k) + 3 >= (10 * 1) + 3 by XREAL_1:6;
hence contradiction by s0, ss, S1; :: thesis: verum

end;

end;

end;

suppose S1: p = 2 ; :: thesis: contradiction

per cases ( (30 * k) + 7 = p + q or (30 * k) + 7 = p - q ) by A1;

suppose s0: (30 * k) + 7 = p + q ; :: thesis: contradiction

then q = 5 * ((6 * k) + 1) by S1;
then 5 divides q ;
then q = 5 by INT_2:def 4;
then k = 0 by s0, S1;
hence contradiction by AA; :: thesis: verum

end;

suppose (30 * k) + 7 = p - q ; :: thesis: contradiction

then - q = (30 * k) + 5 by S1;
hence contradiction ; :: thesis: verum

end;

end;

end;

end;