Metamath Proof Explorer


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 p A < p

Proof

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