Metamath Proof Explorer


Theorem ppifi

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 )

Proof

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 )