Metamath Proof Explorer

Theorem addmodne

Description: The sum of a nonnegative integer and a positive integer modulo a number greater than both integers is not equal to the nonnegative integer. (Contributed by AV, 27-Aug-2025) (Proof shortened by AV, 6-Sep-2025)

Ref Expression
Assertion addmodne 
|- ( ( M e. NN /\ ( A e. NN0 /\ A < M ) /\ ( B e. NN /\ B < M ) ) -> ( ( A + B ) mod M ) =/= A )

Proof

Step Hyp Ref Expression
1 2z 
 |-  2 e. ZZ
2 1 a1i 
 |-  ( ( M e. NN /\ ( B e. NN /\ B < M ) ) -> 2 e. ZZ )
3 nnz 
 |-  ( M e. NN -> M e. ZZ )
4 3 adantr 
 |-  ( ( M e. NN /\ ( B e. NN /\ B < M ) ) -> M e. ZZ )
5 1red 
 |-  ( ( M e. NN /\ ( B e. NN /\ B < M ) ) -> 1 e. RR )
6 nnre 
 |-  ( B e. NN -> B e. RR )
7 6 ad2antrl 
 |-  ( ( M e. NN /\ ( B e. NN /\ B < M ) ) -> B e. RR )
8 nnre 
 |-  ( M e. NN -> M e. RR )
9 8 adantr 
 |-  ( ( M e. NN /\ ( B e. NN /\ B < M ) ) -> M e. RR )
10 nnge1 
 |-  ( B e. NN -> 1 <_ B )
11 10 ad2antrl 
 |-  ( ( M e. NN /\ ( B e. NN /\ B < M ) ) -> 1 <_ B )
12 simprr 
 |-  ( ( M e. NN /\ ( B e. NN /\ B < M ) ) -> B < M )
13 5 7 9 11 12 lelttrd 
 |-  ( ( M e. NN /\ ( B e. NN /\ B < M ) ) -> 1 < M )
14 1zzd 
 |-  ( ( B e. NN /\ B < M ) -> 1 e. ZZ )
15 zltp1le 
 |-  ( ( 1 e. ZZ /\ M e. ZZ ) -> ( 1 < M <-> ( 1 + 1 ) <_ M ) )
16 14 3 15 syl2anr 
 |-  ( ( M e. NN /\ ( B e. NN /\ B < M ) ) -> ( 1 < M <-> ( 1 + 1 ) <_ M ) )
17 1p1e2 
 |-  ( 1 + 1 ) = 2
18 17 breq1i 
 |-  ( ( 1 + 1 ) <_ M <-> 2 <_ M )
19 16 18 bitrdi 
 |-  ( ( M e. NN /\ ( B e. NN /\ B < M ) ) -> ( 1 < M <-> 2 <_ M ) )
20 13 19 mpbid 
 |-  ( ( M e. NN /\ ( B e. NN /\ B < M ) ) -> 2 <_ M )
21 2 4 20 3jca 
 |-  ( ( M e. NN /\ ( B e. NN /\ B < M ) ) -> ( 2 e. ZZ /\ M e. ZZ /\ 2 <_ M ) )
22 21 3adant2 
 |-  ( ( M e. NN /\ ( A e. NN0 /\ A < M ) /\ ( B e. NN /\ B < M ) ) -> ( 2 e. ZZ /\ M e. ZZ /\ 2 <_ M ) )
23 eluz2 
 |-  ( M e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ M e. ZZ /\ 2 <_ M ) )
24 22 23 sylibr 
 |-  ( ( M e. NN /\ ( A e. NN0 /\ A < M ) /\ ( B e. NN /\ B < M ) ) -> M e. ( ZZ>= ` 2 ) )
25 nn0z 
 |-  ( A e. NN0 -> A e. ZZ )
26 25 adantr 
 |-  ( ( A e. NN0 /\ A < M ) -> A e. ZZ )
27 26 3ad2ant2 
 |-  ( ( M e. NN /\ ( A e. NN0 /\ A < M ) /\ ( B e. NN /\ B < M ) ) -> A e. ZZ )
28 simprl 
 |-  ( ( M e. NN /\ ( B e. NN /\ B < M ) ) -> B e. NN )
29 simpl 
 |-  ( ( M e. NN /\ ( B e. NN /\ B < M ) ) -> M e. NN )
30 28 29 12 3jca 
 |-  ( ( M e. NN /\ ( B e. NN /\ B < M ) ) -> ( B e. NN /\ M e. NN /\ B < M ) )
31 30 3adant2 
 |-  ( ( M e. NN /\ ( A e. NN0 /\ A < M ) /\ ( B e. NN /\ B < M ) ) -> ( B e. NN /\ M e. NN /\ B < M ) )
32 elfzo1 
 |-  ( B e. ( 1 ..^ M ) <-> ( B e. NN /\ M e. NN /\ B < M ) )
33 31 32 sylibr 
 |-  ( ( M e. NN /\ ( A e. NN0 /\ A < M ) /\ ( B e. NN /\ B < M ) ) -> B e. ( 1 ..^ M ) )
34 zplusmodne 
 |-  ( ( M e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ( 1 ..^ M ) ) -> ( ( A + B ) mod M ) =/= ( A mod M ) )
35 24 27 33 34 syl3anc 
 |-  ( ( M e. NN /\ ( A e. NN0 /\ A < M ) /\ ( B e. NN /\ B < M ) ) -> ( ( A + B ) mod M ) =/= ( A mod M ) )
36 nnrp 
 |-  ( M e. NN -> M e. RR+ )
37 nn0re 
 |-  ( A e. NN0 -> A e. RR )
38 37 adantr 
 |-  ( ( A e. NN0 /\ A < M ) -> A e. RR )
39 36 38 anim12ci 
 |-  ( ( M e. NN /\ ( A e. NN0 /\ A < M ) ) -> ( A e. RR /\ M e. RR+ ) )
40 39 3adant3 
 |-  ( ( M e. NN /\ ( A e. NN0 /\ A < M ) /\ ( B e. NN /\ B < M ) ) -> ( A e. RR /\ M e. RR+ ) )
41 nn0ge0 
 |-  ( A e. NN0 -> 0 <_ A )
42 41 anim1i 
 |-  ( ( A e. NN0 /\ A < M ) -> ( 0 <_ A /\ A < M ) )
43 42 3ad2ant2 
 |-  ( ( M e. NN /\ ( A e. NN0 /\ A < M ) /\ ( B e. NN /\ B < M ) ) -> ( 0 <_ A /\ A < M ) )
44 modid 
 |-  ( ( ( A e. RR /\ M e. RR+ ) /\ ( 0 <_ A /\ A < M ) ) -> ( A mod M ) = A )
45 40 43 44 syl2anc 
 |-  ( ( M e. NN /\ ( A e. NN0 /\ A < M ) /\ ( B e. NN /\ B < M ) ) -> ( A mod M ) = A )
46 35 45 neeqtrd 
 |-  ( ( M e. NN /\ ( A e. NN0 /\ A < M ) /\ ( B e. NN /\ B < M ) ) -> ( ( A + B ) mod M ) =/= A )