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 · ( ( ; 𝐴 𝐵 · ; 𝐴 𝐵 ) − ( 𝐶 · 𝐶 ) ) )