Description: The set of primes less than A is a finite set. (Contributed by Mario Carneiro, 15-Sep-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | ppifi | |- ( A e. RR -> ( ( 0 [,] A ) i^i Prime ) e. Fin ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ppisval | |- ( A e. RR -> ( ( 0 [,] A ) i^i Prime ) = ( ( 2 ... ( |_ ` A ) ) i^i Prime ) ) |
|
2 | fzfi | |- ( 2 ... ( |_ ` A ) ) e. Fin |
|
3 | inss1 | |- ( ( 2 ... ( |_ ` A ) ) i^i Prime ) C_ ( 2 ... ( |_ ` A ) ) |
|
4 | ssfi | |- ( ( ( 2 ... ( |_ ` A ) ) e. Fin /\ ( ( 2 ... ( |_ ` A ) ) i^i Prime ) C_ ( 2 ... ( |_ ` A ) ) ) -> ( ( 2 ... ( |_ ` A ) ) i^i Prime ) e. Fin ) |
|
5 | 2 3 4 | mp2an | |- ( ( 2 ... ( |_ ` A ) ) i^i Prime ) e. Fin |
6 | 1 5 | eqeltrdi | |- ( A e. RR -> ( ( 0 [,] A ) i^i Prime ) e. Fin ) |