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 AB+AmodB=0AB

Proof

Step Hyp Ref Expression
1 modval AB+AmodB=ABAB
2 1 eqeq1d AB+AmodB=0ABAB=0
3 recn AA
4 3 adantr AB+A
5 rpre B+B
6 5 adantl AB+B
7 refldivcl AB+AB
8 6 7 remulcld AB+BAB
9 8 recnd AB+BAB
10 4 9 subeq0ad AB+ABAB=0A=BAB
11 2 10 bitrd AB+AmodB=0A=BAB
12 7 recnd AB+AB
13 rpcnne0 B+BB0
14 13 adantl AB+BB0
15 divmul2 AABBB0AB=ABA=BAB
16 4 12 14 15 syl3anc AB+AB=ABA=BAB
17 eqcom AB=ABAB=AB
18 16 17 bitr3di AB+A=BABAB=AB
19 11 18 bitrd AB+AmodB=0AB=AB
20 rerpdivcl AB+AB
21 flidz ABAB=ABAB
22 20 21 syl AB+AB=ABAB
23 19 22 bitrd AB+AmodB=0AB