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

Theorem exprmfct 11714
 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 9313 . 2
2 eleq1 2178 . . . 4
32imbi1d 230 . . 3
4 eleq1 2178 . . . 4
5 breq2 3901 . . . . 5
65rexbidv 2413 . . . 4
74, 6imbi12d 233 . . 3
8 eleq1 2178 . . . 4
9 breq2 3901 . . . . 5
109rexbidv 2413 . . . 4
118, 10imbi12d 233 . . 3
12 eleq1 2178 . . . 4
13 breq2 3901 . . . . 5
1413rexbidv 2413 . . . 4
1512, 14imbi12d 233 . . 3
16 eleq1 2178 . . . 4
17 breq2 3901 . . . . 5
1817rexbidv 2413 . . . 4
1916, 18imbi12d 233 . . 3
20 1m1e0 8746 . . . . 5
21 uz2m1nn 9348 . . . . 5
2220, 21eqeltrrid 2203 . . . 4
23 0nnn 8704 . . . . 5
2423pm2.21i 618 . . . 4
2522, 24syl 14 . . 3
26 prmz 11688 . . . . . 6
27 iddvds 11402 . . . . . 6
2826, 27syl 14 . . . . 5
29 breq1 3900 . . . . . 6
3029rspcev 2761 . . . . 5
3128, 30mpdan 415 . . . 4
3231a1d 22 . . 3
33 simpl 108 . . . . . 6
34 eluzelz 9284 . . . . . . . . . 10
3534ad2antrr 477 . . . . . . . . 9
36 eluzelz 9284 . . . . . . . . . 10
3736ad2antlr 478 . . . . . . . . 9
38 dvdsmul1 11411 . . . . . . . . 9
3935, 37, 38syl2anc 406 . . . . . . . 8
40 prmz 11688 . . . . . . . . . 10
4140adantl 273 . . . . . . . . 9
4235, 37zmulcld 9130 . . . . . . . . 9
43 dvdstr 11426 . . . . . . . . 9
4441, 35, 42, 43syl3anc 1199 . . . . . . . 8
4539, 44mpan2d 422 . . . . . . 7
4645reximdva 2509 . . . . . 6
4733, 46embantd 56 . . . . 5
4847a1dd 48 . . . 4