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	⊢ ( ( 𝐹 ∈ ℕ ∧ 𝐺 ∈ ℕ ∧ ( 𝐹 gcd 𝐺 ) = 1 ) → ( ( 𝐼 ∈ ℕ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) → 𝐼 = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		coprmgcdb	⊢ ( ( 𝐹 ∈ ℕ ∧ 𝐺 ∈ ℕ ) → ( ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐹 ∧ 𝑖 ∥ 𝐺 ) → 𝑖 = 1 ) ↔ ( 𝐹 gcd 𝐺 ) = 1 ) )
2		breq1	⊢ ( 𝑖 = 𝐼 → ( 𝑖 ∥ 𝐹 ↔ 𝐼 ∥ 𝐹 ) )
3		breq1	⊢ ( 𝑖 = 𝐼 → ( 𝑖 ∥ 𝐺 ↔ 𝐼 ∥ 𝐺 ) )
4	2 3	anbi12d	⊢ ( 𝑖 = 𝐼 → ( ( 𝑖 ∥ 𝐹 ∧ 𝑖 ∥ 𝐺 ) ↔ ( 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) ) )
5		eqeq1	⊢ ( 𝑖 = 𝐼 → ( 𝑖 = 1 ↔ 𝐼 = 1 ) )
6	4 5	imbi12d	⊢ ( 𝑖 = 𝐼 → ( ( ( 𝑖 ∥ 𝐹 ∧ 𝑖 ∥ 𝐺 ) → 𝑖 = 1 ) ↔ ( ( 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) → 𝐼 = 1 ) ) )
7	6	rspcv	⊢ ( 𝐼 ∈ ℕ → ( ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐹 ∧ 𝑖 ∥ 𝐺 ) → 𝑖 = 1 ) → ( ( 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) → 𝐼 = 1 ) ) )
8	7	com23	⊢ ( 𝐼 ∈ ℕ → ( ( 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) → ( ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐹 ∧ 𝑖 ∥ 𝐺 ) → 𝑖 = 1 ) → 𝐼 = 1 ) ) )
9	8	3impib	⊢ ( ( 𝐼 ∈ ℕ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) → ( ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐹 ∧ 𝑖 ∥ 𝐺 ) → 𝑖 = 1 ) → 𝐼 = 1 ) )
10	9	com12	⊢ ( ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐹 ∧ 𝑖 ∥ 𝐺 ) → 𝑖 = 1 ) → ( ( 𝐼 ∈ ℕ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) → 𝐼 = 1 ) )
11	1 10	syl6bir	⊢ ( ( 𝐹 ∈ ℕ ∧ 𝐺 ∈ ℕ ) → ( ( 𝐹 gcd 𝐺 ) = 1 → ( ( 𝐼 ∈ ℕ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) → 𝐼 = 1 ) ) )
12	11	3impia	⊢ ( ( 𝐹 ∈ ℕ ∧ 𝐺 ∈ ℕ ∧ ( 𝐹 gcd 𝐺 ) = 1 ) → ( ( 𝐼 ∈ ℕ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺 ) → 𝐼 = 1 ) )