Metamath Proof Explorer

Theorem exprmfct

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)

Ref Expression
Assertion exprmfct 
|- ( N e. ( ZZ>= ` 2 ) -> E. p e. Prime p || N )

Proof

Step Hyp Ref Expression
1 eluz2nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
2 eleq1 
 |-  ( x = 1 -> ( x e. ( ZZ>= ` 2 ) <-> 1 e. ( ZZ>= ` 2 ) ) )
3 2 imbi1d 
 |-  ( x = 1 -> ( ( x e. ( ZZ>= ` 2 ) -> E. p e. Prime p || x ) <-> ( 1 e. ( ZZ>= ` 2 ) -> E. p e. Prime p || x ) ) )
4 eleq1 
 |-  ( x = y -> ( x e. ( ZZ>= ` 2 ) <-> y e. ( ZZ>= ` 2 ) ) )
5 breq2 
 |-  ( x = y -> ( p || x <-> p || y ) )
6 5 rexbidv 
 |-  ( x = y -> ( E. p e. Prime p || x <-> E. p e. Prime p || y ) )
7 4 6 imbi12d 
 |-  ( x = y -> ( ( x e. ( ZZ>= ` 2 ) -> E. p e. Prime p || x ) <-> ( y e. ( ZZ>= ` 2 ) -> E. p e. Prime p || y ) ) )
8 eleq1 
 |-  ( x = z -> ( x e. ( ZZ>= ` 2 ) <-> z e. ( ZZ>= ` 2 ) ) )
9 breq2 
 |-  ( x = z -> ( p || x <-> p || z ) )
10 9 rexbidv 
 |-  ( x = z -> ( E. p e. Prime p || x <-> E. p e. Prime p || z ) )
11 8 10 imbi12d 
 |-  ( x = z -> ( ( x e. ( ZZ>= ` 2 ) -> E. p e. Prime p || x ) <-> ( z e. ( ZZ>= ` 2 ) -> E. p e. Prime p || z ) ) )
12 eleq1 
 |-  ( x = ( y x. z ) -> ( x e. ( ZZ>= ` 2 ) <-> ( y x. z ) e. ( ZZ>= ` 2 ) ) )
13 breq2 
 |-  ( x = ( y x. z ) -> ( p || x <-> p || ( y x. z ) ) )
14 13 rexbidv 
 |-  ( x = ( y x. z ) -> ( E. p e. Prime p || x <-> E. p e. Prime p || ( y x. z ) ) )
15 12 14 imbi12d 
 |-  ( x = ( y x. z ) -> ( ( x e. ( ZZ>= ` 2 ) -> E. p e. Prime p || x ) <-> ( ( y x. z ) e. ( ZZ>= ` 2 ) -> E. p e. Prime p || ( y x. z ) ) ) )
16 eleq1 
 |-  ( x = N -> ( x e. ( ZZ>= ` 2 ) <-> N e. ( ZZ>= ` 2 ) ) )
17 breq2 
 |-  ( x = N -> ( p || x <-> p || N ) )
18 17 rexbidv 
 |-  ( x = N -> ( E. p e. Prime p || x <-> E. p e. Prime p || N ) )
19 16 18 imbi12d 
 |-  ( x = N -> ( ( x e. ( ZZ>= ` 2 ) -> E. p e. Prime p || x ) <-> ( N e. ( ZZ>= ` 2 ) -> E. p e. Prime p || N ) ) )
20 1m1e0 
 |-  ( 1 - 1 ) = 0
21 uz2m1nn 
 |-  ( 1 e. ( ZZ>= ` 2 ) -> ( 1 - 1 ) e. NN )
22 20 21 eqeltrrid 
 |-  ( 1 e. ( ZZ>= ` 2 ) -> 0 e. NN )
23 0nnn 
 |-  -. 0 e. NN
24 23 pm2.21i 
 |-  ( 0 e. NN -> E. p e. Prime p || x )
25 22 24 syl 
 |-  ( 1 e. ( ZZ>= ` 2 ) -> E. p e. Prime p || x )
26 prmz 
 |-  ( x e. Prime -> x e. ZZ )
27 iddvds 
 |-  ( x e. ZZ -> x || x )
28 26 27 syl 
 |-  ( x e. Prime -> x || x )
29 breq1 
 |-  ( p = x -> ( p || x <-> x || x ) )
30 29 rspcev 
 |-  ( ( x e. Prime /\ x || x ) -> E. p e. Prime p || x )
31 28 30 mpdan 
 |-  ( x e. Prime -> E. p e. Prime p || x )
32 31 a1d 
 |-  ( x e. Prime -> ( x e. ( ZZ>= ` 2 ) -> E. p e. Prime p || x ) )
33 simpl 
 |-  ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) -> y e. ( ZZ>= ` 2 ) )
34 eluzelz 
 |-  ( y e. ( ZZ>= ` 2 ) -> y e. ZZ )
35 34 ad2antrr 
 |-  ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ p e. Prime ) -> y e. ZZ )
36 eluzelz 
 |-  ( z e. ( ZZ>= ` 2 ) -> z e. ZZ )
37 36 ad2antlr 
 |-  ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ p e. Prime ) -> z e. ZZ )
38 dvdsmul1 
 |-  ( ( y e. ZZ /\ z e. ZZ ) -> y || ( y x. z ) )
39 35 37 38 syl2anc 
 |-  ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ p e. Prime ) -> y || ( y x. z ) )
40 prmz 
 |-  ( p e. Prime -> p e. ZZ )
41 40 adantl 
 |-  ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ p e. Prime ) -> p e. ZZ )
42 35 37 zmulcld 
 |-  ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ p e. Prime ) -> ( y x. z ) e. ZZ )
43 dvdstr 
 |-  ( ( p e. ZZ /\ y e. ZZ /\ ( y x. z ) e. ZZ ) -> ( ( p || y /\ y || ( y x. z ) ) -> p || ( y x. z ) ) )
44 41 35 42 43 syl3anc 
 |-  ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ p e. Prime ) -> ( ( p || y /\ y || ( y x. z ) ) -> p || ( y x. z ) ) )
45 39 44 mpan2d 
 |-  ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ p e. Prime ) -> ( p || y -> p || ( y x. z ) ) )
46 45 reximdva 
 |-  ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) -> ( E. p e. Prime p || y -> E. p e. Prime p || ( y x. z ) ) )
47 33 46 embantd 
 |-  ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) -> ( ( y e. ( ZZ>= ` 2 ) -> E. p e. Prime p || y ) -> E. p e. Prime p || ( y x. z ) ) )
48 47 a1dd 
 |-  ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) -> ( ( y e. ( ZZ>= ` 2 ) -> E. p e. Prime p || y ) -> ( ( y x. z ) e. ( ZZ>= ` 2 ) -> E. p e. Prime p || ( y x. z ) ) ) )
49 48 adantrd 
 |-  ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) -> ( ( ( y e. ( ZZ>= ` 2 ) -> E. p e. Prime p || y ) /\ ( z e. ( ZZ>= ` 2 ) -> E. p e. Prime p || z ) ) -> ( ( y x. z ) e. ( ZZ>= ` 2 ) -> E. p e. Prime p || ( y x. z ) ) ) )
50 3 7 11 15 19 25 32 49 prmind 
 |-  ( N e. NN -> ( N e. ( ZZ>= ` 2 ) -> E. p e. Prime p || N ) )
51 1 50 mpcom 
 |-  ( N e. ( ZZ>= ` 2 ) -> E. p e. Prime p || N )