1arith2

Description: Fundamental theorem of arithmetic, where a prime factorization is represented as a finite monotonic 1-based sequence of primes. Every positive integer has a unique prime factorization. Theorem 1.10 in ApostolNT p. 17. This is Metamath 100 proof #80. (Contributed by Paul Chapman, 17-Nov-2012) (Revised by Mario Carneiro, 30-May-2014)

	Ref	Expression
Hypotheses	1arith.1	⊢ 𝑀 = ( 𝑛 ∈ ℕ ↦ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) )
	1arith.2	⊢ 𝑅 = { 𝑒 ∈ ( ℕ₀ ↑_m ℙ ) ∣ ( ^◡ 𝑒 “ ℕ ) ∈ Fin }
Assertion	1arith2	⊢ ∀ 𝑧 ∈ ℕ ∃! 𝑔 ∈ 𝑅 ( 𝑀 ‘ 𝑧 ) = 𝑔

Proof

Step	Hyp	Ref	Expression
1		1arith.1	⊢ 𝑀 = ( 𝑛 ∈ ℕ ↦ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) )
2		1arith.2	⊢ 𝑅 = { 𝑒 ∈ ( ℕ₀ ↑_m ℙ ) ∣ ( ^◡ 𝑒 “ ℕ ) ∈ Fin }
3	1 2	1arith	⊢ 𝑀 : ℕ –1-1-onto→ 𝑅
4		f1ocnv	⊢ ( 𝑀 : ℕ –1-1-onto→ 𝑅 → ^◡ 𝑀 : 𝑅 –1-1-onto→ ℕ )
5	3 4	ax-mp	⊢ ^◡ 𝑀 : 𝑅 –1-1-onto→ ℕ
6		f1ofveu	⊢ ( ( ^◡ 𝑀 : 𝑅 –1-1-onto→ ℕ ∧ 𝑧 ∈ ℕ ) → ∃! 𝑔 ∈ 𝑅 ( ^◡ 𝑀 ‘ 𝑔 ) = 𝑧 )
7	5 6	mpan	⊢ ( 𝑧 ∈ ℕ → ∃! 𝑔 ∈ 𝑅 ( ^◡ 𝑀 ‘ 𝑔 ) = 𝑧 )
8		f1ocnvfvb	⊢ ( ( 𝑀 : ℕ –1-1-onto→ 𝑅 ∧ 𝑧 ∈ ℕ ∧ 𝑔 ∈ 𝑅 ) → ( ( 𝑀 ‘ 𝑧 ) = 𝑔 ↔ ( ^◡ 𝑀 ‘ 𝑔 ) = 𝑧 ) )
9	3 8	mp3an1	⊢ ( ( 𝑧 ∈ ℕ ∧ 𝑔 ∈ 𝑅 ) → ( ( 𝑀 ‘ 𝑧 ) = 𝑔 ↔ ( ^◡ 𝑀 ‘ 𝑔 ) = 𝑧 ) )
10	9	reubidva	⊢ ( 𝑧 ∈ ℕ → ( ∃! 𝑔 ∈ 𝑅 ( 𝑀 ‘ 𝑧 ) = 𝑔 ↔ ∃! 𝑔 ∈ 𝑅 ( ^◡ 𝑀 ‘ 𝑔 ) = 𝑧 ) )
11	7 10	mpbird	⊢ ( 𝑧 ∈ ℕ → ∃! 𝑔 ∈ 𝑅 ( 𝑀 ‘ 𝑧 ) = 𝑔 )
12	11	rgen	⊢ ∀ 𝑧 ∈ ℕ ∃! 𝑔 ∈ 𝑅 ( 𝑀 ‘ 𝑧 ) = 𝑔

Metamath Proof Explorer

Theorem 1arith2

Proof