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 ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) = 𝐴 ↔ 𝐴 ∥ 𝐵 ) )

Proof

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