Metamath Proof Explorer

Theorem ppisval

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 ppisval 
|- ( A e. RR -> ( ( 0 [,] A ) i^i Prime ) = ( ( 2 ... ( |_ ` A ) ) i^i Prime ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( A e. RR /\ x e. ( ( 0 [,] A ) i^i Prime ) ) -> x e. ( ( 0 [,] A ) i^i Prime ) )
2 1 elin2d 
 |-  ( ( A e. RR /\ x e. ( ( 0 [,] A ) i^i Prime ) ) -> x e. Prime )
3 prmuz2 
 |-  ( x e. Prime -> x e. ( ZZ>= ` 2 ) )
4 2 3 syl 
 |-  ( ( A e. RR /\ x e. ( ( 0 [,] A ) i^i Prime ) ) -> x e. ( ZZ>= ` 2 ) )
5 prmz 
 |-  ( x e. Prime -> x e. ZZ )
6 2 5 syl 
 |-  ( ( A e. RR /\ x e. ( ( 0 [,] A ) i^i Prime ) ) -> x e. ZZ )
7 flcl 
 |-  ( A e. RR -> ( |_ ` A ) e. ZZ )
8 7 adantr 
 |-  ( ( A e. RR /\ x e. ( ( 0 [,] A ) i^i Prime ) ) -> ( |_ ` A ) e. ZZ )
9 1 elin1d 
 |-  ( ( A e. RR /\ x e. ( ( 0 [,] A ) i^i Prime ) ) -> x e. ( 0 [,] A ) )
10 0re 
 |-  0 e. RR
11 simpl 
 |-  ( ( A e. RR /\ x e. ( ( 0 [,] A ) i^i Prime ) ) -> A e. RR )
12 elicc2 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( x e. ( 0 [,] A ) <-> ( x e. RR /\ 0 <_ x /\ x <_ A ) ) )
13 10 11 12 sylancr 
 |-  ( ( A e. RR /\ x e. ( ( 0 [,] A ) i^i Prime ) ) -> ( x e. ( 0 [,] A ) <-> ( x e. RR /\ 0 <_ x /\ x <_ A ) ) )
14 9 13 mpbid 
 |-  ( ( A e. RR /\ x e. ( ( 0 [,] A ) i^i Prime ) ) -> ( x e. RR /\ 0 <_ x /\ x <_ A ) )
15 14 simp3d 
 |-  ( ( A e. RR /\ x e. ( ( 0 [,] A ) i^i Prime ) ) -> x <_ A )
16 flge 
 |-  ( ( A e. RR /\ x e. ZZ ) -> ( x <_ A <-> x <_ ( |_ ` A ) ) )
17 6 16 syldan 
 |-  ( ( A e. RR /\ x e. ( ( 0 [,] A ) i^i Prime ) ) -> ( x <_ A <-> x <_ ( |_ ` A ) ) )
18 15 17 mpbid 
 |-  ( ( A e. RR /\ x e. ( ( 0 [,] A ) i^i Prime ) ) -> x <_ ( |_ ` A ) )
19 eluz2 
 |-  ( ( |_ ` A ) e. ( ZZ>= ` x ) <-> ( x e. ZZ /\ ( |_ ` A ) e. ZZ /\ x <_ ( |_ ` A ) ) )
20 6 8 18 19 syl3anbrc 
 |-  ( ( A e. RR /\ x e. ( ( 0 [,] A ) i^i Prime ) ) -> ( |_ ` A ) e. ( ZZ>= ` x ) )
21 elfzuzb 
 |-  ( x e. ( 2 ... ( |_ ` A ) ) <-> ( x e. ( ZZ>= ` 2 ) /\ ( |_ ` A ) e. ( ZZ>= ` x ) ) )
22 4 20 21 sylanbrc 
 |-  ( ( A e. RR /\ x e. ( ( 0 [,] A ) i^i Prime ) ) -> x e. ( 2 ... ( |_ ` A ) ) )
23 22 2 elind 
 |-  ( ( A e. RR /\ x e. ( ( 0 [,] A ) i^i Prime ) ) -> x e. ( ( 2 ... ( |_ ` A ) ) i^i Prime ) )
24 23 ex 
 |-  ( A e. RR -> ( x e. ( ( 0 [,] A ) i^i Prime ) -> x e. ( ( 2 ... ( |_ ` A ) ) i^i Prime ) ) )
25 24 ssrdv 
 |-  ( A e. RR -> ( ( 0 [,] A ) i^i Prime ) C_ ( ( 2 ... ( |_ ` A ) ) i^i Prime ) )
26 2z 
 |-  2 e. ZZ
27 fzval2 
 |-  ( ( 2 e. ZZ /\ ( |_ ` A ) e. ZZ ) -> ( 2 ... ( |_ ` A ) ) = ( ( 2 [,] ( |_ ` A ) ) i^i ZZ ) )
28 26 7 27 sylancr 
 |-  ( A e. RR -> ( 2 ... ( |_ ` A ) ) = ( ( 2 [,] ( |_ ` A ) ) i^i ZZ ) )
29 inss1 
 |-  ( ( 2 [,] ( |_ ` A ) ) i^i ZZ ) C_ ( 2 [,] ( |_ ` A ) )
30 10 a1i 
 |-  ( A e. RR -> 0 e. RR )
31 id 
 |-  ( A e. RR -> A e. RR )
32 0le2 
 |-  0 <_ 2
33 32 a1i 
 |-  ( A e. RR -> 0 <_ 2 )
34 flle 
 |-  ( A e. RR -> ( |_ ` A ) <_ A )
35 iccss 
 |-  ( ( ( 0 e. RR /\ A e. RR ) /\ ( 0 <_ 2 /\ ( |_ ` A ) <_ A ) ) -> ( 2 [,] ( |_ ` A ) ) C_ ( 0 [,] A ) )
36 30 31 33 34 35 syl22anc 
 |-  ( A e. RR -> ( 2 [,] ( |_ ` A ) ) C_ ( 0 [,] A ) )
37 29 36 sstrid 
 |-  ( A e. RR -> ( ( 2 [,] ( |_ ` A ) ) i^i ZZ ) C_ ( 0 [,] A ) )
38 28 37 eqsstrd 
 |-  ( A e. RR -> ( 2 ... ( |_ ` A ) ) C_ ( 0 [,] A ) )
39 38 ssrind 
 |-  ( A e. RR -> ( ( 2 ... ( |_ ` A ) ) i^i Prime ) C_ ( ( 0 [,] A ) i^i Prime ) )
40 25 39 eqssd 
 |-  ( A e. RR -> ( ( 0 [,] A ) i^i Prime ) = ( ( 2 ... ( |_ ` A ) ) i^i Prime ) )