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 e. NN
nprmi.2 
|- B e. NN
nprmi.3 
|- 1 < A
nprmi.4 
|- 1 < B
nprmi.5 
|- ( A x. B ) = N
Assertion nprmi 
|- -. N e. Prime

Proof

Step Hyp Ref Expression
1 nprmi.1 
 |-  A e. NN
2 nprmi.2 
 |-  B e. NN
3 nprmi.3 
 |-  1 < A
4 nprmi.4 
 |-  1 < B
5 nprmi.5 
 |-  ( A x. B ) = N
6 eluz2b2 
 |-  ( A e. ( ZZ>= ` 2 ) <-> ( A e. NN /\ 1 < A ) )
7 eluz2b2 
 |-  ( B e. ( ZZ>= ` 2 ) <-> ( B e. NN /\ 1 < B ) )
8 nprm 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ B e. ( ZZ>= ` 2 ) ) -> -. ( A x. B ) e. Prime )
9 6 7 8 syl2anbr 
 |-  ( ( ( A e. NN /\ 1 < A ) /\ ( B e. NN /\ 1 < B ) ) -> -. ( A x. B ) e. Prime )
10 1 3 2 4 9 mp4an 
 |-  -. ( A x. B ) e. Prime
11 5 eleq1i 
 |-  ( ( A x. B ) e. Prime <-> N e. Prime )
12 10 11 mtbi 
 |-  -. N e. Prime