# 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 ${⊢}\left({F}\in ℕ\wedge {G}\in ℕ\wedge {F}\mathrm{gcd}{G}=1\right)\to \left(\left({I}\in ℕ\wedge {I}\parallel {F}\wedge {I}\parallel {G}\right)\to {I}=1\right)$

### Proof

Step Hyp Ref Expression
1 coprmgcdb ${⊢}\left({F}\in ℕ\wedge {G}\in ℕ\right)\to \left(\forall {i}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({i}\parallel {F}\wedge {i}\parallel {G}\right)\to {i}=1\right)↔{F}\mathrm{gcd}{G}=1\right)$
2 breq1 ${⊢}{i}={I}\to \left({i}\parallel {F}↔{I}\parallel {F}\right)$
3 breq1 ${⊢}{i}={I}\to \left({i}\parallel {G}↔{I}\parallel {G}\right)$
4 2 3 anbi12d ${⊢}{i}={I}\to \left(\left({i}\parallel {F}\wedge {i}\parallel {G}\right)↔\left({I}\parallel {F}\wedge {I}\parallel {G}\right)\right)$
5 eqeq1 ${⊢}{i}={I}\to \left({i}=1↔{I}=1\right)$
6 4 5 imbi12d ${⊢}{i}={I}\to \left(\left(\left({i}\parallel {F}\wedge {i}\parallel {G}\right)\to {i}=1\right)↔\left(\left({I}\parallel {F}\wedge {I}\parallel {G}\right)\to {I}=1\right)\right)$
7 6 rspcv ${⊢}{I}\in ℕ\to \left(\forall {i}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({i}\parallel {F}\wedge {i}\parallel {G}\right)\to {i}=1\right)\to \left(\left({I}\parallel {F}\wedge {I}\parallel {G}\right)\to {I}=1\right)\right)$
8 7 com23 ${⊢}{I}\in ℕ\to \left(\left({I}\parallel {F}\wedge {I}\parallel {G}\right)\to \left(\forall {i}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({i}\parallel {F}\wedge {i}\parallel {G}\right)\to {i}=1\right)\to {I}=1\right)\right)$
9 8 3impib ${⊢}\left({I}\in ℕ\wedge {I}\parallel {F}\wedge {I}\parallel {G}\right)\to \left(\forall {i}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({i}\parallel {F}\wedge {i}\parallel {G}\right)\to {i}=1\right)\to {I}=1\right)$
10 9 com12 ${⊢}\forall {i}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({i}\parallel {F}\wedge {i}\parallel {G}\right)\to {i}=1\right)\to \left(\left({I}\in ℕ\wedge {I}\parallel {F}\wedge {I}\parallel {G}\right)\to {I}=1\right)$
11 1 10 syl6bir ${⊢}\left({F}\in ℕ\wedge {G}\in ℕ\right)\to \left({F}\mathrm{gcd}{G}=1\to \left(\left({I}\in ℕ\wedge {I}\parallel {F}\wedge {I}\parallel {G}\right)\to {I}=1\right)\right)$
12 11 3impia ${⊢}\left({F}\in ℕ\wedge {G}\in ℕ\wedge {F}\mathrm{gcd}{G}=1\right)\to \left(\left({I}\in ℕ\wedge {I}\parallel {F}\wedge {I}\parallel {G}\right)\to {I}=1\right)$