a mod 4 < 3 + 1
by NAT_D:1;
then
a mod 4 <= 3
by NAT_1:13;
then
not not a mod 4 = 0 & ... & not a mod 4 = 3
;
then
( (a |^ 2) mod 4 = (0 |^ 2) mod 4 or (a |^ 2) mod 4 = (1 |^ 2) mod 4 or (a |^ 2) mod 4 = (2 |^ 2) mod 4 or (a |^ 2) mod 4 = (3 |^ 2) mod 4 )
by GR_CY_3:30;
then A1:
( (a |^ 2) mod 4 = 0 mod 4 or (a |^ 2) mod 4 = 1 mod 4 or (a |^ 2) mod 4 = (2 * 2) mod 4 or (a |^ 2) mod 4 = (3 * 3) mod 4 )
by NEWTON:81;
1 mod (1 + 3) = (1 * ((4 * 2) + 1)) mod 4
;
then
( (a |^ 2) mod 4 = 0 * 0 or (a |^ 2) mod 4 = 1 * 1 )
by A1;
hence
(a |^ 2) mod 4 is square
; verum