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

Metamath Proof Explorer

Theorem nprmi

Description: An inference for compositeness. (Contributed by Mario Carneiro, 18-Feb-2014) (Revised by Mario Carneiro, 20-Jun-2015)

Ref Expression
Hypotheses nprmi.1 ⊢ A ∈ ℕ
nprmi.2 ⊢ B ∈ ℕ
nprmi.3 ⊢ 1 < A
nprmi.4 ⊢ 1 < B
nprmi.5 ⊢ A ⁢ B = N
Assertion nprmi ⊢ ¬ N ∈ ℙ

Proof

Step Hyp Ref Expression
1 nprmi.1 ⊢ A ∈ ℕ
2 nprmi.2 ⊢ B ∈ ℕ
3 nprmi.3 ⊢ 1 < A
4 nprmi.4 ⊢ 1 < B
5 nprmi.5 ⊢ A ⁢ B = N
6 eluz2b2 ⊢ A ∈ ℤ ≥ 2 ↔ A ∈ ℕ ∧ 1 < A
7 eluz2b2 ⊢ B ∈ ℤ ≥ 2 ↔ B ∈ ℕ ∧ 1 < B
8 nprm ⊢ A ∈ ℤ ≥ 2 ∧ B ∈ ℤ ≥ 2 → ¬ A ⁢ B ∈ ℙ
9 6 7 8 syl2anbr ⊢ A ∈ ℕ ∧ 1 < A ∧ B ∈ ℕ ∧ 1 < B → ¬ A ⁢ B ∈ ℙ
10 1 3 2 4 9 mp4an ⊢ ¬ A ⁢ B ∈ ℙ
11 5 eleq1i ⊢ A ⁢ B ∈ ℙ ↔ N ∈ ℙ
12 10 11 mtbi ⊢ ¬ N ∈ ℙ