Metamath Proof Explorer

Theorem modmuladdnn0

Description: Implication of a decomposition of a nonnegative integer into a multiple of a modulus and a remainder. (Contributed by AV, 14-Jul-2021)

Ref Expression
Assertion modmuladdnn0 
|- ( ( A e. NN0 /\ M e. RR+ ) -> ( ( A mod M ) = B -> E. k e. NN0 A = ( ( k x. M ) + B ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( k = i -> ( k x. M ) = ( i x. M ) )
2 1 oveq1d 
 |-  ( k = i -> ( ( k x. M ) + B ) = ( ( i x. M ) + B ) )
3 2 eqeq2d 
 |-  ( k = i -> ( A = ( ( k x. M ) + B ) <-> A = ( ( i x. M ) + B ) ) )
4 simpr 
 |-  ( ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) /\ i e. ZZ ) -> i e. ZZ )
5 4 adantr 
 |-  ( ( ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) /\ i e. ZZ ) /\ A = ( ( i x. M ) + B ) ) -> i e. ZZ )
6 eqcom 
 |-  ( A = ( ( i x. M ) + B ) <-> ( ( i x. M ) + B ) = A )
7 nn0cn 
 |-  ( A e. NN0 -> A e. CC )
8 7 adantr 
 |-  ( ( A e. NN0 /\ M e. RR+ ) -> A e. CC )
9 8 ad2antrr 
 |-  ( ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) /\ i e. ZZ ) -> A e. CC )
10 nn0re 
 |-  ( A e. NN0 -> A e. RR )
11 modcl 
 |-  ( ( A e. RR /\ M e. RR+ ) -> ( A mod M ) e. RR )
12 10 11 sylan 
 |-  ( ( A e. NN0 /\ M e. RR+ ) -> ( A mod M ) e. RR )
13 12 recnd 
 |-  ( ( A e. NN0 /\ M e. RR+ ) -> ( A mod M ) e. CC )
14 13 adantr 
 |-  ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) -> ( A mod M ) e. CC )
15 eleq1 
 |-  ( ( A mod M ) = B -> ( ( A mod M ) e. CC <-> B e. CC ) )
16 15 adantl 
 |-  ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) -> ( ( A mod M ) e. CC <-> B e. CC ) )
17 14 16 mpbid 
 |-  ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) -> B e. CC )
18 17 adantr 
 |-  ( ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) /\ i e. ZZ ) -> B e. CC )
19 zcn 
 |-  ( i e. ZZ -> i e. CC )
20 19 adantl 
 |-  ( ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) /\ i e. ZZ ) -> i e. CC )
21 rpcn 
 |-  ( M e. RR+ -> M e. CC )
22 21 adantl 
 |-  ( ( A e. NN0 /\ M e. RR+ ) -> M e. CC )
23 22 ad2antrr 
 |-  ( ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) /\ i e. ZZ ) -> M e. CC )
24 20 23 mulcld 
 |-  ( ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) /\ i e. ZZ ) -> ( i x. M ) e. CC )
25 9 18 24 subadd2d 
 |-  ( ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) /\ i e. ZZ ) -> ( ( A - B ) = ( i x. M ) <-> ( ( i x. M ) + B ) = A ) )
26 6 25 bitr4id 
 |-  ( ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) /\ i e. ZZ ) -> ( A = ( ( i x. M ) + B ) <-> ( A - B ) = ( i x. M ) ) )
27 7 ad2antrr 
 |-  ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) -> A e. CC )
28 27 17 subcld 
 |-  ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) -> ( A - B ) e. CC )
29 28 adantr 
 |-  ( ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) /\ i e. ZZ ) -> ( A - B ) e. CC )
30 rpcnne0 
 |-  ( M e. RR+ -> ( M e. CC /\ M =/= 0 ) )
31 30 adantl 
 |-  ( ( A e. NN0 /\ M e. RR+ ) -> ( M e. CC /\ M =/= 0 ) )
32 31 ad2antrr 
 |-  ( ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) /\ i e. ZZ ) -> ( M e. CC /\ M =/= 0 ) )
33 divmul3 
 |-  ( ( ( A - B ) e. CC /\ i e. CC /\ ( M e. CC /\ M =/= 0 ) ) -> ( ( ( A - B ) / M ) = i <-> ( A - B ) = ( i x. M ) ) )
34 29 20 32 33 syl3anc 
 |-  ( ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) /\ i e. ZZ ) -> ( ( ( A - B ) / M ) = i <-> ( A - B ) = ( i x. M ) ) )
35 oveq2 
 |-  ( B = ( A mod M ) -> ( A - B ) = ( A - ( A mod M ) ) )
36 35 oveq1d 
 |-  ( B = ( A mod M ) -> ( ( A - B ) / M ) = ( ( A - ( A mod M ) ) / M ) )
37 36 eqcoms 
 |-  ( ( A mod M ) = B -> ( ( A - B ) / M ) = ( ( A - ( A mod M ) ) / M ) )
38 37 adantl 
 |-  ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) -> ( ( A - B ) / M ) = ( ( A - ( A mod M ) ) / M ) )
39 38 adantr 
 |-  ( ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) /\ i e. ZZ ) -> ( ( A - B ) / M ) = ( ( A - ( A mod M ) ) / M ) )
