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 e. NN /\ G e. NN /\ ( F gcd G ) = 1 ) -> ( ( I e. NN /\ I || F /\ I || G ) -> I = 1 ) )

Proof

Step Hyp Ref Expression
1 coprmgcdb 
 |-  ( ( F e. NN /\ G e. NN ) -> ( A. i e. NN ( ( 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 e. NN -> ( A. i e. NN ( ( i || F /\ i || G ) -> i = 1 ) -> ( ( I || F /\ I || G ) -> I = 1 ) ) )
8 7 com23 
 |-  ( I e. NN -> ( ( I || F /\ I || G ) -> ( A. i e. NN ( ( i || F /\ i || G ) -> i = 1 ) -> I = 1 ) ) )
9 8 3impib 
 |-  ( ( I e. NN /\ I || F /\ I || G ) -> ( A. i e. NN ( ( i || F /\ i || G ) -> i = 1 ) -> I = 1 ) )
10 9 com12 
 |-  ( A. i e. NN ( ( i || F /\ i || G ) -> i = 1 ) -> ( ( I e. NN /\ I || F /\ I || G ) -> I = 1 ) )
11 1 10 syl6bir 
 |-  ( ( F e. NN /\ G e. NN ) -> ( ( F gcd G ) = 1 -> ( ( I e. NN /\ I || F /\ I || G ) -> I = 1 ) ) )
12 11 3impia 
 |-  ( ( F e. NN /\ G e. NN /\ ( F gcd G ) = 1 ) -> ( ( I e. NN /\ I || F /\ I || G ) -> I = 1 ) )