Theorem dvdszzq

Description: Divisibility for an integer quotient. (Contributed by Thierry Arnoux, 17-Sep-2023)

	Ref	Expression
Hypotheses	dvdszzq.1	|- N = ( A / B )
	dvdszzq.2	|- ( ph -> P e. Prime )
	dvdszzq.3	|- ( ph -> N e. ZZ )
	dvdszzq.4	|- ( ph -> B e. ZZ )
	dvdszzq.5	|- ( ph -> B =/= 0 )
	dvdszzq.6	|- ( ph -> P || A )
	dvdszzq.7	|- ( ph -> -. P || B )
Assertion	dvdszzq	|- ( ph -> P || N )

Proof

Step	Hyp	Ref	Expression
1		dvdszzq.1	|- N = ( A / B )
2		dvdszzq.2	|- ( ph -> P e. Prime )
3		dvdszzq.3	|- ( ph -> N e. ZZ )
4		dvdszzq.4	|- ( ph -> B e. ZZ )
5		dvdszzq.5	|- ( ph -> B =/= 0 )
6		dvdszzq.6	|- ( ph -> P || A )
7		dvdszzq.7	|- ( ph -> -. P || B )
8	3	zcnd	|- ( ph -> N e. CC )
9	4	zcnd	|- ( ph -> B e. CC )
10		dvdszrcl	|- ( P || A -> ( P e. ZZ /\ A e. ZZ ) )
11	10	simprd	|- ( P || A -> A e. ZZ )
12	6 11	syl	|- ( ph -> A e. ZZ )
13	12	zcnd	|- ( ph -> A e. CC )
14	8 9 13 5	ldiv	|- ( ph -> ( ( N x. B ) = A <-> N = ( A / B ) ) )
15	1 14	mpbiri	|- ( ph -> ( N x. B ) = A )
16	6 15	breqtrrd	|- ( ph -> P || ( N x. B ) )
17		euclemma	|- ( ( P e. Prime /\ N e. ZZ /\ B e. ZZ ) -> ( P || ( N x. B ) <-> ( P || N \/ P || B ) ) )
18	17	biimpa	|- ( ( ( P e. Prime /\ N e. ZZ /\ B e. ZZ ) /\ P || ( N x. B ) ) -> ( P || N \/ P || B ) )
19	2 3 4 16 18	syl31anc	|- ( ph -> ( P || N \/ P || B ) )
20		orcom	|- ( ( P || N \/ P || B ) <-> ( P || B \/ P || N ) )
21		df-or	|- ( ( P || B \/ P || N ) <-> ( -. P || B -> P || N ) )
22	20 21	sylbb	|- ( ( P || N \/ P || B ) -> ( -. P || B -> P || N ) )
23	19 7 22	sylc	|- ( ph -> P || N )