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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rpre | |
|
2 | ax-1rid | |
|
3 | 1 2 | syl | |
4 | 3 | adantl | |
5 | 4 | oveq2d | |
6 | 5 | oveq1d | |
7 | 6 | adantr | |
8 | simpl | |
|
9 | simpr | |
|
10 | 1zzd | |
|
11 | 8 9 10 | 3jca | |
12 | 11 | adantr | |
13 | modcyc2 | |
|
14 | 12 13 | syl | |
15 | resubcl | |
|
16 | 1 15 | sylan2 | |
17 | 16 9 | jca | |
18 | subge0 | |
|
19 | 1 18 | sylan2 | |
20 | 19 | bicomd | |
21 | rpcn | |
|
22 | 21 | 2timesd | |
23 | 22 | adantl | |
24 | 23 | breq2d | |
25 | 1 | adantl | |
26 | 8 25 25 | ltsubaddd | |
27 | 24 26 | bitr4d | |
28 | 20 27 | anbi12d | |
29 | 28 | biimpa | |
30 | modid | |
|
31 | 17 29 30 | syl2an2r | |
32 | 7 14 31 | 3eqtr3d | |