1arith - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > 1arith		GIF version

Theorem 1arith 12365

Description: Fundamental theorem of arithmetic, where a prime factorization is represented as a sequence of prime exponents, for which only finitely many primes have nonzero exponent. The function 𝑀 maps the set of positive integers one-to-one onto the set of prime factorizations 𝑅. (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Mario Carneiro, 30-May-2014.)

**Hypotheses**
Ref	Expression
1arith.1	⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))
1arith.2	⊢ 𝑅 = {𝑒 ∈ (ℕ₀ ↑_𝑚 ℙ) ∣ (^◡𝑒 “ ℕ) ∈ Fin}

**Assertion**
Ref	Expression
1arith	⊢ 𝑀:ℕ–1-1-onto→𝑅

Distinct variable groups: 𝑒,𝑛,𝑝 𝑒,𝑀 𝑅,𝑛 Allowed substitution hints: 𝑅(𝑒,𝑝) 𝑀(𝑛,𝑝)

Proof of Theorem 1arith Dummy variables 𝑓 𝑔 𝑘 𝑞 𝑥 𝑦 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		prmex 12113	. . . . . 6 ⊢ ℙ ∈ V
2	1	mptex 5743	. . . . 5 ⊢ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ V
3		1arith.1	. . . . 5 ⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))
4	2, 3	fnmpti 5345	. . . 4 ⊢ 𝑀 Fn ℕ
5	3	1arithlem3 12363	. . . . . . 7 ⊢ (𝑥 ∈ ℕ → (𝑀‘𝑥):ℙ⟶ℕ₀)
6		nn0ex 9182	. . . . . . . 8 ⊢ ℕ₀ ∈ V
7	6, 1	elmap 6677	. . . . . . 7 ⊢ ((𝑀‘𝑥) ∈ (ℕ₀ ↑_𝑚 ℙ) ↔ (𝑀‘𝑥):ℙ⟶ℕ₀)
8	5, 7	sylibr 134	. . . . . 6 ⊢ (𝑥 ∈ ℕ → (𝑀‘𝑥) ∈ (ℕ₀ ↑_𝑚 ℙ))
9		1zzd 9280	. . . . . . . 8 ⊢ (𝑥 ∈ ℕ → 1 ∈ ℤ)
10		nnz 9272	. . . . . . . 8 ⊢ (𝑥 ∈ ℕ → 𝑥 ∈ ℤ)
11	9, 10	fzfigd 10431	. . . . . . 7 ⊢ (𝑥 ∈ ℕ → (1...𝑥) ∈ Fin)
12		ffn 5366	. . . . . . . . . 10 ⊢ ((𝑀‘𝑥):ℙ⟶ℕ₀ → (𝑀‘𝑥) Fn ℙ)
13		elpreima 5636	. . . . . . . . . 10 ⊢ ((𝑀‘𝑥) Fn ℙ → (𝑞 ∈ (^◡(𝑀‘𝑥) “ ℕ) ↔ (𝑞 ∈ ℙ ∧ ((𝑀‘𝑥)‘𝑞) ∈ ℕ)))
14	5, 12, 13	3syl 17	. . . . . . . . 9 ⊢ (𝑥 ∈ ℕ → (𝑞 ∈ (^◡(𝑀‘𝑥) “ ℕ) ↔ (𝑞 ∈ ℙ ∧ ((𝑀‘𝑥)‘𝑞) ∈ ℕ)))
15	3	1arithlem2 12362	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → ((𝑀‘𝑥)‘𝑞) = (𝑞 pCnt 𝑥))
16	15	eleq1d 2246	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (((𝑀‘𝑥)‘𝑞) ∈ ℕ ↔ (𝑞 pCnt 𝑥) ∈ ℕ))
17		prmz 12111	. . . . . . . . . . . . 13 ⊢ (𝑞 ∈ ℙ → 𝑞 ∈ ℤ)
18		id 19	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℕ → 𝑥 ∈ ℕ)
19		dvdsle 11850	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℤ ∧ 𝑥 ∈ ℕ) → (𝑞 ∥ 𝑥 → 𝑞 ≤ 𝑥))
20	17, 18, 19	syl2anr 290	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (𝑞 ∥ 𝑥 → 𝑞 ≤ 𝑥))
21		pcelnn 12320	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℙ ∧ 𝑥 ∈ ℕ) → ((𝑞 pCnt 𝑥) ∈ ℕ ↔ 𝑞 ∥ 𝑥))
22	21	ancoms 268	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → ((𝑞 pCnt 𝑥) ∈ ℕ ↔ 𝑞 ∥ 𝑥))
23		prmnn 12110	. . . . . . . . . . . . . 14 ⊢ (𝑞 ∈ ℙ → 𝑞 ∈ ℕ)
24		nnuz 9563	. . . . . . . . . . . . . 14 ⊢ ℕ = (ℤ_≥‘1)
25	23, 24	eleqtrdi 2270	. . . . . . . . . . . . 13 ⊢ (𝑞 ∈ ℙ → 𝑞 ∈ (ℤ_≥‘1))
26		elfz5 10017	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ (ℤ_≥‘1) ∧ 𝑥 ∈ ℤ) → (𝑞 ∈ (1...𝑥) ↔ 𝑞 ≤ 𝑥))
27	25, 10, 26	syl2anr 290	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (𝑞 ∈ (1...𝑥) ↔ 𝑞 ≤ 𝑥))
28	20, 22, 27	3imtr4d 203	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → ((𝑞 pCnt 𝑥) ∈ ℕ → 𝑞 ∈ (1...𝑥)))
29	16, 28	sylbid 150	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (((𝑀‘𝑥)‘𝑞) ∈ ℕ → 𝑞 ∈ (1...𝑥)))
30	29	expimpd 363	. . . . . . . . 9 ⊢ (𝑥 ∈ ℕ → ((𝑞 ∈ ℙ ∧ ((𝑀‘𝑥)‘𝑞) ∈ ℕ) → 𝑞 ∈ (1...𝑥)))
31	14, 30	sylbid 150	. . . . . . . 8 ⊢ (𝑥 ∈ ℕ → (𝑞 ∈ (^◡(𝑀‘𝑥) “ ℕ) → 𝑞 ∈ (1...𝑥)))
32	31	ssrdv 3162	. . . . . . 7 ⊢ (𝑥 ∈ ℕ → (^◡(𝑀‘𝑥) “ ℕ) ⊆ (1...𝑥))
33		elfznn 10054	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (1...𝑥) → 𝑗 ∈ ℕ)
34	33	adantl 277	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℕ ∧ 𝑗 ∈ (1...𝑥)) → 𝑗 ∈ ℕ)
35		prmdc 12130	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ℕ → DECID 𝑗 ∈ ℙ)
36	34, 35	syl 14	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℕ ∧ 𝑗 ∈ (1...𝑥)) → DECID 𝑗 ∈ ℙ)
37	36	adantr 276	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℕ ∧ 𝑗 ∈ (1...𝑥)) ∧ 𝑗 ∈ ℙ) → DECID 𝑗 ∈ ℙ)
38	5	ad2antrr 488	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℕ ∧ 𝑗 ∈ (1...𝑥)) ∧ 𝑗 ∈ ℙ) → (𝑀‘𝑥):ℙ⟶ℕ₀)
39		simpr 110	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℕ ∧ 𝑗 ∈ (1...𝑥)) ∧ 𝑗 ∈ ℙ) → 𝑗 ∈ ℙ)
40	38, 39	ffvelcdmd 5653	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℕ ∧ 𝑗 ∈ (1...𝑥)) ∧ 𝑗 ∈ ℙ) → ((𝑀‘𝑥)‘𝑗) ∈ ℕ₀)
41	40	nn0zd 9373	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℕ ∧ 𝑗 ∈ (1...𝑥)) ∧ 𝑗 ∈ ℙ) → ((𝑀‘𝑥)‘𝑗) ∈ ℤ)
42		elnndc 9612	. . . . . . . . . . . 12 ⊢ (((𝑀‘𝑥)‘𝑗) ∈ ℤ → DECID ((𝑀‘𝑥)‘𝑗) ∈ ℕ)
43	41, 42	syl 14	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℕ ∧ 𝑗 ∈ (1...𝑥)) ∧ 𝑗 ∈ ℙ) → DECID ((𝑀‘𝑥)‘𝑗) ∈ ℕ)
44		dcan2 934	. . . . . . . . . . 11 ⊢ (DECID 𝑗 ∈ ℙ → (DECID ((𝑀‘𝑥)‘𝑗) ∈ ℕ → DECID (𝑗 ∈ ℙ ∧ ((𝑀‘𝑥)‘𝑗) ∈ ℕ)))
45	37, 43, 44	sylc 62	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℕ ∧ 𝑗 ∈ (1...𝑥)) ∧ 𝑗 ∈ ℙ) → DECID (𝑗 ∈ ℙ ∧ ((𝑀‘𝑥)‘𝑗) ∈ ℕ))
46		simpr 110	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℕ ∧ 𝑗 ∈ (1...𝑥)) ∧ ¬ 𝑗 ∈ ℙ) → ¬ 𝑗 ∈ ℙ)
47	46	intnanrd 932	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℕ ∧ 𝑗 ∈ (1...𝑥)) ∧ ¬ 𝑗 ∈ ℙ) → ¬ (𝑗 ∈ ℙ ∧ ((𝑀‘𝑥)‘𝑗) ∈ ℕ))
48	47	olcd 734	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℕ ∧ 𝑗 ∈ (1...𝑥)) ∧ ¬ 𝑗 ∈ ℙ) → ((𝑗 ∈ ℙ ∧ ((𝑀‘𝑥)‘𝑗) ∈ ℕ) ∨ ¬ (𝑗 ∈ ℙ ∧ ((𝑀‘𝑥)‘𝑗) ∈ ℕ)))
49		df-dc 835	. . . . . . . . . . 11 ⊢ (DECID (𝑗 ∈ ℙ ∧ ((𝑀‘𝑥)‘𝑗) ∈ ℕ) ↔ ((𝑗 ∈ ℙ ∧ ((𝑀‘𝑥)‘𝑗) ∈ ℕ) ∨ ¬ (𝑗 ∈ ℙ ∧ ((𝑀‘𝑥)‘𝑗) ∈ ℕ)))
50	48, 49	sylibr 134	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℕ ∧ 𝑗 ∈ (1...𝑥)) ∧ ¬ 𝑗 ∈ ℙ) → DECID (𝑗 ∈ ℙ ∧ ((𝑀‘𝑥)‘𝑗) ∈ ℕ))
51		exmiddc 836	. . . . . . . . . . 11 ⊢ (DECID 𝑗 ∈ ℙ → (𝑗 ∈ ℙ ∨ ¬ 𝑗 ∈ ℙ))
52	36, 51	syl 14	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℕ ∧ 𝑗 ∈ (1...𝑥)) → (𝑗 ∈ ℙ ∨ ¬ 𝑗 ∈ ℙ))
53	45, 50, 52	mpjaodan 798	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℕ ∧ 𝑗 ∈ (1...𝑥)) → DECID (𝑗 ∈ ℙ ∧ ((𝑀‘𝑥)‘𝑗) ∈ ℕ))
54		elpreima 5636	. . . . . . . . . . . 12 ⊢ ((𝑀‘𝑥) Fn ℙ → (𝑗 ∈ (^◡(𝑀‘𝑥) “ ℕ) ↔ (𝑗 ∈ ℙ ∧ ((𝑀‘𝑥)‘𝑗) ∈ ℕ)))
55	5, 12, 54	3syl 17	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℕ → (𝑗 ∈ (^◡(𝑀‘𝑥) “ ℕ) ↔ (𝑗 ∈ ℙ ∧ ((𝑀‘𝑥)‘𝑗) ∈ ℕ)))
56	55	dcbid 838	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℕ → (DECID 𝑗 ∈ (^◡(𝑀‘𝑥) “ ℕ) ↔ DECID (𝑗 ∈ ℙ ∧ ((𝑀‘𝑥)‘𝑗) ∈ ℕ)))
57	56	adantr 276	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℕ ∧ 𝑗 ∈ (1...𝑥)) → (DECID 𝑗 ∈ (^◡(𝑀‘𝑥) “ ℕ) ↔ DECID (𝑗 ∈ ℙ ∧ ((𝑀‘𝑥)‘𝑗) ∈ ℕ)))
58	53, 57	mpbird 167	. . . . . . . 8 ⊢ ((𝑥 ∈ ℕ ∧ 𝑗 ∈ (1...𝑥)) → DECID 𝑗 ∈ (^◡(𝑀‘𝑥) “ ℕ))
59	58	ralrimiva 2550	. . . . . . 7 ⊢ (𝑥 ∈ ℕ → ∀𝑗 ∈ (1...𝑥)DECID 𝑗 ∈ (^◡(𝑀‘𝑥) “ ℕ))
60		ssfidc 6934	. . . . . . 7 ⊢ (((1...𝑥) ∈ Fin ∧ (^◡(𝑀‘𝑥) “ ℕ) ⊆ (1...𝑥) ∧ ∀𝑗 ∈ (1...𝑥)DECID 𝑗 ∈ (^◡(𝑀‘𝑥) “ ℕ)) → (^◡(𝑀‘𝑥) “ ℕ) ∈ Fin)
61	11, 32, 59, 60	syl3anc 1238	. . . . . 6 ⊢ (𝑥 ∈ ℕ → (^◡(𝑀‘𝑥) “ ℕ) ∈ Fin)
62		cnveq 4802	. . . . . . . . 9 ⊢ (𝑒 = (𝑀‘𝑥) → ^◡𝑒 = ^◡(𝑀‘𝑥))
63	62	imaeq1d 4970	. . . . . . . 8 ⊢ (𝑒 = (𝑀‘𝑥) → (^◡𝑒 “ ℕ) = (^◡(𝑀‘𝑥) “ ℕ))
64	63	eleq1d 2246	. . . . . . 7 ⊢ (𝑒 = (𝑀‘𝑥) → ((^◡𝑒 “ ℕ) ∈ Fin ↔ (^◡(𝑀‘𝑥) “ ℕ) ∈ Fin))
65		1arith.2	. . . . . . 7 ⊢ 𝑅 = {𝑒 ∈ (ℕ₀ ↑_𝑚 ℙ) ∣ (^◡𝑒 “ ℕ) ∈ Fin}
66	64, 65	elrab2 2897	. . . . . 6 ⊢ ((𝑀‘𝑥) ∈ 𝑅 ↔ ((𝑀‘𝑥) ∈ (ℕ₀ ↑_𝑚 ℙ) ∧ (^◡(𝑀‘𝑥) “ ℕ) ∈ Fin))
67	8, 61, 66	sylanbrc 417	. . . . 5 ⊢ (𝑥 ∈ ℕ → (𝑀‘𝑥) ∈ 𝑅)
68	67	rgen 2530	. . . 4 ⊢ ∀𝑥 ∈ ℕ (𝑀‘𝑥) ∈ 𝑅
69		ffnfv 5675	. . . 4 ⊢ (𝑀:ℕ⟶𝑅 ↔ (𝑀 Fn ℕ ∧ ∀𝑥 ∈ ℕ (𝑀‘𝑥) ∈ 𝑅))
70	4, 68, 69	mpbir2an 942	. . 3 ⊢ 𝑀:ℕ⟶𝑅
71	15	adantlr 477	. . . . . . . 8 ⊢ (((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) ∧ 𝑞 ∈ ℙ) → ((𝑀‘𝑥)‘𝑞) = (𝑞 pCnt 𝑥))
72	3	1arithlem2 12362	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 𝑞 ∈ ℙ) → ((𝑀‘𝑦)‘𝑞) = (𝑞 pCnt 𝑦))
73	72	adantll 476	. . . . . . . 8 ⊢ (((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) ∧ 𝑞 ∈ ℙ) → ((𝑀‘𝑦)‘𝑞) = (𝑞 pCnt 𝑦))
74	71, 73	eqeq12d 2192	. . . . . . 7 ⊢ (((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) ∧ 𝑞 ∈ ℙ) → (((𝑀‘𝑥)‘𝑞) = ((𝑀‘𝑦)‘𝑞) ↔ (𝑞 pCnt 𝑥) = (𝑞 pCnt 𝑦)))
75	74	ralbidva 2473	. . . . . 6 ⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (∀𝑞 ∈ ℙ ((𝑀‘𝑥)‘𝑞) = ((𝑀‘𝑦)‘𝑞) ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt 𝑥) = (𝑞 pCnt 𝑦)))
76	3	1arithlem3 12363	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → (𝑀‘𝑦):ℙ⟶ℕ₀)
77		ffn 5366	. . . . . . . 8 ⊢ ((𝑀‘𝑦):ℙ⟶ℕ₀ → (𝑀‘𝑦) Fn ℙ)
78		eqfnfv 5614	. . . . . . . 8 ⊢ (((𝑀‘𝑥) Fn ℙ ∧ (𝑀‘𝑦) Fn ℙ) → ((𝑀‘𝑥) = (𝑀‘𝑦) ↔ ∀𝑞 ∈ ℙ ((𝑀‘𝑥)‘𝑞) = ((𝑀‘𝑦)‘𝑞)))
79	12, 77, 78	syl2an 289	. . . . . . 7 ⊢ (((𝑀‘𝑥):ℙ⟶ℕ₀ ∧ (𝑀‘𝑦):ℙ⟶ℕ₀) → ((𝑀‘𝑥) = (𝑀‘𝑦) ↔ ∀𝑞 ∈ ℙ ((𝑀‘𝑥)‘𝑞) = ((𝑀‘𝑦)‘𝑞)))
80	5, 76, 79	syl2an 289	. . . . . 6 ⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝑀‘𝑥) = (𝑀‘𝑦) ↔ ∀𝑞 ∈ ℙ ((𝑀‘𝑥)‘𝑞) = ((𝑀‘𝑦)‘𝑞)))
81		nnnn0 9183	. . . . . . 7 ⊢ (𝑥 ∈ ℕ → 𝑥 ∈ ℕ₀)
82		nnnn0 9183	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℕ₀)
83		pc11 12330	. . . . . . 7 ⊢ ((𝑥 ∈ ℕ₀ ∧ 𝑦 ∈ ℕ₀) → (𝑥 = 𝑦 ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt 𝑥) = (𝑞 pCnt 𝑦)))
84	81, 82, 83	syl2an 289	. . . . . 6 ⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑥 = 𝑦 ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt 𝑥) = (𝑞 pCnt 𝑦)))
85	75, 80, 84	3bitr4d 220	. . . . 5 ⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝑀‘𝑥) = (𝑀‘𝑦) ↔ 𝑥 = 𝑦))
86	85	biimpd 144	. . . 4 ⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝑀‘𝑥) = (𝑀‘𝑦) → 𝑥 = 𝑦))
87	86	rgen2 2563	. . 3 ⊢ ∀𝑥 ∈ ℕ ∀𝑦 ∈ ℕ ((𝑀‘𝑥) = (𝑀‘𝑦) → 𝑥 = 𝑦)
88		dff13 5769	. . 3 ⊢ (𝑀:ℕ–1-1→𝑅 ↔ (𝑀:ℕ⟶𝑅 ∧ ∀𝑥 ∈ ℕ ∀𝑦 ∈ ℕ ((𝑀‘𝑥) = (𝑀‘𝑦) → 𝑥 = 𝑦)))
89	70, 87, 88	mpbir2an 942	. 2 ⊢ 𝑀:ℕ–1-1→𝑅
90		eqid 2177	. . . . . 6 ⊢ (𝑔 ∈ ℕ ↦ if(𝑔 ∈ ℙ, (𝑔↑(𝑓‘𝑔)), 1)) = (𝑔 ∈ ℕ ↦ if(𝑔 ∈ ℙ, (𝑔↑(𝑓‘𝑔)), 1))
91		cnveq 4802	. . . . . . . . . . . 12 ⊢ (𝑒 = 𝑓 → ^◡𝑒 = ^◡𝑓)
92	91	imaeq1d 4970	. . . . . . . . . . 11 ⊢ (𝑒 = 𝑓 → (^◡𝑒 “ ℕ) = (^◡𝑓 “ ℕ))
93	92	eleq1d 2246	. . . . . . . . . 10 ⊢ (𝑒 = 𝑓 → ((^◡𝑒 “ ℕ) ∈ Fin ↔ (^◡𝑓 “ ℕ) ∈ Fin))
94	93, 65	elrab2 2897	. . . . . . . . 9 ⊢ (𝑓 ∈ 𝑅 ↔ (𝑓 ∈ (ℕ₀ ↑_𝑚 ℙ) ∧ (^◡𝑓 “ ℕ) ∈ Fin))
95	94	simplbi 274	. . . . . . . 8 ⊢ (𝑓 ∈ 𝑅 → 𝑓 ∈ (ℕ₀ ↑_𝑚 ℙ))
96	6, 1	elmap 6677	. . . . . . . 8 ⊢ (𝑓 ∈ (ℕ₀ ↑_𝑚 ℙ) ↔ 𝑓:ℙ⟶ℕ₀)
97	95, 96	sylib 122	. . . . . . 7 ⊢ (𝑓 ∈ 𝑅 → 𝑓:ℙ⟶ℕ₀)
98	97	ad2antrr 488	. . . . . 6 ⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℕ) ∧ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → 𝑓:ℙ⟶ℕ₀)
99		simplr 528	. . . . . . 7 ⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℕ) ∧ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → 𝑦 ∈ ℕ)
100	99	peano2nnd 8934	. . . . . 6 ⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℕ) ∧ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → (𝑦 + 1) ∈ ℕ)
101	99	adantr 276	. . . . . . . . . . 11 ⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℕ) ∧ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ (𝑦 + 1) ≤ 𝑞)) → 𝑦 ∈ ℕ)
102	101	nnred 8932	. . . . . . . . . 10 ⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℕ) ∧ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ (𝑦 + 1) ≤ 𝑞)) → 𝑦 ∈ ℝ)
103		peano2re 8093	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ → (𝑦 + 1) ∈ ℝ)
104	102, 103	syl 14	. . . . . . . . . 10 ⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℕ) ∧ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ (𝑦 + 1) ≤ 𝑞)) → (𝑦 + 1) ∈ ℝ)
105	23	ad2antrl 490	. . . . . . . . . . 11 ⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℕ) ∧ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ (𝑦 + 1) ≤ 𝑞)) → 𝑞 ∈ ℕ)
106	105	nnred 8932	. . . . . . . . . 10 ⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℕ) ∧ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ (𝑦 + 1) ≤ 𝑞)) → 𝑞 ∈ ℝ)
107	102	ltp1d 8887	. . . . . . . . . 10 ⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℕ) ∧ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ (𝑦 + 1) ≤ 𝑞)) → 𝑦 < (𝑦 + 1))
108		simprr 531	. . . . . . . . . 10 ⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℕ) ∧ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ (𝑦 + 1) ≤ 𝑞)) → (𝑦 + 1) ≤ 𝑞)
109	102, 104, 106, 107, 108	ltletrd 8380	. . . . . . . . 9 ⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℕ) ∧ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ (𝑦 + 1) ≤ 𝑞)) → 𝑦 < 𝑞)
110	101	nnzd 9374	. . . . . . . . . 10 ⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℕ) ∧ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ (𝑦 + 1) ≤ 𝑞)) → 𝑦 ∈ ℤ)
111	17	ad2antrl 490	. . . . . . . . . 10 ⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℕ) ∧ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ (𝑦 + 1) ≤ 𝑞)) → 𝑞 ∈ ℤ)
112		zltnle 9299	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℤ ∧ 𝑞 ∈ ℤ) → (𝑦 < 𝑞 ↔ ¬ 𝑞 ≤ 𝑦))
113	110, 111, 112	syl2anc 411	. . . . . . . . 9 ⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℕ) ∧ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ (𝑦 + 1) ≤ 𝑞)) → (𝑦 < 𝑞 ↔ ¬ 𝑞 ≤ 𝑦))
114	109, 113	mpbid 147	. . . . . . . 8 ⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℕ) ∧ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ (𝑦 + 1) ≤ 𝑞)) → ¬ 𝑞 ≤ 𝑦)
115		simprl 529	. . . . . . . . . . 11 ⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℕ) ∧ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ (𝑦 + 1) ≤ 𝑞)) → 𝑞 ∈ ℙ)
116	115	biantrurd 305	. . . . . . . . . 10 ⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℕ) ∧ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ (𝑦 + 1) ≤ 𝑞)) → ((𝑓‘𝑞) ∈ ℕ ↔ (𝑞 ∈ ℙ ∧ (𝑓‘𝑞) ∈ ℕ)))
117	97	ad3antrrr 492	. . . . . . . . . . 11 ⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℕ) ∧ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ (𝑦 + 1) ≤ 𝑞)) → 𝑓:ℙ⟶ℕ₀)
118		ffn 5366	. . . . . . . . . . 11 ⊢ (𝑓:ℙ⟶ℕ₀ → 𝑓 Fn ℙ)
119		elpreima 5636	. . . . . . . . . . 11 ⊢ (𝑓 Fn ℙ → (𝑞 ∈ (^◡𝑓 “ ℕ) ↔ (𝑞 ∈ ℙ ∧ (𝑓‘𝑞) ∈ ℕ)))
120	117, 118, 119	3syl 17	. . . . . . . . . 10 ⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℕ) ∧ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ (𝑦 + 1) ≤ 𝑞)) → (𝑞 ∈ (^◡𝑓 “ ℕ) ↔ (𝑞 ∈ ℙ ∧ (𝑓‘𝑞) ∈ ℕ)))
121	116, 120	bitr4d 191	. . . . . . . . 9 ⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℕ) ∧ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ (𝑦 + 1) ≤ 𝑞)) → ((𝑓‘𝑞) ∈ ℕ ↔ 𝑞 ∈ (^◡𝑓 “ ℕ)))
122		breq1 4007	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑞 → (𝑘 ≤ 𝑦 ↔ 𝑞 ≤ 𝑦))
123	122	rspccv 2839	. . . . . . . . . 10 ⊢ (∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦 → (𝑞 ∈ (^◡𝑓 “ ℕ) → 𝑞 ≤ 𝑦))
124	123	ad2antlr 489	. . . . . . . . 9 ⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℕ) ∧ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ (𝑦 + 1) ≤ 𝑞)) → (𝑞 ∈ (^◡𝑓 “ ℕ) → 𝑞 ≤ 𝑦))
125	121, 124	sylbid 150	. . . . . . . 8 ⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℕ) ∧ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ (𝑦 + 1) ≤ 𝑞)) → ((𝑓‘𝑞) ∈ ℕ → 𝑞 ≤ 𝑦))
126	114, 125	mtod 663	. . . . . . 7 ⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℕ) ∧ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ (𝑦 + 1) ≤ 𝑞)) → ¬ (𝑓‘𝑞) ∈ ℕ)
127	117, 115	ffvelcdmd 5653	. . . . . . . . 9 ⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℕ) ∧ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ (𝑦 + 1) ≤ 𝑞)) → (𝑓‘𝑞) ∈ ℕ₀)
128		elnn0 9178	. . . . . . . . 9 ⊢ ((𝑓‘𝑞) ∈ ℕ₀ ↔ ((𝑓‘𝑞) ∈ ℕ ∨ (𝑓‘𝑞) = 0))
129	127, 128	sylib 122	. . . . . . . 8 ⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℕ) ∧ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ (𝑦 + 1) ≤ 𝑞)) → ((𝑓‘𝑞) ∈ ℕ ∨ (𝑓‘𝑞) = 0))
130	129	ord 724	. . . . . . 7 ⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℕ) ∧ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ (𝑦 + 1) ≤ 𝑞)) → (¬ (𝑓‘𝑞) ∈ ℕ → (𝑓‘𝑞) = 0))
131	126, 130	mpd 13	. . . . . 6 ⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℕ) ∧ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ (𝑦 + 1) ≤ 𝑞)) → (𝑓‘𝑞) = 0)
132	3, 90, 98, 100, 131	1arithlem4 12364	. . . . 5 ⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℕ) ∧ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → ∃𝑥 ∈ ℕ 𝑓 = (𝑀‘𝑥))
133		cnvimass 4992	. . . . . . 7 ⊢ (^◡𝑓 “ ℕ) ⊆ dom 𝑓
134	97	fdmd 5373	. . . . . . . 8 ⊢ (𝑓 ∈ 𝑅 → dom 𝑓 = ℙ)
135		prmssnn 12112	. . . . . . . 8 ⊢ ℙ ⊆ ℕ
136	134, 135	eqsstrdi 3208	. . . . . . 7 ⊢ (𝑓 ∈ 𝑅 → dom 𝑓 ⊆ ℕ)
137	133, 136	sstrid 3167	. . . . . 6 ⊢ (𝑓 ∈ 𝑅 → (^◡𝑓 “ ℕ) ⊆ ℕ)
138	94	simprbi 275	. . . . . 6 ⊢ (𝑓 ∈ 𝑅 → (^◡𝑓 “ ℕ) ∈ Fin)
139		fiubnn 10810	. . . . . 6 ⊢ (((^◡𝑓 “ ℕ) ⊆ ℕ ∧ (^◡𝑓 “ ℕ) ∈ Fin) → ∃𝑦 ∈ ℕ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦)
140	137, 138, 139	syl2anc 411	. . . . 5 ⊢ (𝑓 ∈ 𝑅 → ∃𝑦 ∈ ℕ ∀𝑘 ∈ (^◡𝑓 “ ℕ)𝑘 ≤ 𝑦)
141	132, 140	r19.29a 2620	. . . 4 ⊢ (𝑓 ∈ 𝑅 → ∃𝑥 ∈ ℕ 𝑓 = (𝑀‘𝑥))
142	141	rgen 2530	. . 3 ⊢ ∀𝑓 ∈ 𝑅 ∃𝑥 ∈ ℕ 𝑓 = (𝑀‘𝑥)
143		dffo3 5664	. . 3 ⊢ (𝑀:ℕ–onto→𝑅 ↔ (𝑀:ℕ⟶𝑅 ∧ ∀𝑓 ∈ 𝑅 ∃𝑥 ∈ ℕ 𝑓 = (𝑀‘𝑥)))
144	70, 142, 143	mpbir2an 942	. 2 ⊢ 𝑀:ℕ–onto→𝑅
145		df-f1o 5224	. 2 ⊢ (𝑀:ℕ–1-1-onto→𝑅 ↔ (𝑀:ℕ–1-1→𝑅 ∧ 𝑀:ℕ–onto→𝑅))
146	89, 144, 145	mpbir2an 942	1 ⊢ 𝑀:ℕ–1-1-onto→𝑅

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 708 DECID wdc 834 = wceq 1353 ∈ wcel 2148 ∀wral 2455 ∃wrex 2456 {crab 2459 ⊆ wss 3130 ifcif 3535 class class class wbr 4004 ↦ cmpt 4065 ^◡ccnv 4626 dom cdm 4627 “ cima 4630 Fn wfn 5212 ⟶wf 5213 –1-1→wf1 5214 –onto→wfo 5215 –1-1-onto→wf1o 5216 ‘cfv 5217 (class class class)co 5875 ↑_𝑚 cmap 6648 Fincfn 6740 ℝcr 7810 0cc0 7811 1c1 7812 + caddc 7814 < clt 7992 ≤ cle 7993 ℕcn 8919 ℕ₀cn0 9176 ℤcz 9253 ℤ_≥cuz 9528 ...cfz 10008 ↑cexp 10519 ∥ cdvds 11794 ℙcprime 12107 pCnt cpc 12284

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-coll 4119 ax-sep 4122 ax-nul 4130 ax-pow 4175 ax-pr 4210 ax-un 4434 ax-setind 4537 ax-iinf 4588 ax-cnex 7902 ax-resscn 7903 ax-1cn 7904 ax-1re 7905 ax-icn 7906 ax-addcl 7907 ax-addrcl 7908 ax-mulcl 7909 ax-mulrcl 7910 ax-addcom 7911 ax-mulcom 7912 ax-addass 7913 ax-mulass 7914 ax-distr 7915 ax-i2m1 7916 ax-0lt1 7917 ax-1rid 7918 ax-0id 7919 ax-rnegex 7920 ax-precex 7921 ax-cnre 7922 ax-pre-ltirr 7923 ax-pre-ltwlin 7924 ax-pre-lttrn 7925 ax-pre-apti 7926 ax-pre-ltadd 7927 ax-pre-mulgt0 7928 ax-pre-mulext 7929 ax-arch 7930 ax-caucvg 7931

This theorem depends on definitions: df-bi 117 df-stab 831 df-dc 835 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-nel 2443 df-ral 2460 df-rex 2461 df-reu 2462 df-rmo 2463 df-rab 2464 df-v 2740 df-sbc 2964 df-csb 3059 df-dif 3132 df-un 3134 df-in 3136 df-ss 3143 df-nul 3424 df-if 3536 df-pw 3578 df-sn 3599 df-pr 3600 df-op 3602 df-uni 3811 df-int 3846 df-iun 3889 df-br 4005 df-opab 4066 df-mpt 4067 df-tr 4103 df-id 4294 df-po 4297 df-iso 4298 df-iord 4367 df-on 4369 df-ilim 4370 df-suc 4372 df-iom 4591 df-xp 4633 df-rel 4634 df-cnv 4635 df-co 4636 df-dm 4637 df-rn 4638 df-res 4639 df-ima 4640 df-iota 5179 df-fun 5219 df-fn 5220 df-f 5221 df-f1 5222 df-fo 5223 df-f1o 5224 df-fv 5225 df-isom 5226 df-riota 5831 df-ov 5878 df-oprab 5879 df-mpo 5880 df-1st 6141 df-2nd 6142 df-recs 6306 df-frec 6392 df-1o 6417 df-2o 6418 df-er 6535 df-map 6650 df-en 6741 df-fin 6743 df-sup 6983 df-inf 6984 df-pnf 7994 df-mnf 7995 df-xr 7996 df-ltxr 7997 df-le 7998 df-sub 8130 df-neg 8131 df-reap 8532 df-ap 8539 df-div 8630 df-inn 8920 df-2 8978 df-3 8979 df-4 8980 df-n0 9177 df-xnn0 9240 df-z 9254 df-uz 9529 df-q 9620 df-rp 9654 df-fz 10009 df-fzo 10143 df-fl 10270 df-mod 10323 df-seqfrec 10446 df-exp 10520 df-cj 10851 df-re 10852 df-im 10853 df-rsqrt 11007 df-abs 11008 df-dvds 11795 df-gcd 11944 df-prm 12108 df-pc 12285

This theorem is referenced by: 1arith2 12366

W3C validator