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 ) ) )