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 )