Metamath Proof Explorer

Theorem modid0

Description: A positive real number modulo itself is 0. (Contributed by Alexander van der Vekens, 15-May-2018)

Ref Expression
Assertion modid0 
|- ( N e. RR+ -> ( N mod N ) = 0 )

Proof

Step Hyp Ref Expression
1 rpcn 
 |-  ( N e. RR+ -> N e. CC )
2 rpne0 
 |-  ( N e. RR+ -> N =/= 0 )
3 1 2 dividd 
 |-  ( N e. RR+ -> ( N / N ) = 1 )
4 1z 
 |-  1 e. ZZ
5 3 4 eqeltrdi 
 |-  ( N e. RR+ -> ( N / N ) e. ZZ )
6 rpre 
 |-  ( N e. RR+ -> N e. RR )
7 mod0 
 |-  ( ( N e. RR /\ N e. RR+ ) -> ( ( N mod N ) = 0 <-> ( N / N ) e. ZZ ) )
8 6 7 mpancom 
 |-  ( N e. RR+ -> ( ( N mod N ) = 0 <-> ( N / N ) e. ZZ ) )
9 5 8 mpbird 
 |-  ( N e. RR+ -> ( N mod N ) = 0 )