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
|- ( ( A e. NN0 /\ B e. NN /\ A < ( 2 x. B ) ) -> ( A mod B ) = if ( A < B , A , ( A - B ) ) )

Proof

Step Hyp Ref Expression
1 nn0re
 |-  ( A e. NN0 -> A e. RR )
2 nnrp
 |-  ( B e. NN -> B e. RR+ )
3 1 2 anim12i
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( A e. RR /\ B e. RR+ ) )
4 3 3adant3
 |-  ( ( A e. NN0 /\ B e. NN /\ A < ( 2 x. B ) ) -> ( A e. RR /\ B e. RR+ ) )
5 nn0ge0
 |-  ( A e. NN0 -> 0 <_ A )
6 5 3ad2ant1
 |-  ( ( A e. NN0 /\ B e. NN /\ A < ( 2 x. B ) ) -> 0 <_ A )
7 6 anim1i
 |-  ( ( ( A e. NN0 /\ B e. NN /\ A < ( 2 x. B ) ) /\ A < B ) -> ( 0 <_ A /\ A < B ) )
8 7 ancoms
 |-  ( ( A < B /\ ( A e. NN0 /\ B e. NN /\ A < ( 2 x. B ) ) ) -> ( 0 <_ A /\ A < B ) )
9 modid
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ ( 0 <_ A /\ A < B ) ) -> ( A mod B ) = A )
10 4 8 9 syl2an2
 |-  ( ( A < B /\ ( A e. NN0 /\ B e. NN /\ A < ( 2 x. B ) ) ) -> ( A mod B ) = A )
11 iftrue
 |-  ( A < B -> if ( A < B , A , ( A - B ) ) = A )
12 11 eqcomd
 |-  ( A < B -> A = if ( A < B , A , ( A - B ) ) )
13 12 adantr
 |-  ( ( A < B /\ ( A e. NN0 /\ B e. NN /\ A < ( 2 x. B ) ) ) -> A = if ( A < B , A , ( A - B ) ) )
14 10 13 eqtrd
 |-  ( ( A < B /\ ( A e. NN0 /\ B e. NN /\ A < ( 2 x. B ) ) ) -> ( A mod B ) = if ( A < B , A , ( A - B ) ) )
15 14 ex
 |-  ( A < B -> ( ( A e. NN0 /\ B e. NN /\ A < ( 2 x. B ) ) -> ( A mod B ) = if ( A < B , A , ( A - B ) ) ) )
16 4 adantr
 |-  ( ( ( A e. NN0 /\ B e. NN /\ A < ( 2 x. B ) ) /\ -. A < B ) -> ( A e. RR /\ B e. RR+ ) )
17 nnre
 |-  ( B e. NN -> B e. RR )
18 lenlt
 |-  ( ( B e. RR /\ A e. RR ) -> ( B <_ A <-> -. A < B ) )
19 17 1 18 syl2anr
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( B <_ A <-> -. A < B ) )
20 19 3adant3
 |-  ( ( A e. NN0 /\ B e. NN /\ A < ( 2 x. B ) ) -> ( B <_ A <-> -. A < B ) )
21 20 biimpar
 |-  ( ( ( A e. NN0 /\ B e. NN /\ A < ( 2 x. B ) ) /\ -. A < B ) -> B <_ A )
22 simpl3
 |-  ( ( ( A e. NN0 /\ B e. NN /\ A < ( 2 x. B ) ) /\ -. A < B ) -> A < ( 2 x. B ) )
23 2submod
 |-  ( ( ( A e. RR /\ B e. RR+ ) /\ ( B <_ A /\ A < ( 2 x. B ) ) ) -> ( A mod B ) = ( A - B ) )
24 16 21 22 23 syl12anc
 |-  ( ( ( A e. NN0 /\ B e. NN /\ A < ( 2 x. B ) ) /\ -. A < B ) -> ( A mod B ) = ( A - B ) )
25 iffalse
 |-  ( -. A < B -> if ( A < B , A , ( A - B ) ) = ( A - B ) )
26 25 adantl
 |-  ( ( ( A e. NN0 /\ B e. NN /\ A < ( 2 x. B ) ) /\ -. A < B ) -> if ( A < B , A , ( A - B ) ) = ( A - B ) )
27 26 eqcomd
 |-  ( ( ( A e. NN0 /\ B e. NN /\ A < ( 2 x. B ) ) /\ -. A < B ) -> ( A - B ) = if ( A < B , A , ( A - B ) ) )
28 24 27 eqtrd
 |-  ( ( ( A e. NN0 /\ B e. NN /\ A < ( 2 x. B ) ) /\ -. A < B ) -> ( A mod B ) = if ( A < B , A , ( A - B ) ) )
29 28 expcom
 |-  ( -. A < B -> ( ( A e. NN0 /\ B e. NN /\ A < ( 2 x. B ) ) -> ( A mod B ) = if ( A < B , A , ( A - B ) ) ) )
30 15 29 pm2.61i
 |-  ( ( A e. NN0 /\ B e. NN /\ A < ( 2 x. B ) ) -> ( A mod B ) = if ( A < B , A , ( A - B ) ) )