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	⊢ ( 𝐴 ∈ ℝ → ∃ 𝑝 ∈ ℙ 𝐴 < 𝑝 )

Proof

Step	Hyp	Ref	Expression
1		simplll	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝐴 < 𝑛 ∧ 𝑛 < 𝑝 ) ) → 𝐴 ∈ ℝ )
2		nnre	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ )
3	2	ad3antlr	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝐴 < 𝑛 ∧ 𝑛 < 𝑝 ) ) → 𝑛 ∈ ℝ )
4		prmz	⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
5	4	zred	⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℝ )
6	5	ad2antlr	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝐴 < 𝑛 ∧ 𝑛 < 𝑝 ) ) → 𝑝 ∈ ℝ )
7		simprl	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝐴 < 𝑛 ∧ 𝑛 < 𝑝 ) ) → 𝐴 < 𝑛 )
8		simprr	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝐴 < 𝑛 ∧ 𝑛 < 𝑝 ) ) → 𝑛 < 𝑝 )
9	1 3 6 7 8	lttrd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ℕ ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝐴 < 𝑛 ∧ 𝑛 < 𝑝 ) ) → 𝐴 < 𝑝 )
10		arch	⊢ ( 𝐴 ∈ ℝ → ∃ 𝑛 ∈ ℕ 𝐴 < 𝑛 )
11		prmunb	⊢ ( 𝑛 ∈ ℕ → ∃ 𝑝 ∈ ℙ 𝑛 < 𝑝 )
12	11	rgen	⊢ ∀ 𝑛 ∈ ℕ ∃ 𝑝 ∈ ℙ 𝑛 < 𝑝
13		r19.29r	⊢ ( ( ∃ 𝑛 ∈ ℕ 𝐴 < 𝑛 ∧ ∀ 𝑛 ∈ ℕ ∃ 𝑝 ∈ ℙ 𝑛 < 𝑝 ) → ∃ 𝑛 ∈ ℕ ( 𝐴 < 𝑛 ∧ ∃ 𝑝 ∈ ℙ 𝑛 < 𝑝 ) )
14	10 12 13	sylancl	⊢ ( 𝐴 ∈ ℝ → ∃ 𝑛 ∈ ℕ ( 𝐴 < 𝑛 ∧ ∃ 𝑝 ∈ ℙ 𝑛 < 𝑝 ) )
15		r19.42v	⊢ ( ∃ 𝑝 ∈ ℙ ( 𝐴 < 𝑛 ∧ 𝑛 < 𝑝 ) ↔ ( 𝐴 < 𝑛 ∧ ∃ 𝑝 ∈ ℙ 𝑛 < 𝑝 ) )
16	15	rexbii	⊢ ( ∃ 𝑛 ∈ ℕ ∃ 𝑝 ∈ ℙ ( 𝐴 < 𝑛 ∧ 𝑛 < 𝑝 ) ↔ ∃ 𝑛 ∈ ℕ ( 𝐴 < 𝑛 ∧ ∃ 𝑝 ∈ ℙ 𝑛 < 𝑝 ) )
17	14 16	sylibr	⊢ ( 𝐴 ∈ ℝ → ∃ 𝑛 ∈ ℕ ∃ 𝑝 ∈ ℙ ( 𝐴 < 𝑛 ∧ 𝑛 < 𝑝 ) )
18	9 17	reximddv2	⊢ ( 𝐴 ∈ ℝ → ∃ 𝑛 ∈ ℕ ∃ 𝑝 ∈ ℙ 𝐴 < 𝑝 )
19		1nn	⊢ 1 ∈ ℕ
20		ne0i	⊢ ( 1 ∈ ℕ → ℕ ≠ ∅ )
21		r19.9rzv	⊢ ( ℕ ≠ ∅ → ( ∃ 𝑝 ∈ ℙ 𝐴 < 𝑝 ↔ ∃ 𝑛 ∈ ℕ ∃ 𝑝 ∈ ℙ 𝐴 < 𝑝 ) )
22	19 20 21	mp2b	⊢ ( ∃ 𝑝 ∈ ℙ 𝐴 < 𝑝 ↔ ∃ 𝑛 ∈ ℕ ∃ 𝑝 ∈ ℙ 𝐴 < 𝑝 )
23	18 22	sylibr	⊢ ( 𝐴 ∈ ℝ → ∃ 𝑝 ∈ ℙ 𝐴 < 𝑝 )