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