40 moddiffl 
 |-  ( ( A e. RR /\ M e. RR+ ) -> ( ( A - ( A mod M ) ) / M ) = ( |_ ` ( A / M ) ) )
41 10 40 sylan 
 |-  ( ( A e. NN0 /\ M e. RR+ ) -> ( ( A - ( A mod M ) ) / M ) = ( |_ ` ( A / M ) ) )
42 41 ad2antrr 
 |-  ( ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) /\ i e. ZZ ) -> ( ( A - ( A mod M ) ) / M ) = ( |_ ` ( A / M ) ) )
43 39 42 eqtrd 
 |-  ( ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) /\ i e. ZZ ) -> ( ( A - B ) / M ) = ( |_ ` ( A / M ) ) )
44 43 eqeq1d 
 |-  ( ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) /\ i e. ZZ ) -> ( ( ( A - B ) / M ) = i <-> ( |_ ` ( A / M ) ) = i ) )
45 26 34 44 3bitr2d 
 |-  ( ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) /\ i e. ZZ ) -> ( A = ( ( i x. M ) + B ) <-> ( |_ ` ( A / M ) ) = i ) )
46 nn0ge0 
 |-  ( A e. NN0 -> 0 <_ A )
47 10 46 jca 
 |-  ( A e. NN0 -> ( A e. RR /\ 0 <_ A ) )
48 rpregt0 
 |-  ( M e. RR+ -> ( M e. RR /\ 0 < M ) )
49 divge0 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( M e. RR /\ 0 < M ) ) -> 0 <_ ( A / M ) )
50 47 48 49 syl2an 
 |-  ( ( A e. NN0 /\ M e. RR+ ) -> 0 <_ ( A / M ) )
51 10 adantr 
 |-  ( ( A e. NN0 /\ M e. RR+ ) -> A e. RR )
52 rpre 
 |-  ( M e. RR+ -> M e. RR )
53 52 adantl 
 |-  ( ( A e. NN0 /\ M e. RR+ ) -> M e. RR )
54 rpne0 
 |-  ( M e. RR+ -> M =/= 0 )
55 54 adantl 
 |-  ( ( A e. NN0 /\ M e. RR+ ) -> M =/= 0 )
56 51 53 55 redivcld 
 |-  ( ( A e. NN0 /\ M e. RR+ ) -> ( A / M ) e. RR )
57 0z 
 |-  0 e. ZZ
58 flge 
 |-  ( ( ( A / M ) e. RR /\ 0 e. ZZ ) -> ( 0 <_ ( A / M ) <-> 0 <_ ( |_ ` ( A / M ) ) ) )
59 56 57 58 sylancl 
 |-  ( ( A e. NN0 /\ M e. RR+ ) -> ( 0 <_ ( A / M ) <-> 0 <_ ( |_ ` ( A / M ) ) ) )
60 50 59 mpbid 
 |-  ( ( A e. NN0 /\ M e. RR+ ) -> 0 <_ ( |_ ` ( A / M ) ) )
61 breq2 
 |-  ( ( |_ ` ( A / M ) ) = i -> ( 0 <_ ( |_ ` ( A / M ) ) <-> 0 <_ i ) )
62 60 61 syl5ibcom 
 |-  ( ( A e. NN0 /\ M e. RR+ ) -> ( ( |_ ` ( A / M ) ) = i -> 0 <_ i ) )
63 62 ad2antrr 
 |-  ( ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) /\ i e. ZZ ) -> ( ( |_ ` ( A / M ) ) = i -> 0 <_ i ) )
64 45 63 sylbid 
 |-  ( ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) /\ i e. ZZ ) -> ( A = ( ( i x. M ) + B ) -> 0 <_ i ) )
65 64 imp 
 |-  ( ( ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) /\ i e. ZZ ) /\ A = ( ( i x. M ) + B ) ) -> 0 <_ i )
66 elnn0z 
 |-  ( i e. NN0 <-> ( i e. ZZ /\ 0 <_ i ) )
67 5 65 66 sylanbrc 
 |-  ( ( ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) /\ i e. ZZ ) /\ A = ( ( i x. M ) + B ) ) -> i e. NN0 )
68 simpr 
 |-  ( ( ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) /\ i e. ZZ ) /\ A = ( ( i x. M ) + B ) ) -> A = ( ( i x. M ) + B ) )
69 3 67 68 rspcedvdw 
 |-  ( ( ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) /\ i e. ZZ ) /\ A = ( ( i x. M ) + B ) ) -> E. k e. NN0 A = ( ( k x. M ) + B ) )
70 nn0z 
 |-  ( A e. NN0 -> A e. ZZ )
71 modmuladdim 
 |-  ( ( A e. ZZ /\ M e. RR+ ) -> ( ( A mod M ) = B -> E. i e. ZZ A = ( ( i x. M ) + B ) ) )
72 70 71 sylan 
 |-  ( ( A e. NN0 /\ M e. RR+ ) -> ( ( A mod M ) = B -> E. i e. ZZ A = ( ( i x. M ) + B ) ) )
73 72 imp 
 |-  ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) -> E. i e. ZZ A = ( ( i x. M ) + B ) )
74 69 73 r19.29a 
 |-  ( ( ( A e. NN0 /\ M e. RR+ ) /\ ( A mod M ) = B ) -> E. k e. NN0 A = ( ( k x. M ) + B ) )
75 74 ex 
 |-  ( ( A e. NN0 /\ M e. RR+ ) -> ( ( A mod M ) = B -> E. k e. NN0 A = ( ( k x. M ) + B ) ) )