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 16965

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 7419	. . . . . 6 ⊢ (𝑘 = 𝐾 → (𝑘 · (𝑃↑𝑁)) = (𝐾 · (𝑃↑𝑁)))
2	1	breq2d 5122	. . . . 5 ⊢ (𝑘 = 𝐾 → (𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ↔ 𝐷 ∥ (𝐾 · (𝑃↑𝑁))))
3		oveq1 7419	. . . . . . 7 ⊢ (𝑘 = 𝐾 → (𝑘 · (𝑃↑(𝑁 − 1))) = (𝐾 · (𝑃↑(𝑁 − 1))))
4	3	breq2d 5122	. . . . . 6 ⊢ (𝑘 = 𝐾 → (𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1))) ↔ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1)))))
5	4	notbid 321	. . . . 5 ⊢ (𝑘 = 𝐾 → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1))) ↔ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1)))))
6	2, 5	anbi12d 643	. . . 4 ⊢ (𝑘 = 𝐾 → ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) ↔ (𝐷 ∥ (𝐾 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1))))))
7	6	imbi1d 344	. . 3 ⊢ (𝑘 = 𝐾 → (((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷) ↔ ((𝐷 ∥ (𝐾 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷)))
8		oveq2 7420	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (𝑃↑𝑥) = (𝑃↑1))
9	8	oveq2d 7428	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → (𝑘 · (𝑃↑𝑥)) = (𝑘 · (𝑃↑1)))
10	9	breq2d 5122	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑1))))
11		oveq1 7419	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 1 → (𝑥 − 1) = (1 − 1))
12	11	oveq2d 7428	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 1 → (𝑃↑(𝑥 − 1)) = (𝑃↑(1 − 1)))
13	12	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (𝑘 · (𝑃↑(𝑥 − 1))) = (𝑘 · (𝑃↑(1 − 1))))
14	13	breq2d 5122	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → (𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))))
15	14	notbid 321	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))))
16	10, 15	anbi12d 643	. . . . . . . . . 10 ⊢ (𝑥 = 1 → ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1))))))
17	8	breq1d 5120	. . . . . . . . . 10 ⊢ (𝑥 = 1 → ((𝑃↑𝑥) ∥ 𝐷 ↔ (𝑃↑1) ∥ 𝐷))
18	16, 17	imbi12d 347	. . . . . . . . 9 ⊢ (𝑥 = 1 → (((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) → (𝑃↑1) ∥ 𝐷)))
19	18	ralbidv 3188	. . . . . . . 8 ⊢ (𝑥 = 1 → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) → (𝑃↑1) ∥ 𝐷)))
20	19	imbi2d 343	. . . . . . 7 ⊢ (𝑥 = 1 → (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷)) ↔ ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) → (𝑃↑1) ∥ 𝐷))))
21		oveq2 7420	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑛 → (𝑃↑𝑥) = (𝑃↑𝑛))
22	21	oveq2d 7428	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑛 → (𝑘 · (𝑃↑𝑥)) = (𝑘 · (𝑃↑𝑛)))
23	22	breq2d 5122	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑛 → (𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
24		oveq1 7419	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑛 → (𝑥 − 1) = (𝑛 − 1))
25	24	oveq2d 7428	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑛 → (𝑃↑(𝑥 − 1)) = (𝑃↑(𝑛 − 1)))
26	25	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑛 → (𝑘 · (𝑃↑(𝑥 − 1))) = (𝑘 · (𝑃↑(𝑛 − 1))))
27	26	breq2d 5122	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑛 → (𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))))
28	27	notbid 321	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑛 → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))))
29	23, 28	anbi12d 643	. . . . . . . . . 10 ⊢ (𝑥 = 𝑛 → ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1))))))
30	21	breq1d 5120	. . . . . . . . . 10 ⊢ (𝑥 = 𝑛 → ((𝑃↑𝑥) ∥ 𝐷 ↔ (𝑃↑𝑛) ∥ 𝐷))
31	29, 30	imbi12d 347	. . . . . . . . 9 ⊢ (𝑥 = 𝑛 → (((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)))
32	31	ralbidv 3188	. . . . . . . 8 ⊢ (𝑥 = 𝑛 → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)))
33	32	imbi2d 343	. . . . . . 7 ⊢ (𝑥 = 𝑛 → (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷)) ↔ ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷))))
34		oveq2 7420	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑛 + 1) → (𝑃↑𝑥) = (𝑃↑(𝑛 + 1)))
35	34	oveq2d 7428	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑛 + 1) → (𝑘 · (𝑃↑𝑥)) = (𝑘 · (𝑃↑(𝑛 + 1))))
36	35	breq2d 5122	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑛 + 1) → (𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1)))))
37		oveq1 7419	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑛 + 1) → (𝑥 − 1) = ((𝑛 + 1) − 1))
38	37	oveq2d 7428	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑛 + 1) → (𝑃↑(𝑥 − 1)) = (𝑃↑((𝑛 + 1) − 1)))
39	38	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑛 + 1) → (𝑘 · (𝑃↑(𝑥 − 1))) = (𝑘 · (𝑃↑((𝑛 + 1) − 1))))
40	39	breq2d 5122	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑛 + 1) → (𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))))
41	40	notbid 321	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑛 + 1) → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))))
42	36, 41	anbi12d 643	. . . . . . . . . 10 ⊢ (𝑥 = (𝑛 + 1) → ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1))))))
43	34	breq1d 5120	. . . . . . . . . 10 ⊢ (𝑥 = (𝑛 + 1) → ((𝑃↑𝑥) ∥ 𝐷 ↔ (𝑃↑(𝑛 + 1)) ∥ 𝐷))
44	42, 43	imbi12d 347	. . . . . . . . 9 ⊢ (𝑥 = (𝑛 + 1) → (((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
45	44	ralbidv 3188	. . . . . . . 8 ⊢ (𝑥 = (𝑛 + 1) → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
46	45	imbi2d 343	. . . . . . 7 ⊢ (𝑥 = (𝑛 + 1) → (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷)) ↔ ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷))))
47		oveq2 7420	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑁 → (𝑃↑𝑥) = (𝑃↑𝑁))
48	47	oveq2d 7428	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑁 → (𝑘 · (𝑃↑𝑥)) = (𝑘 · (𝑃↑𝑁)))
49	48	breq2d 5122	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑁 → (𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑𝑁))))
50		oveq1 7419	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑁 → (𝑥 − 1) = (𝑁 − 1))
51	50	oveq2d 7428	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑁 → (𝑃↑(𝑥 − 1)) = (𝑃↑(𝑁 − 1)))
52	51	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑁 → (𝑘 · (𝑃↑(𝑥 − 1))) = (𝑘 · (𝑃↑(𝑁 − 1))))
53	52	breq2d 5122	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑁 → (𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))))
54	53	notbid 321	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑁 → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))))
55	49, 54	anbi12d 643	. . . . . . . . . 10 ⊢ (𝑥 = 𝑁 → ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1))))))
56	47	breq1d 5120	. . . . . . . . . 10 ⊢ (𝑥 = 𝑁 → ((𝑃↑𝑥) ∥ 𝐷 ↔ (𝑃↑𝑁) ∥ 𝐷))
57	55, 56	imbi12d 347	. . . . . . . . 9 ⊢ (𝑥 = 𝑁 → (((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷)))
58	57	ralbidv 3188	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷)))
59	58	imbi2d 343	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷)) ↔ ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷))))
60		breq1 5113	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐷 → (𝑥 ∥ (𝑘 · 𝑃) ↔ 𝐷 ∥ (𝑘 · 𝑃)))
61		breq1 5113	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝐷 → (𝑥 ∥ 𝑘 ↔ 𝐷 ∥ 𝑘))
62	61	notbid 321	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐷 → (¬ 𝑥 ∥ 𝑘 ↔ ¬ 𝐷 ∥ 𝑘))
63	60, 62	anbi12d 643	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐷 → ((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘) ↔ (𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘)))
64		breq2 5114	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐷 → (𝑃 ∥ 𝑥 ↔ 𝑃 ∥ 𝐷))
65	63, 64	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐷 → (((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘) → 𝑃 ∥ 𝑥) ↔ ((𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘) → 𝑃 ∥ 𝐷)))
66	65	imbi2d 343	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐷 → (((𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘) → 𝑃 ∥ 𝑥)) ↔ ((𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘) → 𝑃 ∥ 𝐷))))
67		simplrl 788	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → 𝑃 ∈ ℙ)
68		simpll 778	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → 𝑥 ∈ ℤ)
69		coprm 16771	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ) → (¬ 𝑃 ∥ 𝑥 ↔ (𝑃 gcd 𝑥) = 1))
70	67, 68, 69	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → (¬ 𝑃 ∥ 𝑥 ↔ (𝑃 gcd 𝑥) = 1))
71		zcn 12597	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℂ)
72	71	ad2antll 741	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℂ)
73		prmz 16734	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
74	73	ad2antrl 740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℤ)
75	74	zcnd 12702	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℂ)
76	72, 75	mulcomd 11231	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · 𝑃) = (𝑃 · 𝑘))
77	76	breq2d 5122	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑥 ∥ (𝑘 · 𝑃) ↔ 𝑥 ∥ (𝑃 · 𝑘)))
78		simpl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑥 ∈ ℤ)
79	74, 78	gcdcomd 16573	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 gcd 𝑥) = (𝑥 gcd 𝑃))
80	79	eqeq1d 2765	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃 gcd 𝑥) = 1 ↔ (𝑥 gcd 𝑃) = 1))
81	77, 80	anbi12d 643	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ (𝑃 gcd 𝑥) = 1) ↔ (𝑥 ∥ (𝑃 · 𝑘) ∧ (𝑥 gcd 𝑃) = 1)))
82		simprr 784	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℤ)
83		coprmdvds 16712	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑥 ∥ (𝑃 · 𝑘) ∧ (𝑥 gcd 𝑃) = 1) → 𝑥 ∥ 𝑘))
84	78, 74, 82, 83	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 ∥ (𝑃 · 𝑘) ∧ (𝑥 gcd 𝑃) = 1) → 𝑥 ∥ 𝑘))
85	81, 84	sylbid 243	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ (𝑃 gcd 𝑥) = 1) → 𝑥 ∥ 𝑘))
86	85	expdimp 457	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → ((𝑃 gcd 𝑥) = 1 → 𝑥 ∥ 𝑘))
87	70, 86	sylbid 243	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → (¬ 𝑃 ∥ 𝑥 → 𝑥 ∥ 𝑘))
88	87	con1d 146	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → (¬ 𝑥 ∥ 𝑘 → 𝑃 ∥ 𝑥))
89	88	expimpd 458	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘) → 𝑃 ∥ 𝑥))
90	89	ex 417	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℤ → ((𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘) → 𝑃 ∥ 𝑥)))
91	66, 90	vtoclga 3542	. . . . . . . . . 10 ⊢ (𝐷 ∈ ℤ → ((𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘) → 𝑃 ∥ 𝐷)))
92	91	impl 460	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘) → 𝑃 ∥ 𝐷))
93	73	zcnd 12702	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℂ)
94	93	exp1d 14179	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ ℙ → (𝑃↑1) = 𝑃)
95	94	ad2antlr 739	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑃↑1) = 𝑃)
96	95	oveq2d 7428	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑘 · (𝑃↑1)) = (𝑘 · 𝑃))
97	96	breq2d 5122	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝐷 ∥ (𝑘 · (𝑃↑1)) ↔ 𝐷 ∥ (𝑘 · 𝑃)))
98		1m1e0 12314	. . . . . . . . . . . . . . . 16 ⊢ (1 − 1) = 0
99	98	oveq2i 7423	. . . . . . . . . . . . . . 15 ⊢ (𝑃↑(1 − 1)) = (𝑃↑0)
100	73	ad2antlr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → 𝑃 ∈ ℤ)
101	100	zcnd 12702	. . . . . . . . . . . . . . . 16 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → 𝑃 ∈ ℂ)
102	101	exp0d 14178	. . . . . . . . . . . . . . 15 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑃↑0) = 1)
103	99, 102	eqtrid 2810	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑃↑(1 − 1)) = 1)
104	103	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑘 · (𝑃↑(1 − 1))) = (𝑘 · 1))
105	71	adantl 486	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℂ)
106	105	mulridd 11227	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑘 · 1) = 𝑘)
107	104, 106	eqtrd 2798	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑘 · (𝑃↑(1 − 1))) = 𝑘)
108	107	breq2d 5122	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝐷 ∥ (𝑘 · (𝑃↑(1 − 1))) ↔ 𝐷 ∥ 𝑘))
109	108	notbid 321	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1))) ↔ ¬ 𝐷 ∥ 𝑘))
110	97, 109	anbi12d 643	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) ↔ (𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘)))
111	101	exp1d 14179	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑃↑1) = 𝑃)
112	111	breq1d 5120	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → ((𝑃↑1) ∥ 𝐷 ↔ 𝑃 ∥ 𝐷))
113	92, 110, 112	3imtr4d 297	. . . . . . . 8 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) → (𝑃↑1) ∥ 𝐷))
114	113	ralrimiva 3157	. . . . . . 7 ⊢ ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) → (𝑃↑1) ∥ 𝐷))
115		oveq1 7419	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝑘 · (𝑃↑𝑛)) = (𝑥 · (𝑃↑𝑛)))
116	115	breq2d 5122	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑥 → (𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ↔ 𝐷 ∥ (𝑥 · (𝑃↑𝑛))))
117		oveq1 7419	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑥 → (𝑘 · (𝑃↑(𝑛 − 1))) = (𝑥 · (𝑃↑(𝑛 − 1))))
118	117	breq2d 5122	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1))) ↔ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))))
119	118	notbid 321	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑥 → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1))) ↔ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))))
120	116, 119	anbi12d 643	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑥 → ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) ↔ (𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1))))))
121	120	imbi1d 344	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑥 → (((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)))
122	121	cbvralvw 3243	. . . . . . . . . 10 ⊢ (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) ↔ ∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷))
123		simprr 784	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℤ)
124	73	ad2antrl 740	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℤ)
125	123, 124	zmulcld 12707	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · 𝑃) ∈ ℤ)
126		oveq1 7419	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑘 · 𝑃) → (𝑥 · (𝑃↑𝑛)) = ((𝑘 · 𝑃) · (𝑃↑𝑛)))
127	126	breq2d 5122	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝑘 · 𝑃) → (𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ↔ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛))))
128		oveq1 7419	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑘 · 𝑃) → (𝑥 · (𝑃↑(𝑛 − 1))) = ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))))
129	128	breq2d 5122	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑘 · 𝑃) → (𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1))) ↔ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))))
130	129	notbid 321	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝑘 · 𝑃) → (¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1))) ↔ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))))
131	127, 130	anbi12d 643	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑘 · 𝑃) → ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) ↔ (𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))))))
132	131	imbi1d 344	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑘 · 𝑃) → (((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) ↔ ((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)))
133	132	rspcv 3578	. . . . . . . . . . . . . 14 ⊢ ((𝑘 · 𝑃) ∈ ℤ → (∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)))
134	125, 133	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)))
135		nnnn0 12512	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀)
136	135	ad2antrr 738	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑛 ∈ ℕ₀)
137		zexpcl 14114	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ ℤ ∧ 𝑛 ∈ ℕ₀) → (𝑃↑𝑛) ∈ ℤ)
138	124, 136, 137	syl2anc 595	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ∈ ℤ)
139		simplr 780	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝐷 ∈ ℤ)
140		divides 16313	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃↑𝑛) ∈ ℤ ∧ 𝐷 ∈ ℤ) → ((𝑃↑𝑛) ∥ 𝐷 ↔ ∃𝑥 ∈ ℤ (𝑥 · (𝑃↑𝑛)) = 𝐷))
141	138, 139, 140	syl2anc 595	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃↑𝑛) ∥ 𝐷 ↔ ∃𝑥 ∈ ℤ (𝑥 · (𝑃↑𝑛)) = 𝐷))
142	89	adantll 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘) → 𝑃 ∥ 𝑥))
143		prmnn 16733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
144	143	ad2antrl 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℕ)
145	144	nncnd 12250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℂ)
146	135	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑛 ∈ ℕ₀)
147	145, 146	expp1d 14185	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 + 1)) = ((𝑃↑𝑛) · 𝑃))
148	144, 146	nnexpcld 14283	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ∈ ℕ)
149	148	nncnd 12250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ∈ ℂ)
150	149, 145	mulcomd 11231	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃↑𝑛) · 𝑃) = (𝑃 · (𝑃↑𝑛)))
151	147, 150	eqtrd 2798	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 + 1)) = (𝑃 · (𝑃↑𝑛)))
152	151	oveq2d 7428	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃↑(𝑛 + 1))) = (𝑘 · (𝑃 · (𝑃↑𝑛))))
153	71	ad2antll 741	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℂ)
154	153, 145, 149	mulassd 11233	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃↑𝑛)) = (𝑘 · (𝑃 · (𝑃↑𝑛))))
155	152, 154	eqtr4d 2801	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃↑(𝑛 + 1))) = ((𝑘 · 𝑃) · (𝑃↑𝑛)))
156	155	breq2d 5122	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ↔ (𝑥 · (𝑃↑𝑛)) ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛))))
157		simplr 780	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑥 ∈ ℤ)
158		simprr 784	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℤ)
159	144	nnzd 12618	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℤ)
160	158, 159	zmulcld 12707	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · 𝑃) ∈ ℤ)
161	148	nnzd 12618	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ∈ ℤ)
162	148	nnne0d 12287	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ≠ 0)
163		dvdsmulcr 16344	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ ℤ ∧ (𝑘 · 𝑃) ∈ ℤ ∧ ((𝑃↑𝑛) ∈ ℤ ∧ (𝑃↑𝑛) ≠ 0)) → ((𝑥 · (𝑃↑𝑛)) ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ↔ 𝑥 ∥ (𝑘 · 𝑃)))
164	157, 160, 161, 162, 163	syl112anc 1401	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 · (𝑃↑𝑛)) ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ↔ 𝑥 ∥ (𝑘 · 𝑃)))
165	156, 164	bitrd 282	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ↔ 𝑥 ∥ (𝑘 · 𝑃)))
166		dvdsmulcr 16344	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ ((𝑃↑𝑛) ∈ ℤ ∧ (𝑃↑𝑛) ≠ 0)) → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛)) ↔ 𝑥 ∥ 𝑘))
167	157, 158, 161, 162, 166	syl112anc 1401	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛)) ↔ 𝑥 ∥ 𝑘))
168	167	notbid 321	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛)) ↔ ¬ 𝑥 ∥ 𝑘))
169	165, 168	anbi12d 643	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛))) ↔ (𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘)))
170	151	breq1d 5120	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃↑𝑛)) ↔ (𝑃 · (𝑃↑𝑛)) ∥ (𝑥 · (𝑃↑𝑛))))
171		dvdsmulcr 16344	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑃 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ ((𝑃↑𝑛) ∈ ℤ ∧ (𝑃↑𝑛) ≠ 0)) → ((𝑃 · (𝑃↑𝑛)) ∥ (𝑥 · (𝑃↑𝑛)) ↔ 𝑃 ∥ 𝑥))
172	159, 157, 161, 162, 171	syl112anc 1401	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃 · (𝑃↑𝑛)) ∥ (𝑥 · (𝑃↑𝑛)) ↔ 𝑃 ∥ 𝑥))
173	170, 172	bitrd 282	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃↑𝑛)) ↔ 𝑃 ∥ 𝑥))
174	142, 169, 173	3imtr4d 297	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃↑𝑛))))
175	174	an32s 664	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∈ ℤ) → (((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃↑𝑛))))
176		breq1 5113	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 · (𝑃↑𝑛)) = 𝐷 → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1)))))
177		breq1 5113	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 · (𝑃↑𝑛)) = 𝐷 → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
178	177	notbid 321	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 · (𝑃↑𝑛)) = 𝐷 → (¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛)) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
179	176, 178	anbi12d 643	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 · (𝑃↑𝑛)) = 𝐷 → (((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛)))))
180		breq2 5114	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 · (𝑃↑𝑛)) = 𝐷 → ((𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃↑𝑛)) ↔ (𝑃↑(𝑛 + 1)) ∥ 𝐷))
181	179, 180	imbi12d 347	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 · (𝑃↑𝑛)) = 𝐷 → ((((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃↑𝑛))) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
182	175, 181	syl5ibcom 248	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∈ ℤ) → ((𝑥 · (𝑃↑𝑛)) = 𝐷 → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
183	182	rexlimdva 3166	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℕ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (∃𝑥 ∈ ℤ (𝑥 · (𝑃↑𝑛)) = 𝐷 → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
184	183	adantlr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (∃𝑥 ∈ ℤ (𝑥 · (𝑃↑𝑛)) = 𝐷 → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
185	141, 184	sylbid 243	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃↑𝑛) ∥ 𝐷 → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
186	185	com23 87	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → ((𝑃↑𝑛) ∥ 𝐷 → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
187	186	a2d 30	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑𝑛) ∥ 𝐷) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
188	71	ad2antll 741	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℂ)
189	124	zcnd 12702	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℂ)
190	138	zcnd 12702	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ∈ ℂ)
191	188, 189, 190	mulassd 11233	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃↑𝑛)) = (𝑘 · (𝑃 · (𝑃↑𝑛))))
192	189, 190	mulcomd 11231	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 · (𝑃↑𝑛)) = ((𝑃↑𝑛) · 𝑃))
193	189, 136	expp1d 14185	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 + 1)) = ((𝑃↑𝑛) · 𝑃))
194	192, 193	eqtr4d 2801	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 · (𝑃↑𝑛)) = (𝑃↑(𝑛 + 1)))
195	194	oveq2d 7428	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃 · (𝑃↑𝑛))) = (𝑘 · (𝑃↑(𝑛 + 1))))
196	191, 195	eqtrd 2798	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃↑𝑛)) = (𝑘 · (𝑃↑(𝑛 + 1))))
197	196	breq2d 5122	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1)))))
198		nnm1nn0 12546	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ₀)
199	198	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑛 − 1) ∈ ℕ₀)
200		zexpcl 14114	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃 ∈ ℤ ∧ (𝑛 − 1) ∈ ℕ₀) → (𝑃↑(𝑛 − 1)) ∈ ℤ)
201	124, 199, 200	syl2anc 595	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 − 1)) ∈ ℤ)
202	201	zcnd 12702	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 − 1)) ∈ ℂ)
203	188, 189, 202	mulassd 11233	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))) = (𝑘 · (𝑃 · (𝑃↑(𝑛 − 1)))))
204	189, 202	mulcomd 11231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 · (𝑃↑(𝑛 − 1))) = ((𝑃↑(𝑛 − 1)) · 𝑃))
205		simpll 778	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑛 ∈ ℕ)
206		expm1t 14128	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃 ∈ ℂ ∧ 𝑛 ∈ ℕ) → (𝑃↑𝑛) = ((𝑃↑(𝑛 − 1)) · 𝑃))
207	189, 205, 206	syl2anc 595	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) = ((𝑃↑(𝑛 − 1)) · 𝑃))
208	204, 207	eqtr4d 2801	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 · (𝑃↑(𝑛 − 1))) = (𝑃↑𝑛))
209	208	oveq2d 7428	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃 · (𝑃↑(𝑛 − 1)))) = (𝑘 · (𝑃↑𝑛)))
210	203, 209	eqtrd 2798	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))) = (𝑘 · (𝑃↑𝑛)))
211	210	breq2d 5122	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
212	211	notbid 321	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
213	197, 212	anbi12d 643	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛)))))
214	213	imbi1d 344	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑𝑛) ∥ 𝐷)))
215		nncn 12242	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
216	215	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑛 ∈ ℂ)
217		ax-1cn 11159	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ ℂ
218		pncan 11464	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 1) = 𝑛)
219	216, 217, 218	sylancl 597	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑛 + 1) − 1) = 𝑛)
220	219	oveq2d 7428	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑((𝑛 + 1) − 1)) = (𝑃↑𝑛))
221	220	oveq2d 7428	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃↑((𝑛 + 1) − 1))) = (𝑘 · (𝑃↑𝑛)))
222	221	breq2d 5122	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
223	222	notbid 321	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
224	223	anbi2d 641	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛)))))
225	224	imbi1d 344	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
226	187, 214, 225	3imtr4d 297	. . . . . . . . . . . . 13 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
227	134, 226	syld 48	. . . . . . . . . . . 12 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
228	227	anassrs 472	. . . . . . . . . . 11 ⊢ ((((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
229	228	ralrimdva 3165	. . . . . . . . . 10 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ 𝑃 ∈ ℙ) → (∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
230	122, 229	biimtrid 245	. . . . . . . . 9 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ 𝑃 ∈ ℙ) → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
231	230	expl 462	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷))))
232	231	a2d 30	. . . . . . 7 ⊢ (𝑛 ∈ ℕ → (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)) → ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷))))
233	20, 33, 46, 59, 114, 232	nnind 12252	. . . . . 6 ⊢ (𝑁 ∈ ℕ → ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷)))
234	233	com12 33	. . . . 5 ⊢ ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → (𝑁 ∈ ℕ → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷)))
235	234	impr 459	. . . 4 ⊢ ((𝐷 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ)) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷))
236	235	adantll 726	. . 3 ⊢ (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ)) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷))
237		simpll 778	. . 3 ⊢ (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ)) → 𝐾 ∈ ℤ)
238	7, 236, 237	rspcdva 3583	. 2 ⊢ (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ)) → ((𝐷 ∥ (𝐾 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷))
239	238	3impia 1135	1 ⊢ (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) ∧ (𝐷 ∥ (𝐾 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1))))) → (𝑃↑𝑁) ∥ 𝐷)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1103 = wceq 1570 ∈ wcel 2143 ≠ wne 2958 ∀wral 3079 ∃wrex 3089 class class class wbr 5110 (class class class)co 7412 ℂcc 11099 0cc0 11101 1c1 11102 + caddc 11104 · cmul 11106 − cmin 11442 ℕcn 12234 ℕ₀cn0 12505 ℤcz 12592 ↑cexp 14099 ∥ cdvds 16311 gcd cgcd 16553 ℙcprime 16730

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5258 ax-nul 5270 ax-pow 5338 ax-pr 5406 ax-un 7734 ax-cnex 11157 ax-resscn 11158 ax-1cn 11159 ax-icn 11160 ax-addcl 11161 ax-addrcl 11162 ax-mulcl 11163 ax-mulrcl 11164 ax-mulcom 11165 ax-addass 11166 ax-mulass 11167 ax-distr 11168 ax-i2m1 11169 ax-1ne0 11170 ax-1rid 11171 ax-rnegex 11172 ax-rrecex 11173 ax-cnre 11174 ax-pre-lttri 11175 ax-pre-lttrn 11176 ax-pre-ltadd 11177 ax-pre-mulgt0 11178 ax-pre-sup 11179

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3746 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4489 df-pw 4565 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4874 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7864 df-2nd 7988 df-frecs 8279 df-wrecs 8310 df-recs 8359 df-rdg 8398 df-1o 8454 df-2o 8455 df-er 8695 df-en 8945 df-dom 8946 df-sdom 8947 df-fin 8948 df-sup 9403 df-inf 9404 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11444 df-neg 11445 df-div 11873 df-nn 12235 df-2 12304 df-3 12305 df-n0 12506 df-z 12593 df-uz 12864 df-rp 13018 df-fl 13827 df-mod 13905 df-seq 14040 df-exp 14100 df-cj 15152 df-re 15153 df-im 15154 df-sqrt 15288 df-abs 15289 df-dvds 16312 df-gcd 16554 df-prm 16731

This theorem is referenced by: pockthlem 16966

W3C validator