Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nprm Structured version   Unicode version

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

Proof of Theorem nprm
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eluzelz 10496 . . . . 5
21adantr 452 . . . 4
32zred 10375 . . 3
4 eluz2b2 10548 . . . . . 6
54simprbi 451 . . . . 5
65adantl 453 . . . 4
7 eluzelz 10496 . . . . . . 7
87adantl 453 . . . . . 6
98zred 10375 . . . . 5
10 eluz2b2 10548 . . . . . . . 8
1110simplbi 447 . . . . . . 7
1211adantr 452 . . . . . 6
1312nngt0d 10043 . . . . 5
14 ltmulgt11 9870 . . . . 5
153, 9, 13, 14syl3anc 1184 . . . 4
166, 15mpbid 202 . . 3
173, 16ltned 9209 . 2
18 dvdsmul1 12871 . . . . 5
191, 7, 18syl2an 464 . . . 4
20 isprm4 13089 . . . . . . 7
2120simprbi 451 . . . . . 6
22 breq1 4215 . . . . . . . 8
23 eqeq1 2442 . . . . . . . 8
2422, 23imbi12d 312 . . . . . . 7
2524rspcv 3048 . . . . . 6
2621, 25syl5 30 . . . . 5
2726adantr 452 . . . 4
2819, 27mpid 39 . . 3