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 16873

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 7370	. . . . . 6 ⊢ (𝑘 = 𝐾 → (𝑘 · (𝑃↑𝑁)) = (𝐾 · (𝑃↑𝑁)))
2	1	breq2d 5091	. . . . 5 ⊢ (𝑘 = 𝐾 → (𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ↔ 𝐷 ∥ (𝐾 · (𝑃↑𝑁))))
3		oveq1 7370	. . . . . . 7 ⊢ (𝑘 = 𝐾 → (𝑘 · (𝑃↑(𝑁 − 1))) = (𝐾 · (𝑃↑(𝑁 − 1))))
4	3	breq2d 5091	. . . . . 6 ⊢ (𝑘 = 𝐾 → (𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1))) ↔ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1)))))
5	4	notbid 319	. . . . 5 ⊢ (𝑘 = 𝐾 → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1))) ↔ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1)))))
6	2, 5	anbi12d 638	. . . 4 ⊢ (𝑘 = 𝐾 → ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) ↔ (𝐷 ∥ (𝐾 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1))))))
7	6	imbi1d 342	. . 3 ⊢ (𝑘 = 𝐾 → (((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷) ↔ ((𝐷 ∥ (𝐾 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷)))
8		oveq2 7371	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (𝑃↑𝑥) = (𝑃↑1))
9	8	oveq2d 7379	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → (𝑘 · (𝑃↑𝑥)) = (𝑘 · (𝑃↑1)))
10	9	breq2d 5091	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑1))))
11		oveq1 7370	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 1 → (𝑥 − 1) = (1 − 1))
12	11	oveq2d 7379	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 1 → (𝑃↑(𝑥 − 1)) = (𝑃↑(1 − 1)))
13	12	oveq2d 7379	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (𝑘 · (𝑃↑(𝑥 − 1))) = (𝑘 · (𝑃↑(1 − 1))))
14	13	breq2d 5091	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → (𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))))
15	14	notbid 319	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))))
16	10, 15	anbi12d 638	. . . . . . . . . 10 ⊢ (𝑥 = 1 → ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1))))))
17	8	breq1d 5089	. . . . . . . . . 10 ⊢ (𝑥 = 1 → ((𝑃↑𝑥) ∥ 𝐷 ↔ (𝑃↑1) ∥ 𝐷))
18	16, 17	imbi12d 345	. . . . . . . . 9 ⊢ (𝑥 = 1 → (((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) → (𝑃↑1) ∥ 𝐷)))
19	18	ralbidv 3163	. . . . . . . 8 ⊢ (𝑥 = 1 → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) → (𝑃↑1) ∥ 𝐷)))
20	19	imbi2d 341	. . . . . . 7 ⊢ (𝑥 = 1 → (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷)) ↔ ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) → (𝑃↑1) ∥ 𝐷))))
21		oveq2 7371	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑛 → (𝑃↑𝑥) = (𝑃↑𝑛))
22	21	oveq2d 7379	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑛 → (𝑘 · (𝑃↑𝑥)) = (𝑘 · (𝑃↑𝑛)))
23	22	breq2d 5091	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑛 → (𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
24		oveq1 7370	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑛 → (𝑥 − 1) = (𝑛 − 1))
25	24	oveq2d 7379	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑛 → (𝑃↑(𝑥 − 1)) = (𝑃↑(𝑛 − 1)))
26	25	oveq2d 7379	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑛 → (𝑘 · (𝑃↑(𝑥 − 1))) = (𝑘 · (𝑃↑(𝑛 − 1))))
27	26	breq2d 5091	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑛 → (𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))))
28	27	notbid 319	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑛 → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))))
29	23, 28	anbi12d 638	. . . . . . . . . 10 ⊢ (𝑥 = 𝑛 → ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1))))))
30	21	breq1d 5089	. . . . . . . . . 10 ⊢ (𝑥 = 𝑛 → ((𝑃↑𝑥) ∥ 𝐷 ↔ (𝑃↑𝑛) ∥ 𝐷))
31	29, 30	imbi12d 345	. . . . . . . . 9 ⊢ (𝑥 = 𝑛 → (((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)))
32	31	ralbidv 3163	. . . . . . . 8 ⊢ (𝑥 = 𝑛 → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)))
33	32	imbi2d 341	. . . . . . 7 ⊢ (𝑥 = 𝑛 → (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷)) ↔ ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷))))
34		oveq2 7371	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑛 + 1) → (𝑃↑𝑥) = (𝑃↑(𝑛 + 1)))
35	34	oveq2d 7379	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑛 + 1) → (𝑘 · (𝑃↑𝑥)) = (𝑘 · (𝑃↑(𝑛 + 1))))
36	35	breq2d 5091	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑛 + 1) → (𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1)))))
37		oveq1 7370	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑛 + 1) → (𝑥 − 1) = ((𝑛 + 1) − 1))
38	37	oveq2d 7379	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑛 + 1) → (𝑃↑(𝑥 − 1)) = (𝑃↑((𝑛 + 1) − 1)))
39	38	oveq2d 7379	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑛 + 1) → (𝑘 · (𝑃↑(𝑥 − 1))) = (𝑘 · (𝑃↑((𝑛 + 1) − 1))))
40	39	breq2d 5091	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑛 + 1) → (𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))))
41	40	notbid 319	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑛 + 1) → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))))
42	36, 41	anbi12d 638	. . . . . . . . . 10 ⊢ (𝑥 = (𝑛 + 1) → ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1))))))
43	34	breq1d 5089	. . . . . . . . . 10 ⊢ (𝑥 = (𝑛 + 1) → ((𝑃↑𝑥) ∥ 𝐷 ↔ (𝑃↑(𝑛 + 1)) ∥ 𝐷))
44	42, 43	imbi12d 345	. . . . . . . . 9 ⊢ (𝑥 = (𝑛 + 1) → (((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
45	44	ralbidv 3163	. . . . . . . 8 ⊢ (𝑥 = (𝑛 + 1) → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
46	45	imbi2d 341	. . . . . . 7 ⊢ (𝑥 = (𝑛 + 1) → (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷)) ↔ ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷))))
47		oveq2 7371	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑁 → (𝑃↑𝑥) = (𝑃↑𝑁))
48	47	oveq2d 7379	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑁 → (𝑘 · (𝑃↑𝑥)) = (𝑘 · (𝑃↑𝑁)))
49	48	breq2d 5091	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑁 → (𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑𝑁))))
50		oveq1 7370	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑁 → (𝑥 − 1) = (𝑁 − 1))
51	50	oveq2d 7379	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑁 → (𝑃↑(𝑥 − 1)) = (𝑃↑(𝑁 − 1)))
52	51	oveq2d 7379	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑁 → (𝑘 · (𝑃↑(𝑥 − 1))) = (𝑘 · (𝑃↑(𝑁 − 1))))
53	52	breq2d 5091	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑁 → (𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))))
54	53	notbid 319	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑁 → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))))
55	49, 54	anbi12d 638	. . . . . . . . . 10 ⊢ (𝑥 = 𝑁 → ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1))))))
56	47	breq1d 5089	. . . . . . . . . 10 ⊢ (𝑥 = 𝑁 → ((𝑃↑𝑥) ∥ 𝐷 ↔ (𝑃↑𝑁) ∥ 𝐷))
57	55, 56	imbi12d 345	. . . . . . . . 9 ⊢ (𝑥 = 𝑁 → (((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷)))
58	57	ralbidv 3163	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷)))
59	58	imbi2d 341	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷)) ↔ ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷))))
60		breq1 5082	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐷 → (𝑥 ∥ (𝑘 · 𝑃) ↔ 𝐷 ∥ (𝑘 · 𝑃)))
61		breq1 5082	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝐷 → (𝑥 ∥ 𝑘 ↔ 𝐷 ∥ 𝑘))
62	61	notbid 319	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐷 → (¬ 𝑥 ∥ 𝑘 ↔ ¬ 𝐷 ∥ 𝑘))
63	60, 62	anbi12d 638	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐷 → ((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘) ↔ (𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘)))
64		breq2 5083	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐷 → (𝑃 ∥ 𝑥 ↔ 𝑃 ∥ 𝐷))
65	63, 64	imbi12d 345	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐷 → (((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘) → 𝑃 ∥ 𝑥) ↔ ((𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘) → 𝑃 ∥ 𝐷)))
66	65	imbi2d 341	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐷 → (((𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘) → 𝑃 ∥ 𝑥)) ↔ ((𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘) → 𝑃 ∥ 𝐷))))
67		simplrl 782	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → 𝑃 ∈ ℙ)
68		simpll 772	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → 𝑥 ∈ ℤ)
69		coprm 16679	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ) → (¬ 𝑃 ∥ 𝑥 ↔ (𝑃 gcd 𝑥) = 1))
70	67, 68, 69	syl2anc 590	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → (¬ 𝑃 ∥ 𝑥 ↔ (𝑃 gcd 𝑥) = 1))
71		zcn 12527	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℂ)
72	71	ad2antll 735	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℂ)
73		prmz 16642	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
74	73	ad2antrl 734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℤ)
75	74	zcnd 12632	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℂ)
76	72, 75	mulcomd 11164	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · 𝑃) = (𝑃 · 𝑘))
77	76	breq2d 5091	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑥 ∥ (𝑘 · 𝑃) ↔ 𝑥 ∥ (𝑃 · 𝑘)))
78		simpl 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑥 ∈ ℤ)
79	74, 78	gcdcomd 16481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 gcd 𝑥) = (𝑥 gcd 𝑃))
80	79	eqeq1d 2742	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃 gcd 𝑥) = 1 ↔ (𝑥 gcd 𝑃) = 1))
81	77, 80	anbi12d 638	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ (𝑃 gcd 𝑥) = 1) ↔ (𝑥 ∥ (𝑃 · 𝑘) ∧ (𝑥 gcd 𝑃) = 1)))
82		simprr 778	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℤ)
83		coprmdvds 16620	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑥 ∥ (𝑃 · 𝑘) ∧ (𝑥 gcd 𝑃) = 1) → 𝑥 ∥ 𝑘))
84	78, 74, 82, 83	syl3anc 1379	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 ∥ (𝑃 · 𝑘) ∧ (𝑥 gcd 𝑃) = 1) → 𝑥 ∥ 𝑘))
85	81, 84	sylbid 241	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ (𝑃 gcd 𝑥) = 1) → 𝑥 ∥ 𝑘))
86	85	expdimp 453	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → ((𝑃 gcd 𝑥) = 1 → 𝑥 ∥ 𝑘))
87	70, 86	sylbid 241	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → (¬ 𝑃 ∥ 𝑥 → 𝑥 ∥ 𝑘))
88	87	con1d 145	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → (¬ 𝑥 ∥ 𝑘 → 𝑃 ∥ 𝑥))
89	88	expimpd 454	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘) → 𝑃 ∥ 𝑥))
90	89	ex 413	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℤ → ((𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘) → 𝑃 ∥ 𝑥)))
91	66, 90	vtoclga 3523	. . . . . . . . . 10 ⊢ (𝐷 ∈ ℤ → ((𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘) → 𝑃 ∥ 𝐷)))
92	91	impl 456	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘) → 𝑃 ∥ 𝐷))
93	73	zcnd 12632	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℂ)
94	93	exp1d 14101	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ ℙ → (𝑃↑1) = 𝑃)
95	94	ad2antlr 733	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑃↑1) = 𝑃)
96	95	oveq2d 7379	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑘 · (𝑃↑1)) = (𝑘 · 𝑃))
97	96	breq2d 5091	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝐷 ∥ (𝑘 · (𝑃↑1)) ↔ 𝐷 ∥ (𝑘 · 𝑃)))
98		1m1e0 12251	. . . . . . . . . . . . . . . 16 ⊢ (1 − 1) = 0
99	98	oveq2i 7374	. . . . . . . . . . . . . . 15 ⊢ (𝑃↑(1 − 1)) = (𝑃↑0)
100	73	ad2antlr 733	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → 𝑃 ∈ ℤ)
101	100	zcnd 12632	. . . . . . . . . . . . . . . 16 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → 𝑃 ∈ ℂ)
102	101	exp0d 14100	. . . . . . . . . . . . . . 15 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑃↑0) = 1)
103	99, 102	eqtrid 2787	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑃↑(1 − 1)) = 1)
104	103	oveq2d 7379	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑘 · (𝑃↑(1 − 1))) = (𝑘 · 1))
105	71	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℂ)
106	105	mulridd 11160	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑘 · 1) = 𝑘)
107	104, 106	eqtrd 2775	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑘 · (𝑃↑(1 − 1))) = 𝑘)
108	107	breq2d 5091	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝐷 ∥ (𝑘 · (𝑃↑(1 − 1))) ↔ 𝐷 ∥ 𝑘))
109	108	notbid 319	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1))) ↔ ¬ 𝐷 ∥ 𝑘))
110	97, 109	anbi12d 638	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) ↔ (𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘)))
111	101	exp1d 14101	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑃↑1) = 𝑃)
112	111	breq1d 5089	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → ((𝑃↑1) ∥ 𝐷 ↔ 𝑃 ∥ 𝐷))
113	92, 110, 112	3imtr4d 295	. . . . . . . 8 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) → (𝑃↑1) ∥ 𝐷))
114	113	ralrimiva 3132	. . . . . . 7 ⊢ ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) → (𝑃↑1) ∥ 𝐷))
115		oveq1 7370	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝑘 · (𝑃↑𝑛)) = (𝑥 · (𝑃↑𝑛)))
116	115	breq2d 5091	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑥 → (𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ↔ 𝐷 ∥ (𝑥 · (𝑃↑𝑛))))
117		oveq1 7370	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑥 → (𝑘 · (𝑃↑(𝑛 − 1))) = (𝑥 · (𝑃↑(𝑛 − 1))))
118	117	breq2d 5091	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1))) ↔ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))))
119	118	notbid 319	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑥 → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1))) ↔ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))))
120	116, 119	anbi12d 638	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑥 → ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) ↔ (𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1))))))
121	120	imbi1d 342	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑥 → (((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)))
122	121	cbvralvw 3218	. . . . . . . . . 10 ⊢ (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) ↔ ∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷))
123		simprr 778	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℤ)
124	73	ad2antrl 734	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℤ)
125	123, 124	zmulcld 12637	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · 𝑃) ∈ ℤ)
126		oveq1 7370	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑘 · 𝑃) → (𝑥 · (𝑃↑𝑛)) = ((𝑘 · 𝑃) · (𝑃↑𝑛)))
127	126	breq2d 5091	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝑘 · 𝑃) → (𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ↔ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛))))
128		oveq1 7370	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑘 · 𝑃) → (𝑥 · (𝑃↑(𝑛 − 1))) = ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))))
129	128	breq2d 5091	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑘 · 𝑃) → (𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1))) ↔ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))))
130	129	notbid 319	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝑘 · 𝑃) → (¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1))) ↔ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))))
131	127, 130	anbi12d 638	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑘 · 𝑃) → ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) ↔ (𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))))))
132	131	imbi1d 342	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑘 · 𝑃) → (((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) ↔ ((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)))
133	132	rspcv 3563	. . . . . . . . . . . . . 14 ⊢ ((𝑘 · 𝑃) ∈ ℤ → (∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)))
134	125, 133	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)))
135		nnnn0 12442	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀)
136	135	ad2antrr 732	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑛 ∈ ℕ₀)
137		zexpcl 14036	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ ℤ ∧ 𝑛 ∈ ℕ₀) → (𝑃↑𝑛) ∈ ℤ)
138	124, 136, 137	syl2anc 590	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ∈ ℤ)
139		simplr 774	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝐷 ∈ ℤ)
140		divides 16221	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃↑𝑛) ∈ ℤ ∧ 𝐷 ∈ ℤ) → ((𝑃↑𝑛) ∥ 𝐷 ↔ ∃𝑥 ∈ ℤ (𝑥 · (𝑃↑𝑛)) = 𝐷))
141	138, 139, 140	syl2anc 590	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃↑𝑛) ∥ 𝐷 ↔ ∃𝑥 ∈ ℤ (𝑥 · (𝑃↑𝑛)) = 𝐷))
142	89	adantll 720	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘) → 𝑃 ∥ 𝑥))
143		prmnn 16641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
144	143	ad2antrl 734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℕ)
145	144	nncnd 12188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℂ)
146	135	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑛 ∈ ℕ₀)
147	145, 146	expp1d 14107	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 + 1)) = ((𝑃↑𝑛) · 𝑃))
148	144, 146	nnexpcld 14205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ∈ ℕ)
149	148	nncnd 12188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ∈ ℂ)
150	149, 145	mulcomd 11164	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃↑𝑛) · 𝑃) = (𝑃 · (𝑃↑𝑛)))
151	147, 150	eqtrd 2775	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 + 1)) = (𝑃 · (𝑃↑𝑛)))
152	151	oveq2d 7379	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃↑(𝑛 + 1))) = (𝑘 · (𝑃 · (𝑃↑𝑛))))
153	71	ad2antll 735	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℂ)
154	153, 145, 149	mulassd 11166	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃↑𝑛)) = (𝑘 · (𝑃 · (𝑃↑𝑛))))
155	152, 154	eqtr4d 2778	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃↑(𝑛 + 1))) = ((𝑘 · 𝑃) · (𝑃↑𝑛)))
156	155	breq2d 5091	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ↔ (𝑥 · (𝑃↑𝑛)) ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛))))
157		simplr 774	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑥 ∈ ℤ)
158		simprr 778	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℤ)
159	144	nnzd 12548	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℤ)
160	158, 159	zmulcld 12637	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · 𝑃) ∈ ℤ)
161	148	nnzd 12548	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ∈ ℤ)
162	148	nnne0d 12225	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ≠ 0)
163		dvdsmulcr 16252	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ ℤ ∧ (𝑘 · 𝑃) ∈ ℤ ∧ ((𝑃↑𝑛) ∈ ℤ ∧ (𝑃↑𝑛) ≠ 0)) → ((𝑥 · (𝑃↑𝑛)) ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ↔ 𝑥 ∥ (𝑘 · 𝑃)))
164	157, 160, 161, 162, 163	syl112anc 1382	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 · (𝑃↑𝑛)) ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ↔ 𝑥 ∥ (𝑘 · 𝑃)))
165	156, 164	bitrd 280	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ↔ 𝑥 ∥ (𝑘 · 𝑃)))
166		dvdsmulcr 16252	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ ((𝑃↑𝑛) ∈ ℤ ∧ (𝑃↑𝑛) ≠ 0)) → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛)) ↔ 𝑥 ∥ 𝑘))
167	157, 158, 161, 162, 166	syl112anc 1382	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛)) ↔ 𝑥 ∥ 𝑘))
168	167	notbid 319	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛)) ↔ ¬ 𝑥 ∥ 𝑘))
169	165, 168	anbi12d 638	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛))) ↔ (𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘)))
170	151	breq1d 5089	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃↑𝑛)) ↔ (𝑃 · (𝑃↑𝑛)) ∥ (𝑥 · (𝑃↑𝑛))))
171		dvdsmulcr 16252	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑃 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ ((𝑃↑𝑛) ∈ ℤ ∧ (𝑃↑𝑛) ≠ 0)) → ((𝑃 · (𝑃↑𝑛)) ∥ (𝑥 · (𝑃↑𝑛)) ↔ 𝑃 ∥ 𝑥))
172	159, 157, 161, 162, 171	syl112anc 1382	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃 · (𝑃↑𝑛)) ∥ (𝑥 · (𝑃↑𝑛)) ↔ 𝑃 ∥ 𝑥))
173	170, 172	bitrd 280	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃↑𝑛)) ↔ 𝑃 ∥ 𝑥))
174	142, 169, 173	3imtr4d 295	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃↑𝑛))))
175	174	an32s 658	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∈ ℤ) → (((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃↑𝑛))))
176		breq1 5082	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 · (𝑃↑𝑛)) = 𝐷 → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1)))))
177		breq1 5082	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 · (𝑃↑𝑛)) = 𝐷 → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
178	177	notbid 319	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 · (𝑃↑𝑛)) = 𝐷 → (¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛)) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
179	176, 178	anbi12d 638	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 · (𝑃↑𝑛)) = 𝐷 → (((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛)))))
180		breq2 5083	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 · (𝑃↑𝑛)) = 𝐷 → ((𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃↑𝑛)) ↔ (𝑃↑(𝑛 + 1)) ∥ 𝐷))
181	179, 180	imbi12d 345	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 · (𝑃↑𝑛)) = 𝐷 → ((((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃↑𝑛))) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
182	175, 181	syl5ibcom 246	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∈ ℤ) → ((𝑥 · (𝑃↑𝑛)) = 𝐷 → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
183	182	rexlimdva 3141	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℕ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (∃𝑥 ∈ ℤ (𝑥 · (𝑃↑𝑛)) = 𝐷 → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
184	183	adantlr 721	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (∃𝑥 ∈ ℤ (𝑥 · (𝑃↑𝑛)) = 𝐷 → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
185	141, 184	sylbid 241	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃↑𝑛) ∥ 𝐷 → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
186	185	com23 86	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → ((𝑃↑𝑛) ∥ 𝐷 → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
187	186	a2d 29	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑𝑛) ∥ 𝐷) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
188	71	ad2antll 735	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℂ)
189	124	zcnd 12632	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℂ)
190	138	zcnd 12632	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ∈ ℂ)
191	188, 189, 190	mulassd 11166	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃↑𝑛)) = (𝑘 · (𝑃 · (𝑃↑𝑛))))
192	189, 190	mulcomd 11164	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 · (𝑃↑𝑛)) = ((𝑃↑𝑛) · 𝑃))
193	189, 136	expp1d 14107	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 + 1)) = ((𝑃↑𝑛) · 𝑃))
194	192, 193	eqtr4d 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 · (𝑃↑𝑛)) = (𝑃↑(𝑛 + 1)))
195	194	oveq2d 7379	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃 · (𝑃↑𝑛))) = (𝑘 · (𝑃↑(𝑛 + 1))))
196	191, 195	eqtrd 2775	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃↑𝑛)) = (𝑘 · (𝑃↑(𝑛 + 1))))
197	196	breq2d 5091	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1)))))
198		nnm1nn0 12476	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ₀)
199	198	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑛 − 1) ∈ ℕ₀)
200		zexpcl 14036	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃 ∈ ℤ ∧ (𝑛 − 1) ∈ ℕ₀) → (𝑃↑(𝑛 − 1)) ∈ ℤ)
201	124, 199, 200	syl2anc 590	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 − 1)) ∈ ℤ)
202	201	zcnd 12632	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 − 1)) ∈ ℂ)
203	188, 189, 202	mulassd 11166	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))) = (𝑘 · (𝑃 · (𝑃↑(𝑛 − 1)))))
204	189, 202	mulcomd 11164	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 · (𝑃↑(𝑛 − 1))) = ((𝑃↑(𝑛 − 1)) · 𝑃))
205		simpll 772	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑛 ∈ ℕ)
206		expm1t 14050	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃 ∈ ℂ ∧ 𝑛 ∈ ℕ) → (𝑃↑𝑛) = ((𝑃↑(𝑛 − 1)) · 𝑃))
207	189, 205, 206	syl2anc 590	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) = ((𝑃↑(𝑛 − 1)) · 𝑃))
208	204, 207	eqtr4d 2778	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 · (𝑃↑(𝑛 − 1))) = (𝑃↑𝑛))
209	208	oveq2d 7379	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃 · (𝑃↑(𝑛 − 1)))) = (𝑘 · (𝑃↑𝑛)))
210	203, 209	eqtrd 2775	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))) = (𝑘 · (𝑃↑𝑛)))
211	210	breq2d 5091	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
212	211	notbid 319	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
213	197, 212	anbi12d 638	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛)))))
214	213	imbi1d 342	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑𝑛) ∥ 𝐷)))
215		nncn 12180	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
216	215	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑛 ∈ ℂ)
217		ax-1cn 11094	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ ℂ
218		pncan 11397	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 1) = 𝑛)
219	216, 217, 218	sylancl 592	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑛 + 1) − 1) = 𝑛)
220	219	oveq2d 7379	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑((𝑛 + 1) − 1)) = (𝑃↑𝑛))
221	220	oveq2d 7379	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃↑((𝑛 + 1) − 1))) = (𝑘 · (𝑃↑𝑛)))
222	221	breq2d 5091	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
223	222	notbid 319	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
224	223	anbi2d 636	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛)))))
225	224	imbi1d 342	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
226	187, 214, 225	3imtr4d 295	. . . . . . . . . . . . 13 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
227	134, 226	syld 47	. . . . . . . . . . . 12 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
228	227	anassrs 468	. . . . . . . . . . 11 ⊢ ((((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
229	228	ralrimdva 3140	. . . . . . . . . 10 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ 𝑃 ∈ ℙ) → (∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
230	122, 229	biimtrid 243	. . . . . . . . 9 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ 𝑃 ∈ ℙ) → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
231	230	expl 458	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷))))
232	231	a2d 29	. . . . . . 7 ⊢ (𝑛 ∈ ℕ → (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)) → ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷))))
233	20, 33, 46, 59, 114, 232	nnind 12190	. . . . . 6 ⊢ (𝑁 ∈ ℕ → ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷)))
234	233	com12 32	. . . . 5 ⊢ ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → (𝑁 ∈ ℕ → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷)))
235	234	impr 455	. . . 4 ⊢ ((𝐷 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ)) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷))
236	235	adantll 720	. . 3 ⊢ (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ)) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷))
237		simpll 772	. . 3 ⊢ (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ)) → 𝐾 ∈ ℤ)
238	7, 236, 237	rspcdva 3568	. 2 ⊢ (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ)) → ((𝐷 ∥ (𝐾 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷))
239	238	3impia 1123	1 ⊢ (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) ∧ (𝐷 ∥ (𝐾 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1))))) → (𝑃↑𝑁) ∥ 𝐷)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∧ w3a 1092 = wceq 1547 ∈ wcel 2119 ≠ wne 2935 ∀wral 3054 ∃wrex 3064 class class class wbr 5079 (class class class)co 7363 ℂcc 11034 0cc0 11036 1c1 11037 + caddc 11039 · cmul 11041 − cmin 11375 ℕcn 12172 ℕ₀cn0 12435 ℤcz 12522 ↑cexp 14021 ∥ cdvds 16219 gcd cgcd 16461 ℙcprime 16638

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2712 ax-sep 5225 ax-nul 5235 ax-pow 5301 ax-pr 5369 ax-un 7685 ax-cnex 11092 ax-resscn 11093 ax-1cn 11094 ax-icn 11095 ax-addcl 11096 ax-addrcl 11097 ax-mulcl 11098 ax-mulrcl 11099 ax-mulcom 11100 ax-addass 11101 ax-mulass 11102 ax-distr 11103 ax-i2m1 11104 ax-1ne0 11105 ax-1rid 11106 ax-rnegex 11107 ax-rrecex 11108 ax-cnre 11109 ax-pre-lttri 11110 ax-pre-lttrn 11111 ax-pre-ltadd 11112 ax-pre-mulgt0 11113 ax-pre-sup 11114

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2719 df-cleq 2732 df-clel 2815 df-nfc 2889 df-ne 2936 df-nel 3040 df-ral 3055 df-rex 3065 df-rmo 3345 df-reu 3346 df-rab 3393 df-v 3434 df-sbc 3731 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4269 df-if 4462 df-pw 4538 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4846 df-iun 4930 df-br 5080 df-opab 5142 df-mpt 5161 df-tr 5187 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7320 df-ov 7366 df-oprab 7367 df-mpo 7368 df-om 7814 df-2nd 7939 df-frecs 8228 df-wrecs 8259 df-recs 8308 df-rdg 8346 df-1o 8402 df-2o 8403 df-er 8640 df-en 8891 df-dom 8892 df-sdom 8893 df-fin 8894 df-sup 9352 df-inf 9353 df-pnf 11179 df-mnf 11180 df-xr 11181 df-ltxr 11182 df-le 11183 df-sub 11377 df-neg 11378 df-div 11806 df-nn 12173 df-2 12242 df-3 12243 df-n0 12436 df-z 12523 df-uz 12787 df-rp 12941 df-fl 13749 df-mod 13827 df-seq 13962 df-exp 14022 df-cj 15059 df-re 15060 df-im 15061 df-sqrt 15195 df-abs 15196 df-dvds 16220 df-gcd 16462 df-prm 16639

This theorem is referenced by: pockthlem 16874

W3C validator