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 𝐵 ) ) )