Metamath Proof Explorer

Theorem sqdeccom12

Description: The square of a number in terms of its digits switched. (Contributed by Steven Nguyen, 3-Jan-2023)

Ref Expression
Hypotheses sqdeccom12.a 
|- A e. NN0
sqdeccom12.b 
|- B e. NN0
Assertion sqdeccom12 
|- ( ( ; A B x. ; A B ) - ( ; B A x. ; B A ) ) = ( ; 9 9 x. ( ( A x. A ) - ( B x. B ) ) )

Proof

Step Hyp Ref Expression
1 sqdeccom12.a 
 |-  A e. NN0
2 sqdeccom12.b 
 |-  B e. NN0
3 1 1 nn0mulcli 
 |-  ( A x. A ) e. NN0
4 0nn0 
 |-  0 e. NN0
5 3 4 deccl 
 |-  ; ( A x. A ) 0 e. NN0
6 5 4 deccl 
 |-  ; ; ( A x. A ) 0 0 e. NN0
7 6 nn0cni 
 |-  ; ; ( A x. A ) 0 0 e. CC
8 2 2 nn0mulcli 
 |-  ( B x. B ) e. NN0
9 8 4 deccl 
 |-  ; ( B x. B ) 0 e. NN0
10 9 4 deccl 
 |-  ; ; ( B x. B ) 0 0 e. NN0
11 10 nn0cni 
 |-  ; ; ( B x. B ) 0 0 e. CC
12 1 nn0cni 
 |-  A e. CC
13 12 12 mulcli 
 |-  ( A x. A ) e. CC
14 2 nn0cni 
 |-  B e. CC
15 14 14 mulcli 
 |-  ( B x. B ) e. CC
16 subadd4 
 |-  ( ( ( ; ; ( A x. A ) 0 0 e. CC /\ ; ; ( B x. B ) 0 0 e. CC ) /\ ( ( A x. A ) e. CC /\ ( B x. B ) e. CC ) ) -> ( ( ; ; ( A x. A ) 0 0 - ; ; ( B x. B ) 0 0 ) - ( ( A x. A ) - ( B x. B ) ) ) = ( ( ; ; ( A x. A ) 0 0 + ( B x. B ) ) - ( ; ; ( B x. B ) 0 0 + ( A x. A ) ) ) )
17 7 11 13 15 16 mp4an 
 |-  ( ( ; ; ( A x. A ) 0 0 - ; ; ( B x. B ) 0 0 ) - ( ( A x. A ) - ( B x. B ) ) ) = ( ( ; ; ( A x. A ) 0 0 + ( B x. B ) ) - ( ; ; ( B x. B ) 0 0 + ( A x. A ) ) )
18 eqid 
 |-  ; ; ( A x. A ) 0 0 = ; ; ( A x. A ) 0 0
19 15 addid2i 
 |-  ( 0 + ( B x. B ) ) = ( B x. B )
20 5 4 8 18 19 decaddi 
 |-  ( ; ; ( A x. A ) 0 0 + ( B x. B ) ) = ; ; ( A x. A ) 0 ( B x. B )
21 eqid 
 |-  ; ; ( B x. B ) 0 0 = ; ; ( B x. B ) 0 0
22 13 addid2i 
 |-  ( 0 + ( A x. A ) ) = ( A x. A )
23 9 4 3 21 22 decaddi 
 |-  ( ; ; ( B x. B ) 0 0 + ( A x. A ) ) = ; ; ( B x. B ) 0 ( A x. A )
24 20 23 oveq12i 
 |-  ( ( ; ; ( A x. A ) 0 0 + ( B x. B ) ) - ( ; ; ( B x. B ) 0 0 + ( A x. A ) ) ) = ( ; ; ( A x. A ) 0 ( B x. B ) - ; ; ( B x. B ) 0 ( A x. A ) )
25 17 24 eqtr2i 
 |-  ( ; ; ( A x. A ) 0 ( B x. B ) - ; ; ( B x. B ) 0 ( A x. A ) ) = ( ( ; ; ( A x. A ) 0 0 - ; ; ( B x. B ) 0 0 ) - ( ( A x. A ) - ( B x. B ) ) )
26 eqid 
 |-  ; ; ( ( B x. B ) + ( A x. A ) ) ( ( ( A x. B ) + ( B x. A ) ) + 0 ) ( ( A x. A ) + ( B x. B ) ) = ; ; ( ( B x. B ) + ( A x. A ) ) ( ( ( A x. B ) + ( B x. A ) ) + 0 ) ( ( A x. A ) + ( B x. B ) )
27 2 1 nn0mulcli 
 |-  ( B x. A ) e. NN0
