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 · ( ( 𝐴 · 𝐴 ) − ( 𝐵 · 𝐵 ) ) )