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\in ℂ$$
	sqmid3api.n	$$⊢N\in ℂ$$
	sqmid3api.b	$$⊢A+N=B$$
	sqmid3api.c	$$⊢B+N=C$$
Assertion	sqmid3api	$$⊢BB=AC+\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$

Proof

Step	Hyp	Ref	Expression
1		sqmid3api.a	$$⊢A\in ℂ$$
2		sqmid3api.n	$$⊢N\in ℂ$$
3		sqmid3api.b	$$⊢A+N=B$$
4		sqmid3api.c	$$⊢B+N=C$$
5	1 2 1 2	muladdi	$$⊢\left(A+N\right)\left(A+N\right)=AA+\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
6	3 3	oveq12i	$$⊢\left(A+N\right)\left(A+N\right)=BB$$
7	1 1	mulcli	$$⊢AA\in ℂ$$
8	2 2	mulcli	$$⊢\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ$$
9	1 2	mulcli	$$⊢A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ$$
10	9 9	addcli	$$⊢A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ$$
11	7 8 10	add32i	$$⊢AA+\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=AA+\left(A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)+\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
12	1 2	addcli	$$⊢A+N\in ℂ$$
13	1 12 2	adddii	$$⊢A\left(A+N+N\right)=A\left(A+N\right)+A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
14	3	oveq1i	$$⊢A+N+N=B+N$$
15	14 4	eqtri	$$⊢A+N+N=C$$
16	15	oveq2i	$$⊢A\left(A+N+N\right)=AC$$
17	1 1 2	adddii	$$⊢A\left(A+N\right)=AA+A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
18	17	oveq1i	$$⊢A\left(A+N\right)+A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=AA+A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
19	7 9 9	addassi	$$⊢AA+A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=AA+A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
20	18 19	eqtri	$$⊢A\left(A+N\right)+A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=AA+A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
21	13 16 20	3eqtr3ri	$$⊢AA+A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=AC$$
22	21	oveq1i	$$⊢AA+\left(A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)+\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=AC+\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
23	11 22	eqtri	$$⊢AA+\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+A\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=AC+\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
24	5 6 23	3eqtr3i	$$⊢BB=AC+\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$