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

Theorem nprm 14103
 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 11094 . . . . 5
21adantr 465 . . . 4
32zred 10969 . . 3
4 eluz2b2 11158 . . . . . 6
54simprbi 464 . . . . 5
65adantl 466 . . . 4
7 eluzelz 11094 . . . . . . 7
87adantl 466 . . . . . 6
98zred 10969 . . . . 5
10 eluz2nn 11123 . . . . . . 7
1110adantr 465 . . . . . 6
1211nngt0d 10580 . . . . 5
13 ltmulgt11 10403 . . . . 5
143, 9, 12, 13syl3anc 1227 . . . 4
156, 14mpbid 210 . . 3
163, 15ltned 9719 . 2
17 dvdsmul1 13877 . . . . 5
181, 7, 17syl2an 477 . . . 4
19 isprm4 14099 . . . . . . 7
2019simprbi 464 . . . . . 6
21 breq1 4436 . . . . . . . 8
22 eqeq1 2445 . . . . . . . 8
2321, 22imbi12d 320 . . . . . . 7
2423rspcv 3190 . . . . . 6
2520, 24syl5 32 . . . . 5
2625adantr 465 . . . 4
2718, 26mpid 41 . . 3