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