Theorem mod0mul

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

	Ref	Expression
Assertion	mod0mul	|- ( ( A e. ZZ /\ N e. NN ) -> ( ( A mod N ) = 0 -> E. x e. ZZ A = ( x x. N ) ) )

Proof

Step	Hyp	Ref	Expression
1		zre	|- ( A e. ZZ -> A e. RR )
2		nnrp	|- ( N e. NN -> N e. RR+ )
3		mod0	|- ( ( A e. RR /\ N e. RR+ ) -> ( ( A mod N ) = 0 <-> ( A / N ) e. ZZ ) )
4	1 2 3	syl2an	|- ( ( A e. ZZ /\ N e. NN ) -> ( ( A mod N ) = 0 <-> ( A / N ) e. ZZ ) )
5		simpr	|- ( ( ( A e. ZZ /\ N e. NN ) /\ ( A / N ) e. ZZ ) -> ( A / N ) e. ZZ )
6		oveq1	|- ( x = ( A / N ) -> ( x x. N ) = ( ( A / N ) x. N ) )
7	6	eqeq2d	|- ( x = ( A / N ) -> ( A = ( x x. N ) <-> A = ( ( A / N ) x. N ) ) )
8	7	adantl	|- ( ( ( ( A e. ZZ /\ N e. NN ) /\ ( A / N ) e. ZZ ) /\ x = ( A / N ) ) -> ( A = ( x x. N ) <-> A = ( ( A / N ) x. N ) ) )
9		zcn	|- ( A e. ZZ -> A e. CC )
10	9	adantr	|- ( ( A e. ZZ /\ N e. NN ) -> A e. CC )
11		nncn	|- ( N e. NN -> N e. CC )
12	11	adantl	|- ( ( A e. ZZ /\ N e. NN ) -> N e. CC )
13		nnne0	|- ( N e. NN -> N =/= 0 )
14	13	adantl	|- ( ( A e. ZZ /\ N e. NN ) -> N =/= 0 )
15	10 12 14	divcan1d	|- ( ( A e. ZZ /\ N e. NN ) -> ( ( A / N ) x. N ) = A )
16	15	adantr	|- ( ( ( A e. ZZ /\ N e. NN ) /\ ( A / N ) e. ZZ ) -> ( ( A / N ) x. N ) = A )
17	16	eqcomd	|- ( ( ( A e. ZZ /\ N e. NN ) /\ ( A / N ) e. ZZ ) -> A = ( ( A / N ) x. N ) )
18	5 8 17	rspcedvd	|- ( ( ( A e. ZZ /\ N e. NN ) /\ ( A / N ) e. ZZ ) -> E. x e. ZZ A = ( x x. N ) )
19	18	ex	|- ( ( A e. ZZ /\ N e. NN ) -> ( ( A / N ) e. ZZ -> E. x e. ZZ A = ( x x. N ) ) )
20	4 19	sylbid	|- ( ( A e. ZZ /\ N e. NN ) -> ( ( A mod N ) = 0 -> E. x e. ZZ A = ( x x. N ) ) )