pczcl - Intuitionistic Logic Explorer

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

Theorem pczcl 12477

Description: Closure of the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014.)

**Assertion**
Ref	Expression
pczcl	⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃 pCnt 𝑁) ∈ ℕ₀)

Proof of Theorem pczcl Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2196	. . 3 ⊢ sup({𝑥 ∈ ℕ₀ ∣ (𝑃↑𝑥) ∥ 𝑁}, ℝ, < ) = sup({𝑥 ∈ ℕ₀ ∣ (𝑃↑𝑥) ∥ 𝑁}, ℝ, < )
2	1	pczpre 12476	. 2 ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃 pCnt 𝑁) = sup({𝑥 ∈ ℕ₀ ∣ (𝑃↑𝑥) ∥ 𝑁}, ℝ, < ))
3		prmuz2 12309	. . . 4 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ_≥‘2))
4		eqid 2196	. . . . 5 ⊢ {𝑥 ∈ ℕ₀ ∣ (𝑃↑𝑥) ∥ 𝑁} = {𝑥 ∈ ℕ₀ ∣ (𝑃↑𝑥) ∥ 𝑁}
5	4, 1	pcprecl 12468	. . . 4 ⊢ ((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (sup({𝑥 ∈ ℕ₀ ∣ (𝑃↑𝑥) ∥ 𝑁}, ℝ, < ) ∈ ℕ₀ ∧ (𝑃↑sup({𝑥 ∈ ℕ₀ ∣ (𝑃↑𝑥) ∥ 𝑁}, ℝ, < )) ∥ 𝑁))
6	3, 5	sylan 283	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (sup({𝑥 ∈ ℕ₀ ∣ (𝑃↑𝑥) ∥ 𝑁}, ℝ, < ) ∈ ℕ₀ ∧ (𝑃↑sup({𝑥 ∈ ℕ₀ ∣ (𝑃↑𝑥) ∥ 𝑁}, ℝ, < )) ∥ 𝑁))
7	6	simpld 112	. 2 ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → sup({𝑥 ∈ ℕ₀ ∣ (𝑃↑𝑥) ∥ 𝑁}, ℝ, < ) ∈ ℕ₀)
8	2, 7	eqeltrd 2273	1 ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃 pCnt 𝑁) ∈ ℕ₀)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ∈ wcel 2167 ≠ wne 2367 {crab 2479 class class class wbr 4034 ‘cfv 5259 (class class class)co 5923 supcsup 7049 ℝcr 7880 0cc0 7881 < clt 8063 2c2 9043 ℕ₀cn0 9251 ℤcz 9328 ℤ_≥cuz 9603 ↑cexp 10632 ∥ cdvds 11954 ℙcprime 12285 pCnt cpc 12463

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 615 ax-in2 616 ax-io 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4149 ax-sep 4152 ax-nul 4160 ax-pow 4208 ax-pr 4243 ax-un 4469 ax-setind 4574 ax-iinf 4625 ax-cnex 7972 ax-resscn 7973 ax-1cn 7974 ax-1re 7975 ax-icn 7976 ax-addcl 7977 ax-addrcl 7978 ax-mulcl 7979 ax-mulrcl 7980 ax-addcom 7981 ax-mulcom 7982 ax-addass 7983 ax-mulass 7984 ax-distr 7985 ax-i2m1 7986 ax-0lt1 7987 ax-1rid 7988 ax-0id 7989 ax-rnegex 7990 ax-precex 7991 ax-cnre 7992 ax-pre-ltirr 7993 ax-pre-ltwlin 7994 ax-pre-lttrn 7995 ax-pre-apti 7996 ax-pre-ltadd 7997 ax-pre-mulgt0 7998 ax-pre-mulext 7999 ax-arch 8000 ax-caucvg 8001

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3452 df-if 3563 df-pw 3608 df-sn 3629 df-pr 3630 df-op 3632 df-uni 3841 df-int 3876 df-iun 3919 df-br 4035 df-opab 4096 df-mpt 4097 df-tr 4133 df-id 4329 df-po 4332 df-iso 4333 df-iord 4402 df-on 4404 df-ilim 4405 df-suc 4407 df-iom 4628 df-xp 4670 df-rel 4671 df-cnv 4672 df-co 4673 df-dm 4674 df-rn 4675 df-res 4676 df-ima 4677 df-iota 5220 df-fun 5261 df-fn 5262 df-f 5263 df-f1 5264 df-fo 5265 df-f1o 5266 df-fv 5267 df-isom 5268 df-riota 5878 df-ov 5926 df-oprab 5927 df-mpo 5928 df-1st 6199 df-2nd 6200 df-recs 6364 df-frec 6450 df-1o 6475 df-2o 6476 df-er 6593 df-en 6801 df-sup 7051 df-inf 7052 df-pnf 8065 df-mnf 8066 df-xr 8067 df-ltxr 8068 df-le 8069 df-sub 8201 df-neg 8202 df-reap 8604 df-ap 8611 df-div 8702 df-inn 8993 df-2 9051 df-3 9052 df-4 9053 df-n0 9252 df-z 9329 df-uz 9604 df-q 9696 df-rp 9731 df-fz 10086 df-fzo 10220 df-fl 10362 df-mod 10417 df-seqfrec 10542 df-exp 10633 df-cj 11009 df-re 11010 df-im 11011 df-rsqrt 11165 df-abs 11166 df-dvds 11955 df-gcd 12131 df-prm 12286 df-pc 12464

This theorem is referenced by: pccl 12478 pcdiv 12481 pcqmul 12482 pcqcl 12485 pcxnn0cl 12489 pcge0 12492 pcdvdsb 12499 pcdvdstr 12506 pcgcd1 12507 pc2dvds 12509 pcz 12511 pcaddlem 12518 pcadd 12519 qexpz 12531 lgsval 15255 lgsfcl2 15257 lgsdir 15286 lgsdilem2 15287 lgsdi 15288 lgsne0 15289

W3C validator