Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  nprm Unicode version

Theorem nprm 11841
 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 9360 . . . . 5
21adantr 274 . . . 4
32zred 9198 . . 3
4 eluz2b2 9425 . . . . . 6
54simprbi 273 . . . . 5
65adantl 275 . . . 4
7 eluzelz 9360 . . . . . . 7
87adantl 275 . . . . . 6
98zred 9198 . . . . 5
10 eluz2nn 9389 . . . . . . 7
1110adantr 274 . . . . . 6
1211nngt0d 8789 . . . . 5
13 ltmulgt11 8647 . . . . 5
143, 9, 12, 13syl3anc 1217 . . . 4
156, 14mpbid 146 . . 3
163, 15ltned 7902 . 2
17 dvdsmul1 11552 . . . . 5
181, 7, 17syl2an 287 . . . 4
19 isprm4 11837 . . . . . . 7
2019simprbi 273 . . . . . 6
21 breq1 3940 . . . . . . . 8
22 eqeq1 2147 . . . . . . . 8
2321, 22imbi12d 233 . . . . . . 7
2423rspcv 2789 . . . . . 6
2520, 24syl5 32 . . . . 5
2625adantr 274 . . . 4
2718, 26mpid 42 . . 3