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 16954

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 7407	. . . . . 6 ⊢ (𝑘 = 𝐾 → (𝑘 · (𝑃↑𝑁)) = (𝐾 · (𝑃↑𝑁)))
2	1	breq2d 5117	. . . . 5 ⊢ (𝑘 = 𝐾 → (𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ↔ 𝐷 ∥ (𝐾 · (𝑃↑𝑁))))
3		oveq1 7407	. . . . . . 7 ⊢ (𝑘 = 𝐾 → (𝑘 · (𝑃↑(𝑁 − 1))) = (𝐾 · (𝑃↑(𝑁 − 1))))
4	3	breq2d 5117	. . . . . 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 7408	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (𝑃↑𝑥) = (𝑃↑1))
9	8	oveq2d 7416	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → (𝑘 · (𝑃↑𝑥)) = (𝑘 · (𝑃↑1)))
10	9	breq2d 5117	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑1))))
11		oveq1 7407	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 1 → (𝑥 − 1) = (1 − 1))
12	11	oveq2d 7416	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 1 → (𝑃↑(𝑥 − 1)) = (𝑃↑(1 − 1)))
13	12	oveq2d 7416	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (𝑘 · (𝑃↑(𝑥 − 1))) = (𝑘 · (𝑃↑(1 − 1))))
14	13	breq2d 5117	. . . . . . . . . . . 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 5115	. . . . . . . . . 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 7408	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑛 → (𝑃↑𝑥) = (𝑃↑𝑛))
22	21	oveq2d 7416	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑛 → (𝑘 · (𝑃↑𝑥)) = (𝑘 · (𝑃↑𝑛)))
23	22	breq2d 5117	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑛 → (𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
24		oveq1 7407	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑛 → (𝑥 − 1) = (𝑛 − 1))
25	24	oveq2d 7416	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑛 → (𝑃↑(𝑥 − 1)) = (𝑃↑(𝑛 − 1)))
26	25	oveq2d 7416	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑛 → (𝑘 · (𝑃↑(𝑥 − 1))) = (𝑘 · (𝑃↑(𝑛 − 1))))
27	26	breq2d 5117	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑛 → (𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))))
28	27	notbid 321	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑛 → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))))
29	23, 28	anbi12d 643	. . . . . . . . . 10 ⊢ (𝑥 = 𝑛 → ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1))))))
30	21	breq1d 5115	. . . . . . . . . 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 7408	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑛 + 1) → (𝑃↑𝑥) = (𝑃↑(𝑛 + 1)))
35	34	oveq2d 7416	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑛 + 1) → (𝑘 · (𝑃↑𝑥)) = (𝑘 · (𝑃↑(𝑛 + 1))))
36	35	breq2d 5117	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑛 + 1) → (𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1)))))
37		oveq1 7407	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑛 + 1) → (𝑥 − 1) = ((𝑛 + 1) − 1))
38	37	oveq2d 7416	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑛 + 1) → (𝑃↑(𝑥 − 1)) = (𝑃↑((𝑛 + 1) − 1)))
39	38	oveq2d 7416	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑛 + 1) → (𝑘 · (𝑃↑(𝑥 − 1))) = (𝑘 · (𝑃↑((𝑛 + 1) − 1))))
40	39	breq2d 5117	. . . . . . . . . . . 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 5115	. . . . . . . . . 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 7408	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑁 → (𝑃↑𝑥) = (𝑃↑𝑁))
48	47	oveq2d 7416	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑁 → (𝑘 · (𝑃↑𝑥)) = (𝑘 · (𝑃↑𝑁)))
49	48	breq2d 5117	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑁 → (𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑𝑁))))
50		oveq1 7407	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑁 → (𝑥 − 1) = (𝑁 − 1))
51	50	oveq2d 7416	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑁 → (𝑃↑(𝑥 − 1)) = (𝑃↑(𝑁 − 1)))
52	51	oveq2d 7416	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑁 → (𝑘 · (𝑃↑(𝑥 − 1))) = (𝑘 · (𝑃↑(𝑁 − 1))))
53	52	breq2d 5117	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑁 → (𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))))
54	53	notbid 321	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑁 → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))))
55	49, 54	anbi12d 643	. . . . . . . . . 10 ⊢ (𝑥 = 𝑁 → ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1))))))
56	47	breq1d 5115	. . . . . . . . . 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 5108	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐷 → (𝑥 ∥ (𝑘 · 𝑃) ↔ 𝐷 ∥ (𝑘 · 𝑃)))
61		breq1 5108	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝐷 → (𝑥 ∥ 𝑘 ↔ 𝐷 ∥ 𝑘))
62	61	notbid 321	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐷 → (¬ 𝑥 ∥ 𝑘 ↔ ¬ 𝐷 ∥ 𝑘))
63	60, 62	anbi12d 643	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐷 → ((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘) ↔ (𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘)))
64		breq2 5109	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐷 → (𝑃 ∥ 𝑥 ↔ 𝑃 ∥ 𝐷))
65	63, 64	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐷 → (((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘) → 𝑃 ∥ 𝑥) ↔ ((𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘) → 𝑃 ∥ 𝐷)))
66	65	imbi2d 343	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐷 → (((𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘) → 𝑃 ∥ 𝑥)) ↔ ((𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘) → 𝑃 ∥ 𝐷))))
67		simplrl 788	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → 𝑃 ∈ ℙ)
68		simpll 778	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → 𝑥 ∈ ℤ)
69		coprm 16760	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ) → (¬ 𝑃 ∥ 𝑥 ↔ (𝑃 gcd 𝑥) = 1))
70	67, 68, 69	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → (¬ 𝑃 ∥ 𝑥 ↔ (𝑃 gcd 𝑥) = 1))
71		zcn 12587	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℂ)
72	71	ad2antll 741	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℂ)
73		prmz 16723	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
74	73	ad2antrl 740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℤ)
75	74	zcnd 12692	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℂ)
76	72, 75	mulcomd 11218	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · 𝑃) = (𝑃 · 𝑘))
77	76	breq2d 5117	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑥 ∥ (𝑘 · 𝑃) ↔ 𝑥 ∥ (𝑃 · 𝑘)))
78		simpl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑥 ∈ ℤ)
79	74, 78	gcdcomd 16562	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 gcd 𝑥) = (𝑥 gcd 𝑃))
80	79	eqeq1d 2767	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃 gcd 𝑥) = 1 ↔ (𝑥 gcd 𝑃) = 1))
81	77, 80	anbi12d 643	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ (𝑃 gcd 𝑥) = 1) ↔ (𝑥 ∥ (𝑃 · 𝑘) ∧ (𝑥 gcd 𝑃) = 1)))
82		simprr 784	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℤ)
83		coprmdvds 16701	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑥 ∥ (𝑃 · 𝑘) ∧ (𝑥 gcd 𝑃) = 1) → 𝑥 ∥ 𝑘))
84	78, 74, 82, 83	syl3anc 1394	. . . . . . . . . . . . . . . . 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 3544	. . . . . . . . . 10 ⊢ (𝐷 ∈ ℤ → ((𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘) → 𝑃 ∥ 𝐷)))
92	91	impl 460	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘) → 𝑃 ∥ 𝐷))
93	73	zcnd 12692	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℂ)
94	93	exp1d 14168	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ ℙ → (𝑃↑1) = 𝑃)
95	94	ad2antlr 739	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑃↑1) = 𝑃)
96	95	oveq2d 7416	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑘 · (𝑃↑1)) = (𝑘 · 𝑃))
97	96	breq2d 5117	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝐷 ∥ (𝑘 · (𝑃↑1)) ↔ 𝐷 ∥ (𝑘 · 𝑃)))
98		1m1e0 12304	. . . . . . . . . . . . . . . 16 ⊢ (1 − 1) = 0
99	98	oveq2i 7411	. . . . . . . . . . . . . . 15 ⊢ (𝑃↑(1 − 1)) = (𝑃↑0)
100	73	ad2antlr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → 𝑃 ∈ ℤ)
101	100	zcnd 12692	. . . . . . . . . . . . . . . 16 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → 𝑃 ∈ ℂ)
102	101	exp0d 14167	. . . . . . . . . . . . . . 15 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑃↑0) = 1)
103	99, 102	eqtrid 2812	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑃↑(1 − 1)) = 1)
104	103	oveq2d 7416	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑘 · (𝑃↑(1 − 1))) = (𝑘 · 1))
105	71	adantl 486	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℂ)
106	105	mulridd 11214	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑘 · 1) = 𝑘)
107	104, 106	eqtrd 2800	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑘 · (𝑃↑(1 − 1))) = 𝑘)
108	107	breq2d 5117	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝐷 ∥ (𝑘 · (𝑃↑(1 − 1))) ↔ 𝐷 ∥ 𝑘))
109	108	notbid 321	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1))) ↔ ¬ 𝐷 ∥ 𝑘))
110	97, 109	anbi12d 643	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) ↔ (𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘)))
111	101	exp1d 14168	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑃↑1) = 𝑃)
112	111	breq1d 5115	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → ((𝑃↑1) ∥ 𝐷 ↔ 𝑃 ∥ 𝐷))
113	92, 110, 112	3imtr4d 297	. . . . . . . 8 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) → (𝑃↑1) ∥ 𝐷))
114	113	ralrimiva 3157	. . . . . . 7 ⊢ ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) → (𝑃↑1) ∥ 𝐷))
115		oveq1 7407	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝑘 · (𝑃↑𝑛)) = (𝑥 · (𝑃↑𝑛)))
116	115	breq2d 5117	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑥 → (𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ↔ 𝐷 ∥ (𝑥 · (𝑃↑𝑛))))
117		oveq1 7407	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑥 → (𝑘 · (𝑃↑(𝑛 − 1))) = (𝑥 · (𝑃↑(𝑛 − 1))))
118	117	breq2d 5117	. . . . . . . . . . . . . 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 12697	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · 𝑃) ∈ ℤ)
126		oveq1 7407	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑘 · 𝑃) → (𝑥 · (𝑃↑𝑛)) = ((𝑘 · 𝑃) · (𝑃↑𝑛)))
127	126	breq2d 5117	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝑘 · 𝑃) → (𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ↔ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛))))
128		oveq1 7407	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑘 · 𝑃) → (𝑥 · (𝑃↑(𝑛 − 1))) = ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))))
129	128	breq2d 5117	. . . . . . . . . . . . . . . . . 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 3580	. . . . . . . . . . . . . 14 ⊢ ((𝑘 · 𝑃) ∈ ℤ → (∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)))
134	125, 133	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)))
135		nnnn0 12502	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀)
136	135	ad2antrr 738	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑛 ∈ ℕ₀)
137		zexpcl 14103	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ ℤ ∧ 𝑛 ∈ ℕ₀) → (𝑃↑𝑛) ∈ ℤ)
138	124, 136, 137	syl2anc 595	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ∈ ℤ)
139		simplr 780	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝐷 ∈ ℤ)
140		divides 16302	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃↑𝑛) ∈ ℤ ∧ 𝐷 ∈ ℤ) → ((𝑃↑𝑛) ∥ 𝐷 ↔ ∃𝑥 ∈ ℤ (𝑥 · (𝑃↑𝑛)) = 𝐷))
141	138, 139, 140	syl2anc 595	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃↑𝑛) ∥ 𝐷 ↔ ∃𝑥 ∈ ℤ (𝑥 · (𝑃↑𝑛)) = 𝐷))
142	89	adantll 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘) → 𝑃 ∥ 𝑥))
143		prmnn 16722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
144	143	ad2antrl 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℕ)
145	144	nncnd 12240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℂ)
146	135	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑛 ∈ ℕ₀)
147	145, 146	expp1d 14174	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 + 1)) = ((𝑃↑𝑛) · 𝑃))
148	144, 146	nnexpcld 14272	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ∈ ℕ)
149	148	nncnd 12240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ∈ ℂ)
150	149, 145	mulcomd 11218	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃↑𝑛) · 𝑃) = (𝑃 · (𝑃↑𝑛)))
151	147, 150	eqtrd 2800	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 + 1)) = (𝑃 · (𝑃↑𝑛)))
152	151	oveq2d 7416	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃↑(𝑛 + 1))) = (𝑘 · (𝑃 · (𝑃↑𝑛))))
153	71	ad2antll 741	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℂ)
154	153, 145, 149	mulassd 11220	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃↑𝑛)) = (𝑘 · (𝑃 · (𝑃↑𝑛))))
155	152, 154	eqtr4d 2803	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃↑(𝑛 + 1))) = ((𝑘 · 𝑃) · (𝑃↑𝑛)))
156	155	breq2d 5117	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ↔ (𝑥 · (𝑃↑𝑛)) ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛))))
157		simplr 780	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑥 ∈ ℤ)
158		simprr 784	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℤ)
159	144	nnzd 12608	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℤ)
160	158, 159	zmulcld 12697	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · 𝑃) ∈ ℤ)
161	148	nnzd 12608	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ∈ ℤ)
162	148	nnne0d 12277	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ≠ 0)
163		dvdsmulcr 16333	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ ℤ ∧ (𝑘 · 𝑃) ∈ ℤ ∧ ((𝑃↑𝑛) ∈ ℤ ∧ (𝑃↑𝑛) ≠ 0)) → ((𝑥 · (𝑃↑𝑛)) ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ↔ 𝑥 ∥ (𝑘 · 𝑃)))
164	157, 160, 161, 162, 163	syl112anc 1397	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 · (𝑃↑𝑛)) ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ↔ 𝑥 ∥ (𝑘 · 𝑃)))
165	156, 164	bitrd 282	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ↔ 𝑥 ∥ (𝑘 · 𝑃)))
166		dvdsmulcr 16333	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ ((𝑃↑𝑛) ∈ ℤ ∧ (𝑃↑𝑛) ≠ 0)) → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛)) ↔ 𝑥 ∥ 𝑘))
167	157, 158, 161, 162, 166	syl112anc 1397	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛)) ↔ 𝑥 ∥ 𝑘))
168	167	notbid 321	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛)) ↔ ¬ 𝑥 ∥ 𝑘))
169	165, 168	anbi12d 643	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛))) ↔ (𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘)))
170	151	breq1d 5115	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃↑𝑛)) ↔ (𝑃 · (𝑃↑𝑛)) ∥ (𝑥 · (𝑃↑𝑛))))
171		dvdsmulcr 16333	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑃 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ ((𝑃↑𝑛) ∈ ℤ ∧ (𝑃↑𝑛) ≠ 0)) → ((𝑃 · (𝑃↑𝑛)) ∥ (𝑥 · (𝑃↑𝑛)) ↔ 𝑃 ∥ 𝑥))
172	159, 157, 161, 162, 171	syl112anc 1397	. . . . . . . . . . . . . . . . . . . . . . 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 5108	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 · (𝑃↑𝑛)) = 𝐷 → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1)))))
177		breq1 5108	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 · (𝑃↑𝑛)) = 𝐷 → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
178	177	notbid 321	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 · (𝑃↑𝑛)) = 𝐷 → (¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛)) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
179	176, 178	anbi12d 643	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 · (𝑃↑𝑛)) = 𝐷 → (((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛)))))
180		breq2 5109	. . . . . . . . . . . . . . . . . . . . 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 12692	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℂ)
190	138	zcnd 12692	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ∈ ℂ)
191	188, 189, 190	mulassd 11220	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃↑𝑛)) = (𝑘 · (𝑃 · (𝑃↑𝑛))))
192	189, 190	mulcomd 11218	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 · (𝑃↑𝑛)) = ((𝑃↑𝑛) · 𝑃))
193	189, 136	expp1d 14174	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 + 1)) = ((𝑃↑𝑛) · 𝑃))
194	192, 193	eqtr4d 2803	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 · (𝑃↑𝑛)) = (𝑃↑(𝑛 + 1)))
195	194	oveq2d 7416	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃 · (𝑃↑𝑛))) = (𝑘 · (𝑃↑(𝑛 + 1))))
196	191, 195	eqtrd 2800	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃↑𝑛)) = (𝑘 · (𝑃↑(𝑛 + 1))))
197	196	breq2d 5117	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1)))))
198		nnm1nn0 12536	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ₀)
199	198	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑛 − 1) ∈ ℕ₀)
200		zexpcl 14103	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃 ∈ ℤ ∧ (𝑛 − 1) ∈ ℕ₀) → (𝑃↑(𝑛 − 1)) ∈ ℤ)
201	124, 199, 200	syl2anc 595	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 − 1)) ∈ ℤ)
202	201	zcnd 12692	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 − 1)) ∈ ℂ)
203	188, 189, 202	mulassd 11220	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))) = (𝑘 · (𝑃 · (𝑃↑(𝑛 − 1)))))
204	189, 202	mulcomd 11218	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 · (𝑃↑(𝑛 − 1))) = ((𝑃↑(𝑛 − 1)) · 𝑃))
205		simpll 778	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑛 ∈ ℕ)
206		expm1t 14117	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃 ∈ ℂ ∧ 𝑛 ∈ ℕ) → (𝑃↑𝑛) = ((𝑃↑(𝑛 − 1)) · 𝑃))
207	189, 205, 206	syl2anc 595	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) = ((𝑃↑(𝑛 − 1)) · 𝑃))
208	204, 207	eqtr4d 2803	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 · (𝑃↑(𝑛 − 1))) = (𝑃↑𝑛))
209	208	oveq2d 7416	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃 · (𝑃↑(𝑛 − 1)))) = (𝑘 · (𝑃↑𝑛)))
210	203, 209	eqtrd 2800	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))) = (𝑘 · (𝑃↑𝑛)))
211	210	breq2d 5117	. . . . . . . . . . . . . . . . 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 12232	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
216	215	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑛 ∈ ℂ)
217		ax-1cn 11146	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ ℂ
218		pncan 11451	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 1) = 𝑛)
219	216, 217, 218	sylancl 597	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑛 + 1) − 1) = 𝑛)
220	219	oveq2d 7416	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑((𝑛 + 1) − 1)) = (𝑃↑𝑛))
221	220	oveq2d 7416	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃↑((𝑛 + 1) − 1))) = (𝑘 · (𝑃↑𝑛)))
222	221	breq2d 5117	. . . . . . . . . . . . . . . . 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 12242	. . . . . 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 3585	. 2 ⊢ (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ)) → ((𝐷 ∥ (𝐾 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷))
239	238	3impia 1133	1 ⊢ (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) ∧ (𝐷 ∥ (𝐾 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1))))) → (𝑃↑𝑁) ∥ 𝐷)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 = wceq 1563 ∈ wcel 2145 ≠ wne 2960 ∀wral 3079 ∃wrex 3089 class class class wbr 5105 (class class class)co 7400 ℂcc 11086 0cc0 11088 1c1 11089 + caddc 11091 · cmul 11093 − cmin 11429 ℕcn 12224 ℕ₀cn0 12495 ℤcz 12582 ↑cexp 14088 ∥ cdvds 16300 gcd cgcd 16542 ℙcprime 16719

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-sep 5251 ax-nul 5261 ax-pow 5327 ax-pr 5395 ax-un 7722 ax-cnex 11144 ax-resscn 11145 ax-1cn 11146 ax-icn 11147 ax-addcl 11148 ax-addrcl 11149 ax-mulcl 11150 ax-mulrcl 11151 ax-mulcom 11152 ax-addass 11153 ax-mulass 11154 ax-distr 11155 ax-i2m1 11156 ax-1ne0 11157 ax-1rid 11158 ax-rnegex 11159 ax-rrecex 11160 ax-cnre 11161 ax-pre-lttri 11162 ax-pre-lttrn 11163 ax-pre-ltadd 11164 ax-pre-mulgt0 11165 ax-pre-sup 11166

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3370 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4869 df-iun 4954 df-br 5106 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5547 df-eprel 5552 df-po 5560 df-so 5561 df-fr 5605 df-we 5607 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-rn 5663 df-res 5664 df-ima 5665 df-pred 6292 df-ord 6353 df-on 6354 df-lim 6355 df-suc 6356 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-riota 7357 df-ov 7403 df-oprab 7404 df-mpo 7405 df-om 7851 df-2nd 7975 df-frecs 8266 df-wrecs 8297 df-recs 8346 df-rdg 8385 df-1o 8441 df-2o 8442 df-er 8682 df-en 8932 df-dom 8933 df-sdom 8934 df-fin 8935 df-sup 9390 df-inf 9391 df-pnf 11233 df-mnf 11234 df-xr 11235 df-ltxr 11236 df-le 11237 df-sub 11431 df-neg 11432 df-div 11860 df-nn 12225 df-2 12294 df-3 12295 df-n0 12496 df-z 12583 df-uz 12854 df-rp 13008 df-fl 13816 df-mod 13894 df-seq 14029 df-exp 14089 df-cj 15140 df-re 15141 df-im 15142 df-sqrt 15276 df-abs 15277 df-dvds 16301 df-gcd 16543 df-prm 16720

This theorem is referenced by: pockthlem 16955

W3C validator