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 A 0
sqdeccom12.b B 0
sq3deccom12.c C 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 0
2 sqdeccom12.b B 0
3 sq3deccom12.c C 0
4 sq3deccom12.d A + C = D
5 0nn0 0 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
9 3 nn0cni C
10 8 9 4 addcomli C + A = D
11 2 nn0cni B
12 11 addid2i 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 addid2i 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 |-