Theorem dvdszzq

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

	Ref	Expression
Hypotheses	dvdszzq.1	⊢ 𝑁 = ( 𝐴 / 𝐵 )
	dvdszzq.2	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	dvdszzq.3	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
	dvdszzq.4	⊢ ( 𝜑 → 𝐵 ∈ ℤ )
	dvdszzq.5	⊢ ( 𝜑 → 𝐵 ≠ 0 )
	dvdszzq.6	⊢ ( 𝜑 → 𝑃 ∥ 𝐴 )
	dvdszzq.7	⊢ ( 𝜑 → ¬ 𝑃 ∥ 𝐵 )
Assertion	dvdszzq	⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		dvdszzq.1	⊢ 𝑁 = ( 𝐴 / 𝐵 )
2		dvdszzq.2	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
3		dvdszzq.3	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
4		dvdszzq.4	⊢ ( 𝜑 → 𝐵 ∈ ℤ )
5		dvdszzq.5	⊢ ( 𝜑 → 𝐵 ≠ 0 )
6		dvdszzq.6	⊢ ( 𝜑 → 𝑃 ∥ 𝐴 )
7		dvdszzq.7	⊢ ( 𝜑 → ¬ 𝑃 ∥ 𝐵 )
8	3	zcnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
9	4	zcnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
10		dvdszrcl	⊢ ( 𝑃 ∥ 𝐴 → ( 𝑃 ∈ ℤ ∧ 𝐴 ∈ ℤ ) )
11	10	simprd	⊢ ( 𝑃 ∥ 𝐴 → 𝐴 ∈ ℤ )
12	6 11	syl	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
13	12	zcnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
14	8 9 13 5	ldiv	⊢ ( 𝜑 → ( ( 𝑁 · 𝐵 ) = 𝐴 ↔ 𝑁 = ( 𝐴 / 𝐵 ) ) )
15	1 14	mpbiri	⊢ ( 𝜑 → ( 𝑁 · 𝐵 ) = 𝐴 )
16	6 15	breqtrrd	⊢ ( 𝜑 → 𝑃 ∥ ( 𝑁 · 𝐵 ) )
17		euclemma	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝑃 ∥ ( 𝑁 · 𝐵 ) ↔ ( 𝑃 ∥ 𝑁 ∨ 𝑃 ∥ 𝐵 ) ) )
18	17	biimpa	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝑃 ∥ ( 𝑁 · 𝐵 ) ) → ( 𝑃 ∥ 𝑁 ∨ 𝑃 ∥ 𝐵 ) )
19	2 3 4 16 18	syl31anc	⊢ ( 𝜑 → ( 𝑃 ∥ 𝑁 ∨ 𝑃 ∥ 𝐵 ) )
20		orcom	⊢ ( ( 𝑃 ∥ 𝑁 ∨ 𝑃 ∥ 𝐵 ) ↔ ( 𝑃 ∥ 𝐵 ∨ 𝑃 ∥ 𝑁 ) )
21		df-or	⊢ ( ( 𝑃 ∥ 𝐵 ∨ 𝑃 ∥ 𝑁 ) ↔ ( ¬ 𝑃 ∥ 𝐵 → 𝑃 ∥ 𝑁 ) )
22	20 21	sylbb	⊢ ( ( 𝑃 ∥ 𝑁 ∨ 𝑃 ∥ 𝐵 ) → ( ¬ 𝑃 ∥ 𝐵 → 𝑃 ∥ 𝑁 ) )
23	19 7 22	sylc	⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )