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

Theorem exprmfct 14350
 Description: Every integer greater than or equal to 2 has a prime factor. (Contributed by Paul Chapman, 26-Oct-2012.) (Proof shortened by Mario Carneiro, 20-Jun-2015.)
Assertion
Ref Expression
exprmfct
Distinct variable group:   ,

Proof of Theorem exprmfct
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eluz2nn 11081 . 2
2 eleq1 2472 . . . 4
32imbi1d 315 . . 3
4 eleq1 2472 . . . 4
5 breq2 4396 . . . . 5
65rexbidv 2915 . . . 4
74, 6imbi12d 318 . . 3
8 eleq1 2472 . . . 4
9 breq2 4396 . . . . 5
109rexbidv 2915 . . . 4
118, 10imbi12d 318 . . 3
12 eleq1 2472 . . . 4
13 breq2 4396 . . . . 5
1413rexbidv 2915 . . . 4
1512, 14imbi12d 318 . . 3
16 eleq1 2472 . . . 4
17 breq2 4396 . . . . 5
1817rexbidv 2915 . . . 4
1916, 18imbi12d 318 . . 3
20 1m1e0 10563 . . . . 5
21 uz2m1nn 11117 . . . . 5
2220, 21syl5eqelr 2493 . . . 4
23 0nnn 10526 . . . . 5
2423pm2.21i 131 . . . 4
2522, 24syl 17 . . 3
26 prmz 14320 . . . . . 6
27 iddvds 14096 . . . . . 6
2826, 27syl 17 . . . . 5
29 breq1 4395 . . . . . 6
3029rspcev 3157 . . . . 5
3128, 30mpdan 666 . . . 4
3231a1d 25 . . 3
33 simpl 455 . . . . . 6
34 eluzelz 11052 . . . . . . . . . 10
3534ad2antrr 724 . . . . . . . . 9
36 eluzelz 11052 . . . . . . . . . 10
3736ad2antlr 725 . . . . . . . . 9
38 dvdsmul1 14104 . . . . . . . . 9
3935, 37, 38syl2anc 659 . . . . . . . 8
40 prmz 14320 . . . . . . . . . 10
4140adantl 464 . . . . . . . . 9
4235, 37zmulcld 10932 . . . . . . . . 9
43 dvdstr 14117 . . . . . . . . 9
4441, 35, 42, 43syl3anc 1228 . . . . . . . 8
4539, 44mpan2d 672 . . . . . . 7
4645reximdva 2876 . . . . . 6
4733, 46embantd 53 . . . . 5
4847a1dd 44 . . . 4