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

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 ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ∃ 𝑛 ∈ ℤ 𝐴 = ( 𝑛 · ( 𝐴 gcd 𝐵 ) ) )

Proof

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