28 1 2 27 numcl 
 |-  ( ( A x. B ) + ( B x. A ) ) e. NN0
29 3 28 deccl 
 |-  ; ( A x. A ) ( ( A x. B ) + ( B x. A ) ) e. NN0
30 eqid 
 |-  ; ; ( A x. A ) ( ( A x. B ) + ( B x. A ) ) ( B x. B ) = ; ; ( A x. A ) ( ( A x. B ) + ( B x. A ) ) ( B x. B )
31 eqid 
 |-  ; ; ( B x. B ) 0 ( A x. A ) = ; ; ( B x. B ) 0 ( A x. A )
32 eqid 
 |-  ; ( A x. A ) ( ( A x. B ) + ( B x. A ) ) = ; ( A x. A ) ( ( A x. B ) + ( B x. A ) )
33 eqid 
 |-  ; ( B x. B ) 0 = ; ( B x. B ) 0
34 13 15 addcomi 
 |-  ( ( A x. A ) + ( B x. B ) ) = ( ( B x. B ) + ( A x. A ) )
35 eqid 
 |-  ( ( ( A x. B ) + ( B x. A ) ) + 0 ) = ( ( ( A x. B ) + ( B x. A ) ) + 0 )
36 3 28 8 4 32 33 34 35 decadd 
 |-  ( ; ( A x. A ) ( ( A x. B ) + ( B x. A ) ) + ; ( B x. B ) 0 ) = ; ( ( B x. B ) + ( A x. A ) ) ( ( ( A x. B ) + ( B x. A ) ) + 0 )
37 15 13 addcomi 
 |-  ( ( B x. B ) + ( A x. A ) ) = ( ( A x. A ) + ( B x. B ) )
38 29 8 9 3 30 31 36 37 decadd 
 |-  ( ; ; ( A x. A ) ( ( A x. B ) + ( B x. A ) ) ( B x. B ) + ; ; ( B x. B ) 0 ( A x. A ) ) = ; ; ( ( B x. B ) + ( A x. A ) ) ( ( ( A x. B ) + ( B x. A ) ) + 0 ) ( ( A x. A ) + ( B x. B ) )
39 8 28 deccl 
 |-  ; ( B x. B ) ( ( A x. B ) + ( B x. A ) ) e. NN0
40 eqid 
 |-  ; ; ( B x. B ) ( ( A x. B ) + ( B x. A ) ) ( A x. A ) = ; ; ( B x. B ) ( ( A x. B ) + ( B x. A ) ) ( A x. A )
41 eqid 
 |-  ; ; ( A x. A ) 0 ( B x. B ) = ; ; ( A x. A ) 0 ( B x. B )
42 eqid 
 |-  ; ( B x. B ) ( ( A x. B ) + ( B x. A ) ) = ; ( B x. B ) ( ( A x. B ) + ( B x. A ) )
43 eqid 
 |-  ; ( A x. A ) 0 = ; ( A x. A ) 0
44 eqid 
 |-  ( ( B x. B ) + ( A x. A ) ) = ( ( B x. B ) + ( A x. A ) )
45 8 28 3 4 42 43 44 35 decadd 
 |-  ( ; ( B x. B ) ( ( A x. B ) + ( B x. A ) ) + ; ( A x. A ) 0 ) = ; ( ( B x. B ) + ( A x. A ) ) ( ( ( A x. B ) + ( B x. A ) ) + 0 )
46 eqid 
 |-  ( ( A x. A ) + ( B x. B ) ) = ( ( A x. A ) + ( B x. B ) )
47 39 3 5 8 40 41 45 46 decadd 
 |-  ( ; ; ( B x. B ) ( ( A x. B ) + ( B x. A ) ) ( A x. A ) + ; ; ( A x. A ) 0 ( B x. B ) ) = ; ; ( ( B x. B ) + ( A x. A ) ) ( ( ( A x. B ) + ( B x. A ) ) + 0 ) ( ( A x. A ) + ( B x. B ) )
48 26 38 47 3eqtr4i 
 |-  ( ; ; ( A x. A ) ( ( A x. B ) + ( B x. A ) ) ( B x. B ) + ; ; ( B x. B ) 0 ( A x. A ) ) = ( ; ; ( B x. B ) ( ( A x. B ) + ( B x. A ) ) ( A x. A ) + ; ; ( A x. A ) 0 ( B x. B ) )
49 29 8 deccl 
 |-  ; ; ( A x. A ) ( ( A x. B ) + ( B x. A ) ) ( B x. B ) e. NN0
50 49 nn0cni 
 |-  ; ; ( A x. A ) ( ( A x. B ) + ( B x. A ) ) ( B x. B ) e. CC
