Metamath Proof Explorer

Theorem negmod0

Description: A is divisible by B iff its negative is. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Fan Zheng, 7-Jun-2016)

Ref Expression
Assertion negmod0 
|- ( ( A e. RR /\ B e. RR+ ) -> ( ( A mod B ) = 0 <-> ( -u A mod B ) = 0 ) )

Proof

Step Hyp Ref Expression
1 rerpdivcl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A / B ) e. RR )
2 recn 
 |-  ( ( A / B ) e. RR -> ( A / B ) e. CC )
3 znegclb 
 |-  ( ( A / B ) e. CC -> ( ( A / B ) e. ZZ <-> -u ( A / B ) e. ZZ ) )
4 1 2 3 3syl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A / B ) e. ZZ <-> -u ( A / B ) e. ZZ ) )
5 recn 
 |-  ( A e. RR -> A e. CC )
6 5 adantr 
 |-  ( ( A e. RR /\ B e. RR+ ) -> A e. CC )
7 rpcn 
 |-  ( B e. RR+ -> B e. CC )
8 7 adantl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> B e. CC )
9 rpne0 
 |-  ( B e. RR+ -> B =/= 0 )
10 9 adantl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> B =/= 0 )
11 6 8 10 divnegd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> -u ( A / B ) = ( -u A / B ) )
12 11 eleq1d 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( -u ( A / B ) e. ZZ <-> ( -u A / B ) e. ZZ ) )
13 4 12 bitrd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A / B ) e. ZZ <-> ( -u A / B ) e. ZZ ) )
14 mod0 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A mod B ) = 0 <-> ( A / B ) e. ZZ ) )
15 renegcl 
 |-  ( A e. RR -> -u A e. RR )
16 mod0 
 |-  ( ( -u A e. RR /\ B e. RR+ ) -> ( ( -u A mod B ) = 0 <-> ( -u A / B ) e. ZZ ) )
17 15 16 sylan 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( -u A mod B ) = 0 <-> ( -u A / B ) e. ZZ ) )
18 13 14 17 3bitr4d 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A mod B ) = 0 <-> ( -u A mod B ) = 0 ) )