Step Hyp Ref
Expression 1 oveq1 6303 . . . 4
2 1 oveq1d 6311 . . 3
3 oveq1 6303 . . 3
4 2 , 3 eqeq12d 2479 . 2
5 oveq1 6303 . . . 4
6 5 oveq1d 6311 . . 3
7 oveq1 6303 . . 3
8 6 , 7 eqeq12d 2479 . 2
9 xmulcl 11494 . . 3
10 xmulcl 11494 . . 3
11 9 , 10 stoic3 1609 . 2
12 simp1 996 . . 3
13 xmulcl 11494 . . . 4
14 13 3adant1 1014 . . 3
15 xmulcl 11494 . . 3
16 12 , 14 , 15 syl2anc 661 . 2
17 oveq2 6304 . . . . 5
18 17 oveq1d 6311 . . . 4
19 oveq1 6303 . . . . 5
20 19 oveq2d 6312 . . . 4
21 18 , 20 eqeq12d 2479 . . 3
22 oveq2 6304 . . . . 5
23 22 oveq1d 6311 . . . 4
24 oveq1 6303 . . . . 5
25 24 oveq2d 6312 . . . 4
26 23 , 25 eqeq12d 2479 . . 3
27 simprl 756 . . . . 5
28 simpl2 1000 . . . . 5
29 xmulcl 11494 . . . . 5
30 27 , 28 , 29 syl2anc 661 . . . 4
31 simpl3 1001 . . . 4
32 xmulcl 11494 . . . 4
33 30 , 31 , 32 syl2anc 661 . . 3
34 14 adantr 465 . . . 4
35 xmulcl 11494 . . . 4
36 27 , 34 , 35 syl2anc 661 . . 3
37 oveq2 6304 . . . . 5
38 oveq2 6304 . . . . . 6
39 38 oveq2d 6312 . . . . 5
40 37 , 39 eqeq12d 2479 . . . 4
41 oveq2 6304 . . . . 5
42 oveq2 6304 . . . . . 6
43 42 oveq2d 6312 . . . . 5
44 41 , 43 eqeq12d 2479 . . . 4
45 27 adantr 465 . . . . . 6
46 simprl 756 . . . . . 6
47 xmulcl 11494 . . . . . 6
48 45 , 46 , 47 syl2anc 661 . . . . 5
49 31 adantr 465 . . . . 5
50 xmulcl 11494 . . . . 5
51 48 , 49 , 50 syl2anc 661 . . . 4
52 xmulcl 11494 . . . . . 6
53 46 , 49 , 52 syl2anc 661 . . . . 5
54 xmulcl 11494 . . . . 5
55 45 , 53 , 54 syl2anc 661 . . . 4
56 xmulasslem3 11507 . . . . . 6
57 56 3expa 1196 . . . . 5
58 57 adantlll 717 . . . 4
59 xmul01 11488 . . . . . . . 8
60 48 , 59 syl 16 . . . . . . 7
61 xmul01 11488 . . . . . . . 8
62 45 , 61 syl 16 . . . . . . 7
63 60 , 62 eqtr4d 2501 . . . . . 6
64 xmul01 11488 . . . . . . . 8
65 64 ad2antrl 727 . . . . . . 7
66 65 oveq2d 6312 . . . . . 6
67 63 , 66 eqtr4d 2501 . . . . 5
68 oveq2 6304 . . . . . 6
69 oveq2 6304 . . . . . . 7
70 69 oveq2d 6312 . . . . . 6
71 68 , 70 eqeq12d 2479 . . . . 5
72 67 , 71 syl5ibrcom 222 . . . 4
73 xmulneg2 11491 . . . . 5
74 48 , 49 , 73 syl2anc 661 . . . 4
75 xmulneg2 11491 . . . . . . 7
76 46 , 49 , 75 syl2anc 661 . . . . . 6
77 76 oveq2d 6312 . . . . 5
78 xmulneg2 11491 . . . . . 6
79 45 , 53 , 78 syl2anc 661 . . . . 5
80 77 , 79 eqtrd 2498 . . . 4
81 40 , 44 , 51 , 55 , 49 , 58 , 72 , 74 , 80 xmulasslem 11506 . . 3
82 xmul02 11489 . . . . . . . 8
83 82 3ad2ant3 1019 . . . . . . 7
84 83 adantr 465 . . . . . 6
85 61 ad2antrl 727 . . . . . 6
86 84 , 85 eqtr4d 2501 . . . . 5
87 85 oveq1d 6311 . . . . 5
88 84 oveq2d 6312 . . . . 5
89 86 , 87 , 88 3eqtr4d 2508 . . . 4
90 oveq2 6304 . . . . . 6
91 90 oveq1d 6311 . . . . 5
92 oveq1 6303 . . . . . 6
93 92 oveq2d 6312 . . . . 5
94 91 , 93 eqeq12d 2479 . . . 4
95 89 , 94 syl5ibrcom 222 . . 3
96 xmulneg2 11491 . . . . . 6
97 27 , 28 , 96 syl2anc 661 . . . . 5
98 97 oveq1d 6311 . . . 4
99 xmulneg1 11490 . . . . 5
100 30 , 31 , 99 syl2anc 661 . . . 4
101 98 , 100 eqtrd 2498 . . 3
102 xmulneg1 11490 . . . . . 6
103 28 , 31 , 102 syl2anc 661 . . . . 5
104 103 oveq2d 6312 . . . 4
105 xmulneg2 11491 . . . . 5
106 27 , 34 , 105 syl2anc 661 . . . 4
107 104 , 106 eqtrd 2498 . . 3
108 21 , 26 , 33 , 36 , 28 , 81 , 95 , 101 , 107 xmulasslem 11506 . 2
109 xmul02 11489 . . . . . 6
110 109 3ad2ant2 1018 . . . . 5
111 110 oveq1d 6311 . . . 4
112 xmul02 11489 . . . . 5
113 14 , 112 syl 16 . . . 4
114 83 , 111 , 113 3eqtr4d 2508 . . 3
115 oveq1 6303 . . . . 5
116 115 oveq1d 6311 . . . 4
117 oveq1 6303 . . . 4
118 116 , 117 eqeq12d 2479 . . 3
119 114 , 118 syl5ibrcom 222 . 2
120 xmulneg1 11490 . . . . 5
121 120 3adant3 1016 . . . 4
122 121 oveq1d 6311 . . 3
123 xmulneg1 11490 . . . 4
124 9 , 123 stoic3 1609 . . 3
125 122 , 124 eqtrd 2498 . 2
126 xmulneg1 11490 . . 3
127 12 , 14 , 126 syl2anc 661 . 2
128 4 , 8 , 11 , 16 , 12 , 108 , 119 , 125 , 127 xmulasslem 11506 1
