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 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 addid2i
 |-  ( 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 addid2i
 |-  ( 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 ) ) )