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

Metamath Proof Explorer

Theorem nprm

Description: A product of two integers greater than one is composite. (Contributed by Mario Carneiro, 20-Jun-2015)

Ref Expression
Assertion nprm 
|- ( ( A e. ( ZZ>= ` 2 ) /\ B e. ( ZZ>= ` 2 ) ) -> -. ( A x. B ) e. Prime )

Proof

Step Hyp Ref Expression
1 eluzelz 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. ZZ )
2 1 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ B e. ( ZZ>= ` 2 ) ) -> A e. ZZ )
3 2 zred 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ B e. ( ZZ>= ` 2 ) ) -> A e. RR )
4 eluz2gt1 
 |-  ( B e. ( ZZ>= ` 2 ) -> 1 < B )
5 4 adantl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ B e. ( ZZ>= ` 2 ) ) -> 1 < B )
6 eluzelz 
 |-  ( B e. ( ZZ>= ` 2 ) -> B e. ZZ )
7 6 adantl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ B e. ( ZZ>= ` 2 ) ) -> B e. ZZ )
8 7 zred 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ B e. ( ZZ>= ` 2 ) ) -> B e. RR )
9 eluz2nn 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. NN )
10 9 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ B e. ( ZZ>= ` 2 ) ) -> A e. NN )
11 10 nngt0d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ B e. ( ZZ>= ` 2 ) ) -> 0 < A )
12 ltmulgt11 
 |-  ( ( A e. RR /\ B e. RR /\ 0 < A ) -> ( 1 < B <-> A < ( A x. B ) ) )
13 3 8 11 12 syl3anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ B e. ( ZZ>= ` 2 ) ) -> ( 1 < B <-> A < ( A x. B ) ) )
14 5 13 mpbid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ B e. ( ZZ>= ` 2 ) ) -> A < ( A x. B ) )
15 3 14 ltned 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ B e. ( ZZ>= ` 2 ) ) -> A =/= ( A x. B ) )
16 dvdsmul1 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> A || ( A x. B ) )
17 1 6 16 syl2an 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ B e. ( ZZ>= ` 2 ) ) -> A || ( A x. B ) )
18 isprm4 
 |-  ( ( A x. B ) e. Prime <-> ( ( A x. B ) e. ( ZZ>= ` 2 ) /\ A. x e. ( ZZ>= ` 2 ) ( x || ( A x. B ) -> x = ( A x. B ) ) ) )
19 18 simprbi 
 |-  ( ( A x. B ) e. Prime -> A. x e. ( ZZ>= ` 2 ) ( x || ( A x. B ) -> x = ( A x. B ) ) )
20 breq1 
 |-  ( x = A -> ( x || ( A x. B ) <-> A || ( A x. B ) ) )
21 eqeq1 
 |-  ( x = A -> ( x = ( A x. B ) <-> A = ( A x. B ) ) )
22 20 21 imbi12d 
 |-  ( x = A -> ( ( x || ( A x. B ) -> x = ( A x. B ) ) <-> ( A || ( A x. B ) -> A = ( A x. B ) ) ) )
23 22 rspcv 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A. x e. ( ZZ>= ` 2 ) ( x || ( A x. B ) -> x = ( A x. B ) ) -> ( A || ( A x. B ) -> A = ( A x. B ) ) ) )
24 19 23 syl5 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A x. B ) e. Prime -> ( A || ( A x. B ) -> A = ( A x. B ) ) ) )
25 24 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ B e. ( ZZ>= ` 2 ) ) -> ( ( A x. B ) e. Prime -> ( A || ( A x. B ) -> A = ( A x. B ) ) ) )
26 17 25 mpid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ B e. ( ZZ>= ` 2 ) ) -> ( ( A x. B ) e. Prime -> A = ( A x. B ) ) )
27 26 necon3ad 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ B e. ( ZZ>= ` 2 ) ) -> ( A =/= ( A x. B ) -> -. ( A x. B ) e. Prime ) )
28 15 27 mpd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ B e. ( ZZ>= ` 2 ) ) -> -. ( A x. B ) e. Prime )