pclemub - Intuitionistic Logic Explorer

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

Theorem pclemub 12287

Description: Lemma for the prime power pre-function's properties. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Jim Kingdon, 7-Oct-2024.)

**Hypothesis**
Ref	Expression
pclem.1	⊢ 𝐴 = {𝑛 ∈ ℕ₀ ∣ (𝑃↑𝑛) ∥ 𝑁}

**Assertion**
Ref	Expression
pclemub	⊢ ((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)

Distinct variable groups: 𝑛,𝑁,𝑦 𝑥,𝑁,𝑦 𝑃,𝑛,𝑦 𝑥,𝑃 Allowed substitution hints: 𝐴(𝑥,𝑦,𝑛)

**Proof of Theorem pclemub**
Step	Hyp	Ref	Expression
1		nnssz 9270	. 2 ⊢ ℕ ⊆ ℤ
2		zcn 9258	. . . . . 6 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
3	2	abscld 11190	. . . . 5 ⊢ (𝑁 ∈ ℤ → (abs‘𝑁) ∈ ℝ)
4	3	ad2antrl 490	. . . 4 ⊢ ((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (abs‘𝑁) ∈ ℝ)
5		eluzelre 9538	. . . . 5 ⊢ (𝑃 ∈ (ℤ_≥‘2) → 𝑃 ∈ ℝ)
6	5	adantr 276	. . . 4 ⊢ ((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → 𝑃 ∈ ℝ)
7		eluz2gt1 9602	. . . . 5 ⊢ (𝑃 ∈ (ℤ_≥‘2) → 1 < 𝑃)
8	7	adantr 276	. . . 4 ⊢ ((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → 1 < 𝑃)
9		expnbnd 10644	. . . 4 ⊢ (((abs‘𝑁) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ 1 < 𝑃) → ∃𝑥 ∈ ℕ (abs‘𝑁) < (𝑃↑𝑥))
10	4, 6, 8, 9	syl3anc 1238	. . 3 ⊢ ((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ∃𝑥 ∈ ℕ (abs‘𝑁) < (𝑃↑𝑥))
11		simprr 531	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → 𝑦 ∈ 𝐴)
12		oveq2 5883	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑦 → (𝑃↑𝑛) = (𝑃↑𝑦))
13	12	breq1d 4014	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑦 → ((𝑃↑𝑛) ∥ 𝑁 ↔ (𝑃↑𝑦) ∥ 𝑁))
14		pclem.1	. . . . . . . . . . . . 13 ⊢ 𝐴 = {𝑛 ∈ ℕ₀ ∣ (𝑃↑𝑛) ∥ 𝑁}
15	13, 14	elrab2 2897	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝐴 ↔ (𝑦 ∈ ℕ₀ ∧ (𝑃↑𝑦) ∥ 𝑁))
16	11, 15	sylib 122	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → (𝑦 ∈ ℕ₀ ∧ (𝑃↑𝑦) ∥ 𝑁))
17	16	simprd 114	. . . . . . . . . 10 ⊢ (((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → (𝑃↑𝑦) ∥ 𝑁)
18		eluz2nn 9566	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ (ℤ_≥‘2) → 𝑃 ∈ ℕ)
19	18	ad2antrr 488	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → 𝑃 ∈ ℕ)
20	16	simpld 112	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → 𝑦 ∈ ℕ₀)
21	19, 20	nnexpcld 10676	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → (𝑃↑𝑦) ∈ ℕ)
22	21	nnzd 9374	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → (𝑃↑𝑦) ∈ ℤ)
23		simplrl 535	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → 𝑁 ∈ ℤ)
24		simplrr 536	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → 𝑁 ≠ 0)
25		dvdsleabs 11851	. . . . . . . . . . 11 ⊢ (((𝑃↑𝑦) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ((𝑃↑𝑦) ∥ 𝑁 → (𝑃↑𝑦) ≤ (abs‘𝑁)))
26	22, 23, 24, 25	syl3anc 1238	. . . . . . . . . 10 ⊢ (((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → ((𝑃↑𝑦) ∥ 𝑁 → (𝑃↑𝑦) ≤ (abs‘𝑁)))
27	17, 26	mpd 13	. . . . . . . . 9 ⊢ (((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → (𝑃↑𝑦) ≤ (abs‘𝑁))
28	21	nnred 8932	. . . . . . . . . 10 ⊢ (((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → (𝑃↑𝑦) ∈ ℝ)
29	4	adantr 276	. . . . . . . . . 10 ⊢ (((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → (abs‘𝑁) ∈ ℝ)
30	5	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → 𝑃 ∈ ℝ)
31		nnnn0 9183	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℕ → 𝑥 ∈ ℕ₀)
32	31	ad2antrl 490	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ ℕ₀)
33	30, 32	reexpcld 10671	. . . . . . . . . 10 ⊢ (((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → (𝑃↑𝑥) ∈ ℝ)
34		lelttr 8046	. . . . . . . . . 10 ⊢ (((𝑃↑𝑦) ∈ ℝ ∧ (abs‘𝑁) ∈ ℝ ∧ (𝑃↑𝑥) ∈ ℝ) → (((𝑃↑𝑦) ≤ (abs‘𝑁) ∧ (abs‘𝑁) < (𝑃↑𝑥)) → (𝑃↑𝑦) < (𝑃↑𝑥)))
35	28, 29, 33, 34	syl3anc 1238	. . . . . . . . 9 ⊢ (((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → (((𝑃↑𝑦) ≤ (abs‘𝑁) ∧ (abs‘𝑁) < (𝑃↑𝑥)) → (𝑃↑𝑦) < (𝑃↑𝑥)))
36	27, 35	mpand 429	. . . . . . . 8 ⊢ (((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → ((abs‘𝑁) < (𝑃↑𝑥) → (𝑃↑𝑦) < (𝑃↑𝑥)))
37	7	ad2antrr 488	. . . . . . . . 9 ⊢ (((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → 1 < 𝑃)
38		nn0ltexp2 10689	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℝ ∧ 𝑦 ∈ ℕ₀ ∧ 𝑥 ∈ ℕ₀) ∧ 1 < 𝑃) → (𝑦 < 𝑥 ↔ (𝑃↑𝑦) < (𝑃↑𝑥)))
39	30, 20, 32, 37, 38	syl31anc 1241	. . . . . . . 8 ⊢ (((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → (𝑦 < 𝑥 ↔ (𝑃↑𝑦) < (𝑃↑𝑥)))
40	36, 39	sylibrd 169	. . . . . . 7 ⊢ (((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → ((abs‘𝑁) < (𝑃↑𝑥) → 𝑦 < 𝑥))
41	20	nn0red 9230	. . . . . . . 8 ⊢ (((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → 𝑦 ∈ ℝ)
42		nnre 8926	. . . . . . . . 9 ⊢ (𝑥 ∈ ℕ → 𝑥 ∈ ℝ)
43	42	ad2antrl 490	. . . . . . . 8 ⊢ (((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ ℝ)
44		ltle 8045	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑦 < 𝑥 → 𝑦 ≤ 𝑥))
45	41, 43, 44	syl2anc 411	. . . . . . 7 ⊢ (((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → (𝑦 < 𝑥 → 𝑦 ≤ 𝑥))
46	40, 45	syld 45	. . . . . 6 ⊢ (((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → ((abs‘𝑁) < (𝑃↑𝑥) → 𝑦 ≤ 𝑥))
47	46	anassrs 400	. . . . 5 ⊢ ((((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ 𝐴) → ((abs‘𝑁) < (𝑃↑𝑥) → 𝑦 ≤ 𝑥))
48	47	ralrimdva 2557	. . . 4 ⊢ (((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) ∧ 𝑥 ∈ ℕ) → ((abs‘𝑁) < (𝑃↑𝑥) → ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥))
49	48	reximdva 2579	. . 3 ⊢ ((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (∃𝑥 ∈ ℕ (abs‘𝑁) < (𝑃↑𝑥) → ∃𝑥 ∈ ℕ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥))
50	10, 49	mpd 13	. 2 ⊢ ((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ∃𝑥 ∈ ℕ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)
51		ssrexv 3221	. 2 ⊢ (ℕ ⊆ ℤ → (∃𝑥 ∈ ℕ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥))
52	1, 50, 51	mpsyl 65	1 ⊢ ((𝑃 ∈ (ℤ_≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 = wceq 1353 ∈ wcel 2148 ≠ wne 2347 ∀wral 2455 ∃wrex 2456 {crab 2459 ⊆ wss 3130 class class class wbr 4004 ‘cfv 5217 (class class class)co 5875 ℝcr 7810 0cc0 7811 1c1 7812 < clt 7992 ≤ cle 7993 ℕcn 8919 2c2 8970 ℕ₀cn0 9176 ℤcz 9253 ℤ_≥cuz 9528 ↑cexp 10519 abscabs 11006 ∥ cdvds 11794

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-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-riota 5831 df-ov 5878 df-oprab 5879 df-mpo 5880 df-1st 6141 df-2nd 6142 df-recs 6306 df-frec 6392 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-z 9254 df-uz 9529 df-q 9620 df-rp 9654 df-seqfrec 10446 df-exp 10520 df-cj 10851 df-re 10852 df-im 10853 df-rsqrt 11007 df-abs 11008 df-dvds 11795

This theorem is referenced by: pcprecl 12289 pcprendvds 12290 pcpremul 12293

W3C validator