This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem maxprmfct

Description: The set of prime factors of an integer greater than or equal to 2 satisfies the conditions to have a supremum, and that supremum is a member of the set. (Contributed by Paul Chapman, 17-Nov-2012)

Ref Expression
Hypothesis maxprmfct.1 
|- S = { z e. Prime | z || N }
Assertion maxprmfct 
|- ( N e. ( ZZ>= ` 2 ) -> ( ( S C_ ZZ /\ S =/= (/) /\ E. x e. ZZ A. y e. S y <_ x ) /\ sup ( S , RR , < ) e. S ) )

Proof

Step Hyp Ref Expression
1 maxprmfct.1 
 |-  S = { z e. Prime | z || N }
2 1 ssrab3 
 |-  S C_ Prime
3 prmz 
 |-  ( y e. Prime -> y e. ZZ )
4 3 ssriv 
 |-  Prime C_ ZZ
5 2 4 sstri 
 |-  S C_ ZZ
6 5 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> S C_ ZZ )
7 exprmfct 
 |-  ( N e. ( ZZ>= ` 2 ) -> E. y e. Prime y || N )
8 breq1 
 |-  ( z = y -> ( z || N <-> y || N ) )
9 8 1 elrab2 
 |-  ( y e. S <-> ( y e. Prime /\ y || N ) )
10 9 exbii 
 |-  ( E. y y e. S <-> E. y ( y e. Prime /\ y || N ) )
11 n0 
 |-  ( S =/= (/) <-> E. y y e. S )
12 df-rex 
 |-  ( E. y e. Prime y || N <-> E. y ( y e. Prime /\ y || N ) )
13 10 11 12 3bitr4ri 
 |-  ( E. y e. Prime y || N <-> S =/= (/) )
14 7 13 sylib 
 |-  ( N e. ( ZZ>= ` 2 ) -> S =/= (/) )
15 eluzelz 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. ZZ )
16 eluz2nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
17 3 anim1i 
 |-  ( ( y e. Prime /\ y || N ) -> ( y e. ZZ /\ y || N ) )
18 9 17 sylbi 
 |-  ( y e. S -> ( y e. ZZ /\ y || N ) )
19 dvdsle 
 |-  ( ( y e. ZZ /\ N e. NN ) -> ( y || N -> y <_ N ) )
20 19 expcom 
 |-  ( N e. NN -> ( y e. ZZ -> ( y || N -> y <_ N ) ) )
21 20 impd 
 |-  ( N e. NN -> ( ( y e. ZZ /\ y || N ) -> y <_ N ) )
22 18 21 syl5 
 |-  ( N e. NN -> ( y e. S -> y <_ N ) )
23 22 ralrimiv 
 |-  ( N e. NN -> A. y e. S y <_ N )
24 16 23 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> A. y e. S y <_ N )
25 brralrspcev 
 |-  ( ( N e. ZZ /\ A. y e. S y <_ N ) -> E. x e. ZZ A. y e. S y <_ x )
26 15 24 25 syl2anc 
 |-  ( N e. ( ZZ>= ` 2 ) -> E. x e. ZZ A. y e. S y <_ x )
27 6 14 26 3jca 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( S C_ ZZ /\ S =/= (/) /\ E. x e. ZZ A. y e. S y <_ x ) )
28 suprzcl2 
 |-  ( ( S C_ ZZ /\ S =/= (/) /\ E. x e. ZZ A. y e. S y <_ x ) -> sup ( S , RR , < ) e. S )
29 27 28 jccir 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( S C_ ZZ /\ S =/= (/) /\ E. x e. ZZ A. y e. S y <_ x ) /\ sup ( S , RR , < ) e. S ) )