Metamath Proof Explorer

Theorem modid

Description: Identity law for modulo. (Contributed by NM, 29-Dec-2008)

Ref Expression
Assertion modid 
|- ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( A mod B ) = A )

Proof

Step Hyp Ref Expression
1 modval 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) = ( A - ( B x. ( |_ ` ( A / B ) ) ) ) )
2 1 adantr 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( A mod B ) = ( A - ( B x. ( |_ ` ( A / B ) ) ) ) )
3 rerpdivcl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A / B ) e. RR )
4 3 adantr 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( A / B ) e. RR )
5 4 recnd 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( A / B ) e. CC )
6 addid2 
 |-  ( ( A / B ) e. CC -> ( 0 + ( A / B ) ) = ( A / B ) )
7 6 fveq2d 
 |-  ( ( A / B ) e. CC -> ( |_ ` ( 0 + ( A / B ) ) ) = ( |_ ` ( A / B ) ) )
8 5 7 syl 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( |_ ` ( 0 + ( A / B ) ) ) = ( |_ ` ( A / B ) ) )
9 rpregt0 
 |-  ( B e. RR+ -> ( B e. RR /\ 0 < B ) )
10 divge0 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 < B ) ) -> 0 <_ ( A / B ) )
11 9 10 sylan2 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ ) -> 0 <_ ( A / B ) )
12 11 an32s 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ 0 <_ A ) -> 0 <_ ( A / B ) )
13 12 adantrr 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> 0 <_ ( A / B ) )
14 simpr 
 |-  ( ( B e. RR+ /\ A < B ) -> A < B )
15 rpcn 
 |-  ( B e. RR+ -> B e. CC )
16 15 mulid1d 
 |-  ( B e. RR+ -> ( B x. 1 ) = B )
17 16 adantr 
 |-  ( ( B e. RR+ /\ A < B ) -> ( B x. 1 ) = B )
18 14 17 breqtrrd 
 |-  ( ( B e. RR+ /\ A < B ) -> A < ( B x. 1 ) )
19 18 ad2ant2l 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> A < ( B x. 1 ) )
20 simpll 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> A e. RR )
21 9 ad2antlr 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( B e. RR /\ 0 < B ) )
22 1re 
 |-  1 e. RR
23 ltdivmul 
 |-  ( ( A e. RR /\ 1 e. RR /\ ( B e. RR /\ 0 < B ) ) -> ( ( A / B ) < 1 <-> A < ( B x. 1 ) ) )
24 22 23 mp3an2 
 |-  ( ( A e. RR /\ ( B e. RR /\ 0 < B ) ) -> ( ( A / B ) < 1 <-> A < ( B x. 1 ) ) )
25 20 21 24 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( ( A / B ) < 1 <-> A < ( B x. 1 ) ) )
26 19 25 mpbird 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( A / B ) < 1 )
27 0z 
 |-  0 e. ZZ
28 flbi2 
 |-  ( ( 0 e. ZZ /\ ( A / B ) e. RR ) -> ( ( |_ ` ( 0 + ( A / B ) ) ) = 0 <-> ( 0 <_ ( A / B ) /\ ( A / B ) < 1 ) ) )
29 27 4 28 sylancr 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( ( |_ ` ( 0 + ( A / B ) ) ) = 0 <-> ( 0 <_ ( A / B ) /\ ( A / B ) < 1 ) ) )
30 13 26 29 mpbir2and 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( |_ ` ( 0 + ( A / B ) ) ) = 0 )
31 8 30 eqtr3d 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( |_ ` ( A / B ) ) = 0 )
32 31 oveq2d 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( B x. ( |_ ` ( A / B ) ) ) = ( B x. 0 ) )
33 15 mul01d 
 |-  ( B e. RR+ -> ( B x. 0 ) = 0 )
34 33 ad2antlr 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( B x. 0 ) = 0 )
35 32 34 eqtrd 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( B x. ( |_ ` ( A / B ) ) ) = 0 )
36 35 oveq2d 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( A - ( B x. ( |_ ` ( A / B ) ) ) ) = ( A - 0 ) )
37 recn 
 |-  ( A e. RR -> A e. CC )
38 37 subid1d 
 |-  ( A e. RR -> ( A - 0 ) = A )
39 38 ad2antrr 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( A - 0 ) = A )
40 36 39 eqtrd 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( A - ( B x. ( |_ ` ( A / B ) ) ) ) = A )
41 2 40 eqtrd 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( A mod B ) = A )