Metamath Proof Explorer

Theorem divgcdz

Description: An integer divided by the gcd of it and a nonzero integer is an integer. (Contributed by AV, 11-Jul-2021)

Ref Expression
Assertion divgcdz ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≠ 0 → A A gcd B ∈ ℤ

Proof

Step Hyp Ref Expression
1 gcddvds ⊢ A ∈ ℤ ∧ B ∈ ℤ → A gcd B ∥ A ∧ A gcd B ∥ B
2 1 3adant3 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≠ 0 → A gcd B ∥ A ∧ A gcd B ∥ B
3 2 simpld ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≠ 0 → A gcd B ∥ A
4 gcd2n0cl ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≠ 0 → A gcd B ∈ ℕ
5 nnz ⊢ A gcd B ∈ ℕ → A gcd B ∈ ℤ
6 nnne0 ⊢ A gcd B ∈ ℕ → A gcd B ≠ 0
7 5 6 jca ⊢ A gcd B ∈ ℕ → A gcd B ∈ ℤ ∧ A gcd B ≠ 0
8 4 7 syl ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≠ 0 → A gcd B ∈ ℤ ∧ A gcd B ≠ 0
9 simp1 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≠ 0 → A ∈ ℤ
10 df-3an ⊢ A gcd B ∈ ℤ ∧ A gcd B ≠ 0 ∧ A ∈ ℤ ↔ A gcd B ∈ ℤ ∧ A gcd B ≠ 0 ∧ A ∈ ℤ
11 8 9 10 sylanbrc ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≠ 0 → A gcd B ∈ ℤ ∧ A gcd B ≠ 0 ∧ A ∈ ℤ
12 dvdsval2 ⊢ A gcd B ∈ ℤ ∧ A gcd B ≠ 0 ∧ A ∈ ℤ → A gcd B ∥ A ↔ A A gcd B ∈ ℤ
13 11 12 syl ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≠ 0 → A gcd B ∥ A ↔ A A gcd B ∈ ℤ
14 3 13 mpbid ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ B ≠ 0 → A A gcd B ∈ ℤ