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 ) )