let a, b be Integer; :: thesis: for p being odd prime Nat st not p divides b & p divides a - b holds
not p divides a + b
let p be odd prime Nat; :: thesis: ( not p divides b & p divides a - b implies not p divides a + b )
assume A1: not p divides b ; :: thesis: ( not p divides a - b or not p divides a + b )
p gcd 2 = 1 by Def3;
then not p divides 2 by INT_2:28, PEPIN:2, PYTHTRIP:def 2;
then A2: not p divides 2 * b by A1, INT_5:7;
assume p divides a - b ; :: thesis: not p divides a + b
then not p divides (a - b) + (2 * b) by A2, INT_2:1;
hence not p divides a + b ; :: thesis: verum