Theorem prmunb2

Description: The primes are unbounded. This generalizes prmunb to real A with arch and lttrd : every real is less than some positive integer, itself less than some prime. (Contributed by Steve Rodriguez, 20-Jan-2020)

	Ref	Expression
Assertion	prmunb2	|- ( A e. RR -> E. p e. Prime A < p )

Proof

Step	Hyp	Ref	Expression
1		simplll	|- ( ( ( ( A e. RR /\ n e. NN ) /\ p e. Prime ) /\ ( A < n /\ n < p ) ) -> A e. RR )
2		nnre	|- ( n e. NN -> n e. RR )
3	2	ad3antlr	|- ( ( ( ( A e. RR /\ n e. NN ) /\ p e. Prime ) /\ ( A < n /\ n < p ) ) -> n e. RR )
4		prmz	|- ( p e. Prime -> p e. ZZ )
5	4	zred	|- ( p e. Prime -> p e. RR )
6	5	ad2antlr	|- ( ( ( ( A e. RR /\ n e. NN ) /\ p e. Prime ) /\ ( A < n /\ n < p ) ) -> p e. RR )
7		simprl	|- ( ( ( ( A e. RR /\ n e. NN ) /\ p e. Prime ) /\ ( A < n /\ n < p ) ) -> A < n )
8		simprr	|- ( ( ( ( A e. RR /\ n e. NN ) /\ p e. Prime ) /\ ( A < n /\ n < p ) ) -> n < p )
9	1 3 6 7 8	lttrd	|- ( ( ( ( A e. RR /\ n e. NN ) /\ p e. Prime ) /\ ( A < n /\ n < p ) ) -> A < p )
10		arch	|- ( A e. RR -> E. n e. NN A < n )
11		prmunb	|- ( n e. NN -> E. p e. Prime n < p )
12	11	rgen	|- A. n e. NN E. p e. Prime n < p
13		r19.29r	|- ( ( E. n e. NN A < n /\ A. n e. NN E. p e. Prime n < p ) -> E. n e. NN ( A < n /\ E. p e. Prime n < p ) )
14	10 12 13	sylancl	|- ( A e. RR -> E. n e. NN ( A < n /\ E. p e. Prime n < p ) )
15		r19.42v	|- ( E. p e. Prime ( A < n /\ n < p ) <-> ( A < n /\ E. p e. Prime n < p ) )
16	15	rexbii	|- ( E. n e. NN E. p e. Prime ( A < n /\ n < p ) <-> E. n e. NN ( A < n /\ E. p e. Prime n < p ) )
17	14 16	sylibr	|- ( A e. RR -> E. n e. NN E. p e. Prime ( A < n /\ n < p ) )
18	9 17	reximddv2	|- ( A e. RR -> E. n e. NN E. p e. Prime A < p )
19		1nn	|- 1 e. NN
20		ne0i	|- ( 1 e. NN -> NN =/= (/) )
21		r19.9rzv	|- ( NN =/= (/) -> ( E. p e. Prime A < p <-> E. n e. NN E. p e. Prime A < p ) )
22	19 20 21	mp2b	|- ( E. p e. Prime A < p <-> E. n e. NN E. p e. Prime A < p )
23	18 22	sylibr	|- ( A e. RR -> E. p e. Prime A < p )