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\in {\mathbb{N}}_0$$
	sqdeccom12.b	$$⊢B\in {\mathbb{N}}_0$$
Assertion	sqdeccom12	Could not format assertion : No typesetting found for |- ( ( ; A B x. ; A B ) - ( ; B A x. ; B A ) ) = ( ; 9 9 x. ( ( A x. A ) - ( B x. B ) ) ) with typecode |-

Proof

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