Theorem dvdszzq

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

	Ref	Expression
Hypotheses	dvdszzq.1	$$⊢N=\frac{A}{B}$$
	dvdszzq.2	$$⊢\phi \to P\in \mathbb{P}$$
	dvdszzq.3	$$⊢\phi \to N\in \mathbb{Z}$$
	dvdszzq.4	$$⊢\phi \to B\in \mathbb{Z}$$
	dvdszzq.5	$$⊢\phi \to B\ne 0$$
	dvdszzq.6	$$⊢\phi \to P\parallel A$$
	dvdszzq.7	$$⊢\phi \to \neg P\parallel B$$
Assertion	dvdszzq	$$⊢\phi \to P\parallel N$$

Proof

Step	Hyp	Ref	Expression
1		dvdszzq.1	$$⊢N=\frac{A}{B}$$
2		dvdszzq.2	$$⊢\phi \to P\in \mathbb{P}$$
3		dvdszzq.3	$$⊢\phi \to N\in \mathbb{Z}$$
4		dvdszzq.4	$$⊢\phi \to B\in \mathbb{Z}$$
5		dvdszzq.5	$$⊢\phi \to B\ne 0$$
6		dvdszzq.6	$$⊢\phi \to P\parallel A$$
7		dvdszzq.7	$$⊢\phi \to \neg P\parallel B$$
8	3	zcnd	$$⊢\phi \to N\in ℂ$$
9	4	zcnd	$$⊢\phi \to B\in ℂ$$
10		dvdszrcl	$$⊢P\parallel A\to \left(P\in \mathbb{Z}\wedge A\in \mathbb{Z}\right)$$
11	10	simprd	$$⊢P\parallel A\to A\in \mathbb{Z}$$
12	6 11	syl	$$⊢\phi \to A\in \mathbb{Z}$$
13	12	zcnd	$$⊢\phi \to A\in ℂ$$
14	8 9 13 5	ldiv	$$⊢\phi \to \left(NB=A\leftrightarrow N=\frac{A}{B}\right)$$
15	1 14	mpbiri	$$⊢\phi \to NB=A$$
16	6 15	breqtrrd	$$⊢\phi \to P\parallel NB$$
17		euclemma	$$⊢\left(P\in \mathbb{P}\wedge N\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\to \left(P\parallel NB\leftrightarrow \left(P\parallel N\vee P\parallel B\right)\right)$$
18	17	biimpa	$$⊢\left(\left(P\in \mathbb{P}\wedge N\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\wedge P\parallel NB\right)\to \left(P\parallel N\vee P\parallel B\right)$$
19	2 3 4 16 18	syl31anc	$$⊢\phi \to \left(P\parallel N\vee P\parallel B\right)$$
20		orcom	$$⊢\left(P\parallel N\vee P\parallel B\right)\leftrightarrow \left(P\parallel B\vee P\parallel N\right)$$
21		df-or	$$⊢\left(P\parallel B\vee P\parallel N\right)\leftrightarrow \left(\neg P\parallel B\to P\parallel N\right)$$
22	20 21	sylbb	$$⊢\left(P\parallel N\vee P\parallel B\right)\to \left(\neg P\parallel B\to P\parallel N\right)$$
23	19 7 22	sylc	$$⊢\phi \to P\parallel N$$