infpn2

Description: There exist infinitely many prime numbers: the set of all primes S is unbounded by infpn , so by unben it is infinite. This is Metamath 100 proof #11. (Contributed by NM, 5-May-2005)

		Ref	Expression
	Hypothesis	infpn2.1	⊢ 𝑆 = { 𝑛 ∈ ℕ ∣ ( 1 < 𝑛 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑛 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑛 ) ) ) }
	Assertion	infpn2	⊢ 𝑆 ≈ ℕ

Proof

Step	Hyp	Ref	Expression
1		infpn2.1	⊢ 𝑆 = { 𝑛 ∈ ℕ ∣ ( 1 < 𝑛 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑛 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑛 ) ) ) }
2	1	ssrab3	⊢ 𝑆 ⊆ ℕ
3		infpn	⊢ ( 𝑗 ∈ ℕ → ∃ 𝑘 ∈ ℕ ( 𝑗 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) )
4		nnge1	⊢ ( 𝑗 ∈ ℕ → 1 ≤ 𝑗 )
5	4	adantr	⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) → 1 ≤ 𝑗 )
6		1re	⊢ 1 ∈ ℝ
7		nnre	⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℝ )
8		nnre	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
9		lelttr	⊢ ( ( 1 ∈ ℝ ∧ 𝑗 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( ( 1 ≤ 𝑗 ∧ 𝑗 < 𝑘 ) → 1 < 𝑘 ) )
10	6 7 8 9	mp3an3an	⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) → ( ( 1 ≤ 𝑗 ∧ 𝑗 < 𝑘 ) → 1 < 𝑘 ) )
11	5 10	mpand	⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) → ( 𝑗 < 𝑘 → 1 < 𝑘 ) )
12	11	ancld	⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) → ( 𝑗 < 𝑘 → ( 𝑗 < 𝑘 ∧ 1 < 𝑘 ) ) )
13	12	anim1d	⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) → ( ( 𝑗 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) → ( ( 𝑗 < 𝑘 ∧ 1 < 𝑘 ) ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ) )
14		anass	⊢ ( ( ( 𝑗 < 𝑘 ∧ 1 < 𝑘 ) ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ↔ ( 𝑗 < 𝑘 ∧ ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ) )
15	13 14	syl6ib	⊢ ( ( 𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ ) → ( ( 𝑗 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) → ( 𝑗 < 𝑘 ∧ ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ) ) )
16	15	reximdva	⊢ ( 𝑗 ∈ ℕ → ( ∃ 𝑘 ∈ ℕ ( 𝑗 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) → ∃ 𝑘 ∈ ℕ ( 𝑗 < 𝑘 ∧ ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ) ) )
17	3 16	mpd	⊢ ( 𝑗 ∈ ℕ → ∃ 𝑘 ∈ ℕ ( 𝑗 < 𝑘 ∧ ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ) )
18		breq2	⊢ ( 𝑛 = 𝑘 → ( 1 < 𝑛 ↔ 1 < 𝑘 ) )
19		oveq1	⊢ ( 𝑛 = 𝑘 → ( 𝑛 / 𝑚 ) = ( 𝑘 / 𝑚 ) )
20	19	eleq1d	⊢ ( 𝑛 = 𝑘 → ( ( 𝑛 / 𝑚 ) ∈ ℕ ↔ ( 𝑘 / 𝑚 ) ∈ ℕ ) )
21		equequ2	⊢ ( 𝑛 = 𝑘 → ( 𝑚 = 𝑛 ↔ 𝑚 = 𝑘 ) )
22	21	orbi2d	⊢ ( 𝑛 = 𝑘 → ( ( 𝑚 = 1 ∨ 𝑚 = 𝑛 ) ↔ ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) )
23	20 22	imbi12d	⊢ ( 𝑛 = 𝑘 → ( ( ( 𝑛 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑛 ) ) ↔ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) )
24	23	ralbidv	⊢ ( 𝑛 = 𝑘 → ( ∀ 𝑚 ∈ ℕ ( ( 𝑛 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑛 ) ) ↔ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) )
25	18 24	anbi12d	⊢ ( 𝑛 = 𝑘 → ( ( 1 < 𝑛 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑛 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑛 ) ) ) ↔ ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ) )
26	25 1	elrab2	⊢ ( 𝑘 ∈ 𝑆 ↔ ( 𝑘 ∈ ℕ ∧ ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ) )
27	26	anbi1i	⊢ ( ( 𝑘 ∈ 𝑆 ∧ 𝑗 < 𝑘 ) ↔ ( ( 𝑘 ∈ ℕ ∧ ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ) ∧ 𝑗 < 𝑘 ) )
28		anass	⊢ ( ( ( 𝑘 ∈ ℕ ∧ ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ) ∧ 𝑗 < 𝑘 ) ↔ ( 𝑘 ∈ ℕ ∧ ( ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ∧ 𝑗 < 𝑘 ) ) )
29		ancom	⊢ ( ( ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ∧ 𝑗 < 𝑘 ) ↔ ( 𝑗 < 𝑘 ∧ ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ) )
30	29	anbi2i	⊢ ( ( 𝑘 ∈ ℕ ∧ ( ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ∧ 𝑗 < 𝑘 ) ) ↔ ( 𝑘 ∈ ℕ ∧ ( 𝑗 < 𝑘 ∧ ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ) ) )
31	27 28 30	3bitri	⊢ ( ( 𝑘 ∈ 𝑆 ∧ 𝑗 < 𝑘 ) ↔ ( 𝑘 ∈ ℕ ∧ ( 𝑗 < 𝑘 ∧ ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ) ) )
32	31	rexbii2	⊢ ( ∃ 𝑘 ∈ 𝑆 𝑗 < 𝑘 ↔ ∃ 𝑘 ∈ ℕ ( 𝑗 < 𝑘 ∧ ( 1 < 𝑘 ∧ ∀ 𝑚 ∈ ℕ ( ( 𝑘 / 𝑚 ) ∈ ℕ → ( 𝑚 = 1 ∨ 𝑚 = 𝑘 ) ) ) ) )
33	17 32	sylibr	⊢ ( 𝑗 ∈ ℕ → ∃ 𝑘 ∈ 𝑆 𝑗 < 𝑘 )
34	33	rgen	⊢ ∀ 𝑗 ∈ ℕ ∃ 𝑘 ∈ 𝑆 𝑗 < 𝑘
35		unben	⊢ ( ( 𝑆 ⊆ ℕ ∧ ∀ 𝑗 ∈ ℕ ∃ 𝑘 ∈ 𝑆 𝑗 < 𝑘 ) → 𝑆 ≈ ℕ )
36	2 34 35	mp2an	⊢ 𝑆 ≈ ℕ

Metamath Proof Explorer

Theorem infpn2

Proof