Metamath Proof Explorer

Theorem coprmgcdb

Description: Two positive integers are coprime, i.e. the only positive integer that divides both of them is 1, iff their greatest common divisor is 1. (Contributed by AV, 9-Aug-2020)

Ref Expression
Assertion coprmgcdb ⊢ A ∈ ℕ ∧ B ∈ ℕ → ∀ i ∈ ℕ i ∥ A ∧ i ∥ B → i = 1 ↔ A gcd B = 1

Proof

Step Hyp Ref Expression
1 nnz ⊢ A ∈ ℕ → A ∈ ℤ
2 nnz ⊢ B ∈ ℕ → B ∈ ℤ
3 gcddvds ⊢ A ∈ ℤ ∧ B ∈ ℤ → A gcd B ∥ A ∧ A gcd B ∥ B
4 1 2 3 syl2an ⊢ A ∈ ℕ ∧ B ∈ ℕ → A gcd B ∥ A ∧ A gcd B ∥ B
5 simpr ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ A gcd B ∥ A ∧ A gcd B ∥ B → A gcd B ∥ A ∧ A gcd B ∥ B
6 gcdnncl ⊢ A ∈ ℕ ∧ B ∈ ℕ → A gcd B ∈ ℕ
7 6 adantr ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ A gcd B ∥ A ∧ A gcd B ∥ B → A gcd B ∈ ℕ
8 breq1 ⊢ i = A gcd B → i ∥ A ↔ A gcd B ∥ A
9 breq1 ⊢ i = A gcd B → i ∥ B ↔ A gcd B ∥ B
10 8 9 anbi12d ⊢ i = A gcd B → i ∥ A ∧ i ∥ B ↔ A gcd B ∥ A ∧ A gcd B ∥ B
11 eqeq1 ⊢ i = A gcd B → i = 1 ↔ A gcd B = 1
12 10 11 imbi12d ⊢ i = A gcd B → i ∥ A ∧ i ∥ B → i = 1 ↔ A gcd B ∥ A ∧ A gcd B ∥ B → A gcd B = 1
13 12 rspcv ⊢ A gcd B ∈ ℕ → ∀ i ∈ ℕ i ∥ A ∧ i ∥ B → i = 1 → A gcd B ∥ A ∧ A gcd B ∥ B → A gcd B = 1
14 7 13 syl ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ A gcd B ∥ A ∧ A gcd B ∥ B → ∀ i ∈ ℕ i ∥ A ∧ i ∥ B → i = 1 → A gcd B ∥ A ∧ A gcd B ∥ B → A gcd B = 1
15 5 14 mpid ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ A gcd B ∥ A ∧ A gcd B ∥ B → ∀ i ∈ ℕ i ∥ A ∧ i ∥ B → i = 1 → A gcd B = 1
16 4 15 mpdan ⊢ A ∈ ℕ ∧ B ∈ ℕ → ∀ i ∈ ℕ i ∥ A ∧ i ∥ B → i = 1 → A gcd B = 1
17 simpl ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ A gcd B = 1 → A ∈ ℕ ∧ B ∈ ℕ
18 17 anim1ci ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ A gcd B = 1 ∧ i ∈ ℕ → i ∈ ℕ ∧ A ∈ ℕ ∧ B ∈ ℕ
19 3anass ⊢ i ∈ ℕ ∧ A ∈ ℕ ∧ B ∈ ℕ ↔ i ∈ ℕ ∧ A ∈ ℕ ∧ B ∈ ℕ
20 18 19 sylibr ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ A gcd B = 1 ∧ i ∈ ℕ → i ∈ ℕ ∧ A ∈ ℕ ∧ B ∈ ℕ
21 nndvdslegcd ⊢ i ∈ ℕ ∧ A ∈ ℕ ∧ B ∈ ℕ → i ∥ A ∧ i ∥ B → i ≤ A gcd B
22 20 21 syl ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ A gcd B = 1 ∧ i ∈ ℕ → i ∥ A ∧ i ∥ B → i ≤ A gcd B
23 breq2 ⊢ A gcd B = 1 → i ≤ A gcd B ↔ i ≤ 1
24 23 adantr ⊢ A gcd B = 1 ∧ i ∈ ℕ → i ≤ A gcd B ↔ i ≤ 1
25 nnge1 ⊢ i ∈ ℕ → 1 ≤ i
26 nnre ⊢ i ∈ ℕ → i ∈ ℝ
27 1red ⊢ i ∈ ℕ → 1 ∈ ℝ
28 26 27 letri3d ⊢ i ∈ ℕ → i = 1 ↔ i ≤ 1 ∧ 1 ≤ i
29 28 biimprd ⊢ i ∈ ℕ → i ≤ 1 ∧ 1 ≤ i → i = 1
30 25 29 mpan2d ⊢ i ∈ ℕ → i ≤ 1 → i = 1
31 30 adantl ⊢ A gcd B = 1 ∧ i ∈ ℕ → i ≤ 1 → i = 1
32 24 31 sylbid ⊢ A gcd B = 1 ∧ i ∈ ℕ → i ≤ A gcd B → i = 1
33 32 adantll ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ A gcd B = 1 ∧ i ∈ ℕ → i ≤ A gcd B → i = 1
34 22 33 syld ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ A gcd B = 1 ∧ i ∈ ℕ → i ∥ A ∧ i ∥ B → i = 1
35 34 ralrimiva ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ A gcd B = 1 → ∀ i ∈ ℕ i ∥ A ∧ i ∥ B → i = 1
36 35 ex ⊢ A ∈ ℕ ∧ B ∈ ℕ → A gcd B = 1 → ∀ i ∈ ℕ i ∥ A ∧ i ∥ B → i = 1
37 16 36 impbid ⊢ A ∈ ℕ ∧ B ∈ ℕ → ∀ i ∈ ℕ i ∥ A ∧ i ∥ B → i = 1 ↔ A gcd B = 1