Metamath Proof Explorer

Theorem gcdzeq

Description: A positive integer A is equal to its gcd with an integer B if and only if A divides B . Generalization of gcdeq . (Contributed by AV, 1-Jul-2020)

Ref Expression
Assertion gcdzeq ⊢ A ∈ ℕ ∧ B ∈ ℤ → A gcd B = A ↔ A ∥ B

Proof

Step Hyp Ref Expression
1 nnz ⊢ A ∈ ℕ → A ∈ ℤ
2 gcddvds ⊢ A ∈ ℤ ∧ B ∈ ℤ → A gcd B ∥ A ∧ A gcd B ∥ B
3 1 2 sylan ⊢ A ∈ ℕ ∧ B ∈ ℤ → A gcd B ∥ A ∧ A gcd B ∥ B
4 3 simprd ⊢ A ∈ ℕ ∧ B ∈ ℤ → A gcd B ∥ B
5 breq1 ⊢ A gcd B = A → A gcd B ∥ B ↔ A ∥ B
6 4 5 syl5ibcom ⊢ A ∈ ℕ ∧ B ∈ ℤ → A gcd B = A → A ∥ B
7 1 adantr ⊢ A ∈ ℕ ∧ B ∈ ℤ → A ∈ ℤ
8 iddvds ⊢ A ∈ ℤ → A ∥ A
9 7 8 syl ⊢ A ∈ ℕ ∧ B ∈ ℤ → A ∥ A
10 simpr ⊢ A ∈ ℕ ∧ B ∈ ℤ → B ∈ ℤ
11 nnne0 ⊢ A ∈ ℕ → A ≠ 0
12 simpl ⊢ A = 0 ∧ B = 0 → A = 0
13 12 necon3ai ⊢ A ≠ 0 → ¬ A = 0 ∧ B = 0
14 11 13 syl ⊢ A ∈ ℕ → ¬ A = 0 ∧ B = 0
15 14 adantr ⊢ A ∈ ℕ ∧ B ∈ ℤ → ¬ A = 0 ∧ B = 0
16 dvdslegcd ⊢ A ∈ ℤ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ A = 0 ∧ B = 0 → A ∥ A ∧ A ∥ B → A ≤ A gcd B
17 7 7 10 15 16 syl31anc ⊢ A ∈ ℕ ∧ B ∈ ℤ → A ∥ A ∧ A ∥ B → A ≤ A gcd B
18 9 17 mpand ⊢ A ∈ ℕ ∧ B ∈ ℤ → A ∥ B → A ≤ A gcd B
19 3 simpld ⊢ A ∈ ℕ ∧ B ∈ ℤ → A gcd B ∥ A
20 gcdcl ⊢ A ∈ ℤ ∧ B ∈ ℤ → A gcd B ∈ ℕ 0
21 1 20 sylan ⊢ A ∈ ℕ ∧ B ∈ ℤ → A gcd B ∈ ℕ 0
22 21 nn0zd ⊢ A ∈ ℕ ∧ B ∈ ℤ → A gcd B ∈ ℤ
23 simpl ⊢ A ∈ ℕ ∧ B ∈ ℤ → A ∈ ℕ
24 dvdsle ⊢ A gcd B ∈ ℤ ∧ A ∈ ℕ → A gcd B ∥ A → A gcd B ≤ A
25 22 23 24 syl2anc ⊢ A ∈ ℕ ∧ B ∈ ℤ → A gcd B ∥ A → A gcd B ≤ A
26 19 25 mpd ⊢ A ∈ ℕ ∧ B ∈ ℤ → A gcd B ≤ A
27 18 26 jctild ⊢ A ∈ ℕ ∧ B ∈ ℤ → A ∥ B → A gcd B ≤ A ∧ A ≤ A gcd B
28 21 nn0red ⊢ A ∈ ℕ ∧ B ∈ ℤ → A gcd B ∈ ℝ
29 nnre ⊢ A ∈ ℕ → A ∈ ℝ
30 29 adantr ⊢ A ∈ ℕ ∧ B ∈ ℤ → A ∈ ℝ
31 28 30 letri3d ⊢ A ∈ ℕ ∧ B ∈ ℤ → A gcd B = A ↔ A gcd B ≤ A ∧ A ≤ A gcd B
32 27 31 sylibrd ⊢ A ∈ ℕ ∧ B ∈ ℤ → A ∥ B → A gcd B = A
33 6 32 impbid ⊢ A ∈ ℕ ∧ B ∈ ℤ → A gcd B = A ↔ A ∥ B