This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem modcl

Description: Closure law for the modulo operation. (Contributed by NM, 10-Nov-2008)

Ref Expression
Assertion modcl 
|- ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) e. RR )

Proof

Step Hyp Ref Expression
1 modval 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) = ( A - ( B x. ( |_ ` ( A / B ) ) ) ) )
2 rpre 
 |-  ( B e. RR+ -> B e. RR )
3 2 adantl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> B e. RR )
4 refldivcl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( |_ ` ( A / B ) ) e. RR )
5 3 4 remulcld 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( B x. ( |_ ` ( A / B ) ) ) e. RR )
6 resubcl 
 |-  ( ( A e. RR /\ ( B x. ( |_ ` ( A / B ) ) ) e. RR ) -> ( A - ( B x. ( |_ ` ( A / B ) ) ) ) e. RR )
7 5 6 syldan 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A - ( B x. ( |_ ` ( A / B ) ) ) ) e. RR )
8 1 7 eqeltrd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) e. RR )