This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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