prmpwdvds - Metamath Proof Explorer

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

Theorem prmpwdvds 16234

Description: A relation involving divisibility by a prime power. (Contributed by Mario Carneiro, 2-Mar-2014.)

**Assertion**
Ref	Expression
prmpwdvds	⊢ (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) ∧ (𝐷 ∥ (𝐾 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1))))) → (𝑃↑𝑁) ∥ 𝐷)

Proof of Theorem prmpwdvds Dummy variables 𝑘 𝑛 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq1 7157	. . . . . 6 ⊢ (𝑘 = 𝐾 → (𝑘 · (𝑃↑𝑁)) = (𝐾 · (𝑃↑𝑁)))
2	1	breq2d 5071	. . . . 5 ⊢ (𝑘 = 𝐾 → (𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ↔ 𝐷 ∥ (𝐾 · (𝑃↑𝑁))))
3		oveq1 7157	. . . . . . 7 ⊢ (𝑘 = 𝐾 → (𝑘 · (𝑃↑(𝑁 − 1))) = (𝐾 · (𝑃↑(𝑁 − 1))))
4	3	breq2d 5071	. . . . . 6 ⊢ (𝑘 = 𝐾 → (𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1))) ↔ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1)))))
5	4	notbid 320	. . . . 5 ⊢ (𝑘 = 𝐾 → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1))) ↔ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1)))))
6	2, 5	anbi12d 632	. . . 4 ⊢ (𝑘 = 𝐾 → ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) ↔ (𝐷 ∥ (𝐾 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1))))))
7	6	imbi1d 344	. . 3 ⊢ (𝑘 = 𝐾 → (((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷) ↔ ((𝐷 ∥ (𝐾 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷)))
8		oveq2 7158	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (𝑃↑𝑥) = (𝑃↑1))
9	8	oveq2d 7166	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → (𝑘 · (𝑃↑𝑥)) = (𝑘 · (𝑃↑1)))
10	9	breq2d 5071	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑1))))
11		oveq1 7157	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 1 → (𝑥 − 1) = (1 − 1))
12	11	oveq2d 7166	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 1 → (𝑃↑(𝑥 − 1)) = (𝑃↑(1 − 1)))
13	12	oveq2d 7166	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (𝑘 · (𝑃↑(𝑥 − 1))) = (𝑘 · (𝑃↑(1 − 1))))
14	13	breq2d 5071	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → (𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))))
15	14	notbid 320	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))))
16	10, 15	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑥 = 1 → ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1))))))
17	8	breq1d 5069	. . . . . . . . . 10 ⊢ (𝑥 = 1 → ((𝑃↑𝑥) ∥ 𝐷 ↔ (𝑃↑1) ∥ 𝐷))
18	16, 17	imbi12d 347	. . . . . . . . 9 ⊢ (𝑥 = 1 → (((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) → (𝑃↑1) ∥ 𝐷)))
19	18	ralbidv 3197	. . . . . . . 8 ⊢ (𝑥 = 1 → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) → (𝑃↑1) ∥ 𝐷)))
20	19	imbi2d 343	. . . . . . 7 ⊢ (𝑥 = 1 → (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷)) ↔ ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) → (𝑃↑1) ∥ 𝐷))))
21		oveq2 7158	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑛 → (𝑃↑𝑥) = (𝑃↑𝑛))
22	21	oveq2d 7166	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑛 → (𝑘 · (𝑃↑𝑥)) = (𝑘 · (𝑃↑𝑛)))
23	22	breq2d 5071	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑛 → (𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
24		oveq1 7157	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑛 → (𝑥 − 1) = (𝑛 − 1))
25	24	oveq2d 7166	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑛 → (𝑃↑(𝑥 − 1)) = (𝑃↑(𝑛 − 1)))
26	25	oveq2d 7166	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑛 → (𝑘 · (𝑃↑(𝑥 − 1))) = (𝑘 · (𝑃↑(𝑛 − 1))))
27	26	breq2d 5071	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑛 → (𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))))
28	27	notbid 320	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑛 → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))))
29	23, 28	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑥 = 𝑛 → ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1))))))
30	21	breq1d 5069	. . . . . . . . . 10 ⊢ (𝑥 = 𝑛 → ((𝑃↑𝑥) ∥ 𝐷 ↔ (𝑃↑𝑛) ∥ 𝐷))
31	29, 30	imbi12d 347	. . . . . . . . 9 ⊢ (𝑥 = 𝑛 → (((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)))
32	31	ralbidv 3197	. . . . . . . 8 ⊢ (𝑥 = 𝑛 → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)))
33	32	imbi2d 343	. . . . . . 7 ⊢ (𝑥 = 𝑛 → (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷)) ↔ ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷))))
34		oveq2 7158	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑛 + 1) → (𝑃↑𝑥) = (𝑃↑(𝑛 + 1)))
35	34	oveq2d 7166	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑛 + 1) → (𝑘 · (𝑃↑𝑥)) = (𝑘 · (𝑃↑(𝑛 + 1))))
36	35	breq2d 5071	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑛 + 1) → (𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1)))))
37		oveq1 7157	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑛 + 1) → (𝑥 − 1) = ((𝑛 + 1) − 1))
38	37	oveq2d 7166	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑛 + 1) → (𝑃↑(𝑥 − 1)) = (𝑃↑((𝑛 + 1) − 1)))
39	38	oveq2d 7166	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑛 + 1) → (𝑘 · (𝑃↑(𝑥 − 1))) = (𝑘 · (𝑃↑((𝑛 + 1) − 1))))
40	39	breq2d 5071	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑛 + 1) → (𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))))
41	40	notbid 320	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑛 + 1) → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))))
42	36, 41	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑥 = (𝑛 + 1) → ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1))))))
43	34	breq1d 5069	. . . . . . . . . 10 ⊢ (𝑥 = (𝑛 + 1) → ((𝑃↑𝑥) ∥ 𝐷 ↔ (𝑃↑(𝑛 + 1)) ∥ 𝐷))
44	42, 43	imbi12d 347	. . . . . . . . 9 ⊢ (𝑥 = (𝑛 + 1) → (((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
45	44	ralbidv 3197	. . . . . . . 8 ⊢ (𝑥 = (𝑛 + 1) → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
46	45	imbi2d 343	. . . . . . 7 ⊢ (𝑥 = (𝑛 + 1) → (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷)) ↔ ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷))))
47		oveq2 7158	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑁 → (𝑃↑𝑥) = (𝑃↑𝑁))
48	47	oveq2d 7166	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑁 → (𝑘 · (𝑃↑𝑥)) = (𝑘 · (𝑃↑𝑁)))
49	48	breq2d 5071	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑁 → (𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑𝑁))))
50		oveq1 7157	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑁 → (𝑥 − 1) = (𝑁 − 1))
51	50	oveq2d 7166	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑁 → (𝑃↑(𝑥 − 1)) = (𝑃↑(𝑁 − 1)))
52	51	oveq2d 7166	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑁 → (𝑘 · (𝑃↑(𝑥 − 1))) = (𝑘 · (𝑃↑(𝑁 − 1))))
53	52	breq2d 5071	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑁 → (𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))))
54	53	notbid 320	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑁 → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))))
55	49, 54	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑥 = 𝑁 → ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1))))))
56	47	breq1d 5069	. . . . . . . . . 10 ⊢ (𝑥 = 𝑁 → ((𝑃↑𝑥) ∥ 𝐷 ↔ (𝑃↑𝑁) ∥ 𝐷))
57	55, 56	imbi12d 347	. . . . . . . . 9 ⊢ (𝑥 = 𝑁 → (((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷)))
58	57	ralbidv 3197	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷)))
59	58	imbi2d 343	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷)) ↔ ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷))))
60		breq1 5062	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐷 → (𝑥 ∥ (𝑘 · 𝑃) ↔ 𝐷 ∥ (𝑘 · 𝑃)))
61		breq1 5062	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝐷 → (𝑥 ∥ 𝑘 ↔ 𝐷 ∥ 𝑘))
62	61	notbid 320	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐷 → (¬ 𝑥 ∥ 𝑘 ↔ ¬ 𝐷 ∥ 𝑘))
63	60, 62	anbi12d 632	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐷 → ((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘) ↔ (𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘)))
64		breq2 5063	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐷 → (𝑃 ∥ 𝑥 ↔ 𝑃 ∥ 𝐷))
65	63, 64	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐷 → (((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘) → 𝑃 ∥ 𝑥) ↔ ((𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘) → 𝑃 ∥ 𝐷)))
66	65	imbi2d 343	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐷 → (((𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘) → 𝑃 ∥ 𝑥)) ↔ ((𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘) → 𝑃 ∥ 𝐷))))
67		simplrl 775	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → 𝑃 ∈ ℙ)
68		simpll 765	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → 𝑥 ∈ ℤ)
69		coprm 16049	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ) → (¬ 𝑃 ∥ 𝑥 ↔ (𝑃 gcd 𝑥) = 1))
70	67, 68, 69	syl2anc 586	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → (¬ 𝑃 ∥ 𝑥 ↔ (𝑃 gcd 𝑥) = 1))
71		zcn 11980	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℂ)
72	71	ad2antll 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℂ)
73		prmz 16013	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
74	73	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℤ)
75	74	zcnd 12082	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℂ)
76	72, 75	mulcomd 10656	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · 𝑃) = (𝑃 · 𝑘))
77	76	breq2d 5071	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑥 ∥ (𝑘 · 𝑃) ↔ 𝑥 ∥ (𝑃 · 𝑘)))
78		simpl 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑥 ∈ ℤ)
79		gcdcom 15856	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (𝑃 gcd 𝑥) = (𝑥 gcd 𝑃))
80	74, 78, 79	syl2anc 586	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 gcd 𝑥) = (𝑥 gcd 𝑃))
81	80	eqeq1d 2823	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃 gcd 𝑥) = 1 ↔ (𝑥 gcd 𝑃) = 1))
82	77, 81	anbi12d 632	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ (𝑃 gcd 𝑥) = 1) ↔ (𝑥 ∥ (𝑃 · 𝑘) ∧ (𝑥 gcd 𝑃) = 1)))
83		simprr 771	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℤ)
84		coprmdvds 15991	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑥 ∥ (𝑃 · 𝑘) ∧ (𝑥 gcd 𝑃) = 1) → 𝑥 ∥ 𝑘))
85	78, 74, 83, 84	syl3anc 1367	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 ∥ (𝑃 · 𝑘) ∧ (𝑥 gcd 𝑃) = 1) → 𝑥 ∥ 𝑘))
86	82, 85	sylbid 242	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ (𝑃 gcd 𝑥) = 1) → 𝑥 ∥ 𝑘))
87	86	expdimp 455	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → ((𝑃 gcd 𝑥) = 1 → 𝑥 ∥ 𝑘))
88	70, 87	sylbid 242	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → (¬ 𝑃 ∥ 𝑥 → 𝑥 ∥ 𝑘))
89	88	con1d 147	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → (¬ 𝑥 ∥ 𝑘 → 𝑃 ∥ 𝑥))
90	89	expimpd 456	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘) → 𝑃 ∥ 𝑥))
91	90	ex 415	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℤ → ((𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘) → 𝑃 ∥ 𝑥)))
92	66, 91	vtoclga 3574	. . . . . . . . . 10 ⊢ (𝐷 ∈ ℤ → ((𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘) → 𝑃 ∥ 𝐷)))
93	92	impl 458	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘) → 𝑃 ∥ 𝐷))
94	73	zcnd 12082	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℂ)
95	94	exp1d 13499	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ ℙ → (𝑃↑1) = 𝑃)
96	95	ad2antlr 725	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑃↑1) = 𝑃)
97	96	oveq2d 7166	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑘 · (𝑃↑1)) = (𝑘 · 𝑃))
98	97	breq2d 5071	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝐷 ∥ (𝑘 · (𝑃↑1)) ↔ 𝐷 ∥ (𝑘 · 𝑃)))
99		1m1e0 11703	. . . . . . . . . . . . . . . 16 ⊢ (1 − 1) = 0
100	99	oveq2i 7161	. . . . . . . . . . . . . . 15 ⊢ (𝑃↑(1 − 1)) = (𝑃↑0)
101	73	ad2antlr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → 𝑃 ∈ ℤ)
102	101	zcnd 12082	. . . . . . . . . . . . . . . 16 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → 𝑃 ∈ ℂ)
103	102	exp0d 13498	. . . . . . . . . . . . . . 15 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑃↑0) = 1)
104	100, 103	syl5eq 2868	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑃↑(1 − 1)) = 1)
105	104	oveq2d 7166	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑘 · (𝑃↑(1 − 1))) = (𝑘 · 1))
106	71	adantl 484	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℂ)
107	106	mulid1d 10652	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑘 · 1) = 𝑘)
108	105, 107	eqtrd 2856	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑘 · (𝑃↑(1 − 1))) = 𝑘)
109	108	breq2d 5071	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝐷 ∥ (𝑘 · (𝑃↑(1 − 1))) ↔ 𝐷 ∥ 𝑘))
110	109	notbid 320	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1))) ↔ ¬ 𝐷 ∥ 𝑘))
111	98, 110	anbi12d 632	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) ↔ (𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘)))
112	102	exp1d 13499	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑃↑1) = 𝑃)
113	112	breq1d 5069	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → ((𝑃↑1) ∥ 𝐷 ↔ 𝑃 ∥ 𝐷))
114	93, 111, 113	3imtr4d 296	. . . . . . . 8 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) → (𝑃↑1) ∥ 𝐷))
115	114	ralrimiva 3182	. . . . . . 7 ⊢ ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) → (𝑃↑1) ∥ 𝐷))
116		oveq1 7157	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝑘 · (𝑃↑𝑛)) = (𝑥 · (𝑃↑𝑛)))
117	116	breq2d 5071	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑥 → (𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ↔ 𝐷 ∥ (𝑥 · (𝑃↑𝑛))))
118		oveq1 7157	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑥 → (𝑘 · (𝑃↑(𝑛 − 1))) = (𝑥 · (𝑃↑(𝑛 − 1))))
119	118	breq2d 5071	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1))) ↔ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))))
120	119	notbid 320	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑥 → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1))) ↔ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))))
121	117, 120	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑥 → ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) ↔ (𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1))))))
122	121	imbi1d 344	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑥 → (((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)))
123	122	cbvralvw 3450	. . . . . . . . . 10 ⊢ (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) ↔ ∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷))
124		simprr 771	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℤ)
125	73	ad2antrl 726	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℤ)
126	124, 125	zmulcld 12087	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · 𝑃) ∈ ℤ)
127		oveq1 7157	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑘 · 𝑃) → (𝑥 · (𝑃↑𝑛)) = ((𝑘 · 𝑃) · (𝑃↑𝑛)))
128	127	breq2d 5071	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝑘 · 𝑃) → (𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ↔ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛))))
129		oveq1 7157	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑘 · 𝑃) → (𝑥 · (𝑃↑(𝑛 − 1))) = ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))))
130	129	breq2d 5071	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑘 · 𝑃) → (𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1))) ↔ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))))
131	130	notbid 320	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝑘 · 𝑃) → (¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1))) ↔ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))))
132	128, 131	anbi12d 632	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑘 · 𝑃) → ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) ↔ (𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))))))
133	132	imbi1d 344	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑘 · 𝑃) → (((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) ↔ ((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)))
134	133	rspcv 3618	. . . . . . . . . . . . . 14 ⊢ ((𝑘 · 𝑃) ∈ ℤ → (∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)))
135	126, 134	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)))
136		nnnn0 11898	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀)
137	136	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑛 ∈ ℕ₀)
138		zexpcl 13438	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ ℤ ∧ 𝑛 ∈ ℕ₀) → (𝑃↑𝑛) ∈ ℤ)
139	125, 137, 138	syl2anc 586	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ∈ ℤ)
140		simplr 767	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝐷 ∈ ℤ)
141		divides 15603	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃↑𝑛) ∈ ℤ ∧ 𝐷 ∈ ℤ) → ((𝑃↑𝑛) ∥ 𝐷 ↔ ∃𝑥 ∈ ℤ (𝑥 · (𝑃↑𝑛)) = 𝐷))
142	139, 140, 141	syl2anc 586	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃↑𝑛) ∥ 𝐷 ↔ ∃𝑥 ∈ ℤ (𝑥 · (𝑃↑𝑛)) = 𝐷))
143	90	adantll 712	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘) → 𝑃 ∥ 𝑥))
144		prmnn 16012	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
145	144	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℕ)
146	145	nncnd 11648	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℂ)
147	136	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑛 ∈ ℕ₀)
148	146, 147	expp1d 13505	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 + 1)) = ((𝑃↑𝑛) · 𝑃))
149	145, 147	nnexpcld 13600	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ∈ ℕ)
150	149	nncnd 11648	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ∈ ℂ)
151	150, 146	mulcomd 10656	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃↑𝑛) · 𝑃) = (𝑃 · (𝑃↑𝑛)))
152	148, 151	eqtrd 2856	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 + 1)) = (𝑃 · (𝑃↑𝑛)))
153	152	oveq2d 7166	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃↑(𝑛 + 1))) = (𝑘 · (𝑃 · (𝑃↑𝑛))))
154	71	ad2antll 727	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℂ)
155	154, 146, 150	mulassd 10658	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃↑𝑛)) = (𝑘 · (𝑃 · (𝑃↑𝑛))))
156	153, 155	eqtr4d 2859	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃↑(𝑛 + 1))) = ((𝑘 · 𝑃) · (𝑃↑𝑛)))
157	156	breq2d 5071	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ↔ (𝑥 · (𝑃↑𝑛)) ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛))))
158		simplr 767	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑥 ∈ ℤ)
159		simprr 771	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℤ)
160	145	nnzd 12080	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℤ)
161	159, 160	zmulcld 12087	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · 𝑃) ∈ ℤ)
162	149	nnzd 12080	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ∈ ℤ)
163	149	nnne0d 11681	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ≠ 0)
164		dvdsmulcr 15633	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ ℤ ∧ (𝑘 · 𝑃) ∈ ℤ ∧ ((𝑃↑𝑛) ∈ ℤ ∧ (𝑃↑𝑛) ≠ 0)) → ((𝑥 · (𝑃↑𝑛)) ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ↔ 𝑥 ∥ (𝑘 · 𝑃)))
165	158, 161, 162, 163, 164	syl112anc 1370	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 · (𝑃↑𝑛)) ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ↔ 𝑥 ∥ (𝑘 · 𝑃)))
166	157, 165	bitrd 281	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ↔ 𝑥 ∥ (𝑘 · 𝑃)))
167		dvdsmulcr 15633	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ ((𝑃↑𝑛) ∈ ℤ ∧ (𝑃↑𝑛) ≠ 0)) → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛)) ↔ 𝑥 ∥ 𝑘))
168	158, 159, 162, 163, 167	syl112anc 1370	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛)) ↔ 𝑥 ∥ 𝑘))
169	168	notbid 320	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛)) ↔ ¬ 𝑥 ∥ 𝑘))
170	166, 169	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛))) ↔ (𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘)))
171	152	breq1d 5069	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃↑𝑛)) ↔ (𝑃 · (𝑃↑𝑛)) ∥ (𝑥 · (𝑃↑𝑛))))
172		dvdsmulcr 15633	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑃 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ ((𝑃↑𝑛) ∈ ℤ ∧ (𝑃↑𝑛) ≠ 0)) → ((𝑃 · (𝑃↑𝑛)) ∥ (𝑥 · (𝑃↑𝑛)) ↔ 𝑃 ∥ 𝑥))
173	160, 158, 162, 163, 172	syl112anc 1370	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃 · (𝑃↑𝑛)) ∥ (𝑥 · (𝑃↑𝑛)) ↔ 𝑃 ∥ 𝑥))
174	171, 173	bitrd 281	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃↑𝑛)) ↔ 𝑃 ∥ 𝑥))
175	143, 170, 174	3imtr4d 296	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃↑𝑛))))
176	175	an32s 650	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∈ ℤ) → (((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃↑𝑛))))
177		breq1 5062	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 · (𝑃↑𝑛)) = 𝐷 → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1)))))
178		breq1 5062	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 · (𝑃↑𝑛)) = 𝐷 → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
179	178	notbid 320	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 · (𝑃↑𝑛)) = 𝐷 → (¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛)) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
180	177, 179	anbi12d 632	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 · (𝑃↑𝑛)) = 𝐷 → (((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛)))))
181		breq2 5063	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 · (𝑃↑𝑛)) = 𝐷 → ((𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃↑𝑛)) ↔ (𝑃↑(𝑛 + 1)) ∥ 𝐷))
182	180, 181	imbi12d 347	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 · (𝑃↑𝑛)) = 𝐷 → ((((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃↑𝑛))) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
183	176, 182	syl5ibcom 247	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∈ ℤ) → ((𝑥 · (𝑃↑𝑛)) = 𝐷 → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
184	183	rexlimdva 3284	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℕ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (∃𝑥 ∈ ℤ (𝑥 · (𝑃↑𝑛)) = 𝐷 → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
185	184	adantlr 713	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (∃𝑥 ∈ ℤ (𝑥 · (𝑃↑𝑛)) = 𝐷 → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
186	142, 185	sylbid 242	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃↑𝑛) ∥ 𝐷 → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
187	186	com23 86	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → ((𝑃↑𝑛) ∥ 𝐷 → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
188	187	a2d 29	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑𝑛) ∥ 𝐷) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
189	71	ad2antll 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℂ)
190	125	zcnd 12082	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℂ)
191	139	zcnd 12082	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ∈ ℂ)
192	189, 190, 191	mulassd 10658	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃↑𝑛)) = (𝑘 · (𝑃 · (𝑃↑𝑛))))
193	190, 191	mulcomd 10656	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 · (𝑃↑𝑛)) = ((𝑃↑𝑛) · 𝑃))
194	190, 137	expp1d 13505	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 + 1)) = ((𝑃↑𝑛) · 𝑃))
195	193, 194	eqtr4d 2859	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 · (𝑃↑𝑛)) = (𝑃↑(𝑛 + 1)))
196	195	oveq2d 7166	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃 · (𝑃↑𝑛))) = (𝑘 · (𝑃↑(𝑛 + 1))))
197	192, 196	eqtrd 2856	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃↑𝑛)) = (𝑘 · (𝑃↑(𝑛 + 1))))
198	197	breq2d 5071	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1)))))
199		nnm1nn0 11932	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ₀)
200	199	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑛 − 1) ∈ ℕ₀)
201		zexpcl 13438	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃 ∈ ℤ ∧ (𝑛 − 1) ∈ ℕ₀) → (𝑃↑(𝑛 − 1)) ∈ ℤ)
202	125, 200, 201	syl2anc 586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 − 1)) ∈ ℤ)
203	202	zcnd 12082	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 − 1)) ∈ ℂ)
204	189, 190, 203	mulassd 10658	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))) = (𝑘 · (𝑃 · (𝑃↑(𝑛 − 1)))))
205	190, 203	mulcomd 10656	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 · (𝑃↑(𝑛 − 1))) = ((𝑃↑(𝑛 − 1)) · 𝑃))
206		simpll 765	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑛 ∈ ℕ)
207		expm1t 13451	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃 ∈ ℂ ∧ 𝑛 ∈ ℕ) → (𝑃↑𝑛) = ((𝑃↑(𝑛 − 1)) · 𝑃))
208	190, 206, 207	syl2anc 586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) = ((𝑃↑(𝑛 − 1)) · 𝑃))
209	205, 208	eqtr4d 2859	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 · (𝑃↑(𝑛 − 1))) = (𝑃↑𝑛))
210	209	oveq2d 7166	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃 · (𝑃↑(𝑛 − 1)))) = (𝑘 · (𝑃↑𝑛)))
211	204, 210	eqtrd 2856	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))) = (𝑘 · (𝑃↑𝑛)))
212	211	breq2d 5071	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
213	212	notbid 320	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
214	198, 213	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛)))))
215	214	imbi1d 344	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑𝑛) ∥ 𝐷)))
216		nncn 11640	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
217	216	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑛 ∈ ℂ)
218		ax-1cn 10589	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ ℂ
219		pncan 10886	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 1) = 𝑛)
220	217, 218, 219	sylancl 588	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑛 + 1) − 1) = 𝑛)
221	220	oveq2d 7166	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑((𝑛 + 1) − 1)) = (𝑃↑𝑛))
222	221	oveq2d 7166	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃↑((𝑛 + 1) − 1))) = (𝑘 · (𝑃↑𝑛)))
223	222	breq2d 5071	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
224	223	notbid 320	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
225	224	anbi2d 630	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛)))))
226	225	imbi1d 344	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
227	188, 215, 226	3imtr4d 296	. . . . . . . . . . . . 13 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
228	135, 227	syld 47	. . . . . . . . . . . 12 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
229	228	anassrs 470	. . . . . . . . . . 11 ⊢ ((((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
230	229	ralrimdva 3189	. . . . . . . . . 10 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ 𝑃 ∈ ℙ) → (∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
231	123, 230	syl5bi 244	. . . . . . . . 9 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ 𝑃 ∈ ℙ) → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
232	231	expl 460	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷))))
233	232	a2d 29	. . . . . . 7 ⊢ (𝑛 ∈ ℕ → (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)) → ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷))))
234	20, 33, 46, 59, 115, 233	nnind 11650	. . . . . 6 ⊢ (𝑁 ∈ ℕ → ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷)))
235	234	com12 32	. . . . 5 ⊢ ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → (𝑁 ∈ ℕ → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷)))
236	235	impr 457	. . . 4 ⊢ ((𝐷 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ)) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷))
237	236	adantll 712	. . 3 ⊢ (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ)) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷))
238		simpll 765	. . 3 ⊢ (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ)) → 𝐾 ∈ ℤ)
239	7, 237, 238	rspcdva 3625	. 2 ⊢ (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ)) → ((𝐷 ∥ (𝐾 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷))
240	239	3impia 1113	1 ⊢ (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) ∧ (𝐷 ∥ (𝐾 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1))))) → (𝑃↑𝑁) ∥ 𝐷)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1533 ∈ wcel 2110 ≠ wne 3016 ∀wral 3138 ∃wrex 3139 class class class wbr 5059 (class class class)co 7150 ℂcc 10529 0cc0 10531 1c1 10532 + caddc 10534 · cmul 10536 − cmin 10864 ℕcn 11632 ℕ₀cn0 11891 ℤcz 11975 ↑cexp 13423 ∥ cdvds 15601 gcd cgcd 15837 ℙcprime 16009

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 ax-sep 5196 ax-nul 5203 ax-pow 5259 ax-pr 5322 ax-un 7455 ax-cnex 10587 ax-resscn 10588 ax-1cn 10589 ax-icn 10590 ax-addcl 10591 ax-addrcl 10592 ax-mulcl 10593 ax-mulrcl 10594 ax-mulcom 10595 ax-addass 10596 ax-mulass 10597 ax-distr 10598 ax-i2m1 10599 ax-1ne0 10600 ax-1rid 10601 ax-rnegex 10602 ax-rrecex 10603 ax-cnre 10604 ax-pre-lttri 10605 ax-pre-lttrn 10606 ax-pre-ltadd 10607 ax-pre-mulgt0 10608 ax-pre-sup 10609

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3497 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4562 df-pr 4564 df-tp 4566 df-op 4568 df-uni 4833 df-iun 4914 df-br 5060 df-opab 5122 df-mpt 5140 df-tr 5166 df-id 5455 df-eprel 5460 df-po 5469 df-so 5470 df-fr 5509 df-we 5511 df-xp 5556 df-rel 5557 df-cnv 5558 df-co 5559 df-dm 5560 df-rn 5561 df-res 5562 df-ima 5563 df-pred 6143 df-ord 6189 df-on 6190 df-lim 6191 df-suc 6192 df-iota 6309 df-fun 6352 df-fn 6353 df-f 6354 df-f1 6355 df-fo 6356 df-f1o 6357 df-fv 6358 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-om 7575 df-2nd 7684 df-wrecs 7941 df-recs 8002 df-rdg 8040 df-1o 8096 df-2o 8097 df-er 8283 df-en 8504 df-dom 8505 df-sdom 8506 df-fin 8507 df-sup 8900 df-inf 8901 df-pnf 10671 df-mnf 10672 df-xr 10673 df-ltxr 10674 df-le 10675 df-sub 10866 df-neg 10867 df-div 11292 df-nn 11633 df-2 11694 df-3 11695 df-n0 11892 df-z 11976 df-uz 12238 df-rp 12384 df-fl 13156 df-mod 13232 df-seq 13364 df-exp 13424 df-cj 14452 df-re 14453 df-im 14454 df-sqrt 14588 df-abs 14589 df-dvds 15602 df-gcd 15838 df-prm 16010

This theorem is referenced by: pockthlem 16235

W3C validator