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