Metamath Proof Explorer

Theorem zeqzmulgcd

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

Ref Expression
Assertion zeqzmulgcd ⊢ A ∈ ℤ ∧ B ∈ ℤ → ∃ n ∈ ℤ A = n ⁢ A gcd B

Proof

Step Hyp Ref Expression
1 gcddvds ⊢ A ∈ ℤ ∧ B ∈ ℤ → A gcd B ∥ A ∧ A gcd B ∥ B
2 gcdcl ⊢ A ∈ ℤ ∧ B ∈ ℤ → A gcd B ∈ ℕ 0
3 2 nn0zd ⊢ A ∈ ℤ ∧ B ∈ ℤ → A gcd B ∈ ℤ
4 simpl ⊢ A ∈ ℤ ∧ B ∈ ℤ → A ∈ ℤ
5 divides ⊢ A gcd B ∈ ℤ ∧ A ∈ ℤ → A gcd B ∥ A ↔ ∃ n ∈ ℤ n ⁢ A gcd B = A
6 3 4 5 syl2anc ⊢ A ∈ ℤ ∧ B ∈ ℤ → A gcd B ∥ A ↔ ∃ n ∈ ℤ n ⁢ A gcd B = A
7 eqcom ⊢ n ⁢ A gcd B = A ↔ A = n ⁢ A gcd B
8 7 a1i ⊢ A ∈ ℤ ∧ B ∈ ℤ → n ⁢ A gcd B = A ↔ A = n ⁢ A gcd B
9 8 rexbidv ⊢ A ∈ ℤ ∧ B ∈ ℤ → ∃ n ∈ ℤ n ⁢ A gcd B = A ↔ ∃ n ∈ ℤ A = n ⁢ A gcd B
10 9 biimpd ⊢ A ∈ ℤ ∧ B ∈ ℤ → ∃ n ∈ ℤ n ⁢ A gcd B = A → ∃ n ∈ ℤ A = n ⁢ A gcd B
11 6 10 sylbid ⊢ A ∈ ℤ ∧ B ∈ ℤ → A gcd B ∥ A → ∃ n ∈ ℤ A = n ⁢ A gcd B
12 11 adantrd ⊢ A ∈ ℤ ∧ B ∈ ℤ → A gcd B ∥ A ∧ A gcd B ∥ B → ∃ n ∈ ℤ A = n ⁢ A gcd B
13 1 12 mpd ⊢ A ∈ ℤ ∧ B ∈ ℤ → ∃ n ∈ ℤ A = n ⁢ A gcd B