let a, b be odd Nat; :: thesis: ( 4 divides a + b iff not 4 divides a - b )

( a + b is even & a - b is even ) ;

then ( 2 divides a + b & 2 divides a - b ) ;

then consider t, z being Integer such that

A3: ( a + b = 2 * t & a - b = 2 * z ) ;

A5: ( t is odd iff z is even ) A6: 2 * (2 gcd z) = |.2.| * (2 gcd z)

.= (2 * 2) gcd (2 * z) by INT_6:16 ;

A7: ( 2 * 2 divides a + b implies not 2 * 2 divides a - b )

( a + b is even & a - b is even ) ;

then ( 2 divides a + b & 2 divides a - b ) ;

then consider t, z being Integer such that

A3: ( a + b = 2 * t & a - b = 2 * z ) ;

A5: ( t is odd iff z is even ) A6: 2 * (2 gcd z) = |.2.| * (2 gcd z)

.= (2 * 2) gcd (2 * z) by INT_6:16 ;

A7: ( 2 * 2 divides a + b implies not 2 * 2 divides a - b )

proof

( not 2 * 2 divides a + b implies 2 * 2 divides a - b )
assume
2 * 2 divides a + b
; :: thesis: not 2 * 2 divides a - b

then |.(2 * 2).| = (2 * 2) gcd (2 * t) by A3, Th3

.= |.2.| * (t gcd 2) by INT_6:16 ;

then (2 * 2) gcd (2 * z) <> |.4.| by A5, A6, Th3;

hence not 2 * 2 divides a - b by A3, Th3; :: thesis: verum

end;then |.(2 * 2).| = (2 * 2) gcd (2 * t) by A3, Th3

.= |.2.| * (t gcd 2) by INT_6:16 ;

then (2 * 2) gcd (2 * z) <> |.4.| by A5, A6, Th3;

hence not 2 * 2 divides a - b by A3, Th3; :: thesis: verum

proof

hence
( 4 divides a + b iff not 4 divides a - b )
by A7; :: thesis: verum
assume
not 2 * 2 divides a + b
; :: thesis: 2 * 2 divides a - b

then not |.(2 * 2).| = (2 * 2) gcd (2 * t) by A3, Th3;

then not |.(2 * 2).| = |.2.| * (t gcd 2) by INT_6:16;

then (2 * 2) gcd (2 * z) = |.4.| by A5, A6, Th3;

hence 2 * 2 divides a - b by A3, Th3; :: thesis: verum

end;then not |.(2 * 2).| = (2 * 2) gcd (2 * t) by A3, Th3;

then not |.(2 * 2).| = |.2.| * (t gcd 2) by INT_6:16;

then (2 * 2) gcd (2 * z) = |.4.| by A5, A6, Th3;

hence 2 * 2 divides a - b by A3, Th3; :: thesis: verum