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 ⊢ N = A B
dvdszzq.2 ⊢ φ → P ∈ ℙ
dvdszzq.3 ⊢ φ → N ∈ ℤ
dvdszzq.4 ⊢ φ → B ∈ ℤ
dvdszzq.5 ⊢ φ → B ≠ 0
dvdszzq.6 ⊢ φ → P ∥ A
dvdszzq.7 ⊢ φ → ¬ P ∥ B
Assertion dvdszzq ⊢ φ → P ∥ N

Proof

Step Hyp Ref Expression
1 dvdszzq.1 ⊢ N = A B
2 dvdszzq.2 ⊢ φ → P ∈ ℙ
3 dvdszzq.3 ⊢ φ → N ∈ ℤ
4 dvdszzq.4 ⊢ φ → B ∈ ℤ
5 dvdszzq.5 ⊢ φ → B ≠ 0
6 dvdszzq.6 ⊢ φ → P ∥ A
7 dvdszzq.7 ⊢ φ → ¬ P ∥ B
8 3 zcnd ⊢ φ → N ∈ ℂ
9 4 zcnd ⊢ φ → B ∈ ℂ
10 dvdszrcl ⊢ P ∥ A → P ∈ ℤ ∧ A ∈ ℤ
11 10 simprd ⊢ P ∥ A → A ∈ ℤ
12 6 11 syl ⊢ φ → A ∈ ℤ
13 12 zcnd ⊢ φ → A ∈ ℂ
14 8 9 13 5 ldiv ⊢ φ → N ⁢ B = A ↔ N = A B
15 1 14 mpbiri ⊢ φ → N ⁢ B = A
16 6 15 breqtrrd ⊢ φ → P ∥ N ⁢ B
17 euclemma ⊢ P ∈ ℙ ∧ N ∈ ℤ ∧ B ∈ ℤ → P ∥ N ⁢ B ↔ P ∥ N ∨ P ∥ B
18 17 biimpa ⊢ P ∈ ℙ ∧ N ∈ ℤ ∧ B ∈ ℤ ∧ P ∥ N ⁢ B → P ∥ N ∨ P ∥ B
19 2 3 4 16 18 syl31anc ⊢ φ → 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 ⊢ φ → P ∥ N