Theorem aks4d1p8d1

Description: If a prime divides one number M , but not another number N , then it divides the quotient of M and the gcd of M and N . (Contributed by Thierry Arnoux, 10-Nov-2024)

	Ref	Expression
Hypotheses	aks4d1p8d1.1	|- ( ph -> P e. Prime )
	aks4d1p8d1.2	|- ( ph -> M e. NN )
	aks4d1p8d1.3	|- ( ph -> N e. NN )
	aks4d1p8d1.4	|- ( ph -> P || M )
	aks4d1p8d1.5	|- ( ph -> -. P || N )
Assertion	aks4d1p8d1	|- ( ph -> P || ( M / ( M gcd N ) ) )

Proof

Step	Hyp	Ref	Expression
1		aks4d1p8d1.1	|- ( ph -> P e. Prime )
2		aks4d1p8d1.2	|- ( ph -> M e. NN )
3		aks4d1p8d1.3	|- ( ph -> N e. NN )
4		aks4d1p8d1.4	|- ( ph -> P || M )
5		aks4d1p8d1.5	|- ( ph -> -. P || N )
6		prmnn	|- ( P e. Prime -> P e. NN )
7	1 6	syl	|- ( ph -> P e. NN )
8	7	nnzd	|- ( ph -> P e. ZZ )
9		gcdnncl	|- ( ( M e. NN /\ N e. NN ) -> ( M gcd N ) e. NN )
10	2 3 9	syl2anc	|- ( ph -> ( M gcd N ) e. NN )
11	10	nnzd	|- ( ph -> ( M gcd N ) e. ZZ )
12	2	nnzd	|- ( ph -> M e. ZZ )
13	5	intnand	|- ( ph -> -. ( P || M /\ P || N ) )
14	3	nnzd	|- ( ph -> N e. ZZ )
15		dvdsgcdb	|- ( ( P e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( P || M /\ P || N ) <-> P || ( M gcd N ) ) )
16	8 12 14 15	syl3anc	|- ( ph -> ( ( P || M /\ P || N ) <-> P || ( M gcd N ) ) )
17	13 16	mtbid	|- ( ph -> -. P || ( M gcd N ) )
18		coprm	|- ( ( P e. Prime /\ ( M gcd N ) e. ZZ ) -> ( -. P || ( M gcd N ) <-> ( P gcd ( M gcd N ) ) = 1 ) )
19	18	biimpa	|- ( ( ( P e. Prime /\ ( M gcd N ) e. ZZ ) /\ -. P || ( M gcd N ) ) -> ( P gcd ( M gcd N ) ) = 1 )
20	1 11 17 19	syl21anc	|- ( ph -> ( P gcd ( M gcd N ) ) = 1 )
21		gcddvds	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M gcd N ) || M /\ ( M gcd N ) || N ) )
22	12 14 21	syl2anc	|- ( ph -> ( ( M gcd N ) || M /\ ( M gcd N ) || N ) )
23	22	simpld	|- ( ph -> ( M gcd N ) || M )
24	8 11 12 20 4 23	coprmdvds2d	|- ( ph -> ( P x. ( M gcd N ) ) || M )
25	7 10 2	nnproddivdvdsd	|- ( ph -> ( ( P x. ( M gcd N ) ) || M <-> P || ( M / ( M gcd N ) ) ) )
26	24 25	mpbid	|- ( ph -> P || ( M / ( M gcd N ) ) )