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

Theorem exprmfct 10726
 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 8790 . 2
2 eleq1 2145 . . . 4
32imbi1d 229 . . 3
4 eleq1 2145 . . . 4
5 breq2 3809 . . . . 5
65rexbidv 2374 . . . 4
74, 6imbi12d 232 . . 3
8 eleq1 2145 . . . 4
9 breq2 3809 . . . . 5
109rexbidv 2374 . . . 4
118, 10imbi12d 232 . . 3
12 eleq1 2145 . . . 4
13 breq2 3809 . . . . 5
1413rexbidv 2374 . . . 4
1512, 14imbi12d 232 . . 3
16 eleq1 2145 . . . 4
17 breq2 3809 . . . . 5
1817rexbidv 2374 . . . 4
1916, 18imbi12d 232 . . 3
20 1m1e0 8227 . . . . 5
21 uz2m1nn 8825 . . . . 5
2220, 21syl5eqelr 2170 . . . 4
23 0nnn 8185 . . . . 5
2423pm2.21i 608 . . . 4
2522, 24syl 14 . . 3
26 prmz 10700 . . . . . 6
27 iddvds 10416 . . . . . 6
2826, 27syl 14 . . . . 5
29 breq1 3808 . . . . . 6
3029rspcev 2710 . . . . 5
3128, 30mpdan 412 . . . 4
3231a1d 22 . . 3
33 simpl 107 . . . . . 6
34 eluzelz 8761 . . . . . . . . . 10
3534ad2antrr 472 . . . . . . . . 9
36 eluzelz 8761 . . . . . . . . . 10
3736ad2antlr 473 . . . . . . . . 9
38 dvdsmul1 10425 . . . . . . . . 9
3935, 37, 38syl2anc 403 . . . . . . . 8
40 prmz 10700 . . . . . . . . . 10
4140adantl 271 . . . . . . . . 9
4235, 37zmulcld 8608 . . . . . . . . 9
43 dvdstr 10440 . . . . . . . . 9
4441, 35, 42, 43syl3anc 1170 . . . . . . . 8
4539, 44mpan2d 419 . . . . . . 7
4645reximdva 2468 . . . . . 6
4733, 46embantd 55 . . . . 5
4847a1dd 47 . . . 4