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 AB+BAA<2BAmodB=AB

Proof

Step Hyp Ref Expression
1 rpre B+B
2 ax-1rid BB1=B
3 1 2 syl B+B1=B
4 3 adantl AB+B1=B
5 4 oveq2d AB+AB1=AB
6 5 oveq1d AB+AB1modB=ABmodB
7 6 adantr AB+BAA<2BAB1modB=ABmodB
8 simpl AB+A
9 simpr AB+B+
10 1zzd AB+1
11 8 9 10 3jca AB+AB+1
12 11 adantr AB+BAA<2BAB+1
13 modcyc2 AB+1AB1modB=AmodB
14 12 13 syl AB+BAA<2BAB1modB=AmodB
15 resubcl ABAB
16 1 15 sylan2 AB+AB
17 16 9 jca AB+ABB+
18 subge0 AB0ABBA
19 1 18 sylan2 AB+0ABBA
20 19 bicomd AB+BA0AB
21 rpcn B+B
22 21 2timesd B+2B=B+B
23 22 adantl AB+2B=B+B
24 23 breq2d AB+A<2BA<B+B
25 1 adantl AB+B
26 8 25 25 ltsubaddd AB+AB<BA<B+B
27 24 26 bitr4d AB+A<2BAB<B
28 20 27 anbi12d AB+BAA<2B0ABAB<B
29 28 biimpa AB+BAA<2B0ABAB<B
30 modid ABB+0ABAB<BABmodB=AB
31 17 29 30 syl2an2r AB+BAA<2BABmodB=AB
32 7 14 31 3eqtr3d AB+BAA<2BAmodB=AB