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