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