Theorem sqmid3api

Description: Value of the square of the middle term of a 3-term arithmetic progression. (Contributed by Steven Nguyen, 20-Sep-2022)

	Ref	Expression
Hypotheses	sqmid3api.a	|- A e. CC
	sqmid3api.n	|- N e. CC
	sqmid3api.b	|- ( A + N ) = B
	sqmid3api.c	|- ( B + N ) = C
Assertion	sqmid3api	|- ( B x. B ) = ( ( A x. C ) + ( N x. N ) )

Proof

Step	Hyp	Ref	Expression
1		sqmid3api.a	|- A e. CC
2		sqmid3api.n	|- N e. CC
3		sqmid3api.b	|- ( A + N ) = B
4		sqmid3api.c	|- ( B + N ) = C
5	1 2 1 2	muladdi	|- ( ( A + N ) x. ( A + N ) ) = ( ( ( A x. A ) + ( N x. N ) ) + ( ( A x. N ) + ( A x. N ) ) )
6	3 3	oveq12i	|- ( ( A + N ) x. ( A + N ) ) = ( B x. B )
7	1 1	mulcli	|- ( A x. A ) e. CC
8	2 2	mulcli	|- ( N x. N ) e. CC
9	1 2	mulcli	|- ( A x. N ) e. CC
10	9 9	addcli	|- ( ( A x. N ) + ( A x. N ) ) e. CC
11	7 8 10	add32i	|- ( ( ( A x. A ) + ( N x. N ) ) + ( ( A x. N ) + ( A x. N ) ) ) = ( ( ( A x. A ) + ( ( A x. N ) + ( A x. N ) ) ) + ( N x. N ) )
12	1 2	addcli	|- ( A + N ) e. CC
13	1 12 2	adddii	|- ( A x. ( ( A + N ) + N ) ) = ( ( A x. ( A + N ) ) + ( A x. N ) )
14	3	oveq1i	|- ( ( A + N ) + N ) = ( B + N )
15	14 4	eqtri	|- ( ( A + N ) + N ) = C
16	15	oveq2i	|- ( A x. ( ( A + N ) + N ) ) = ( A x. C )
17	1 1 2	adddii	|- ( A x. ( A + N ) ) = ( ( A x. A ) + ( A x. N ) )
18	17	oveq1i	|- ( ( A x. ( A + N ) ) + ( A x. N ) ) = ( ( ( A x. A ) + ( A x. N ) ) + ( A x. N ) )
19	7 9 9	addassi	|- ( ( ( A x. A ) + ( A x. N ) ) + ( A x. N ) ) = ( ( A x. A ) + ( ( A x. N ) + ( A x. N ) ) )
20	18 19	eqtri	|- ( ( A x. ( A + N ) ) + ( A x. N ) ) = ( ( A x. A ) + ( ( A x. N ) + ( A x. N ) ) )
21	13 16 20	3eqtr3ri	|- ( ( A x. A ) + ( ( A x. N ) + ( A x. N ) ) ) = ( A x. C )
22	21	oveq1i	|- ( ( ( A x. A ) + ( ( A x. N ) + ( A x. N ) ) ) + ( N x. N ) ) = ( ( A x. C ) + ( N x. N ) )
23	11 22	eqtri	|- ( ( ( A x. A ) + ( N x. N ) ) + ( ( A x. N ) + ( A x. N ) ) ) = ( ( A x. C ) + ( N x. N ) )
24	5 6 23	3eqtr3i	|- ( B x. B ) = ( ( A x. C ) + ( N x. N ) )