let p be Prime; for g2, a, b being Element of (GF p) st g2 = 2 mod p holds
(a - b) |^ 2 = ((a |^ 2) - ((g2 * a) * b)) + (b |^ 2)
let g2, a, b be Element of (GF p); ( g2 = 2 mod p implies (a - b) |^ 2 = ((a |^ 2) - ((g2 * a) * b)) + (b |^ 2) )
assume A1:
g2 = 2 mod p
; (a - b) |^ 2 = ((a |^ 2) - ((g2 * a) * b)) + (b |^ 2)
thus (a - b) |^ 2 =
(a - b) * (a - b)
by EC_PF_1:22
.=
(a * (a - b)) - (b * (a - b))
by VECTSP_1:13
.=
((a * a) - (a * b)) - (b * (a - b))
by VECTSP_1:11
.=
((a |^ 2) - (a * b)) - (b * (a - b))
by EC_PF_1:22
.=
((a |^ 2) - (a * b)) - ((b * a) - (b * b))
by VECTSP_1:11
.=
((a |^ 2) - (a * b)) - ((a * b) - (b |^ 2))
by EC_PF_1:22
.=
(a |^ 2) + ((- (a * b)) - ((a * b) - (b |^ 2)))
by ALGSTR_1:7
.=
(a |^ 2) + ((- (a * b)) + ((- (a * b)) + (b |^ 2)))
by VECTSP_1:17
.=
(a |^ 2) + (((- (a * b)) - (a * b)) + (b |^ 2))
by ALGSTR_1:7
.=
(a |^ 2) + ((g2 * (- (a * b))) + (b |^ 2))
by A1, Th20
.=
((a |^ 2) + (g2 * (- (a * b)))) + (b |^ 2)
by ALGSTR_1:7
.=
((a |^ 2) - (g2 * (a * b))) + (b |^ 2)
by VECTSP_1:8
.=
((a |^ 2) - ((g2 * a) * b)) + (b |^ 2)
by GROUP_1:def 3
; verum