This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem absmod0

Description: A is divisible by B iff its absolute value is. (Contributed by Jeff Madsen, 2-Sep-2009)

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

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( A = ( abs ` A ) -> ( A mod B ) = ( ( abs ` A ) mod B ) )
2 1 eqcoms 
 |-  ( ( abs ` A ) = A -> ( A mod B ) = ( ( abs ` A ) mod B ) )
3 2 eqeq1d 
 |-  ( ( abs ` A ) = A -> ( ( A mod B ) = 0 <-> ( ( abs ` A ) mod B ) = 0 ) )
4 3 a1i 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( abs ` A ) = A -> ( ( A mod B ) = 0 <-> ( ( abs ` A ) mod B ) = 0 ) ) )
5 negmod0 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A mod B ) = 0 <-> ( -u A mod B ) = 0 ) )
6 oveq1 
 |-  ( ( abs ` A ) = -u A -> ( ( abs ` A ) mod B ) = ( -u A mod B ) )
7 6 eqeq1d 
 |-  ( ( abs ` A ) = -u A -> ( ( ( abs ` A ) mod B ) = 0 <-> ( -u A mod B ) = 0 ) )
8 7 bibi2d 
 |-  ( ( abs ` A ) = -u A -> ( ( ( A mod B ) = 0 <-> ( ( abs ` A ) mod B ) = 0 ) <-> ( ( A mod B ) = 0 <-> ( -u A mod B ) = 0 ) ) )
9 5 8 syl5ibrcom 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( abs ` A ) = -u A -> ( ( A mod B ) = 0 <-> ( ( abs ` A ) mod B ) = 0 ) ) )
10 absor 
 |-  ( A e. RR -> ( ( abs ` A ) = A \/ ( abs ` A ) = -u A ) )
11 10 adantr 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( abs ` A ) = A \/ ( abs ` A ) = -u A ) )
12 4 9 11 mpjaod 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A mod B ) = 0 <-> ( ( abs ` A ) mod B ) = 0 ) )