This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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