Metamath Proof Explorer


Theorem sq3deccom12

Description: Variant of sqdeccom12 with a three digit square. (Contributed by Steven Nguyen, 3-Jan-2023)

Ref Expression
Hypotheses sqdeccom12.a 𝐴 ∈ ℕ0
sqdeccom12.b 𝐵 ∈ ℕ0
sq3deccom12.c 𝐶 ∈ ℕ0
sq3deccom12.d ( 𝐴 + 𝐶 ) = 𝐷
Assertion sq3deccom12 ( ( 𝐴 𝐵 𝐶 · 𝐴 𝐵 𝐶 ) − ( 𝐷 𝐵 · 𝐷 𝐵 ) ) = ( 9 9 · ( ( 𝐴 𝐵 · 𝐴 𝐵 ) − ( 𝐶 · 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 sqdeccom12.a 𝐴 ∈ ℕ0
2 sqdeccom12.b 𝐵 ∈ ℕ0
3 sq3deccom12.c 𝐶 ∈ ℕ0
4 sq3deccom12.d ( 𝐴 + 𝐶 ) = 𝐷
5 0nn0 0 ∈ ℕ0
6 eqid 𝐶 0 = 𝐶 0
7 eqid 𝐴 𝐵 = 𝐴 𝐵
8 1 nn0cni 𝐴 ∈ ℂ
9 3 nn0cni 𝐶 ∈ ℂ
10 8 9 4 addcomli ( 𝐶 + 𝐴 ) = 𝐷
11 2 nn0cni 𝐵 ∈ ℂ
12 11 addid2i ( 0 + 𝐵 ) = 𝐵
13 3 5 1 2 6 7 10 12 decadd ( 𝐶 0 + 𝐴 𝐵 ) = 𝐷 𝐵
14 1 2 deccl 𝐴 𝐵 ∈ ℕ0
15 14 nn0cni 𝐴 𝐵 ∈ ℂ
16 15 addid2i ( 0 + 𝐴 𝐵 ) = 𝐴 𝐵
17 3 5 14 6 16 decaddi ( 𝐶 0 + 𝐴 𝐵 ) = 𝐶 𝐴 𝐵
18 13 17 eqtr3i 𝐷 𝐵 = 𝐶 𝐴 𝐵
19 18 18 oveq12i ( 𝐷 𝐵 · 𝐷 𝐵 ) = ( 𝐶 𝐴 𝐵 · 𝐶 𝐴 𝐵 )
20 19 oveq2i ( ( 𝐴 𝐵 𝐶 · 𝐴 𝐵 𝐶 ) − ( 𝐷 𝐵 · 𝐷 𝐵 ) ) = ( ( 𝐴 𝐵 𝐶 · 𝐴 𝐵 𝐶 ) − ( 𝐶 𝐴 𝐵 · 𝐶 𝐴 𝐵 ) )
21 14 3 sqdeccom12 ( ( 𝐴 𝐵 𝐶 · 𝐴 𝐵 𝐶 ) − ( 𝐶 𝐴 𝐵 · 𝐶 𝐴 𝐵 ) ) = ( 9 9 · ( ( 𝐴 𝐵 · 𝐴 𝐵 ) − ( 𝐶 · 𝐶 ) ) )
22 20 21 eqtri ( ( 𝐴 𝐵 𝐶 · 𝐴 𝐵 𝐶 ) − ( 𝐷 𝐵 · 𝐷 𝐵 ) ) = ( 9 9 · ( ( 𝐴 𝐵 · 𝐴 𝐵 ) − ( 𝐶 · 𝐶 ) ) )