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

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 ) )