Theorem sq3deccom12

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

	Ref	Expression
Hypotheses	sqdeccom12.a	$$⊢A\in {\mathbb{N}}_0$$
	sqdeccom12.b	$$⊢B\in {\mathbb{N}}_0$$
	sq3deccom12.c	$$⊢C\in {\mathbb{N}}_0$$
	sq3deccom12.d	$$⊢A+C=D$$
Assertion	sq3deccom12	Could not format assertion : No typesetting found for |- ( ( ; ; A B C x. ; ; A B C ) - ( ; D B x. ; D B ) ) = ( ; 9 9 x. ( ( ; A B x. ; A B ) - ( C x. C ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		sqdeccom12.a	$$⊢A\in {\mathbb{N}}_0$$
2		sqdeccom12.b	$$⊢B\in {\mathbb{N}}_0$$
3		sq3deccom12.c	$$⊢C\in {\mathbb{N}}_0$$
4		sq3deccom12.d	$$⊢A+C=D$$
5		0nn0	$$⊢0\in {\mathbb{N}}_0$$
6		eqid	Could not format ; C 0 = ; C 0 : No typesetting found for |- ; C 0 = ; C 0 with typecode |-
7		eqid	Could not format ; A B = ; A B : No typesetting found for |- ; A B = ; A B with typecode |-
8	1	nn0cni	$$⊢A\in ℂ$$
9	3	nn0cni	$$⊢C\in ℂ$$
10	8 9 4	addcomli	$$⊢C+A=D$$
11	2	nn0cni	$$⊢B\in ℂ$$
12	11	addlidi	$$⊢0+B=B$$
13	3 5 1 2 6 7 10 12	decadd	Could not format ( ; C 0 + ; A B ) = ; D B : No typesetting found for |- ( ; C 0 + ; A B ) = ; D B with typecode |-
14	1 2	deccl	Could not format ; A B e. NN0 : No typesetting found for |- ; A B e. NN0 with typecode |-
15	14	nn0cni	Could not format ; A B e. CC : No typesetting found for |- ; A B e. CC with typecode |-
16	15	addlidi	Could not format ( 0 + ; A B ) = ; A B : No typesetting found for |- ( 0 + ; A B ) = ; A B with typecode |-
17	3 5 14 6 16	decaddi	Could not format ( ; C 0 + ; A B ) = ; C ; A B : No typesetting found for |- ( ; C 0 + ; A B ) = ; C ; A B with typecode |-
18	13 17	eqtr3i	Could not format ; D B = ; C ; A B : No typesetting found for |- ; D B = ; C ; A B with typecode |-
19	18 18	oveq12i	Could not format ( ; D B x. ; D B ) = ( ; C ; A B x. ; C ; A B ) : No typesetting found for |- ( ; D B x. ; D B ) = ( ; C ; A B x. ; C ; A B ) with typecode |-
20	19	oveq2i	Could not format ( ( ; ; 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 ) ) : No typesetting found for |- ( ( ; ; 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 ) ) with typecode |-
21	14 3	sqdeccom12	Could not format ( ( ; ; 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 ) ) ) : No typesetting found for |- ( ( ; ; 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 ) ) ) with typecode |-
22	20 21	eqtri	Could not format ( ( ; ; A B C x. ; ; A B C ) - ( ; D B x. ; D B ) ) = ( ; 9 9 x. ( ( ; A B x. ; A B ) - ( C x. C ) ) ) : No typesetting found for |- ( ( ; ; A B C x. ; ; A B C ) - ( ; D B x. ; D B ) ) = ( ; 9 9 x. ( ( ; A B x. ; A B ) - ( C x. C ) ) ) with typecode |-