Metamath Proof Explorer

Theorem 0mod

Description: Special case: 0 modulo a positive real number is 0. (Contributed by Mario Carneiro, 22-Feb-2014)

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

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 1 jctl 
 |-  ( N e. RR+ -> ( 0 e. RR /\ N e. RR+ ) )
3 rpgt0 
 |-  ( N e. RR+ -> 0 < N )
4 0le0 
 |-  0 <_ 0
5 3 4 jctil 
 |-  ( N e. RR+ -> ( 0 <_ 0 /\ 0 < N ) )
6 modid 
 |-  ( ( ( 0 e. RR /\ N e. RR+ ) /\ ( 0 <_ 0 /\ 0 < N ) ) -> ( 0 mod N ) = 0 )
7 2 5 6 syl2anc 
 |-  ( N e. RR+ -> ( 0 mod N ) = 0 )