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	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) → ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ )

Proof

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