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	⊢ 𝐴 ∈ ℂ
	sqmid3api.n	⊢ 𝑁 ∈ ℂ
	sqmid3api.b	⊢ ( 𝐴 + 𝑁 ) = 𝐵
	sqmid3api.c	⊢ ( 𝐵 + 𝑁 ) = 𝐶
Assertion	sqmid3api	⊢ ( 𝐵 · 𝐵 ) = ( ( 𝐴 · 𝐶 ) + ( 𝑁 · 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		sqmid3api.a	⊢ 𝐴 ∈ ℂ
2		sqmid3api.n	⊢ 𝑁 ∈ ℂ
3		sqmid3api.b	⊢ ( 𝐴 + 𝑁 ) = 𝐵
4		sqmid3api.c	⊢ ( 𝐵 + 𝑁 ) = 𝐶
5	1 2 1 2	muladdi	⊢ ( ( 𝐴 + 𝑁 ) · ( 𝐴 + 𝑁 ) ) = ( ( ( 𝐴 · 𝐴 ) + ( 𝑁 · 𝑁 ) ) + ( ( 𝐴 · 𝑁 ) + ( 𝐴 · 𝑁 ) ) )
6	3 3	oveq12i	⊢ ( ( 𝐴 + 𝑁 ) · ( 𝐴 + 𝑁 ) ) = ( 𝐵 · 𝐵 )
7	1 1	mulcli	⊢ ( 𝐴 · 𝐴 ) ∈ ℂ
8	2 2	mulcli	⊢ ( 𝑁 · 𝑁 ) ∈ ℂ
9	1 2	mulcli	⊢ ( 𝐴 · 𝑁 ) ∈ ℂ
10	9 9	addcli	⊢ ( ( 𝐴 · 𝑁 ) + ( 𝐴 · 𝑁 ) ) ∈ ℂ
11	7 8 10	add32i	⊢ ( ( ( 𝐴 · 𝐴 ) + ( 𝑁 · 𝑁 ) ) + ( ( 𝐴 · 𝑁 ) + ( 𝐴 · 𝑁 ) ) ) = ( ( ( 𝐴 · 𝐴 ) + ( ( 𝐴 · 𝑁 ) + ( 𝐴 · 𝑁 ) ) ) + ( 𝑁 · 𝑁 ) )
12	1 2	addcli	⊢ ( 𝐴 + 𝑁 ) ∈ ℂ
13	1 12 2	adddii	⊢ ( 𝐴 · ( ( 𝐴 + 𝑁 ) + 𝑁 ) ) = ( ( 𝐴 · ( 𝐴 + 𝑁 ) ) + ( 𝐴 · 𝑁 ) )
14	3	oveq1i	⊢ ( ( 𝐴 + 𝑁 ) + 𝑁 ) = ( 𝐵 + 𝑁 )
15	14 4	eqtri	⊢ ( ( 𝐴 + 𝑁 ) + 𝑁 ) = 𝐶
16	15	oveq2i	⊢ ( 𝐴 · ( ( 𝐴 + 𝑁 ) + 𝑁 ) ) = ( 𝐴 · 𝐶 )
17	1 1 2	adddii	⊢ ( 𝐴 · ( 𝐴 + 𝑁 ) ) = ( ( 𝐴 · 𝐴 ) + ( 𝐴 · 𝑁 ) )
18	17	oveq1i	⊢ ( ( 𝐴 · ( 𝐴 + 𝑁 ) ) + ( 𝐴 · 𝑁 ) ) = ( ( ( 𝐴 · 𝐴 ) + ( 𝐴 · 𝑁 ) ) + ( 𝐴 · 𝑁 ) )
19	7 9 9	addassi	⊢ ( ( ( 𝐴 · 𝐴 ) + ( 𝐴 · 𝑁 ) ) + ( 𝐴 · 𝑁 ) ) = ( ( 𝐴 · 𝐴 ) + ( ( 𝐴 · 𝑁 ) + ( 𝐴 · 𝑁 ) ) )
20	18 19	eqtri	⊢ ( ( 𝐴 · ( 𝐴 + 𝑁 ) ) + ( 𝐴 · 𝑁 ) ) = ( ( 𝐴 · 𝐴 ) + ( ( 𝐴 · 𝑁 ) + ( 𝐴 · 𝑁 ) ) )
21	13 16 20	3eqtr3ri	⊢ ( ( 𝐴 · 𝐴 ) + ( ( 𝐴 · 𝑁 ) + ( 𝐴 · 𝑁 ) ) ) = ( 𝐴 · 𝐶 )
22	21	oveq1i	⊢ ( ( ( 𝐴 · 𝐴 ) + ( ( 𝐴 · 𝑁 ) + ( 𝐴 · 𝑁 ) ) ) + ( 𝑁 · 𝑁 ) ) = ( ( 𝐴 · 𝐶 ) + ( 𝑁 · 𝑁 ) )
23	11 22	eqtri	⊢ ( ( ( 𝐴 · 𝐴 ) + ( 𝑁 · 𝑁 ) ) + ( ( 𝐴 · 𝑁 ) + ( 𝐴 · 𝑁 ) ) ) = ( ( 𝐴 · 𝐶 ) + ( 𝑁 · 𝑁 ) )
24	5 6 23	3eqtr3i	⊢ ( 𝐵 · 𝐵 ) = ( ( 𝐴 · 𝐶 ) + ( 𝑁 · 𝑁 ) )