MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1arith Structured version   Visualization version   GIF version

Theorem 1arith 16799
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 𝑅 = {𝑒 ∈ (ℕ0m ℙ) ∣ (𝑒 “ ℕ) ∈ 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.
StepHypRef Expression
1 prmex 16553 . . . . . 6 ℙ ∈ V
21mptex 7173 . . . . 5 (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ V
3 1arith.1 . . . . 5 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))
42, 3fnmpti 6644 . . . 4 𝑀 Fn ℕ
531arithlem3 16797 . . . . . . 7 (𝑥 ∈ ℕ → (𝑀𝑥):ℙ⟶ℕ0)
6 nn0ex 12419 . . . . . . . 8 0 ∈ V
76, 1elmap 8809 . . . . . . 7 ((𝑀𝑥) ∈ (ℕ0m ℙ) ↔ (𝑀𝑥):ℙ⟶ℕ0)
85, 7sylibr 233 . . . . . 6 (𝑥 ∈ ℕ → (𝑀𝑥) ∈ (ℕ0m ℙ))
9 fzfi 13877 . . . . . . 7 (1...𝑥) ∈ Fin
10 ffn 6668 . . . . . . . . . 10 ((𝑀𝑥):ℙ⟶ℕ0 → (𝑀𝑥) Fn ℙ)
11 elpreima 7008 . . . . . . . . . 10 ((𝑀𝑥) Fn ℙ → (𝑞 ∈ ((𝑀𝑥) “ ℕ) ↔ (𝑞 ∈ ℙ ∧ ((𝑀𝑥)‘𝑞) ∈ ℕ)))
125, 10, 113syl 18 . . . . . . . . 9 (𝑥 ∈ ℕ → (𝑞 ∈ ((𝑀𝑥) “ ℕ) ↔ (𝑞 ∈ ℙ ∧ ((𝑀𝑥)‘𝑞) ∈ ℕ)))
1331arithlem2 16796 . . . . . . . . . . . 12 ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → ((𝑀𝑥)‘𝑞) = (𝑞 pCnt 𝑥))
1413eleq1d 2822 . . . . . . . . . . 11 ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (((𝑀𝑥)‘𝑞) ∈ ℕ ↔ (𝑞 pCnt 𝑥) ∈ ℕ))
15 prmz 16551 . . . . . . . . . . . . 13 (𝑞 ∈ ℙ → 𝑞 ∈ ℤ)
16 id 22 . . . . . . . . . . . . 13 (𝑥 ∈ ℕ → 𝑥 ∈ ℕ)
17 dvdsle 16192 . . . . . . . . . . . . 13 ((𝑞 ∈ ℤ ∧ 𝑥 ∈ ℕ) → (𝑞𝑥𝑞𝑥))
1815, 16, 17syl2anr 597 . . . . . . . . . . . 12 ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (𝑞𝑥𝑞𝑥))
19 pcelnn 16742 . . . . . . . . . . . . 13 ((𝑞 ∈ ℙ ∧ 𝑥 ∈ ℕ) → ((𝑞 pCnt 𝑥) ∈ ℕ ↔ 𝑞𝑥))
2019ancoms 459 . . . . . . . . . . . 12 ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → ((𝑞 pCnt 𝑥) ∈ ℕ ↔ 𝑞𝑥))
21 prmnn 16550 . . . . . . . . . . . . . 14 (𝑞 ∈ ℙ → 𝑞 ∈ ℕ)
22 nnuz 12806 . . . . . . . . . . . . . 14 ℕ = (ℤ‘1)
2321, 22eleqtrdi 2848 . . . . . . . . . . . . 13 (𝑞 ∈ ℙ → 𝑞 ∈ (ℤ‘1))
24 nnz 12520 . . . . . . . . . . . . 13 (𝑥 ∈ ℕ → 𝑥 ∈ ℤ)
25 elfz5 13433 . . . . . . . . . . . . 13 ((𝑞 ∈ (ℤ‘1) ∧ 𝑥 ∈ ℤ) → (𝑞 ∈ (1...𝑥) ↔ 𝑞𝑥))
2623, 24, 25syl2anr 597 . . . . . . . . . . . 12 ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (𝑞 ∈ (1...𝑥) ↔ 𝑞𝑥))
2718, 20, 263imtr4d 293 . . . . . . . . . . 11 ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → ((𝑞 pCnt 𝑥) ∈ ℕ → 𝑞 ∈ (1...𝑥)))
2814, 27sylbid 239 . . . . . . . . . 10 ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (((𝑀𝑥)‘𝑞) ∈ ℕ → 𝑞 ∈ (1...𝑥)))
2928expimpd 454 . . . . . . . . 9 (𝑥 ∈ ℕ → ((𝑞 ∈ ℙ ∧ ((𝑀𝑥)‘𝑞) ∈ ℕ) → 𝑞 ∈ (1...𝑥)))
3012, 29sylbid 239 . . . . . . . 8 (𝑥 ∈ ℕ → (𝑞 ∈ ((𝑀𝑥) “ ℕ) → 𝑞 ∈ (1...𝑥)))
3130ssrdv 3950 . . . . . . 7 (𝑥 ∈ ℕ → ((𝑀𝑥) “ ℕ) ⊆ (1...𝑥))
32 ssfi 9117 . . . . . . 7 (((1...𝑥) ∈ Fin ∧ ((𝑀𝑥) “ ℕ) ⊆ (1...𝑥)) → ((𝑀𝑥) “ ℕ) ∈ Fin)
339, 31, 32sylancr 587 . . . . . 6 (𝑥 ∈ ℕ → ((𝑀𝑥) “ ℕ) ∈ Fin)
34 cnveq 5829 . . . . . . . . 9 (𝑒 = (𝑀𝑥) → 𝑒 = (𝑀𝑥))
3534imaeq1d 6012 . . . . . . . 8 (𝑒 = (𝑀𝑥) → (𝑒 “ ℕ) = ((𝑀𝑥) “ ℕ))
3635eleq1d 2822 . . . . . . 7 (𝑒 = (𝑀𝑥) → ((𝑒 “ ℕ) ∈ Fin ↔ ((𝑀𝑥) “ ℕ) ∈ Fin))
37 1arith.2 . . . . . . 7 𝑅 = {𝑒 ∈ (ℕ0m ℙ) ∣ (𝑒 “ ℕ) ∈ Fin}
3836, 37elrab2 3648 . . . . . 6 ((𝑀𝑥) ∈ 𝑅 ↔ ((𝑀𝑥) ∈ (ℕ0m ℙ) ∧ ((𝑀𝑥) “ ℕ) ∈ Fin))
398, 33, 38sylanbrc 583 . . . . 5 (𝑥 ∈ ℕ → (𝑀𝑥) ∈ 𝑅)
4039rgen 3066 . . . 4 𝑥 ∈ ℕ (𝑀𝑥) ∈ 𝑅
41 ffnfv 7066 . . . 4 (𝑀:ℕ⟶𝑅 ↔ (𝑀 Fn ℕ ∧ ∀𝑥 ∈ ℕ (𝑀𝑥) ∈ 𝑅))
424, 40, 41mpbir2an 709 . . 3 𝑀:ℕ⟶𝑅
4313adantlr 713 . . . . . . . 8 (((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) ∧ 𝑞 ∈ ℙ) → ((𝑀𝑥)‘𝑞) = (𝑞 pCnt 𝑥))
4431arithlem2 16796 . . . . . . . . 9 ((𝑦 ∈ ℕ ∧ 𝑞 ∈ ℙ) → ((𝑀𝑦)‘𝑞) = (𝑞 pCnt 𝑦))
4544adantll 712 . . . . . . . 8 (((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) ∧ 𝑞 ∈ ℙ) → ((𝑀𝑦)‘𝑞) = (𝑞 pCnt 𝑦))
4643, 45eqeq12d 2752 . . . . . . 7 (((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) ∧ 𝑞 ∈ ℙ) → (((𝑀𝑥)‘𝑞) = ((𝑀𝑦)‘𝑞) ↔ (𝑞 pCnt 𝑥) = (𝑞 pCnt 𝑦)))
4746ralbidva 3172 . . . . . 6 ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (∀𝑞 ∈ ℙ ((𝑀𝑥)‘𝑞) = ((𝑀𝑦)‘𝑞) ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt 𝑥) = (𝑞 pCnt 𝑦)))
4831arithlem3 16797 . . . . . . 7 (𝑦 ∈ ℕ → (𝑀𝑦):ℙ⟶ℕ0)
49 ffn 6668 . . . . . . . 8 ((𝑀𝑦):ℙ⟶ℕ0 → (𝑀𝑦) Fn ℙ)
50 eqfnfv 6982 . . . . . . . 8 (((𝑀𝑥) Fn ℙ ∧ (𝑀𝑦) Fn ℙ) → ((𝑀𝑥) = (𝑀𝑦) ↔ ∀𝑞 ∈ ℙ ((𝑀𝑥)‘𝑞) = ((𝑀𝑦)‘𝑞)))
5110, 49, 50syl2an 596 . . . . . . 7 (((𝑀𝑥):ℙ⟶ℕ0 ∧ (𝑀𝑦):ℙ⟶ℕ0) → ((𝑀𝑥) = (𝑀𝑦) ↔ ∀𝑞 ∈ ℙ ((𝑀𝑥)‘𝑞) = ((𝑀𝑦)‘𝑞)))
525, 48, 51syl2an 596 . . . . . 6 ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝑀𝑥) = (𝑀𝑦) ↔ ∀𝑞 ∈ ℙ ((𝑀𝑥)‘𝑞) = ((𝑀𝑦)‘𝑞)))
53 nnnn0 12420 . . . . . . 7 (𝑥 ∈ ℕ → 𝑥 ∈ ℕ0)
54 nnnn0 12420 . . . . . . 7 (𝑦 ∈ ℕ → 𝑦 ∈ ℕ0)
55 pc11 16752 . . . . . . 7 ((𝑥 ∈ ℕ0𝑦 ∈ ℕ0) → (𝑥 = 𝑦 ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt 𝑥) = (𝑞 pCnt 𝑦)))
5653, 54, 55syl2an 596 . . . . . 6 ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑥 = 𝑦 ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt 𝑥) = (𝑞 pCnt 𝑦)))
5747, 52, 563bitr4d 310 . . . . 5 ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝑀𝑥) = (𝑀𝑦) ↔ 𝑥 = 𝑦))
5857biimpd 228 . . . 4 ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝑀𝑥) = (𝑀𝑦) → 𝑥 = 𝑦))
5958rgen2 3194 . . 3 𝑥 ∈ ℕ ∀𝑦 ∈ ℕ ((𝑀𝑥) = (𝑀𝑦) → 𝑥 = 𝑦)
60 dff13 7202 . . 3 (𝑀:ℕ–1-1𝑅 ↔ (𝑀:ℕ⟶𝑅 ∧ ∀𝑥 ∈ ℕ ∀𝑦 ∈ ℕ ((𝑀𝑥) = (𝑀𝑦) → 𝑥 = 𝑦)))
6142, 59, 60mpbir2an 709 . 2 𝑀:ℕ–1-1𝑅
62 eqid 2736 . . . . . 6 (𝑔 ∈ ℕ ↦ if(𝑔 ∈ ℙ, (𝑔↑(𝑓𝑔)), 1)) = (𝑔 ∈ ℕ ↦ if(𝑔 ∈ ℙ, (𝑔↑(𝑓𝑔)), 1))
63 cnveq 5829 . . . . . . . . . . . 12 (𝑒 = 𝑓𝑒 = 𝑓)
6463imaeq1d 6012 . . . . . . . . . . 11 (𝑒 = 𝑓 → (𝑒 “ ℕ) = (𝑓 “ ℕ))
6564eleq1d 2822 . . . . . . . . . 10 (𝑒 = 𝑓 → ((𝑒 “ ℕ) ∈ Fin ↔ (𝑓 “ ℕ) ∈ Fin))
6665, 37elrab2 3648 . . . . . . . . 9 (𝑓𝑅 ↔ (𝑓 ∈ (ℕ0m ℙ) ∧ (𝑓 “ ℕ) ∈ Fin))
6766simplbi 498 . . . . . . . 8 (𝑓𝑅𝑓 ∈ (ℕ0m ℙ))
686, 1elmap 8809 . . . . . . . 8 (𝑓 ∈ (ℕ0m ℙ) ↔ 𝑓:ℙ⟶ℕ0)
6967, 68sylib 217 . . . . . . 7 (𝑓𝑅𝑓:ℙ⟶ℕ0)
7069ad2antrr 724 . . . . . 6 (((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) → 𝑓:ℙ⟶ℕ0)
71 simplr 767 . . . . . . . . 9 (((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) → 𝑦 ∈ ℝ)
72 0re 11157 . . . . . . . . 9 0 ∈ ℝ
73 ifcl 4531 . . . . . . . . 9 ((𝑦 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ)
7471, 72, 73sylancl 586 . . . . . . . 8 (((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ)
75 max1 13104 . . . . . . . . 9 ((0 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 0 ≤ if(0 ≤ 𝑦, 𝑦, 0))
7672, 71, 75sylancr 587 . . . . . . . 8 (((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) → 0 ≤ if(0 ≤ 𝑦, 𝑦, 0))
77 flge0nn0 13725 . . . . . . . 8 ((if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ ∧ 0 ≤ if(0 ≤ 𝑦, 𝑦, 0)) → (⌊‘if(0 ≤ 𝑦, 𝑦, 0)) ∈ ℕ0)
7874, 76, 77syl2anc 584 . . . . . . 7 (((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) → (⌊‘if(0 ≤ 𝑦, 𝑦, 0)) ∈ ℕ0)
79 nn0p1nn 12452 . . . . . . 7 ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) ∈ ℕ0 → ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ∈ ℕ)
8078, 79syl 17 . . . . . 6 (((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) → ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ∈ ℕ)
8171adantr 481 . . . . . . . . . 10 ((((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑦 ∈ ℝ)
8280adantr 481 . . . . . . . . . . 11 ((((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ∈ ℕ)
8382nnred 12168 . . . . . . . . . 10 ((((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ∈ ℝ)
8415ssriv 3948 . . . . . . . . . . . 12 ℙ ⊆ ℤ
85 zssre 12506 . . . . . . . . . . . 12 ℤ ⊆ ℝ
8684, 85sstri 3953 . . . . . . . . . . 11 ℙ ⊆ ℝ
87 simprl 769 . . . . . . . . . . 11 ((((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑞 ∈ ℙ)
8886, 87sselid 3942 . . . . . . . . . 10 ((((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑞 ∈ ℝ)
8974adantr 481 . . . . . . . . . . 11 ((((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ)
90 max2 13106 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ≤ if(0 ≤ 𝑦, 𝑦, 0))
9172, 81, 90sylancr 587 . . . . . . . . . . 11 ((((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑦 ≤ if(0 ≤ 𝑦, 𝑦, 0))
92 flltp1 13705 . . . . . . . . . . . 12 (if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ → if(0 ≤ 𝑦, 𝑦, 0) < ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1))
9389, 92syl 17 . . . . . . . . . . 11 ((((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → if(0 ≤ 𝑦, 𝑦, 0) < ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1))
9481, 89, 83, 91, 93lelttrd 11313 . . . . . . . . . 10 ((((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑦 < ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1))
95 simprr 771 . . . . . . . . . 10 ((((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)
9681, 83, 88, 94, 95ltletrd 11315 . . . . . . . . 9 ((((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑦 < 𝑞)
9781, 88ltnled 11302 . . . . . . . . 9 ((((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (𝑦 < 𝑞 ↔ ¬ 𝑞𝑦))
9896, 97mpbid 231 . . . . . . . 8 ((((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ¬ 𝑞𝑦)
9987biantrurd 533 . . . . . . . . . 10 ((((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((𝑓𝑞) ∈ ℕ ↔ (𝑞 ∈ ℙ ∧ (𝑓𝑞) ∈ ℕ)))
10070adantr 481 . . . . . . . . . . 11 ((((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑓:ℙ⟶ℕ0)
101 ffn 6668 . . . . . . . . . . 11 (𝑓:ℙ⟶ℕ0𝑓 Fn ℙ)
102 elpreima 7008 . . . . . . . . . . 11 (𝑓 Fn ℙ → (𝑞 ∈ (𝑓 “ ℕ) ↔ (𝑞 ∈ ℙ ∧ (𝑓𝑞) ∈ ℕ)))
103100, 101, 1023syl 18 . . . . . . . . . 10 ((((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (𝑞 ∈ (𝑓 “ ℕ) ↔ (𝑞 ∈ ℙ ∧ (𝑓𝑞) ∈ ℕ)))
10499, 103bitr4d 281 . . . . . . . . 9 ((((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((𝑓𝑞) ∈ ℕ ↔ 𝑞 ∈ (𝑓 “ ℕ)))
105 simplr 767 . . . . . . . . . 10 ((((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦)
106 breq1 5108 . . . . . . . . . . 11 (𝑘 = 𝑞 → (𝑘𝑦𝑞𝑦))
107106rspccv 3578 . . . . . . . . . 10 (∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦 → (𝑞 ∈ (𝑓 “ ℕ) → 𝑞𝑦))
108105, 107syl 17 . . . . . . . . 9 ((((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (𝑞 ∈ (𝑓 “ ℕ) → 𝑞𝑦))
109104, 108sylbid 239 . . . . . . . 8 ((((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((𝑓𝑞) ∈ ℕ → 𝑞𝑦))
11098, 109mtod 197 . . . . . . 7 ((((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ¬ (𝑓𝑞) ∈ ℕ)
111100, 87ffvelcdmd 7036 . . . . . . . . 9 ((((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (𝑓𝑞) ∈ ℕ0)
112 elnn0 12415 . . . . . . . . 9 ((𝑓𝑞) ∈ ℕ0 ↔ ((𝑓𝑞) ∈ ℕ ∨ (𝑓𝑞) = 0))
113111, 112sylib 217 . . . . . . . 8 ((((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((𝑓𝑞) ∈ ℕ ∨ (𝑓𝑞) = 0))
114113ord 862 . . . . . . 7 ((((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (¬ (𝑓𝑞) ∈ ℕ → (𝑓𝑞) = 0))
115110, 114mpd 15 . . . . . 6 ((((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (𝑓𝑞) = 0)
1163, 62, 70, 80, 1151arithlem4 16798 . . . . 5 (((𝑓𝑅𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦) → ∃𝑥 ∈ ℕ 𝑓 = (𝑀𝑥))
117 cnvimass 6033 . . . . . . 7 (𝑓 “ ℕ) ⊆ dom 𝑓
11869fdmd 6679 . . . . . . . 8 (𝑓𝑅 → dom 𝑓 = ℙ)
119118, 86eqsstrdi 3998 . . . . . . 7 (𝑓𝑅 → dom 𝑓 ⊆ ℝ)
120117, 119sstrid 3955 . . . . . 6 (𝑓𝑅 → (𝑓 “ ℕ) ⊆ ℝ)
12166simprbi 497 . . . . . 6 (𝑓𝑅 → (𝑓 “ ℕ) ∈ Fin)
122 fimaxre2 12100 . . . . . 6 (((𝑓 “ ℕ) ⊆ ℝ ∧ (𝑓 “ ℕ) ∈ Fin) → ∃𝑦 ∈ ℝ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦)
123120, 121, 122syl2anc 584 . . . . 5 (𝑓𝑅 → ∃𝑦 ∈ ℝ ∀𝑘 ∈ (𝑓 “ ℕ)𝑘𝑦)
124116, 123r19.29a 3159 . . . 4 (𝑓𝑅 → ∃𝑥 ∈ ℕ 𝑓 = (𝑀𝑥))
125124rgen 3066 . . 3 𝑓𝑅𝑥 ∈ ℕ 𝑓 = (𝑀𝑥)
126 dffo3 7052 . . 3 (𝑀:ℕ–onto𝑅 ↔ (𝑀:ℕ⟶𝑅 ∧ ∀𝑓𝑅𝑥 ∈ ℕ 𝑓 = (𝑀𝑥)))
12742, 125, 126mpbir2an 709 . 2 𝑀:ℕ–onto𝑅
128 df-f1o 6503 . 2 (𝑀:ℕ–1-1-onto𝑅 ↔ (𝑀:ℕ–1-1𝑅𝑀:ℕ–onto𝑅))
12961, 127, 128mpbir2an 709 1 𝑀:ℕ–1-1-onto𝑅
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845   = wceq 1541  wcel 2106  wral 3064  wrex 3073  {crab 3407  wss 3910  ifcif 4486   class class class wbr 5105  cmpt 5188  ccnv 5632  dom cdm 5633  cima 5636   Fn wfn 6491  wf 6492  1-1wf1 6493  ontowfo 6494  1-1-ontowf1o 6495  cfv 6496  (class class class)co 7357  m cmap 8765  Fincfn 8883  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   < clt 11189  cle 11190  cn 12153  0cn0 12413  cz 12499  cuz 12763  ...cfz 13424  cfl 13695  cexp 13967  cdvds 16136  cprime 16547   pCnt cpc 16708
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-er 8648  df-map 8767  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-sup 9378  df-inf 9379  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-n0 12414  df-z 12500  df-uz 12764  df-q 12874  df-rp 12916  df-fz 13425  df-fl 13697  df-mod 13775  df-seq 13907  df-exp 13968  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-dvds 16137  df-gcd 16375  df-prm 16548  df-pc 16709
This theorem is referenced by:  1arith2  16800  sqff1o  26531
  Copyright terms: Public domain W3C validator