# 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 ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left({B}\le {A}\wedge {A}<2{B}\right)\right)\to {A}\mathrm{mod}{B}={A}-{B}$

### Proof

Step Hyp Ref Expression
1 rpre ${⊢}{B}\in {ℝ}^{+}\to {B}\in ℝ$
2 ax-1rid ${⊢}{B}\in ℝ\to {B}\cdot 1={B}$
3 1 2 syl ${⊢}{B}\in {ℝ}^{+}\to {B}\cdot 1={B}$
4 3 adantl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {B}\cdot 1={B}$
5 4 oveq2d ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}-{B}\cdot 1={A}-{B}$
6 5 oveq1d ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({A}-{B}\cdot 1\right)\mathrm{mod}{B}=\left({A}-{B}\right)\mathrm{mod}{B}$
7 6 adantr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left({B}\le {A}\wedge {A}<2{B}\right)\right)\to \left({A}-{B}\cdot 1\right)\mathrm{mod}{B}=\left({A}-{B}\right)\mathrm{mod}{B}$
8 simpl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}\in ℝ$
9 simpr ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {B}\in {ℝ}^{+}$
10 1zzd ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to 1\in ℤ$
11 8 9 10 3jca ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\wedge 1\in ℤ\right)$
12 11 adantr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left({B}\le {A}\wedge {A}<2{B}\right)\right)\to \left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\wedge 1\in ℤ\right)$
13 modcyc2 ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\wedge 1\in ℤ\right)\to \left({A}-{B}\cdot 1\right)\mathrm{mod}{B}={A}\mathrm{mod}{B}$
14 12 13 syl ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left({B}\le {A}\wedge {A}<2{B}\right)\right)\to \left({A}-{B}\cdot 1\right)\mathrm{mod}{B}={A}\mathrm{mod}{B}$
15 resubcl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}-{B}\in ℝ$
16 1 15 sylan2 ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {A}-{B}\in ℝ$
17 16 9 jca ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({A}-{B}\in ℝ\wedge {B}\in {ℝ}^{+}\right)$
18 subge0 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(0\le {A}-{B}↔{B}\le {A}\right)$
19 1 18 sylan2 ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left(0\le {A}-{B}↔{B}\le {A}\right)$
20 19 bicomd ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({B}\le {A}↔0\le {A}-{B}\right)$
21 rpcn ${⊢}{B}\in {ℝ}^{+}\to {B}\in ℂ$
22 21 2timesd ${⊢}{B}\in {ℝ}^{+}\to 2{B}={B}+{B}$
23 22 adantl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to 2{B}={B}+{B}$
24 23 breq2d ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({A}<2{B}↔{A}<{B}+{B}\right)$
25 1 adantl ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to {B}\in ℝ$
26 8 25 25 ltsubaddd ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({A}-{B}<{B}↔{A}<{B}+{B}\right)$
27 24 26 bitr4d ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left({A}<2{B}↔{A}-{B}<{B}\right)$
28 20 27 anbi12d ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\to \left(\left({B}\le {A}\wedge {A}<2{B}\right)↔\left(0\le {A}-{B}\wedge {A}-{B}<{B}\right)\right)$
29 28 biimpa ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left({B}\le {A}\wedge {A}<2{B}\right)\right)\to \left(0\le {A}-{B}\wedge {A}-{B}<{B}\right)$
30 modid ${⊢}\left(\left({A}-{B}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left(0\le {A}-{B}\wedge {A}-{B}<{B}\right)\right)\to \left({A}-{B}\right)\mathrm{mod}{B}={A}-{B}$
31 17 29 30 syl2an2r ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left({B}\le {A}\wedge {A}<2{B}\right)\right)\to \left({A}-{B}\right)\mathrm{mod}{B}={A}-{B}$
32 7 14 31 3eqtr3d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left({B}\le {A}\wedge {A}<2{B}\right)\right)\to {A}\mathrm{mod}{B}={A}-{B}$