Metamath Proof Explorer


Theorem zmulcomlem

Description: Lemma for zmulcom . (Contributed by SN, 25-Jan-2025)

Ref Expression
Assertion zmulcomlem A 0 - A B 0 A B = B A

Proof

Step Hyp Ref Expression
1 elnn0 B 0 B B = 0
2 renegneg A 0 - 0 - A = A
3 2 oveq1d A 0 - 0 - A B = A B
4 3 ad2antrr A 0 - A B 0 - 0 - A B = A B
5 rernegcl A 0 - A
6 5 ad2antrr A 0 - A B 0 - A
7 simpr A 0 - A B B
8 6 7 renegmulnnass A 0 - A B 0 - 0 - A B = 0 - 0 - A B
9 nnmulcom 0 - A B 0 - A B = B 0 - A
10 9 adantll A 0 - A B 0 - A B = B 0 - A
11 10 oveq2d A 0 - A B 0 - 0 - A B = 0 - B 0 - A
12 nnre B B
13 12 adantl A 0 - A B B
14 0red A 0 - A B 0
15 resubdi B 0 0 - A B 0 - 0 - A = B 0 - B 0 - A
16 13 14 6 15 syl3anc A 0 - A B B 0 - 0 - A = B 0 - B 0 - A
17 remul01 B B 0 = 0
18 12 17 syl B B 0 = 0
19 18 adantl A 0 - A B B 0 = 0
20 19 oveq1d A 0 - A B B 0 - B 0 - A = 0 - B 0 - A
21 16 20 eqtrd A 0 - A B B 0 - 0 - A = 0 - B 0 - A
22 2 ad2antrr A 0 - A B 0 - 0 - A = A
23 22 oveq2d A 0 - A B B 0 - 0 - A = B A
24 11 21 23 3eqtr2d A 0 - A B 0 - 0 - A B = B A
25 8 4 24 3eqtr3d A 0 - A B A B = B A
26 4 4 25 3eqtr3d A 0 - A B A B = B A
27 remul01 A A 0 = 0
28 remul02 A 0 A = 0
29 27 28 eqtr4d A A 0 = 0 A
30 29 adantr A 0 - A A 0 = 0 A
31 oveq2 B = 0 A B = A 0
32 oveq1 B = 0 B A = 0 A
33 31 32 eqeq12d B = 0 A B = B A A 0 = 0 A
34 30 33 syl5ibrcom A 0 - A B = 0 A B = B A
35 34 imp A 0 - A B = 0 A B = B A
36 26 35 jaodan A 0 - A B B = 0 A B = B A
37 1 36 sylan2b A 0 - A B 0 A B = B A