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	⊢ 𝐴 ∈ ℕ
	nprmi.2	⊢ 𝐵 ∈ ℕ
	nprmi.3	⊢ 1 < 𝐴
	nprmi.4	⊢ 1 < 𝐵
	nprmi.5	⊢ ( 𝐴 · 𝐵 ) = 𝑁
Assertion	nprmi	⊢ ¬ 𝑁 ∈ ℙ

Proof

Step	Hyp	Ref	Expression
1		nprmi.1	⊢ 𝐴 ∈ ℕ
2		nprmi.2	⊢ 𝐵 ∈ ℕ
3		nprmi.3	⊢ 1 < 𝐴
4		nprmi.4	⊢ 1 < 𝐵
5		nprmi.5	⊢ ( 𝐴 · 𝐵 ) = 𝑁
6		eluz2b2	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝐴 ∈ ℕ ∧ 1 < 𝐴 ) )
7		eluz2b2	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝐵 ∈ ℕ ∧ 1 < 𝐵 ) )
8		nprm	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ¬ ( 𝐴 · 𝐵 ) ∈ ℙ )
9	6 7 8	syl2anbr	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℕ ∧ 1 < 𝐵 ) ) → ¬ ( 𝐴 · 𝐵 ) ∈ ℙ )
10	1 3 2 4 9	mp4an	⊢ ¬ ( 𝐴 · 𝐵 ) ∈ ℙ
11	5	eleq1i	⊢ ( ( 𝐴 · 𝐵 ) ∈ ℙ ↔ 𝑁 ∈ ℙ )
12	10 11	mtbi	⊢ ¬ 𝑁 ∈ ℙ