Metamath Proof Explorer

Theorem modn0mul

Description: If an integer is not 0 modulo a positive integer, this integer must be the sum of a multiple of the modulus and a positive integer less than the modulus. (Contributed by AV, 7-Jun-2020)

Ref Expression
Assertion modn0mul 
|- ( ( A e. ZZ /\ N e. NN ) -> ( ( A mod N ) =/= 0 -> E. x e. ZZ E. y e. ( 1 ..^ N ) A = ( ( x x. N ) + y ) ) )

Proof

Step Hyp Ref Expression
1 zre 
 |-  ( A e. ZZ -> A e. RR )
2 1 adantr 
 |-  ( ( A e. ZZ /\ N e. NN ) -> A e. RR )
3 nnre 
 |-  ( N e. NN -> N e. RR )
4 3 adantl 
 |-  ( ( A e. ZZ /\ N e. NN ) -> N e. RR )
5 nnne0 
 |-  ( N e. NN -> N =/= 0 )
6 5 adantl 
 |-  ( ( A e. ZZ /\ N e. NN ) -> N =/= 0 )
7 2 4 6 redivcld 
 |-  ( ( A e. ZZ /\ N e. NN ) -> ( A / N ) e. RR )
8 7 flcld 
 |-  ( ( A e. ZZ /\ N e. NN ) -> ( |_ ` ( A / N ) ) e. ZZ )
9 8 adantr 
 |-  ( ( ( A e. ZZ /\ N e. NN ) /\ ( A mod N ) =/= 0 ) -> ( |_ ` ( A / N ) ) e. ZZ )
10 zmodfzo 
 |-  ( ( A e. ZZ /\ N e. NN ) -> ( A mod N ) e. ( 0 ..^ N ) )
11 10 anim1i 
 |-  ( ( ( A e. ZZ /\ N e. NN ) /\ ( A mod N ) =/= 0 ) -> ( ( A mod N ) e. ( 0 ..^ N ) /\ ( A mod N ) =/= 0 ) )
12 fzo1fzo0n0 
 |-  ( ( A mod N ) e. ( 1 ..^ N ) <-> ( ( A mod N ) e. ( 0 ..^ N ) /\ ( A mod N ) =/= 0 ) )
13 11 12 sylibr 
 |-  ( ( ( A e. ZZ /\ N e. NN ) /\ ( A mod N ) =/= 0 ) -> ( A mod N ) e. ( 1 ..^ N ) )
14 nnrp 
 |-  ( N e. NN -> N e. RR+ )
15 1 14 anim12i 
 |-  ( ( A e. ZZ /\ N e. NN ) -> ( A e. RR /\ N e. RR+ ) )
16 15 adantr 
 |-  ( ( ( A e. ZZ /\ N e. NN ) /\ ( A mod N ) =/= 0 ) -> ( A e. RR /\ N e. RR+ ) )
17 flpmodeq 
 |-  ( ( A e. RR /\ N e. RR+ ) -> ( ( ( |_ ` ( A / N ) ) x. N ) + ( A mod N ) ) = A )
18 16 17 syl 
 |-  ( ( ( A e. ZZ /\ N e. NN ) /\ ( A mod N ) =/= 0 ) -> ( ( ( |_ ` ( A / N ) ) x. N ) + ( A mod N ) ) = A )
19 18 eqcomd 
 |-  ( ( ( A e. ZZ /\ N e. NN ) /\ ( A mod N ) =/= 0 ) -> A = ( ( ( |_ ` ( A / N ) ) x. N ) + ( A mod N ) ) )
20 oveq1 
 |-  ( x = ( |_ ` ( A / N ) ) -> ( x x. N ) = ( ( |_ ` ( A / N ) ) x. N ) )
21 20 oveq1d 
 |-  ( x = ( |_ ` ( A / N ) ) -> ( ( x x. N ) + y ) = ( ( ( |_ ` ( A / N ) ) x. N ) + y ) )
22 21 eqeq2d 
 |-  ( x = ( |_ ` ( A / N ) ) -> ( A = ( ( x x. N ) + y ) <-> A = ( ( ( |_ ` ( A / N ) ) x. N ) + y ) ) )
23 oveq2 
 |-  ( y = ( A mod N ) -> ( ( ( |_ ` ( A / N ) ) x. N ) + y ) = ( ( ( |_ ` ( A / N ) ) x. N ) + ( A mod N ) ) )
24 23 eqeq2d 
 |-  ( y = ( A mod N ) -> ( A = ( ( ( |_ ` ( A / N ) ) x. N ) + y ) <-> A = ( ( ( |_ ` ( A / N ) ) x. N ) + ( A mod N ) ) ) )
25 22 24 rspc2ev 
 |-  ( ( ( |_ ` ( A / N ) ) e. ZZ /\ ( A mod N ) e. ( 1 ..^ N ) /\ A = ( ( ( |_ ` ( A / N ) ) x. N ) + ( A mod N ) ) ) -> E. x e. ZZ E. y e. ( 1 ..^ N ) A = ( ( x x. N ) + y ) )
26 9 13 19 25 syl3anc 
 |-  ( ( ( A e. ZZ /\ N e. NN ) /\ ( A mod N ) =/= 0 ) -> E. x e. ZZ E. y e. ( 1 ..^ N ) A = ( ( x x. N ) + y ) )
27 26 ex 
 |-  ( ( A e. ZZ /\ N e. NN ) -> ( ( A mod N ) =/= 0 -> E. x e. ZZ E. y e. ( 1 ..^ N ) A = ( ( x x. N ) + y ) ) )