prmpwdvds - Intuitionistic Logic Explorer

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

Theorem prmpwdvds 12493

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 5925	. . . . . 6 ⊢ (𝑘 = 𝐾 → (𝑘 · (𝑃↑𝑁)) = (𝐾 · (𝑃↑𝑁)))
2	1	breq2d 4041	. . . . 5 ⊢ (𝑘 = 𝐾 → (𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ↔ 𝐷 ∥ (𝐾 · (𝑃↑𝑁))))
3		oveq1 5925	. . . . . . 7 ⊢ (𝑘 = 𝐾 → (𝑘 · (𝑃↑(𝑁 − 1))) = (𝐾 · (𝑃↑(𝑁 − 1))))
4	3	breq2d 4041	. . . . . 6 ⊢ (𝑘 = 𝐾 → (𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1))) ↔ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1)))))
5	4	notbid 668	. . . . 5 ⊢ (𝑘 = 𝐾 → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1))) ↔ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1)))))
6	2, 5	anbi12d 473	. . . 4 ⊢ (𝑘 = 𝐾 → ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) ↔ (𝐷 ∥ (𝐾 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1))))))
7	6	imbi1d 231	. . 3 ⊢ (𝑘 = 𝐾 → (((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷) ↔ ((𝐷 ∥ (𝐾 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷)))
8		oveq2 5926	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (𝑃↑𝑥) = (𝑃↑1))
9	8	oveq2d 5934	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → (𝑘 · (𝑃↑𝑥)) = (𝑘 · (𝑃↑1)))
10	9	breq2d 4041	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑1))))
11		oveq1 5925	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 1 → (𝑥 − 1) = (1 − 1))
12	11	oveq2d 5934	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 1 → (𝑃↑(𝑥 − 1)) = (𝑃↑(1 − 1)))
13	12	oveq2d 5934	. . . . . . . . . . . . 13 ⊢ (𝑥 = 1 → (𝑘 · (𝑃↑(𝑥 − 1))) = (𝑘 · (𝑃↑(1 − 1))))
14	13	breq2d 4041	. . . . . . . . . . . 12 ⊢ (𝑥 = 1 → (𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))))
15	14	notbid 668	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))))
16	10, 15	anbi12d 473	. . . . . . . . . 10 ⊢ (𝑥 = 1 → ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1))))))
17	8	breq1d 4039	. . . . . . . . . 10 ⊢ (𝑥 = 1 → ((𝑃↑𝑥) ∥ 𝐷 ↔ (𝑃↑1) ∥ 𝐷))
18	16, 17	imbi12d 234	. . . . . . . . 9 ⊢ (𝑥 = 1 → (((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) → (𝑃↑1) ∥ 𝐷)))
19	18	ralbidv 2494	. . . . . . . 8 ⊢ (𝑥 = 1 → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) → (𝑃↑1) ∥ 𝐷)))
20	19	imbi2d 230	. . . . . . 7 ⊢ (𝑥 = 1 → (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷)) ↔ ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) → (𝑃↑1) ∥ 𝐷))))
21		oveq2 5926	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑛 → (𝑃↑𝑥) = (𝑃↑𝑛))
22	21	oveq2d 5934	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑛 → (𝑘 · (𝑃↑𝑥)) = (𝑘 · (𝑃↑𝑛)))
23	22	breq2d 4041	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑛 → (𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
24		oveq1 5925	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑛 → (𝑥 − 1) = (𝑛 − 1))
25	24	oveq2d 5934	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑛 → (𝑃↑(𝑥 − 1)) = (𝑃↑(𝑛 − 1)))
26	25	oveq2d 5934	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑛 → (𝑘 · (𝑃↑(𝑥 − 1))) = (𝑘 · (𝑃↑(𝑛 − 1))))
27	26	breq2d 4041	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑛 → (𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))))
28	27	notbid 668	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑛 → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))))
29	23, 28	anbi12d 473	. . . . . . . . . 10 ⊢ (𝑥 = 𝑛 → ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1))))))
30	21	breq1d 4039	. . . . . . . . . 10 ⊢ (𝑥 = 𝑛 → ((𝑃↑𝑥) ∥ 𝐷 ↔ (𝑃↑𝑛) ∥ 𝐷))
31	29, 30	imbi12d 234	. . . . . . . . 9 ⊢ (𝑥 = 𝑛 → (((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)))
32	31	ralbidv 2494	. . . . . . . 8 ⊢ (𝑥 = 𝑛 → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)))
33	32	imbi2d 230	. . . . . . 7 ⊢ (𝑥 = 𝑛 → (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷)) ↔ ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷))))
34		oveq2 5926	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑛 + 1) → (𝑃↑𝑥) = (𝑃↑(𝑛 + 1)))
35	34	oveq2d 5934	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑛 + 1) → (𝑘 · (𝑃↑𝑥)) = (𝑘 · (𝑃↑(𝑛 + 1))))
36	35	breq2d 4041	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑛 + 1) → (𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1)))))
37		oveq1 5925	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑛 + 1) → (𝑥 − 1) = ((𝑛 + 1) − 1))
38	37	oveq2d 5934	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑛 + 1) → (𝑃↑(𝑥 − 1)) = (𝑃↑((𝑛 + 1) − 1)))
39	38	oveq2d 5934	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑛 + 1) → (𝑘 · (𝑃↑(𝑥 − 1))) = (𝑘 · (𝑃↑((𝑛 + 1) − 1))))
40	39	breq2d 4041	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑛 + 1) → (𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))))
41	40	notbid 668	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑛 + 1) → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))))
42	36, 41	anbi12d 473	. . . . . . . . . 10 ⊢ (𝑥 = (𝑛 + 1) → ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1))))))
43	34	breq1d 4039	. . . . . . . . . 10 ⊢ (𝑥 = (𝑛 + 1) → ((𝑃↑𝑥) ∥ 𝐷 ↔ (𝑃↑(𝑛 + 1)) ∥ 𝐷))
44	42, 43	imbi12d 234	. . . . . . . . 9 ⊢ (𝑥 = (𝑛 + 1) → (((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
45	44	ralbidv 2494	. . . . . . . 8 ⊢ (𝑥 = (𝑛 + 1) → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
46	45	imbi2d 230	. . . . . . 7 ⊢ (𝑥 = (𝑛 + 1) → (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷)) ↔ ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷))))
47		oveq2 5926	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑁 → (𝑃↑𝑥) = (𝑃↑𝑁))
48	47	oveq2d 5934	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑁 → (𝑘 · (𝑃↑𝑥)) = (𝑘 · (𝑃↑𝑁)))
49	48	breq2d 4041	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑁 → (𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑𝑁))))
50		oveq1 5925	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑁 → (𝑥 − 1) = (𝑁 − 1))
51	50	oveq2d 5934	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑁 → (𝑃↑(𝑥 − 1)) = (𝑃↑(𝑁 − 1)))
52	51	oveq2d 5934	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑁 → (𝑘 · (𝑃↑(𝑥 − 1))) = (𝑘 · (𝑃↑(𝑁 − 1))))
53	52	breq2d 4041	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑁 → (𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))))
54	53	notbid 668	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑁 → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))))
55	49, 54	anbi12d 473	. . . . . . . . . 10 ⊢ (𝑥 = 𝑁 → ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1))))))
56	47	breq1d 4039	. . . . . . . . . 10 ⊢ (𝑥 = 𝑁 → ((𝑃↑𝑥) ∥ 𝐷 ↔ (𝑃↑𝑁) ∥ 𝐷))
57	55, 56	imbi12d 234	. . . . . . . . 9 ⊢ (𝑥 = 𝑁 → (((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷)))
58	57	ralbidv 2494	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷) ↔ ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷)))
59	58	imbi2d 230	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃↑𝑥) ∥ 𝐷)) ↔ ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷))))
60		breq1 4032	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐷 → (𝑥 ∥ (𝑘 · 𝑃) ↔ 𝐷 ∥ (𝑘 · 𝑃)))
61		breq1 4032	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝐷 → (𝑥 ∥ 𝑘 ↔ 𝐷 ∥ 𝑘))
62	61	notbid 668	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐷 → (¬ 𝑥 ∥ 𝑘 ↔ ¬ 𝐷 ∥ 𝑘))
63	60, 62	anbi12d 473	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐷 → ((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘) ↔ (𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘)))
64		breq2 4033	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐷 → (𝑃 ∥ 𝑥 ↔ 𝑃 ∥ 𝐷))
65	63, 64	imbi12d 234	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐷 → (((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘) → 𝑃 ∥ 𝑥) ↔ ((𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘) → 𝑃 ∥ 𝐷)))
66	65	imbi2d 230	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐷 → (((𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘) → 𝑃 ∥ 𝑥)) ↔ ((𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘) → 𝑃 ∥ 𝐷))))
67		simplrl 535	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → 𝑃 ∈ ℙ)
68		prmnn 12248	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
69	67, 68	syl 14	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → 𝑃 ∈ ℕ)
70		simpll 527	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → 𝑥 ∈ ℤ)
71		dvdsdc 11941	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ ℕ ∧ 𝑥 ∈ ℤ) → DECID 𝑃 ∥ 𝑥)
72	69, 70, 71	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → DECID 𝑃 ∥ 𝑥)
73		coprm 12282	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ) → (¬ 𝑃 ∥ 𝑥 ↔ (𝑃 gcd 𝑥) = 1))
74	67, 70, 73	syl2anc 411	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → (¬ 𝑃 ∥ 𝑥 ↔ (𝑃 gcd 𝑥) = 1))
75		zcn 9322	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℂ)
76	75	ad2antll 491	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℂ)
77		prmz 12249	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
78	77	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℤ)
79	78	zcnd 9440	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℂ)
80	76, 79	mulcomd 8041	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · 𝑃) = (𝑃 · 𝑘))
81	80	breq2d 4041	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑥 ∥ (𝑘 · 𝑃) ↔ 𝑥 ∥ (𝑃 · 𝑘)))
82		simpl 109	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑥 ∈ ℤ)
83	78, 82	gcdcomd 12111	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 gcd 𝑥) = (𝑥 gcd 𝑃))
84	83	eqeq1d 2202	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃 gcd 𝑥) = 1 ↔ (𝑥 gcd 𝑃) = 1))
85	81, 84	anbi12d 473	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ (𝑃 gcd 𝑥) = 1) ↔ (𝑥 ∥ (𝑃 · 𝑘) ∧ (𝑥 gcd 𝑃) = 1)))
86		simprr 531	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℤ)
87		coprmdvds 12230	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑥 ∥ (𝑃 · 𝑘) ∧ (𝑥 gcd 𝑃) = 1) → 𝑥 ∥ 𝑘))
88	82, 78, 86, 87	syl3anc 1249	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 ∥ (𝑃 · 𝑘) ∧ (𝑥 gcd 𝑃) = 1) → 𝑥 ∥ 𝑘))
89	85, 88	sylbid 150	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ (𝑃 gcd 𝑥) = 1) → 𝑥 ∥ 𝑘))
90	89	expdimp 259	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → ((𝑃 gcd 𝑥) = 1 → 𝑥 ∥ 𝑘))
91	74, 90	sylbid 150	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → (¬ 𝑃 ∥ 𝑥 → 𝑥 ∥ 𝑘))
92		con1dc 857	. . . . . . . . . . . . . 14 ⊢ (DECID 𝑃 ∥ 𝑥 → ((¬ 𝑃 ∥ 𝑥 → 𝑥 ∥ 𝑘) → (¬ 𝑥 ∥ 𝑘 → 𝑃 ∥ 𝑥)))
93	72, 91, 92	sylc 62	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → (¬ 𝑥 ∥ 𝑘 → 𝑃 ∥ 𝑥))
94	93	expimpd 363	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘) → 𝑃 ∥ 𝑥))
95	94	ex 115	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℤ → ((𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘) → 𝑃 ∥ 𝑥)))
96	66, 95	vtoclga 2826	. . . . . . . . . 10 ⊢ (𝐷 ∈ ℤ → ((𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘) → 𝑃 ∥ 𝐷)))
97	96	impl 380	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘) → 𝑃 ∥ 𝐷))
98	77	zcnd 9440	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℂ)
99	98	exp1d 10739	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ ℙ → (𝑃↑1) = 𝑃)
100	99	ad2antlr 489	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑃↑1) = 𝑃)
101	100	oveq2d 5934	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑘 · (𝑃↑1)) = (𝑘 · 𝑃))
102	101	breq2d 4041	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝐷 ∥ (𝑘 · (𝑃↑1)) ↔ 𝐷 ∥ (𝑘 · 𝑃)))
103		1m1e0 9051	. . . . . . . . . . . . . . . 16 ⊢ (1 − 1) = 0
104	103	oveq2i 5929	. . . . . . . . . . . . . . 15 ⊢ (𝑃↑(1 − 1)) = (𝑃↑0)
105	77	ad2antlr 489	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → 𝑃 ∈ ℤ)
106	105	zcnd 9440	. . . . . . . . . . . . . . . 16 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → 𝑃 ∈ ℂ)
107	106	exp0d 10738	. . . . . . . . . . . . . . 15 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑃↑0) = 1)
108	104, 107	eqtrid 2238	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑃↑(1 − 1)) = 1)
109	108	oveq2d 5934	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑘 · (𝑃↑(1 − 1))) = (𝑘 · 1))
110	75	adantl 277	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℂ)
111	110	mulridd 8036	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑘 · 1) = 𝑘)
112	109, 111	eqtrd 2226	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑘 · (𝑃↑(1 − 1))) = 𝑘)
113	112	breq2d 4041	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝐷 ∥ (𝑘 · (𝑃↑(1 − 1))) ↔ 𝐷 ∥ 𝑘))
114	113	notbid 668	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1))) ↔ ¬ 𝐷 ∥ 𝑘))
115	102, 114	anbi12d 473	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) ↔ (𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷 ∥ 𝑘)))
116	106	exp1d 10739	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑃↑1) = 𝑃)
117	116	breq1d 4039	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → ((𝑃↑1) ∥ 𝐷 ↔ 𝑃 ∥ 𝐷))
118	97, 115, 117	3imtr4d 203	. . . . . . . 8 ⊢ (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) → (𝑃↑1) ∥ 𝐷))
119	118	ralrimiva 2567	. . . . . . 7 ⊢ ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) → (𝑃↑1) ∥ 𝐷))
120		oveq1 5925	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝑘 · (𝑃↑𝑛)) = (𝑥 · (𝑃↑𝑛)))
121	120	breq2d 4041	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑥 → (𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ↔ 𝐷 ∥ (𝑥 · (𝑃↑𝑛))))
122		oveq1 5925	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑥 → (𝑘 · (𝑃↑(𝑛 − 1))) = (𝑥 · (𝑃↑(𝑛 − 1))))
123	122	breq2d 4041	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → (𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1))) ↔ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))))
124	123	notbid 668	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑥 → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1))) ↔ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))))
125	121, 124	anbi12d 473	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑥 → ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) ↔ (𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1))))))
126	125	imbi1d 231	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑥 → (((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)))
127	126	cbvralvw 2730	. . . . . . . . . 10 ⊢ (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) ↔ ∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷))
128		simprr 531	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℤ)
129	77	ad2antrl 490	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℤ)
130	128, 129	zmulcld 9445	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · 𝑃) ∈ ℤ)
131		oveq1 5925	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑘 · 𝑃) → (𝑥 · (𝑃↑𝑛)) = ((𝑘 · 𝑃) · (𝑃↑𝑛)))
132	131	breq2d 4041	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝑘 · 𝑃) → (𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ↔ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛))))
133		oveq1 5925	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑘 · 𝑃) → (𝑥 · (𝑃↑(𝑛 − 1))) = ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))))
134	133	breq2d 4041	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑘 · 𝑃) → (𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1))) ↔ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))))
135	134	notbid 668	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝑘 · 𝑃) → (¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1))) ↔ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))))
136	132, 135	anbi12d 473	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑘 · 𝑃) → ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) ↔ (𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))))))
137	136	imbi1d 231	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑘 · 𝑃) → (((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) ↔ ((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)))
138	137	rspcv 2860	. . . . . . . . . . . . . 14 ⊢ ((𝑘 · 𝑃) ∈ ℤ → (∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)))
139	130, 138	syl 14	. . . . . . . . . . . . 13 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)))
140		nnnn0 9247	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀)
141	140	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑛 ∈ ℕ₀)
142		zexpcl 10625	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ ℤ ∧ 𝑛 ∈ ℕ₀) → (𝑃↑𝑛) ∈ ℤ)
143	129, 141, 142	syl2anc 411	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ∈ ℤ)
144		simplr 528	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝐷 ∈ ℤ)
145		divides 11932	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃↑𝑛) ∈ ℤ ∧ 𝐷 ∈ ℤ) → ((𝑃↑𝑛) ∥ 𝐷 ↔ ∃𝑥 ∈ ℤ (𝑥 · (𝑃↑𝑛)) = 𝐷))
146	143, 144, 145	syl2anc 411	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃↑𝑛) ∥ 𝐷 ↔ ∃𝑥 ∈ ℤ (𝑥 · (𝑃↑𝑛)) = 𝐷))
147	94	adantll 476	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘) → 𝑃 ∥ 𝑥))
148	68	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℕ)
149	148	nncnd 8996	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℂ)
150	140	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑛 ∈ ℕ₀)
151	149, 150	expp1d 10745	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 + 1)) = ((𝑃↑𝑛) · 𝑃))
152	148, 150	nnexpcld 10766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ∈ ℕ)
153	152	nncnd 8996	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ∈ ℂ)
154	153, 149	mulcomd 8041	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃↑𝑛) · 𝑃) = (𝑃 · (𝑃↑𝑛)))
155	151, 154	eqtrd 2226	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 + 1)) = (𝑃 · (𝑃↑𝑛)))
156	155	oveq2d 5934	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃↑(𝑛 + 1))) = (𝑘 · (𝑃 · (𝑃↑𝑛))))
157	75	ad2antll 491	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℂ)
158	157, 149, 153	mulassd 8043	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃↑𝑛)) = (𝑘 · (𝑃 · (𝑃↑𝑛))))
159	156, 158	eqtr4d 2229	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃↑(𝑛 + 1))) = ((𝑘 · 𝑃) · (𝑃↑𝑛)))
160	159	breq2d 4041	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ↔ (𝑥 · (𝑃↑𝑛)) ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛))))
161		simplr 528	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑥 ∈ ℤ)
162		simprr 531	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℤ)
163	148	nnzd 9438	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℤ)
164	162, 163	zmulcld 9445	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · 𝑃) ∈ ℤ)
165	152	nnzd 9438	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ∈ ℤ)
166	152	nnne0d 9027	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ≠ 0)
167		dvdsmulcr 11964	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ ℤ ∧ (𝑘 · 𝑃) ∈ ℤ ∧ ((𝑃↑𝑛) ∈ ℤ ∧ (𝑃↑𝑛) ≠ 0)) → ((𝑥 · (𝑃↑𝑛)) ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ↔ 𝑥 ∥ (𝑘 · 𝑃)))
168	161, 164, 165, 166, 167	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 · (𝑃↑𝑛)) ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ↔ 𝑥 ∥ (𝑘 · 𝑃)))
169	160, 168	bitrd 188	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ↔ 𝑥 ∥ (𝑘 · 𝑃)))
170		dvdsmulcr 11964	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ ((𝑃↑𝑛) ∈ ℤ ∧ (𝑃↑𝑛) ≠ 0)) → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛)) ↔ 𝑥 ∥ 𝑘))
171	161, 162, 165, 166, 170	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛)) ↔ 𝑥 ∥ 𝑘))
172	171	notbid 668	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛)) ↔ ¬ 𝑥 ∥ 𝑘))
173	169, 172	anbi12d 473	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛))) ↔ (𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥 ∥ 𝑘)))
174	155	breq1d 4039	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃↑𝑛)) ↔ (𝑃 · (𝑃↑𝑛)) ∥ (𝑥 · (𝑃↑𝑛))))
175		dvdsmulcr 11964	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑃 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ ((𝑃↑𝑛) ∈ ℤ ∧ (𝑃↑𝑛) ≠ 0)) → ((𝑃 · (𝑃↑𝑛)) ∥ (𝑥 · (𝑃↑𝑛)) ↔ 𝑃 ∥ 𝑥))
176	163, 161, 165, 166, 175	syl112anc 1253	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃 · (𝑃↑𝑛)) ∥ (𝑥 · (𝑃↑𝑛)) ↔ 𝑃 ∥ 𝑥))
177	174, 176	bitrd 188	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃↑𝑛)) ↔ 𝑃 ∥ 𝑥))
178	147, 173, 177	3imtr4d 203	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃↑𝑛))))
179	178	an32s 568	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∈ ℤ) → (((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃↑𝑛))))
180		breq1 4032	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 · (𝑃↑𝑛)) = 𝐷 → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1)))))
181		breq1 4032	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 · (𝑃↑𝑛)) = 𝐷 → ((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
182	181	notbid 668	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 · (𝑃↑𝑛)) = 𝐷 → (¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛)) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
183	180, 182	anbi12d 473	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 · (𝑃↑𝑛)) = 𝐷 → (((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛)))))
184		breq2 4033	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 · (𝑃↑𝑛)) = 𝐷 → ((𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃↑𝑛)) ↔ (𝑃↑(𝑛 + 1)) ∥ 𝐷))
185	183, 184	imbi12d 234	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 · (𝑃↑𝑛)) = 𝐷 → ((((𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ (𝑥 · (𝑃↑𝑛)) ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃↑𝑛))) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
186	179, 185	syl5ibcom 155	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∈ ℤ) → ((𝑥 · (𝑃↑𝑛)) = 𝐷 → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
187	186	rexlimdva 2611	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℕ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (∃𝑥 ∈ ℤ (𝑥 · (𝑃↑𝑛)) = 𝐷 → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
188	187	adantlr 477	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (∃𝑥 ∈ ℤ (𝑥 · (𝑃↑𝑛)) = 𝐷 → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
189	146, 188	sylbid 150	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃↑𝑛) ∥ 𝐷 → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
190	189	com23 78	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → ((𝑃↑𝑛) ∥ 𝐷 → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
191	190	a2d 26	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑𝑛) ∥ 𝐷) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
192	75	ad2antll 491	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℂ)
193	129	zcnd 9440	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℂ)
194	143	zcnd 9440	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) ∈ ℂ)
195	192, 193, 194	mulassd 8043	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃↑𝑛)) = (𝑘 · (𝑃 · (𝑃↑𝑛))))
196	193, 194	mulcomd 8041	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 · (𝑃↑𝑛)) = ((𝑃↑𝑛) · 𝑃))
197	193, 141	expp1d 10745	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 + 1)) = ((𝑃↑𝑛) · 𝑃))
198	196, 197	eqtr4d 2229	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 · (𝑃↑𝑛)) = (𝑃↑(𝑛 + 1)))
199	198	oveq2d 5934	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃 · (𝑃↑𝑛))) = (𝑘 · (𝑃↑(𝑛 + 1))))
200	195, 199	eqtrd 2226	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃↑𝑛)) = (𝑘 · (𝑃↑(𝑛 + 1))))
201	200	breq2d 4041	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1)))))
202		nnm1nn0 9281	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ₀)
203	202	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑛 − 1) ∈ ℕ₀)
204		zexpcl 10625	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃 ∈ ℤ ∧ (𝑛 − 1) ∈ ℕ₀) → (𝑃↑(𝑛 − 1)) ∈ ℤ)
205	129, 203, 204	syl2anc 411	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 − 1)) ∈ ℤ)
206	205	zcnd 9440	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 − 1)) ∈ ℂ)
207	192, 193, 206	mulassd 8043	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))) = (𝑘 · (𝑃 · (𝑃↑(𝑛 − 1)))))
208	193, 206	mulcomd 8041	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 · (𝑃↑(𝑛 − 1))) = ((𝑃↑(𝑛 − 1)) · 𝑃))
209		simpll 527	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑛 ∈ ℕ)
210		expm1t 10638	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃 ∈ ℂ ∧ 𝑛 ∈ ℕ) → (𝑃↑𝑛) = ((𝑃↑(𝑛 − 1)) · 𝑃))
211	193, 209, 210	syl2anc 411	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑𝑛) = ((𝑃↑(𝑛 − 1)) · 𝑃))
212	208, 211	eqtr4d 2229	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 · (𝑃↑(𝑛 − 1))) = (𝑃↑𝑛))
213	212	oveq2d 5934	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃 · (𝑃↑(𝑛 − 1)))) = (𝑘 · (𝑃↑𝑛)))
214	207, 213	eqtrd 2226	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))) = (𝑘 · (𝑃↑𝑛)))
215	214	breq2d 4041	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
216	215	notbid 668	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
217	201, 216	anbi12d 473	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛)))))
218	217	imbi1d 231	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑𝑛) ∥ 𝐷)))
219		nncn 8990	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
220	219	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑛 ∈ ℂ)
221		ax-1cn 7965	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ ℂ
222		pncan 8225	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 1) = 𝑛)
223	220, 221, 222	sylancl 413	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑛 + 1) − 1) = 𝑛)
224	223	oveq2d 5934	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑((𝑛 + 1) − 1)) = (𝑃↑𝑛))
225	224	oveq2d 5934	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃↑((𝑛 + 1) − 1))) = (𝑘 · (𝑃↑𝑛)))
226	225	breq2d 4041	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
227	226	notbid 668	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))))
228	227	anbi2d 464	. . . . . . . . . . . . . . 15 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛)))))
229	228	imbi1d 231	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
230	191, 218, 229	3imtr4d 203	. . . . . . . . . . . . 13 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
231	139, 230	syld 45	. . . . . . . . . . . 12 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
232	231	anassrs 400	. . . . . . . . . . 11 ⊢ ((((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
233	232	ralrimdva 2574	. . . . . . . . . 10 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ 𝑃 ∈ ℙ) → (∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
234	127, 233	biimtrid 152	. . . . . . . . 9 ⊢ (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ 𝑃 ∈ ℙ) → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
235	234	expl 378	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷))))
236	235	a2d 26	. . . . . . 7 ⊢ (𝑛 ∈ ℕ → (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃↑𝑛) ∥ 𝐷)) → ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷))))
237	20, 33, 46, 59, 119, 236	nnind 8998	. . . . . 6 ⊢ (𝑁 ∈ ℕ → ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷)))
238	237	com12 30	. . . . 5 ⊢ ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → (𝑁 ∈ ℕ → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷)))
239	238	impr 379	. . . 4 ⊢ ((𝐷 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ)) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷))
240	239	adantll 476	. . 3 ⊢ (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ)) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷))
241		simpll 527	. . 3 ⊢ (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ)) → 𝐾 ∈ ℤ)
242	7, 240, 241	rspcdva 2869	. 2 ⊢ (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ)) → ((𝐷 ∥ (𝐾 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1)))) → (𝑃↑𝑁) ∥ 𝐷))
243	242	3impia 1202	1 ⊢ (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) ∧ (𝐷 ∥ (𝐾 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1))))) → (𝑃↑𝑁) ∥ 𝐷)

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 DECID wdc 835 ∧ w3a 980 = wceq 1364 ∈ wcel 2164 ≠ wne 2364 ∀wral 2472 ∃wrex 2473 class class class wbr 4029 (class class class)co 5918 ℂcc 7870 0cc0 7872 1c1 7873 + caddc 7875 · cmul 7877 − cmin 8190 ℕcn 8982 ℕ₀cn0 9240 ℤcz 9317 ↑cexp 10609 ∥ cdvds 11930 gcd cgcd 12079 ℙcprime 12245

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-coll 4144 ax-sep 4147 ax-nul 4155 ax-pow 4203 ax-pr 4238 ax-un 4464 ax-setind 4569 ax-iinf 4620 ax-cnex 7963 ax-resscn 7964 ax-1cn 7965 ax-1re 7966 ax-icn 7967 ax-addcl 7968 ax-addrcl 7969 ax-mulcl 7970 ax-mulrcl 7971 ax-addcom 7972 ax-mulcom 7973 ax-addass 7974 ax-mulass 7975 ax-distr 7976 ax-i2m1 7977 ax-0lt1 7978 ax-1rid 7979 ax-0id 7980 ax-rnegex 7981 ax-precex 7982 ax-cnre 7983 ax-pre-ltirr 7984 ax-pre-ltwlin 7985 ax-pre-lttrn 7986 ax-pre-apti 7987 ax-pre-ltadd 7988 ax-pre-mulgt0 7989 ax-pre-mulext 7990 ax-arch 7991 ax-caucvg 7992

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-nel 2460 df-ral 2477 df-rex 2478 df-reu 2479 df-rmo 2480 df-rab 2481 df-v 2762 df-sbc 2986 df-csb 3081 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-nul 3447 df-if 3558 df-pw 3603 df-sn 3624 df-pr 3625 df-op 3627 df-uni 3836 df-int 3871 df-iun 3914 df-br 4030 df-opab 4091 df-mpt 4092 df-tr 4128 df-id 4324 df-po 4327 df-iso 4328 df-iord 4397 df-on 4399 df-ilim 4400 df-suc 4402 df-iom 4623 df-xp 4665 df-rel 4666 df-cnv 4667 df-co 4668 df-dm 4669 df-rn 4670 df-res 4671 df-ima 4672 df-iota 5215 df-fun 5256 df-fn 5257 df-f 5258 df-f1 5259 df-fo 5260 df-f1o 5261 df-fv 5262 df-riota 5873 df-ov 5921 df-oprab 5922 df-mpo 5923 df-1st 6193 df-2nd 6194 df-recs 6358 df-frec 6444 df-1o 6469 df-2o 6470 df-er 6587 df-en 6795 df-sup 7043 df-pnf 8056 df-mnf 8057 df-xr 8058 df-ltxr 8059 df-le 8060 df-sub 8192 df-neg 8193 df-reap 8594 df-ap 8601 df-div 8692 df-inn 8983 df-2 9041 df-3 9042 df-4 9043 df-n0 9241 df-z 9318 df-uz 9593 df-q 9685 df-rp 9720 df-fz 10075 df-fzo 10209 df-fl 10339 df-mod 10394 df-seqfrec 10519 df-exp 10610 df-cj 10986 df-re 10987 df-im 10988 df-rsqrt 11142 df-abs 11143 df-dvds 11931 df-gcd 12080 df-prm 12246

This theorem is referenced by: pockthlem 12494

W3C validator