# Metamath Proof Explorer

## Theorem modifeq2int

Description: If a nonnegative integer is less than twice a positive integer, the nonnegative integer modulo the positive integer equals the nonnegative integer or the nonnegative integer minus the positive integer. (Contributed by Alexander van der Vekens, 21-May-2018)

Ref Expression
Assertion modifeq2int ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in ℕ\wedge {A}<2{B}\right)\to {A}\mathrm{mod}{B}=if\left({A}<{B},{A},{A}-{B}\right)$

### Proof

Step Hyp Ref Expression
1 nn0re ${⊢}{A}\in {ℕ}_{0}\to {A}\in ℝ$
2 nnrp ${⊢}{B}\in ℕ\to {B}\in {ℝ}^{+}$
3 1 2 anim12i ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in ℕ\right)\to \left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)$
4 3 3adant3 ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in ℕ\wedge {A}<2{B}\right)\to \left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)$
5 nn0ge0 ${⊢}{A}\in {ℕ}_{0}\to 0\le {A}$
6 5 3ad2ant1 ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in ℕ\wedge {A}<2{B}\right)\to 0\le {A}$
7 6 anim1i ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {B}\in ℕ\wedge {A}<2{B}\right)\wedge {A}<{B}\right)\to \left(0\le {A}\wedge {A}<{B}\right)$
8 7 ancoms ${⊢}\left({A}<{B}\wedge \left({A}\in {ℕ}_{0}\wedge {B}\in ℕ\wedge {A}<2{B}\right)\right)\to \left(0\le {A}\wedge {A}<{B}\right)$
9 modid ${⊢}\left(\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)\wedge \left(0\le {A}\wedge {A}<{B}\right)\right)\to {A}\mathrm{mod}{B}={A}$
10 4 8 9 syl2an2 ${⊢}\left({A}<{B}\wedge \left({A}\in {ℕ}_{0}\wedge {B}\in ℕ\wedge {A}<2{B}\right)\right)\to {A}\mathrm{mod}{B}={A}$
11 iftrue ${⊢}{A}<{B}\to if\left({A}<{B},{A},{A}-{B}\right)={A}$
12 11 eqcomd ${⊢}{A}<{B}\to {A}=if\left({A}<{B},{A},{A}-{B}\right)$
13 12 adantr ${⊢}\left({A}<{B}\wedge \left({A}\in {ℕ}_{0}\wedge {B}\in ℕ\wedge {A}<2{B}\right)\right)\to {A}=if\left({A}<{B},{A},{A}-{B}\right)$
14 10 13 eqtrd ${⊢}\left({A}<{B}\wedge \left({A}\in {ℕ}_{0}\wedge {B}\in ℕ\wedge {A}<2{B}\right)\right)\to {A}\mathrm{mod}{B}=if\left({A}<{B},{A},{A}-{B}\right)$
15 14 ex ${⊢}{A}<{B}\to \left(\left({A}\in {ℕ}_{0}\wedge {B}\in ℕ\wedge {A}<2{B}\right)\to {A}\mathrm{mod}{B}=if\left({A}<{B},{A},{A}-{B}\right)\right)$
16 4 adantr ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {B}\in ℕ\wedge {A}<2{B}\right)\wedge ¬{A}<{B}\right)\to \left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\right)$
17 nnre ${⊢}{B}\in ℕ\to {B}\in ℝ$
18 lenlt ${⊢}\left({B}\in ℝ\wedge {A}\in ℝ\right)\to \left({B}\le {A}↔¬{A}<{B}\right)$
19 17 1 18 syl2anr ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in ℕ\right)\to \left({B}\le {A}↔¬{A}<{B}\right)$
20 19 3adant3 ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in ℕ\wedge {A}<2{B}\right)\to \left({B}\le {A}↔¬{A}<{B}\right)$
21 20 biimpar ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {B}\in ℕ\wedge {A}<2{B}\right)\wedge ¬{A}<{B}\right)\to {B}\le {A}$
22 simpl3 ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {B}\in ℕ\wedge {A}<2{B}\right)\wedge ¬{A}<{B}\right)\to {A}<2{B}$
23 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}$
24 16 21 22 23 syl12anc ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {B}\in ℕ\wedge {A}<2{B}\right)\wedge ¬{A}<{B}\right)\to {A}\mathrm{mod}{B}={A}-{B}$
25 iffalse ${⊢}¬{A}<{B}\to if\left({A}<{B},{A},{A}-{B}\right)={A}-{B}$
26 25 adantl ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {B}\in ℕ\wedge {A}<2{B}\right)\wedge ¬{A}<{B}\right)\to if\left({A}<{B},{A},{A}-{B}\right)={A}-{B}$
27 26 eqcomd ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {B}\in ℕ\wedge {A}<2{B}\right)\wedge ¬{A}<{B}\right)\to {A}-{B}=if\left({A}<{B},{A},{A}-{B}\right)$
28 24 27 eqtrd ${⊢}\left(\left({A}\in {ℕ}_{0}\wedge {B}\in ℕ\wedge {A}<2{B}\right)\wedge ¬{A}<{B}\right)\to {A}\mathrm{mod}{B}=if\left({A}<{B},{A},{A}-{B}\right)$
29 28 expcom ${⊢}¬{A}<{B}\to \left(\left({A}\in {ℕ}_{0}\wedge {B}\in ℕ\wedge {A}<2{B}\right)\to {A}\mathrm{mod}{B}=if\left({A}<{B},{A},{A}-{B}\right)\right)$
30 15 29 pm2.61i ${⊢}\left({A}\in {ℕ}_{0}\wedge {B}\in ℕ\wedge {A}<2{B}\right)\to {A}\mathrm{mod}{B}=if\left({A}<{B},{A},{A}-{B}\right)$