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 \in ℕ \land G \in ℕ \land F \gcd G = 1) \to ((I \in ℕ \land I ∥ F \land I ∥ G) \to I = 1)$

Proof

Step	Hyp	Ref	Expression
1		coprmgcdb	$⊢ (F \in ℕ \land G \in ℕ) \to (\forall i \in ℕ ((i ∥ F \land i ∥ G) \to i = 1) \leftrightarrow F \gcd G = 1)$
2		breq1	$⊢ i = I \to (i ∥ F \leftrightarrow I ∥ F)$
3		breq1	$⊢ i = I \to (i ∥ G \leftrightarrow I ∥ G)$
4	2 3	anbi12d	$⊢ i = I \to ((i ∥ F \land i ∥ G) \leftrightarrow (I ∥ F \land I ∥ G))$
5		eqeq1	$⊢ i = I \to (i = 1 \leftrightarrow I = 1)$
6	4 5	imbi12d	$⊢ i = I \to (((i ∥ F \land i ∥ G) \to i = 1) \leftrightarrow ((I ∥ F \land I ∥ G) \to I = 1))$
7	6	rspcv	$⊢ I \in ℕ \to (\forall i \in ℕ ((i ∥ F \land i ∥ G) \to i = 1) \to ((I ∥ F \land I ∥ G) \to I = 1))$
8	7	com23	$⊢ I \in ℕ \to ((I ∥ F \land I ∥ G) \to (\forall i \in ℕ ((i ∥ F \land i ∥ G) \to i = 1) \to I = 1))$
9	8	3impib	$⊢ (I \in ℕ \land I ∥ F \land I ∥ G) \to (\forall i \in ℕ ((i ∥ F \land i ∥ G) \to i = 1) \to I = 1)$
10	9	com12	$⊢ \forall i \in ℕ ((i ∥ F \land i ∥ G) \to i = 1) \to ((I \in ℕ \land I ∥ F \land I ∥ G) \to I = 1)$
11	1 10	syl6bir	$⊢ (F \in ℕ \land G \in ℕ) \to (F \gcd G = 1 \to ((I \in ℕ \land I ∥ F \land I ∥ G) \to I = 1))$
12	11	3impia	$⊢ (F \in ℕ \land G \in ℕ \land F \gcd G = 1) \to ((I \in ℕ \land I ∥ F \land I ∥ G) \to I = 1)$