Metamath Proof Explorer

Theorem coprmdvds1

Description: If two positive integers are coprime, i.e. their greatest common divisor is 1, the only positive integer that divides both of them is 1. (Contributed by AV, 4-Aug-2021)

Ref Expression
Assertion coprmdvds1 ⊢ F ∈ ℕ ∧ G ∈ ℕ ∧ F gcd G = 1 → I ∈ ℕ ∧ I ∥ F ∧ I ∥ G → I = 1

Proof

Step Hyp Ref Expression
1 coprmgcdb ⊢ F ∈ ℕ ∧ G ∈ ℕ → ∀ i ∈ ℕ i ∥ F ∧ i ∥ G → i = 1 ↔ F gcd G = 1
2 breq1 ⊢ i = I → i ∥ F ↔ I ∥ F
3 breq1 ⊢ i = I → i ∥ G ↔ I ∥ G
4 2 3 anbi12d ⊢ i = I → i ∥ F ∧ i ∥ G ↔ I ∥ F ∧ I ∥ G
5 eqeq1 ⊢ i = I → i = 1 ↔ I = 1
6 4 5 imbi12d ⊢ i = I → i ∥ F ∧ i ∥ G → i = 1 ↔ I ∥ F ∧ I ∥ G → I = 1
7 6 rspcv ⊢ I ∈ ℕ → ∀ i ∈ ℕ i ∥ F ∧ i ∥ G → i = 1 → I ∥ F ∧ I ∥ G → I = 1
8 7 com23 ⊢ I ∈ ℕ → I ∥ F ∧ I ∥ G → ∀ i ∈ ℕ i ∥ F ∧ i ∥ G → i = 1 → I = 1
9 8 3impib ⊢ I ∈ ℕ ∧ I ∥ F ∧ I ∥ G → ∀ i ∈ ℕ i ∥ F ∧ i ∥ G → i = 1 → I = 1
10 9 com12 ⊢ ∀ i ∈ ℕ i ∥ F ∧ i ∥ G → i = 1 → I ∈ ℕ ∧ I ∥ F ∧ I ∥ G → I = 1
11 1 10 biimtrrdi ⊢ F ∈ ℕ ∧ G ∈ ℕ → F gcd G = 1 → I ∈ ℕ ∧ I ∥ F ∧ I ∥ G → I = 1
12 11 3impia ⊢ F ∈ ℕ ∧ G ∈ ℕ ∧ F gcd G = 1 → I ∈ ℕ ∧ I ∥ F ∧ I ∥ G → I = 1