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:def 7
.=
((a * a) + (a * b)) + (b * (a + b))
by VECTSP_1:def 7
.=
((a |^ 2) + (a * b)) + (b * (a + b))
by EC_PF_1:22
.=
((a |^ 2) + (a * b)) + ((b * a) + (b * b))
by VECTSP_1:def 7
.=
((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 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 GROUP_1:def 3
; verum