51 9 3 deccl 
 |-  ; ; ( B x. B ) 0 ( A x. A ) e. NN0
52 51 nn0cni 
 |-  ; ; ( B x. B ) 0 ( A x. A ) e. CC
53 39 3 deccl 
 |-  ; ; ( B x. B ) ( ( A x. B ) + ( B x. A ) ) ( A x. A ) e. NN0
54 53 nn0cni 
 |-  ; ; ( B x. B ) ( ( A x. B ) + ( B x. A ) ) ( A x. A ) e. CC
55 5 8 deccl 
 |-  ; ; ( A x. A ) 0 ( B x. B ) e. NN0
56 55 nn0cni 
 |-  ; ; ( A x. A ) 0 ( B x. B ) e. CC
57 addsubeq4com 
 |-  ( ( ( ; ; ( A x. A ) ( ( A x. B ) + ( B x. A ) ) ( B x. B ) e. CC /\ ; ; ( B x. B ) 0 ( A x. A ) e. CC ) /\ ( ; ; ( B x. B ) ( ( A x. B ) + ( B x. A ) ) ( A x. A ) e. CC /\ ; ; ( A x. A ) 0 ( B x. B ) e. CC ) ) -> ( ( ; ; ( A x. A ) ( ( A x. B ) + ( B x. A ) ) ( B x. B ) + ; ; ( B x. B ) 0 ( A x. A ) ) = ( ; ; ( B x. B ) ( ( A x. B ) + ( B x. A ) ) ( A x. A ) + ; ; ( A x. A ) 0 ( B x. B ) ) <-> ( ; ; ( A x. A ) ( ( A x. B ) + ( B x. A ) ) ( B x. B ) - ; ; ( B x. B ) ( ( A x. B ) + ( B x. A ) ) ( A x. A ) ) = ( ; ; ( A x. A ) 0 ( B x. B ) - ; ; ( B x. B ) 0 ( A x. A ) ) ) )
58 50 52 54 56 57 mp4an 
 |-  ( ( ; ; ( A x. A ) ( ( A x. B ) + ( B x. A ) ) ( B x. B ) + ; ; ( B x. B ) 0 ( A x. A ) ) = ( ; ; ( B x. B ) ( ( A x. B ) + ( B x. A ) ) ( A x. A ) + ; ; ( A x. A ) 0 ( B x. B ) ) <-> ( ; ; ( A x. A ) ( ( A x. B ) + ( B x. A ) ) ( B x. B ) - ; ; ( B x. B ) ( ( A x. B ) + ( B x. A ) ) ( A x. A ) ) = ( ; ; ( A x. A ) 0 ( B x. B ) - ; ; ( B x. B ) 0 ( A x. A ) ) )
59 48 58 mpbi 
 |-  ( ; ; ( A x. A ) ( ( A x. B ) + ( B x. A ) ) ( B x. B ) - ; ; ( B x. B ) ( ( A x. B ) + ( B x. A ) ) ( A x. A ) ) = ( ; ; ( A x. A ) 0 ( B x. B ) - ; ; ( B x. B ) 0 ( A x. A ) )
60 10nn0 
 |-  ; 1 0 e. NN0
61 60 4 deccl 
 |-  ; ; 1 0 0 e. NN0
62 61 nn0cni 
 |-  ; ; 1 0 0 e. CC
63 ax-1cn 
 |-  1 e. CC
64 13 15 subcli 
 |-  ( ( A x. A ) - ( B x. B ) ) e. CC
65 62 63 64 subdiri 
 |-  ( ( ; ; 1 0 0 - 1 ) x. ( ( A x. A ) - ( B x. B ) ) ) = ( ( ; ; 1 0 0 x. ( ( A x. A ) - ( B x. B ) ) ) - ( 1 x. ( ( A x. A ) - ( B x. B ) ) ) )
66 62 13 15 subdii 
 |-  ( ; ; 1 0 0 x. ( ( A x. A ) - ( B x. B ) ) ) = ( ( ; ; 1 0 0 x. ( A x. A ) ) - ( ; ; 1 0 0 x. ( B x. B ) ) )
67 eqid 
 |-  ; ; 1 0 0 = ; ; 1 0 0
68 3 dec0u 
 |-  ( ; 1 0 x. ( A x. A ) ) = ; ( A x. A ) 0
69 13 mul02i 
 |-  ( 0 x. ( A x. A ) ) = 0
70 3 60 4 67 68 69 decmul1 
 |-  ( ; ; 1 0 0 x. ( A x. A ) ) = ; ; ( A x. A ) 0 0
71 8 dec0u 
 |-  ( ; 1 0 x. ( B x. B ) ) = ; ( B x. B ) 0
72 15 mul02i 
 |-  ( 0 x. ( B x. B ) ) = 0
73 8 60 4 67 71 72 decmul1 
 |-  ( ; ; 1 0 0 x. ( B x. B ) ) = ; ; ( B x. B ) 0 0
74 70 73 oveq12i 
 |-  ( ( ; ; 1 0 0 x. ( A x. A ) ) - ( ; ; 1 0 0 x. ( B x. B ) ) ) = ( ; ; ( A x. A ) 0 0 - ; ; ( B x. B ) 0 0 )
75 66 74 eqtri 
 |-  ( ; ; 1 0 0 x. ( ( A x. A ) - ( B x. B ) ) ) = ( ; ; ( A x. A ) 0 0 - ; ; ( B x. B ) 0 0 )
76 64 mulid2i 
 |-  ( 1 x. ( ( A x. A ) - ( B x. B ) ) ) = ( ( A x. A ) - ( B x. B ) )
77 75 76 oveq12i 
 |-  ( ( ; ; 1 0 0 x. ( ( A x. A ) - ( B x. B ) ) ) - ( 1 x. ( ( A x. A ) - ( B x. B ) ) ) ) = ( ( ; ; ( A x. A ) 0 0 - ; ; ( B x. B ) 0 0 ) - ( ( A x. A ) - ( B x. B ) ) )
78 65 77 eqtri 
 |-  ( ( ; ; 1 0 0 - 1 ) x. ( ( A x. A ) - ( B x. B ) ) ) = ( ( ; ; ( A x. A ) 0 0 - ; ; ( B x. B ) 0 0 ) - ( ( A x. A ) - ( B x. B ) ) )
79 25 59 78 3eqtr4i 
 |-  ( ; ; ( A x. A ) ( ( A x. B ) + ( B x. A ) ) ( B x. B ) - ; ; ( B x. B ) ( ( A x. B ) + ( B x. A ) ) ( A x. A ) ) = ( ( ; ; 1 0 0 - 1 ) x. ( ( A x. A ) - ( B x. B ) ) )
80 eqid 
 |-  ( A x. A ) = ( A x. A )
81 eqid 
 |-  ( ( A x. B ) + ( B x. A ) ) = ( ( A x. B ) + ( B x. A ) )
82 eqid 
 |-  ( B x. B ) = ( B x. B )
83 1 2 1 2 80 81 82 decpmulnc 
 |-  ( ; A B x. ; A B ) = ; ; ( A x. A ) ( ( A x. B ) + ( B x. A ) ) ( B x. B )
84 14 12 mulcli 
 |-  ( B x. A ) e. CC
85 12 14 mulcli 
 |-  ( A x. B ) e. CC
86 84 85 addcomi 
 |-  ( ( B x. A ) + ( A x. B ) ) = ( ( A x. B ) + ( B x. A ) )
87 2 1 2 1 82 86 80 decpmulnc 
 |-  ( ; B A x. ; B A ) = ; ; ( B x. B ) ( ( A x. B ) + ( B x. A ) ) ( A x. A )
88 83 87 oveq12i 
 |-  ( ( ; A B x. ; A B ) - ( ; B A x. ; B A ) ) = ( ; ; ( A x. A ) ( ( A x. B ) + ( B x. A ) ) ( B x. B ) - ; ; ( B x. B ) ( ( A x. B ) + ( B x. A ) ) ( A x. A ) )
89 9nn0 
 |-  9 e. NN0
90 89 89 deccl 
 |-  ; 9 9 e. NN0
91 90 nn0cni 
 |-  ; 9 9 e. CC
92 9p1e10 
 |-  ( 9 + 1 ) = ; 1 0
93 eqid 
 |-  ; 9 9 = ; 9 9
94 89 92 93 decsucc 
 |-  ( ; 9 9 + 1 ) = ; ; 1 0 0
95 91 63 94 addcomli 
 |-  ( 1 + ; 9 9 ) = ; ; 1 0 0
96 63 91 95 mvlladdi 
 |-  ; 9 9 = ( ; ; 1 0 0 - 1 )
97 96 oveq1i 
 |-  ( ; 9 9 x. ( ( A x. A ) - ( B x. B ) ) ) = ( ( ; ; 1 0 0 - 1 ) x. ( ( A x. A ) - ( B x. B ) ) )
98 79 88 97 3eqtr4i 
 |-  ( ( ; A B x. ; A B ) - ( ; B A x. ; B A ) ) = ( ; 9 9 x. ( ( A x. A ) - ( B x. B ) ) )