This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 addlidi ⊢ ( 0 + 𝐵 ) = 𝐵
13 3 5 1 2 6 7 10 12 decadd ⊢ ( 𝐶 0 + 𝐴 𝐵 ) = 𝐷 𝐵
14 1 2 deccl ⊢ 𝐴 𝐵 ∈ ℕ0
15 14 nn0cni ⊢ 𝐴 𝐵 ∈ ℂ
16 15 addlidi ⊢ ( 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 · ( ( 𝐴 𝐵 · 𝐴 𝐵 ) − ( 𝐶 · 𝐶 ) ) )