This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )