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 𝐴 ∈ ℕ0
sqdeccom12.b 𝐵 ∈ ℕ0
Assertion sqdeccom12 ( ( 𝐴 𝐵 · 𝐴 𝐵 ) − ( 𝐵 𝐴 · 𝐵 𝐴 ) ) = ( 9 9 · ( ( 𝐴 · 𝐴 ) − ( 𝐵 · 𝐵 ) ) )

Proof

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