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 addlidi ⊢ ( 0 + ( 𝐵 · 𝐵 ) ) = ( 𝐵 · 𝐵 )
20 5 4 8 18 19 decaddi ⊢ ( ( 𝐴 · 𝐴 ) 0 0 + ( 𝐵 · 𝐵 ) ) = ( 𝐴 · 𝐴 ) 0 ( 𝐵 · 𝐵 )
21 eqid ⊢ ( 𝐵 · 𝐵 ) 0 0 = ( 𝐵 · 𝐵 ) 0 0
22 13 addlidi ⊢ ( 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 mullidi ⊢ ( 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 · ( ( 𝐴 · 𝐴 ) − ( 𝐵 · 𝐵 ) ) )