Theorem sq3deccom12

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

	Ref	Expression
Hypotheses	sqdeccom12.a	|- A e. NN0
	sqdeccom12.b	|- B e. NN0
	sq3deccom12.c	|- C e. NN0
	sq3deccom12.d	|- ( A + C ) = D
Assertion	sq3deccom12	|- ( ( ; ; A B C x. ; ; A B C ) - ( ; D B x. ; D B ) ) = ( ; 9 9 x. ( ( ; A B x. ; A B ) - ( C x. C ) ) )

Proof

Step	Hyp	Ref	Expression
1		sqdeccom12.a	|- A e. NN0
2		sqdeccom12.b	|- B e. NN0
3		sq3deccom12.c	|- C e. NN0
4		sq3deccom12.d	|- ( A + C ) = D
5		0nn0	|- 0 e. NN0
6		eqid	|- ; C 0 = ; C 0
7		eqid	|- ; A B = ; A B
8	1	nn0cni	|- A e. CC
9	3	nn0cni	|- C e. CC
10	8 9 4	addcomli	|- ( C + A ) = D
11	2	nn0cni	|- B e. CC
12	11	addlidi	|- ( 0 + B ) = B
13	3 5 1 2 6 7 10 12	decadd	|- ( ; C 0 + ; A B ) = ; D B
14	1 2	deccl	|- ; A B e. NN0
15	14	nn0cni	|- ; A B e. CC
16	15	addlidi	|- ( 0 + ; A B ) = ; A B
17	3 5 14 6 16	decaddi	|- ( ; C 0 + ; A B ) = ; C ; A B
18	13 17	eqtr3i	|- ; D B = ; C ; A B
19	18 18	oveq12i	|- ( ; D B x. ; D B ) = ( ; C ; A B x. ; C ; A B )
20	19	oveq2i	|- ( ( ; ; A B C x. ; ; A B C ) - ( ; D B x. ; D B ) ) = ( ( ; ; A B C x. ; ; A B C ) - ( ; C ; A B x. ; C ; A B ) )
21	14 3	sqdeccom12	|- ( ( ; ; A B C x. ; ; A B C ) - ( ; C ; A B x. ; C ; A B ) ) = ( ; 9 9 x. ( ( ; A B x. ; A B ) - ( C x. C ) ) )
22	20 21	eqtri	|- ( ( ; ; A B C x. ; ; A B C ) - ( ; D B x. ; D B ) ) = ( ; 9 9 x. ( ( ; A B x. ; A B ) - ( C x. C ) ) )