Metamath Proof Explorer

Theorem mod0

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

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

Proof

Step Hyp Ref Expression
1 modval 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) = ( A - ( B x. ( |_ ` ( A / B ) ) ) ) )
2 1 eqeq1d 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A mod B ) = 0 <-> ( A - ( B x. ( |_ ` ( A / B ) ) ) ) = 0 ) )
3 recn 
 |-  ( A e. RR -> A e. CC )
4 3 adantr 
 |-  ( ( A e. RR /\ B e. RR+ ) -> A e. CC )
5 rpre 
 |-  ( B e. RR+ -> B e. RR )
6 5 adantl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> B e. RR )
7 refldivcl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( |_ ` ( A / B ) ) e. RR )
8 6 7 remulcld 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( B x. ( |_ ` ( A / B ) ) ) e. RR )
9 8 recnd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( B x. ( |_ ` ( A / B ) ) ) e. CC )
10 4 9 subeq0ad 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A - ( B x. ( |_ ` ( A / B ) ) ) ) = 0 <-> A = ( B x. ( |_ ` ( A / B ) ) ) ) )
11 2 10 bitrd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A mod B ) = 0 <-> A = ( B x. ( |_ ` ( A / B ) ) ) ) )
12 7 recnd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( |_ ` ( A / B ) ) e. CC )
13 rpcnne0 
 |-  ( B e. RR+ -> ( B e. CC /\ B =/= 0 ) )
14 13 adantl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( B e. CC /\ B =/= 0 ) )
15 divmul2 
 |-  ( ( A e. CC /\ ( |_ ` ( A / B ) ) e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( A / B ) = ( |_ ` ( A / B ) ) <-> A = ( B x. ( |_ ` ( A / B ) ) ) ) )
16 4 12 14 15 syl3anc 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A / B ) = ( |_ ` ( A / B ) ) <-> A = ( B x. ( |_ ` ( A / B ) ) ) ) )
17 eqcom 
 |-  ( ( A / B ) = ( |_ ` ( A / B ) ) <-> ( |_ ` ( A / B ) ) = ( A / B ) )
18 16 17 bitr3di 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A = ( B x. ( |_ ` ( A / B ) ) ) <-> ( |_ ` ( A / B ) ) = ( A / B ) ) )
19 11 18 bitrd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A mod B ) = 0 <-> ( |_ ` ( A / B ) ) = ( A / B ) ) )
20 rerpdivcl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A / B ) e. RR )
21 flidz 
 |-  ( ( A / B ) e. RR -> ( ( |_ ` ( A / B ) ) = ( A / B ) <-> ( A / B ) e. ZZ ) )
22 20 21 syl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( |_ ` ( A / B ) ) = ( A / B ) <-> ( A / B ) e. ZZ ) )
23 19 22 bitrd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A mod B ) = 0 <-> ( A / B ) e. ZZ ) )