Metamath Proof Explorer

Theorem 2submod

Description: If a real number is between a positive real number and twice the positive real number, the real number modulo the positive real number equals the real number minus the positive real number. (Contributed by Alexander van der Vekens, 13-May-2018)

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

Proof

Step Hyp Ref Expression
1 rpre 
 |-  ( B e. RR+ -> B e. RR )
2 ax-1rid 
 |-  ( B e. RR -> ( B x. 1 ) = B )
3 1 2 syl 
 |-  ( B e. RR+ -> ( B x. 1 ) = B )
4 3 adantl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( B x. 1 ) = B )
5 4 oveq2d 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A - ( B x. 1 ) ) = ( A - B ) )
6 5 oveq1d 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A - ( B x. 1 ) ) mod B ) = ( ( A - B ) mod B ) )
7 6 adantr 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ ( B <_ A /\ A < ( 2 x. B ) ) ) -> ( ( A - ( B x. 1 ) ) mod B ) = ( ( A - B ) mod B ) )
8 simpl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> A e. RR )
9 simpr 
 |-  ( ( A e. RR /\ B e. RR+ ) -> B e. RR+ )
10 1zzd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> 1 e. ZZ )
11 8 9 10 3jca 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A e. RR /\ B e. RR+ /\ 1 e. ZZ ) )
12 11 adantr 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ ( B <_ A /\ A < ( 2 x. B ) ) ) -> ( A e. RR /\ B e. RR+ /\ 1 e. ZZ ) )
13 modcyc2 
 |-  ( ( A e. RR /\ B e. RR+ /\ 1 e. ZZ ) -> ( ( A - ( B x. 1 ) ) mod B ) = ( A mod B ) )
14 12 13 syl 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ ( B <_ A /\ A < ( 2 x. B ) ) ) -> ( ( A - ( B x. 1 ) ) mod B ) = ( A mod B ) )
15 resubcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A - B ) e. RR )
16 1 15 sylan2 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A - B ) e. RR )
17 16 9 jca 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A - B ) e. RR /\ B e. RR+ ) )
18 subge0 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 <_ ( A - B ) <-> B <_ A ) )
19 1 18 sylan2 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( 0 <_ ( A - B ) <-> B <_ A ) )
20 19 bicomd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( B <_ A <-> 0 <_ ( A - B ) ) )
21 rpcn 
 |-  ( B e. RR+ -> B e. CC )
22 21 2timesd 
 |-  ( B e. RR+ -> ( 2 x. B ) = ( B + B ) )
23 22 adantl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( 2 x. B ) = ( B + B ) )
24 23 breq2d 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A < ( 2 x. B ) <-> A < ( B + B ) ) )
25 1 adantl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> B e. RR )
26 8 25 25 ltsubaddd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A - B ) < B <-> A < ( B + B ) ) )
27 24 26 bitr4d 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A < ( 2 x. B ) <-> ( A - B ) < B ) )
28 20 27 anbi12d 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( B <_ A /\ A < ( 2 x. B ) ) <-> ( 0 <_ ( A - B ) /\ ( A - B ) < B ) ) )
29 28 biimpa 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ ( B <_ A /\ A < ( 2 x. B ) ) ) -> ( 0 <_ ( A - B ) /\ ( A - B ) < B ) )
30 modid 
 |-  ( ( ( ( A - B ) e. RR /\ B e. RR+ ) /\ ( 0 <_ ( A - B ) /\ ( A - B ) < B ) ) -> ( ( A - B ) mod B ) = ( A - B ) )
31 17 29 30 syl2an2r 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ ( B <_ A /\ A < ( 2 x. B ) ) ) -> ( ( A - B ) mod B ) = ( A - B ) )
32 7 14 31 3eqtr3d 
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ ( B <_ A /\ A < ( 2 x. B ) ) ) -> ( A mod B ) = ( A - B ) )