Metamath Proof Explorer

Theorem ppisval2

Description: The set of primes less than A expressed using a finite set of integers. (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Assertion ppisval2 
|- ( ( A e. RR /\ 2 e. ( ZZ>= ` M ) ) -> ( ( 0 [,] A ) i^i Prime ) = ( ( M ... ( |_ ` A ) ) i^i Prime ) )

Proof

Step Hyp Ref Expression
1 ppisval 
 |-  ( A e. RR -> ( ( 0 [,] A ) i^i Prime ) = ( ( 2 ... ( |_ ` A ) ) i^i Prime ) )
2 1 adantr 
 |-  ( ( A e. RR /\ 2 e. ( ZZ>= ` M ) ) -> ( ( 0 [,] A ) i^i Prime ) = ( ( 2 ... ( |_ ` A ) ) i^i Prime ) )
3 fzss1 
 |-  ( 2 e. ( ZZ>= ` M ) -> ( 2 ... ( |_ ` A ) ) C_ ( M ... ( |_ ` A ) ) )
4 3 adantl 
 |-  ( ( A e. RR /\ 2 e. ( ZZ>= ` M ) ) -> ( 2 ... ( |_ ` A ) ) C_ ( M ... ( |_ ` A ) ) )
5 4 ssrind 
 |-  ( ( A e. RR /\ 2 e. ( ZZ>= ` M ) ) -> ( ( 2 ... ( |_ ` A ) ) i^i Prime ) C_ ( ( M ... ( |_ ` A ) ) i^i Prime ) )
6 simpr 
 |-  ( ( ( A e. RR /\ 2 e. ( ZZ>= ` M ) ) /\ x e. ( ( M ... ( |_ ` A ) ) i^i Prime ) ) -> x e. ( ( M ... ( |_ ` A ) ) i^i Prime ) )
7 elin 
 |-  ( x e. ( ( M ... ( |_ ` A ) ) i^i Prime ) <-> ( x e. ( M ... ( |_ ` A ) ) /\ x e. Prime ) )
8 6 7 sylib 
 |-  ( ( ( A e. RR /\ 2 e. ( ZZ>= ` M ) ) /\ x e. ( ( M ... ( |_ ` A ) ) i^i Prime ) ) -> ( x e. ( M ... ( |_ ` A ) ) /\ x e. Prime ) )
9 8 simprd 
 |-  ( ( ( A e. RR /\ 2 e. ( ZZ>= ` M ) ) /\ x e. ( ( M ... ( |_ ` A ) ) i^i Prime ) ) -> x e. Prime )
10 prmuz2 
 |-  ( x e. Prime -> x e. ( ZZ>= ` 2 ) )
11 9 10 syl 
 |-  ( ( ( A e. RR /\ 2 e. ( ZZ>= ` M ) ) /\ x e. ( ( M ... ( |_ ` A ) ) i^i Prime ) ) -> x e. ( ZZ>= ` 2 ) )
12 8 simpld 
 |-  ( ( ( A e. RR /\ 2 e. ( ZZ>= ` M ) ) /\ x e. ( ( M ... ( |_ ` A ) ) i^i Prime ) ) -> x e. ( M ... ( |_ ` A ) ) )
13 elfzuz3 
 |-  ( x e. ( M ... ( |_ ` A ) ) -> ( |_ ` A ) e. ( ZZ>= ` x ) )
14 12 13 syl 
 |-  ( ( ( A e. RR /\ 2 e. ( ZZ>= ` M ) ) /\ x e. ( ( M ... ( |_ ` A ) ) i^i Prime ) ) -> ( |_ ` A ) e. ( ZZ>= ` x ) )
15 elfzuzb 
 |-  ( x e. ( 2 ... ( |_ ` A ) ) <-> ( x e. ( ZZ>= ` 2 ) /\ ( |_ ` A ) e. ( ZZ>= ` x ) ) )
16 11 14 15 sylanbrc 
 |-  ( ( ( A e. RR /\ 2 e. ( ZZ>= ` M ) ) /\ x e. ( ( M ... ( |_ ` A ) ) i^i Prime ) ) -> x e. ( 2 ... ( |_ ` A ) ) )
17 16 9 elind 
 |-  ( ( ( A e. RR /\ 2 e. ( ZZ>= ` M ) ) /\ x e. ( ( M ... ( |_ ` A ) ) i^i Prime ) ) -> x e. ( ( 2 ... ( |_ ` A ) ) i^i Prime ) )
18 5 17 eqelssd 
 |-  ( ( A e. RR /\ 2 e. ( ZZ>= ` M ) ) -> ( ( 2 ... ( |_ ` A ) ) i^i Prime ) = ( ( M ... ( |_ ` A ) ) i^i Prime ) )
19 2 18 eqtrd 
 |-  ( ( A e. RR /\ 2 e. ( ZZ>= ` M ) ) -> ( ( 0 [,] A ) i^i Prime ) = ( ( M ... ( |_ ` A ) ) i^i Prime ) )