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 0
sqdeccom12.b B 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 0
2 sqdeccom12.b B 0
3 1 1 nn0mulcli A A 0
4 0nn0 0 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 B B 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
13 12 12 mulcli A A
14 2 nn0cni B
15 14 14 mulcli B B
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 + B B = B B
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 + A A = A A
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 B A 0
28 1 2 27 numcl A B + B A 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 A A + B B = B B + A A
35 eqid A B + B A + 0 = A B + B A + 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 B B + A A = A A + B B
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 B B + A A = B B + A A
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 A A + B B = A A + B B
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 0
61 60 4 deccl 100 0
62 61 nn0cni 100
63 ax-1cn 1
64 13 15 subcli A A B B
65 62 63 64 subdiri 100 1 A A B B = 100 A A B B 1 A A B B
66 62 13 15 subdii 100 A A B B = 100 A A 100 B B
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 A A = 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 B B = 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 A A B B = A A B B
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 A A = A A
81 eqid A B + B A = A B + B A
82 eqid B B = B B
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 B A
85 12 14 mulcli A B
86 84 85 addcomi B A + A B = A B + B A
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 0
90 89 89 deccl 99 0
91 90 nn0cni 99
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 A A B B = 100 1 A A B B
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 |-