pcprod - Intuitionistic Logic Explorer

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

Theorem pcprod 12302

Description: The product of the primes taken to their respective powers reconstructs the original number. (Contributed by Mario Carneiro, 12-Mar-2014.)

**Hypothesis**
Ref	Expression
pcprod.1	⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt 𝑁)), 1))

**Assertion**
Ref	Expression
pcprod	⊢ (𝑁 ∈ ℕ → (seq1( · , 𝐹)‘𝑁) = 𝑁)

Distinct variable group: 𝑛,𝑁 Allowed substitution hint: 𝐹(𝑛)

Proof of Theorem pcprod Dummy variable 𝑝 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		pcprod.1	. . . . . 6 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt 𝑁)), 1))
2		pccl 12257	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℙ ∧ 𝑁 ∈ ℕ) → (𝑛 pCnt 𝑁) ∈ ℕ₀)
3	2	ancoms 266	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑁) ∈ ℕ₀)
4	3	ralrimiva 2544	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ∀𝑛 ∈ ℙ (𝑛 pCnt 𝑁) ∈ ℕ₀)
5	4	adantl 275	. . . . . 6 ⊢ ((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ∀𝑛 ∈ ℙ (𝑛 pCnt 𝑁) ∈ ℕ₀)
6		simpr 109	. . . . . 6 ⊢ ((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℕ)
7		simpl 108	. . . . . 6 ⊢ ((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℕ) → 𝑝 ∈ ℙ)
8		oveq1 5864	. . . . . 6 ⊢ (𝑛 = 𝑝 → (𝑛 pCnt 𝑁) = (𝑝 pCnt 𝑁))
9	1, 5, 6, 7, 8	pcmpt 12299	. . . . 5 ⊢ ((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℕ) → (𝑝 pCnt (seq1( · , 𝐹)‘𝑁)) = if(𝑝 ≤ 𝑁, (𝑝 pCnt 𝑁), 0))
10		iftrue 3532	. . . . . . 7 ⊢ (𝑝 ≤ 𝑁 → if(𝑝 ≤ 𝑁, (𝑝 pCnt 𝑁), 0) = (𝑝 pCnt 𝑁))
11	10	adantl 275	. . . . . 6 ⊢ (((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℕ) ∧ 𝑝 ≤ 𝑁) → if(𝑝 ≤ 𝑁, (𝑝 pCnt 𝑁), 0) = (𝑝 pCnt 𝑁))
12		iffalse 3535	. . . . . . . 8 ⊢ (¬ 𝑝 ≤ 𝑁 → if(𝑝 ≤ 𝑁, (𝑝 pCnt 𝑁), 0) = 0)
13	12	adantl 275	. . . . . . 7 ⊢ (((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑝 ≤ 𝑁) → if(𝑝 ≤ 𝑁, (𝑝 pCnt 𝑁), 0) = 0)
14		prmz 12069	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
15		dvdsle 11808	. . . . . . . . . 10 ⊢ ((𝑝 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑝 ∥ 𝑁 → 𝑝 ≤ 𝑁))
16	14, 15	sylan 281	. . . . . . . . 9 ⊢ ((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℕ) → (𝑝 ∥ 𝑁 → 𝑝 ≤ 𝑁))
17	16	con3dimp 631	. . . . . . . 8 ⊢ (((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑝 ≤ 𝑁) → ¬ 𝑝 ∥ 𝑁)
18		pceq0 12279	. . . . . . . . 9 ⊢ ((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ((𝑝 pCnt 𝑁) = 0 ↔ ¬ 𝑝 ∥ 𝑁))
19	18	adantr 274	. . . . . . . 8 ⊢ (((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑝 ≤ 𝑁) → ((𝑝 pCnt 𝑁) = 0 ↔ ¬ 𝑝 ∥ 𝑁))
20	17, 19	mpbird 166	. . . . . . 7 ⊢ (((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑝 ≤ 𝑁) → (𝑝 pCnt 𝑁) = 0)
21	13, 20	eqtr4d 2207	. . . . . 6 ⊢ (((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℕ) ∧ ¬ 𝑝 ≤ 𝑁) → if(𝑝 ≤ 𝑁, (𝑝 pCnt 𝑁), 0) = (𝑝 pCnt 𝑁))
22	14	adantr 274	. . . . . . . 8 ⊢ ((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℕ) → 𝑝 ∈ ℤ)
23	6	nnzd 9337	. . . . . . . 8 ⊢ ((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℤ)
24		zdcle 9292	. . . . . . . 8 ⊢ ((𝑝 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝑝 ≤ 𝑁)
25	22, 23, 24	syl2anc 409	. . . . . . 7 ⊢ ((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℕ) → DECID 𝑝 ≤ 𝑁)
26		exmiddc 832	. . . . . . 7 ⊢ (DECID 𝑝 ≤ 𝑁 → (𝑝 ≤ 𝑁 ∨ ¬ 𝑝 ≤ 𝑁))
27	25, 26	syl 14	. . . . . 6 ⊢ ((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℕ) → (𝑝 ≤ 𝑁 ∨ ¬ 𝑝 ≤ 𝑁))
28	11, 21, 27	mpjaodan 794	. . . . 5 ⊢ ((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℕ) → if(𝑝 ≤ 𝑁, (𝑝 pCnt 𝑁), 0) = (𝑝 pCnt 𝑁))
29	9, 28	eqtrd 2204	. . . 4 ⊢ ((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℕ) → (𝑝 pCnt (seq1( · , 𝐹)‘𝑁)) = (𝑝 pCnt 𝑁))
30	29	ancoms 266	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (seq1( · , 𝐹)‘𝑁)) = (𝑝 pCnt 𝑁))
31	30	ralrimiva 2544	. 2 ⊢ (𝑁 ∈ ℕ → ∀𝑝 ∈ ℙ (𝑝 pCnt (seq1( · , 𝐹)‘𝑁)) = (𝑝 pCnt 𝑁))
32	1, 4	pcmptcl 12298	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (𝐹:ℕ⟶ℕ ∧ seq1( · , 𝐹):ℕ⟶ℕ))
33	32	simprd 113	. . . . 5 ⊢ (𝑁 ∈ ℕ → seq1( · , 𝐹):ℕ⟶ℕ)
34		ffvelcdm 5633	. . . . 5 ⊢ ((seq1( · , 𝐹):ℕ⟶ℕ ∧ 𝑁 ∈ ℕ) → (seq1( · , 𝐹)‘𝑁) ∈ ℕ)
35	33, 34	mpancom 420	. . . 4 ⊢ (𝑁 ∈ ℕ → (seq1( · , 𝐹)‘𝑁) ∈ ℕ)
36	35	nnnn0d 9192	. . 3 ⊢ (𝑁 ∈ ℕ → (seq1( · , 𝐹)‘𝑁) ∈ ℕ₀)
37		nnnn0 9146	. . 3 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ₀)
38		pc11 12288	. . 3 ⊢ (((seq1( · , 𝐹)‘𝑁) ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → ((seq1( · , 𝐹)‘𝑁) = 𝑁 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt (seq1( · , 𝐹)‘𝑁)) = (𝑝 pCnt 𝑁)))
39	36, 37, 38	syl2anc 409	. 2 ⊢ (𝑁 ∈ ℕ → ((seq1( · , 𝐹)‘𝑁) = 𝑁 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt (seq1( · , 𝐹)‘𝑁)) = (𝑝 pCnt 𝑁)))
40	31, 39	mpbird 166	1 ⊢ (𝑁 ∈ ℕ → (seq1( · , 𝐹)‘𝑁) = 𝑁)

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ↔ wb 104 ∨ wo 704 DECID wdc 830 = wceq 1349 ∈ wcel 2142 ∀wral 2449 ifcif 3527 class class class wbr 3990 ↦ cmpt 4051 ⟶wf 5196 ‘cfv 5200 (class class class)co 5857 0cc0 7778 1c1 7779 · cmul 7783 ≤ cle 7959 ℕcn 8882 ℕ₀cn0 9139 ℤcz 9216 seqcseq 10405 ↑cexp 10479 ∥ cdvds 11753 ℙcprime 12065 pCnt cpc 12242

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 610 ax-in2 611 ax-io 705 ax-5 1441 ax-7 1442 ax-gen 1443 ax-ie1 1487 ax-ie2 1488 ax-8 1498 ax-10 1499 ax-11 1500 ax-i12 1501 ax-bndl 1503 ax-4 1504 ax-17 1520 ax-i9 1524 ax-ial 1528 ax-i5r 1529 ax-13 2144 ax-14 2145 ax-ext 2153 ax-coll 4105 ax-sep 4108 ax-nul 4116 ax-pow 4161 ax-pr 4195 ax-un 4419 ax-setind 4522 ax-iinf 4573 ax-cnex 7869 ax-resscn 7870 ax-1cn 7871 ax-1re 7872 ax-icn 7873 ax-addcl 7874 ax-addrcl 7875 ax-mulcl 7876 ax-mulrcl 7877 ax-addcom 7878 ax-mulcom 7879 ax-addass 7880 ax-mulass 7881 ax-distr 7882 ax-i2m1 7883 ax-0lt1 7884 ax-1rid 7885 ax-0id 7886 ax-rnegex 7887 ax-precex 7888 ax-cnre 7889 ax-pre-ltirr 7890 ax-pre-ltwlin 7891 ax-pre-lttrn 7892 ax-pre-apti 7893 ax-pre-ltadd 7894 ax-pre-mulgt0 7895 ax-pre-mulext 7896 ax-arch 7897 ax-caucvg 7898

This theorem depends on definitions: df-bi 116 df-stab 827 df-dc 831 df-3or 975 df-3an 976 df-tru 1352 df-fal 1355 df-nf 1455 df-sb 1757 df-eu 2023 df-mo 2024 df-clab 2158 df-cleq 2164 df-clel 2167 df-nfc 2302 df-ne 2342 df-nel 2437 df-ral 2454 df-rex 2455 df-reu 2456 df-rmo 2457 df-rab 2458 df-v 2733 df-sbc 2957 df-csb 3051 df-dif 3124 df-un 3126 df-in 3128 df-ss 3135 df-nul 3416 df-if 3528 df-pw 3569 df-sn 3590 df-pr 3591 df-op 3593 df-uni 3798 df-int 3833 df-iun 3876 df-br 3991 df-opab 4052 df-mpt 4053 df-tr 4089 df-id 4279 df-po 4282 df-iso 4283 df-iord 4352 df-on 4354 df-ilim 4355 df-suc 4357 df-iom 4576 df-xp 4618 df-rel 4619 df-cnv 4620 df-co 4621 df-dm 4622 df-rn 4623 df-res 4624 df-ima 4625 df-iota 5162 df-fun 5202 df-fn 5203 df-f 5204 df-f1 5205 df-fo 5206 df-f1o 5207 df-fv 5208 df-isom 5209 df-riota 5813 df-ov 5860 df-oprab 5861 df-mpo 5862 df-1st 6123 df-2nd 6124 df-recs 6288 df-frec 6374 df-1o 6399 df-2o 6400 df-er 6517 df-en 6723 df-fin 6725 df-sup 6965 df-inf 6966 df-pnf 7960 df-mnf 7961 df-xr 7962 df-ltxr 7963 df-le 7964 df-sub 8096 df-neg 8097 df-reap 8498 df-ap 8505 df-div 8594 df-inn 8883 df-2 8941 df-3 8942 df-4 8943 df-n0 9140 df-xnn0 9203 df-z 9217 df-uz 9492 df-q 9583 df-rp 9615 df-fz 9970 df-fzo 10103 df-fl 10230 df-mod 10283 df-seqfrec 10406 df-exp 10480 df-cj 10810 df-re 10811 df-im 10812 df-rsqrt 10966 df-abs 10967 df-dvds 11754 df-gcd 11902 df-prm 12066 df-pc 12243

This theorem is referenced by: (None)

W3C validator