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

Theorem prmpwdvds 12296
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.
StepHypRef Expression
1 oveq1 5858 . . . . . 6 (𝑘 = 𝐾 → (𝑘 · (𝑃𝑁)) = (𝐾 · (𝑃𝑁)))
21breq2d 3999 . . . . 5 (𝑘 = 𝐾 → (𝐷 ∥ (𝑘 · (𝑃𝑁)) ↔ 𝐷 ∥ (𝐾 · (𝑃𝑁))))
3 oveq1 5858 . . . . . . 7 (𝑘 = 𝐾 → (𝑘 · (𝑃↑(𝑁 − 1))) = (𝐾 · (𝑃↑(𝑁 − 1))))
43breq2d 3999 . . . . . 6 (𝑘 = 𝐾 → (𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1))) ↔ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1)))))
54notbid 662 . . . . 5 (𝑘 = 𝐾 → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1))) ↔ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1)))))
62, 5anbi12d 470 . . . 4 (𝑘 = 𝐾 → ((𝐷 ∥ (𝑘 · (𝑃𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) ↔ (𝐷 ∥ (𝐾 · (𝑃𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1))))))
76imbi1d 230 . . 3 (𝑘 = 𝐾 → (((𝐷 ∥ (𝑘 · (𝑃𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃𝑁) ∥ 𝐷) ↔ ((𝐷 ∥ (𝐾 · (𝑃𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1)))) → (𝑃𝑁) ∥ 𝐷)))
8 oveq2 5859 . . . . . . . . . . . . 13 (𝑥 = 1 → (𝑃𝑥) = (𝑃↑1))
98oveq2d 5867 . . . . . . . . . . . 12 (𝑥 = 1 → (𝑘 · (𝑃𝑥)) = (𝑘 · (𝑃↑1)))
109breq2d 3999 . . . . . . . . . . 11 (𝑥 = 1 → (𝐷 ∥ (𝑘 · (𝑃𝑥)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑1))))
11 oveq1 5858 . . . . . . . . . . . . . . 15 (𝑥 = 1 → (𝑥 − 1) = (1 − 1))
1211oveq2d 5867 . . . . . . . . . . . . . 14 (𝑥 = 1 → (𝑃↑(𝑥 − 1)) = (𝑃↑(1 − 1)))
1312oveq2d 5867 . . . . . . . . . . . . 13 (𝑥 = 1 → (𝑘 · (𝑃↑(𝑥 − 1))) = (𝑘 · (𝑃↑(1 − 1))))
1413breq2d 3999 . . . . . . . . . . . 12 (𝑥 = 1 → (𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))))
1514notbid 662 . . . . . . . . . . 11 (𝑥 = 1 → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))))
1610, 15anbi12d 470 . . . . . . . . . 10 (𝑥 = 1 → ((𝐷 ∥ (𝑘 · (𝑃𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1))))))
178breq1d 3997 . . . . . . . . . 10 (𝑥 = 1 → ((𝑃𝑥) ∥ 𝐷 ↔ (𝑃↑1) ∥ 𝐷))
1816, 17imbi12d 233 . . . . . . . . 9 (𝑥 = 1 → (((𝐷 ∥ (𝑘 · (𝑃𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃𝑥) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) → (𝑃↑1) ∥ 𝐷)))
1918ralbidv 2470 . . . . . . . 8 (𝑥 = 1 → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃𝑥) ∥ 𝐷) ↔ ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) → (𝑃↑1) ∥ 𝐷)))
2019imbi2d 229 . . . . . . 7 (𝑥 = 1 → (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃𝑥) ∥ 𝐷)) ↔ ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) → (𝑃↑1) ∥ 𝐷))))
21 oveq2 5859 . . . . . . . . . . . . 13 (𝑥 = 𝑛 → (𝑃𝑥) = (𝑃𝑛))
2221oveq2d 5867 . . . . . . . . . . . 12 (𝑥 = 𝑛 → (𝑘 · (𝑃𝑥)) = (𝑘 · (𝑃𝑛)))
2322breq2d 3999 . . . . . . . . . . 11 (𝑥 = 𝑛 → (𝐷 ∥ (𝑘 · (𝑃𝑥)) ↔ 𝐷 ∥ (𝑘 · (𝑃𝑛))))
24 oveq1 5858 . . . . . . . . . . . . . . 15 (𝑥 = 𝑛 → (𝑥 − 1) = (𝑛 − 1))
2524oveq2d 5867 . . . . . . . . . . . . . 14 (𝑥 = 𝑛 → (𝑃↑(𝑥 − 1)) = (𝑃↑(𝑛 − 1)))
2625oveq2d 5867 . . . . . . . . . . . . 13 (𝑥 = 𝑛 → (𝑘 · (𝑃↑(𝑥 − 1))) = (𝑘 · (𝑃↑(𝑛 − 1))))
2726breq2d 3999 . . . . . . . . . . . 12 (𝑥 = 𝑛 → (𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))))
2827notbid 662 . . . . . . . . . . 11 (𝑥 = 𝑛 → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))))
2923, 28anbi12d 470 . . . . . . . . . 10 (𝑥 = 𝑛 → ((𝐷 ∥ (𝑘 · (𝑃𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1))))))
3021breq1d 3997 . . . . . . . . . 10 (𝑥 = 𝑛 → ((𝑃𝑥) ∥ 𝐷 ↔ (𝑃𝑛) ∥ 𝐷))
3129, 30imbi12d 233 . . . . . . . . 9 (𝑥 = 𝑛 → (((𝐷 ∥ (𝑘 · (𝑃𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃𝑥) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃𝑛) ∥ 𝐷)))
3231ralbidv 2470 . . . . . . . 8 (𝑥 = 𝑛 → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃𝑥) ∥ 𝐷) ↔ ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃𝑛) ∥ 𝐷)))
3332imbi2d 229 . . . . . . 7 (𝑥 = 𝑛 → (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃𝑥) ∥ 𝐷)) ↔ ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃𝑛) ∥ 𝐷))))
34 oveq2 5859 . . . . . . . . . . . . 13 (𝑥 = (𝑛 + 1) → (𝑃𝑥) = (𝑃↑(𝑛 + 1)))
3534oveq2d 5867 . . . . . . . . . . . 12 (𝑥 = (𝑛 + 1) → (𝑘 · (𝑃𝑥)) = (𝑘 · (𝑃↑(𝑛 + 1))))
3635breq2d 3999 . . . . . . . . . . 11 (𝑥 = (𝑛 + 1) → (𝐷 ∥ (𝑘 · (𝑃𝑥)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1)))))
37 oveq1 5858 . . . . . . . . . . . . . . 15 (𝑥 = (𝑛 + 1) → (𝑥 − 1) = ((𝑛 + 1) − 1))
3837oveq2d 5867 . . . . . . . . . . . . . 14 (𝑥 = (𝑛 + 1) → (𝑃↑(𝑥 − 1)) = (𝑃↑((𝑛 + 1) − 1)))
3938oveq2d 5867 . . . . . . . . . . . . 13 (𝑥 = (𝑛 + 1) → (𝑘 · (𝑃↑(𝑥 − 1))) = (𝑘 · (𝑃↑((𝑛 + 1) − 1))))
4039breq2d 3999 . . . . . . . . . . . 12 (𝑥 = (𝑛 + 1) → (𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))))
4140notbid 662 . . . . . . . . . . 11 (𝑥 = (𝑛 + 1) → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))))
4236, 41anbi12d 470 . . . . . . . . . 10 (𝑥 = (𝑛 + 1) → ((𝐷 ∥ (𝑘 · (𝑃𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1))))))
4334breq1d 3997 . . . . . . . . . 10 (𝑥 = (𝑛 + 1) → ((𝑃𝑥) ∥ 𝐷 ↔ (𝑃↑(𝑛 + 1)) ∥ 𝐷))
4442, 43imbi12d 233 . . . . . . . . 9 (𝑥 = (𝑛 + 1) → (((𝐷 ∥ (𝑘 · (𝑃𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃𝑥) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
4544ralbidv 2470 . . . . . . . 8 (𝑥 = (𝑛 + 1) → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃𝑥) ∥ 𝐷) ↔ ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
4645imbi2d 229 . . . . . . 7 (𝑥 = (𝑛 + 1) → (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃𝑥) ∥ 𝐷)) ↔ ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷))))
47 oveq2 5859 . . . . . . . . . . . . 13 (𝑥 = 𝑁 → (𝑃𝑥) = (𝑃𝑁))
4847oveq2d 5867 . . . . . . . . . . . 12 (𝑥 = 𝑁 → (𝑘 · (𝑃𝑥)) = (𝑘 · (𝑃𝑁)))
4948breq2d 3999 . . . . . . . . . . 11 (𝑥 = 𝑁 → (𝐷 ∥ (𝑘 · (𝑃𝑥)) ↔ 𝐷 ∥ (𝑘 · (𝑃𝑁))))
50 oveq1 5858 . . . . . . . . . . . . . . 15 (𝑥 = 𝑁 → (𝑥 − 1) = (𝑁 − 1))
5150oveq2d 5867 . . . . . . . . . . . . . 14 (𝑥 = 𝑁 → (𝑃↑(𝑥 − 1)) = (𝑃↑(𝑁 − 1)))
5251oveq2d 5867 . . . . . . . . . . . . 13 (𝑥 = 𝑁 → (𝑘 · (𝑃↑(𝑥 − 1))) = (𝑘 · (𝑃↑(𝑁 − 1))))
5352breq2d 3999 . . . . . . . . . . . 12 (𝑥 = 𝑁 → (𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))))
5453notbid 662 . . . . . . . . . . 11 (𝑥 = 𝑁 → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))))
5549, 54anbi12d 470 . . . . . . . . . 10 (𝑥 = 𝑁 → ((𝐷 ∥ (𝑘 · (𝑃𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1))))))
5647breq1d 3997 . . . . . . . . . 10 (𝑥 = 𝑁 → ((𝑃𝑥) ∥ 𝐷 ↔ (𝑃𝑁) ∥ 𝐷))
5755, 56imbi12d 233 . . . . . . . . 9 (𝑥 = 𝑁 → (((𝐷 ∥ (𝑘 · (𝑃𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃𝑥) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃𝑁) ∥ 𝐷)))
5857ralbidv 2470 . . . . . . . 8 (𝑥 = 𝑁 → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃𝑥) ∥ 𝐷) ↔ ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃𝑁) ∥ 𝐷)))
5958imbi2d 229 . . . . . . 7 (𝑥 = 𝑁 → (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃𝑥)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑥 − 1)))) → (𝑃𝑥) ∥ 𝐷)) ↔ ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃𝑁) ∥ 𝐷))))
60 breq1 3990 . . . . . . . . . . . . . 14 (𝑥 = 𝐷 → (𝑥 ∥ (𝑘 · 𝑃) ↔ 𝐷 ∥ (𝑘 · 𝑃)))
61 breq1 3990 . . . . . . . . . . . . . . 15 (𝑥 = 𝐷 → (𝑥𝑘𝐷𝑘))
6261notbid 662 . . . . . . . . . . . . . 14 (𝑥 = 𝐷 → (¬ 𝑥𝑘 ↔ ¬ 𝐷𝑘))
6360, 62anbi12d 470 . . . . . . . . . . . . 13 (𝑥 = 𝐷 → ((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥𝑘) ↔ (𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷𝑘)))
64 breq2 3991 . . . . . . . . . . . . 13 (𝑥 = 𝐷 → (𝑃𝑥𝑃𝐷))
6563, 64imbi12d 233 . . . . . . . . . . . 12 (𝑥 = 𝐷 → (((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥𝑘) → 𝑃𝑥) ↔ ((𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷𝑘) → 𝑃𝐷)))
6665imbi2d 229 . . . . . . . . . . 11 (𝑥 = 𝐷 → (((𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥𝑘) → 𝑃𝑥)) ↔ ((𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷𝑘) → 𝑃𝐷))))
67 simplrl 530 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → 𝑃 ∈ ℙ)
68 prmnn 12053 . . . . . . . . . . . . . . . 16 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
6967, 68syl 14 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → 𝑃 ∈ ℕ)
70 simpll 524 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → 𝑥 ∈ ℤ)
71 dvdsdc 11749 . . . . . . . . . . . . . . 15 ((𝑃 ∈ ℕ ∧ 𝑥 ∈ ℤ) → DECID 𝑃𝑥)
7269, 70, 71syl2anc 409 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → DECID 𝑃𝑥)
73 coprm 12087 . . . . . . . . . . . . . . . 16 ((𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ) → (¬ 𝑃𝑥 ↔ (𝑃 gcd 𝑥) = 1))
7467, 70, 73syl2anc 409 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → (¬ 𝑃𝑥 ↔ (𝑃 gcd 𝑥) = 1))
75 zcn 9206 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ℤ → 𝑘 ∈ ℂ)
7675ad2antll 488 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℂ)
77 prmz 12054 . . . . . . . . . . . . . . . . . . . . . 22 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
7877ad2antrl 487 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℤ)
7978zcnd 9324 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℂ)
8076, 79mulcomd 7930 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · 𝑃) = (𝑃 · 𝑘))
8180breq2d 3999 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑥 ∥ (𝑘 · 𝑃) ↔ 𝑥 ∥ (𝑃 · 𝑘)))
82 simpl 108 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑥 ∈ ℤ)
8378, 82gcdcomd 11918 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 gcd 𝑥) = (𝑥 gcd 𝑃))
8483eqeq1d 2179 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃 gcd 𝑥) = 1 ↔ (𝑥 gcd 𝑃) = 1))
8581, 84anbi12d 470 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ (𝑃 gcd 𝑥) = 1) ↔ (𝑥 ∥ (𝑃 · 𝑘) ∧ (𝑥 gcd 𝑃) = 1)))
86 simprr 527 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℤ)
87 coprmdvds 12035 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑥 ∥ (𝑃 · 𝑘) ∧ (𝑥 gcd 𝑃) = 1) → 𝑥𝑘))
8882, 78, 86, 87syl3anc 1233 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 ∥ (𝑃 · 𝑘) ∧ (𝑥 gcd 𝑃) = 1) → 𝑥𝑘))
8985, 88sylbid 149 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ (𝑃 gcd 𝑥) = 1) → 𝑥𝑘))
9089expdimp 257 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → ((𝑃 gcd 𝑥) = 1 → 𝑥𝑘))
9174, 90sylbid 149 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → (¬ 𝑃𝑥𝑥𝑘))
92 con1dc 851 . . . . . . . . . . . . . 14 (DECID 𝑃𝑥 → ((¬ 𝑃𝑥𝑥𝑘) → (¬ 𝑥𝑘𝑃𝑥)))
9372, 91, 92sylc 62 . . . . . . . . . . . . 13 (((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∥ (𝑘 · 𝑃)) → (¬ 𝑥𝑘𝑃𝑥))
9493expimpd 361 . . . . . . . . . . . 12 ((𝑥 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥𝑘) → 𝑃𝑥))
9594ex 114 . . . . . . . . . . 11 (𝑥 ∈ ℤ → ((𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥𝑘) → 𝑃𝑥)))
9666, 95vtoclga 2796 . . . . . . . . . 10 (𝐷 ∈ ℤ → ((𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷𝑘) → 𝑃𝐷)))
9796impl 378 . . . . . . . . 9 (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷𝑘) → 𝑃𝐷))
9877zcnd 9324 . . . . . . . . . . . . . 14 (𝑃 ∈ ℙ → 𝑃 ∈ ℂ)
9998exp1d 10593 . . . . . . . . . . . . 13 (𝑃 ∈ ℙ → (𝑃↑1) = 𝑃)
10099ad2antlr 486 . . . . . . . . . . . 12 (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑃↑1) = 𝑃)
101100oveq2d 5867 . . . . . . . . . . 11 (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑘 · (𝑃↑1)) = (𝑘 · 𝑃))
102101breq2d 3999 . . . . . . . . . 10 (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝐷 ∥ (𝑘 · (𝑃↑1)) ↔ 𝐷 ∥ (𝑘 · 𝑃)))
103 1m1e0 8936 . . . . . . . . . . . . . . . 16 (1 − 1) = 0
104103oveq2i 5862 . . . . . . . . . . . . . . 15 (𝑃↑(1 − 1)) = (𝑃↑0)
10577ad2antlr 486 . . . . . . . . . . . . . . . . 17 (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → 𝑃 ∈ ℤ)
106105zcnd 9324 . . . . . . . . . . . . . . . 16 (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → 𝑃 ∈ ℂ)
107106exp0d 10592 . . . . . . . . . . . . . . 15 (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑃↑0) = 1)
108104, 107eqtrid 2215 . . . . . . . . . . . . . 14 (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑃↑(1 − 1)) = 1)
109108oveq2d 5867 . . . . . . . . . . . . 13 (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑘 · (𝑃↑(1 − 1))) = (𝑘 · 1))
11075adantl 275 . . . . . . . . . . . . . 14 (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℂ)
111110mulid1d 7926 . . . . . . . . . . . . 13 (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑘 · 1) = 𝑘)
112109, 111eqtrd 2203 . . . . . . . . . . . 12 (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑘 · (𝑃↑(1 − 1))) = 𝑘)
113112breq2d 3999 . . . . . . . . . . 11 (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝐷 ∥ (𝑘 · (𝑃↑(1 − 1))) ↔ 𝐷𝑘))
114113notbid 662 . . . . . . . . . 10 (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1))) ↔ ¬ 𝐷𝑘))
115102, 114anbi12d 470 . . . . . . . . 9 (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) ↔ (𝐷 ∥ (𝑘 · 𝑃) ∧ ¬ 𝐷𝑘)))
116106exp1d 10593 . . . . . . . . . 10 (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (𝑃↑1) = 𝑃)
117116breq1d 3997 . . . . . . . . 9 (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → ((𝑃↑1) ∥ 𝐷𝑃𝐷))
11897, 115, 1173imtr4d 202 . . . . . . . 8 (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) → (𝑃↑1) ∥ 𝐷))
119118ralrimiva 2543 . . . . . . 7 ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑1)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(1 − 1)))) → (𝑃↑1) ∥ 𝐷))
120 oveq1 5858 . . . . . . . . . . . . . 14 (𝑘 = 𝑥 → (𝑘 · (𝑃𝑛)) = (𝑥 · (𝑃𝑛)))
121120breq2d 3999 . . . . . . . . . . . . 13 (𝑘 = 𝑥 → (𝐷 ∥ (𝑘 · (𝑃𝑛)) ↔ 𝐷 ∥ (𝑥 · (𝑃𝑛))))
122 oveq1 5858 . . . . . . . . . . . . . . 15 (𝑘 = 𝑥 → (𝑘 · (𝑃↑(𝑛 − 1))) = (𝑥 · (𝑃↑(𝑛 − 1))))
123122breq2d 3999 . . . . . . . . . . . . . 14 (𝑘 = 𝑥 → (𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1))) ↔ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))))
124123notbid 662 . . . . . . . . . . . . 13 (𝑘 = 𝑥 → (¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1))) ↔ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))))
125121, 124anbi12d 470 . . . . . . . . . . . 12 (𝑘 = 𝑥 → ((𝐷 ∥ (𝑘 · (𝑃𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) ↔ (𝐷 ∥ (𝑥 · (𝑃𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1))))))
126125imbi1d 230 . . . . . . . . . . 11 (𝑘 = 𝑥 → (((𝐷 ∥ (𝑘 · (𝑃𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃𝑛) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑥 · (𝑃𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃𝑛) ∥ 𝐷)))
127126cbvralvw 2700 . . . . . . . . . 10 (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃𝑛) ∥ 𝐷) ↔ ∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃𝑛) ∥ 𝐷))
128 simprr 527 . . . . . . . . . . . . . . 15 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℤ)
12977ad2antrl 487 . . . . . . . . . . . . . . 15 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℤ)
130128, 129zmulcld 9329 . . . . . . . . . . . . . 14 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · 𝑃) ∈ ℤ)
131 oveq1 5858 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑘 · 𝑃) → (𝑥 · (𝑃𝑛)) = ((𝑘 · 𝑃) · (𝑃𝑛)))
132131breq2d 3999 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑘 · 𝑃) → (𝐷 ∥ (𝑥 · (𝑃𝑛)) ↔ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃𝑛))))
133 oveq1 5858 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑘 · 𝑃) → (𝑥 · (𝑃↑(𝑛 − 1))) = ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))))
134133breq2d 3999 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑘 · 𝑃) → (𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1))) ↔ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))))
135134notbid 662 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑘 · 𝑃) → (¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1))) ↔ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))))
136132, 135anbi12d 470 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑘 · 𝑃) → ((𝐷 ∥ (𝑥 · (𝑃𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) ↔ (𝐷 ∥ ((𝑘 · 𝑃) · (𝑃𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))))))
137136imbi1d 230 . . . . . . . . . . . . . . 15 (𝑥 = (𝑘 · 𝑃) → (((𝐷 ∥ (𝑥 · (𝑃𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃𝑛) ∥ 𝐷) ↔ ((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) → (𝑃𝑛) ∥ 𝐷)))
138137rspcv 2830 . . . . . . . . . . . . . 14 ((𝑘 · 𝑃) ∈ ℤ → (∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃𝑛) ∥ 𝐷) → ((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) → (𝑃𝑛) ∥ 𝐷)))
139130, 138syl 14 . . . . . . . . . . . . 13 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃𝑛) ∥ 𝐷) → ((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) → (𝑃𝑛) ∥ 𝐷)))
140 nnnn0 9131 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
141140ad2antrr 485 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑛 ∈ ℕ0)
142 zexpcl 10480 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ ℤ ∧ 𝑛 ∈ ℕ0) → (𝑃𝑛) ∈ ℤ)
143129, 141, 142syl2anc 409 . . . . . . . . . . . . . . . . . 18 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃𝑛) ∈ ℤ)
144 simplr 525 . . . . . . . . . . . . . . . . . 18 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝐷 ∈ ℤ)
145 divides 11740 . . . . . . . . . . . . . . . . . 18 (((𝑃𝑛) ∈ ℤ ∧ 𝐷 ∈ ℤ) → ((𝑃𝑛) ∥ 𝐷 ↔ ∃𝑥 ∈ ℤ (𝑥 · (𝑃𝑛)) = 𝐷))
146143, 144, 145syl2anc 409 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃𝑛) ∥ 𝐷 ↔ ∃𝑥 ∈ ℤ (𝑥 · (𝑃𝑛)) = 𝐷))
14794adantll 473 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥𝑘) → 𝑃𝑥))
14868ad2antrl 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℕ)
149148nncnd 8881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℂ)
150140ad2antrr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑛 ∈ ℕ0)
151149, 150expp1d 10599 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 + 1)) = ((𝑃𝑛) · 𝑃))
152148, 150nnexpcld 10620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃𝑛) ∈ ℕ)
153152nncnd 8881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃𝑛) ∈ ℂ)
154153, 149mulcomd 7930 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃𝑛) · 𝑃) = (𝑃 · (𝑃𝑛)))
155151, 154eqtrd 2203 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 + 1)) = (𝑃 · (𝑃𝑛)))
156155oveq2d 5867 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃↑(𝑛 + 1))) = (𝑘 · (𝑃 · (𝑃𝑛))))
15775ad2antll 488 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℂ)
158157, 149, 153mulassd 7932 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃𝑛)) = (𝑘 · (𝑃 · (𝑃𝑛))))
159156, 158eqtr4d 2206 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃↑(𝑛 + 1))) = ((𝑘 · 𝑃) · (𝑃𝑛)))
160159breq2d 3999 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 · (𝑃𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ↔ (𝑥 · (𝑃𝑛)) ∥ ((𝑘 · 𝑃) · (𝑃𝑛))))
161 simplr 525 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑥 ∈ ℤ)
162 simprr 527 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℤ)
163148nnzd 9322 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℤ)
164162, 163zmulcld 9329 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · 𝑃) ∈ ℤ)
165152nnzd 9322 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃𝑛) ∈ ℤ)
166152nnne0d 8912 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃𝑛) ≠ 0)
167 dvdsmulcr 11772 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 ∈ ℤ ∧ (𝑘 · 𝑃) ∈ ℤ ∧ ((𝑃𝑛) ∈ ℤ ∧ (𝑃𝑛) ≠ 0)) → ((𝑥 · (𝑃𝑛)) ∥ ((𝑘 · 𝑃) · (𝑃𝑛)) ↔ 𝑥 ∥ (𝑘 · 𝑃)))
168161, 164, 165, 166, 167syl112anc 1237 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 · (𝑃𝑛)) ∥ ((𝑘 · 𝑃) · (𝑃𝑛)) ↔ 𝑥 ∥ (𝑘 · 𝑃)))
169160, 168bitrd 187 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 · (𝑃𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ↔ 𝑥 ∥ (𝑘 · 𝑃)))
170 dvdsmulcr 11772 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ ((𝑃𝑛) ∈ ℤ ∧ (𝑃𝑛) ≠ 0)) → ((𝑥 · (𝑃𝑛)) ∥ (𝑘 · (𝑃𝑛)) ↔ 𝑥𝑘))
171161, 162, 165, 166, 170syl112anc 1237 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑥 · (𝑃𝑛)) ∥ (𝑘 · (𝑃𝑛)) ↔ 𝑥𝑘))
172171notbid 662 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (¬ (𝑥 · (𝑃𝑛)) ∥ (𝑘 · (𝑃𝑛)) ↔ ¬ 𝑥𝑘))
173169, 172anbi12d 470 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝑥 · (𝑃𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ (𝑥 · (𝑃𝑛)) ∥ (𝑘 · (𝑃𝑛))) ↔ (𝑥 ∥ (𝑘 · 𝑃) ∧ ¬ 𝑥𝑘)))
174155breq1d 3997 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃𝑛)) ↔ (𝑃 · (𝑃𝑛)) ∥ (𝑥 · (𝑃𝑛))))
175 dvdsmulcr 11772 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑃 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ ((𝑃𝑛) ∈ ℤ ∧ (𝑃𝑛) ≠ 0)) → ((𝑃 · (𝑃𝑛)) ∥ (𝑥 · (𝑃𝑛)) ↔ 𝑃𝑥))
176163, 161, 165, 166, 175syl112anc 1237 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃 · (𝑃𝑛)) ∥ (𝑥 · (𝑃𝑛)) ↔ 𝑃𝑥))
177174, 176bitrd 187 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃𝑛)) ↔ 𝑃𝑥))
178147, 173, 1773imtr4d 202 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝑥 · (𝑃𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ (𝑥 · (𝑃𝑛)) ∥ (𝑘 · (𝑃𝑛))) → (𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃𝑛))))
179178an32s 563 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ ℕ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∈ ℤ) → (((𝑥 · (𝑃𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ (𝑥 · (𝑃𝑛)) ∥ (𝑘 · (𝑃𝑛))) → (𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃𝑛))))
180 breq1 3990 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 · (𝑃𝑛)) = 𝐷 → ((𝑥 · (𝑃𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1)))))
181 breq1 3990 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 · (𝑃𝑛)) = 𝐷 → ((𝑥 · (𝑃𝑛)) ∥ (𝑘 · (𝑃𝑛)) ↔ 𝐷 ∥ (𝑘 · (𝑃𝑛))))
182181notbid 662 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 · (𝑃𝑛)) = 𝐷 → (¬ (𝑥 · (𝑃𝑛)) ∥ (𝑘 · (𝑃𝑛)) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃𝑛))))
183180, 182anbi12d 470 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 · (𝑃𝑛)) = 𝐷 → (((𝑥 · (𝑃𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ (𝑥 · (𝑃𝑛)) ∥ (𝑘 · (𝑃𝑛))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃𝑛)))))
184 breq2 3991 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 · (𝑃𝑛)) = 𝐷 → ((𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃𝑛)) ↔ (𝑃↑(𝑛 + 1)) ∥ 𝐷))
185183, 184imbi12d 233 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 · (𝑃𝑛)) = 𝐷 → ((((𝑥 · (𝑃𝑛)) ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ (𝑥 · (𝑃𝑛)) ∥ (𝑘 · (𝑃𝑛))) → (𝑃↑(𝑛 + 1)) ∥ (𝑥 · (𝑃𝑛))) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
186179, 185syl5ibcom 154 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ ℕ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) ∧ 𝑥 ∈ ℤ) → ((𝑥 · (𝑃𝑛)) = 𝐷 → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
187186rexlimdva 2587 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (∃𝑥 ∈ ℤ (𝑥 · (𝑃𝑛)) = 𝐷 → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
188187adantlr 474 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (∃𝑥 ∈ ℤ (𝑥 · (𝑃𝑛)) = 𝐷 → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
189146, 188sylbid 149 . . . . . . . . . . . . . . . 16 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑃𝑛) ∥ 𝐷 → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
190189com23 78 . . . . . . . . . . . . . . 15 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃𝑛))) → ((𝑃𝑛) ∥ 𝐷 → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
191190a2d 26 . . . . . . . . . . . . . 14 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃𝑛))) → (𝑃𝑛) ∥ 𝐷) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
19275ad2antll 488 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℂ)
193129zcnd 9324 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑃 ∈ ℂ)
194143zcnd 9324 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃𝑛) ∈ ℂ)
195192, 193, 194mulassd 7932 . . . . . . . . . . . . . . . . . 18 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃𝑛)) = (𝑘 · (𝑃 · (𝑃𝑛))))
196193, 194mulcomd 7930 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 · (𝑃𝑛)) = ((𝑃𝑛) · 𝑃))
197193, 141expp1d 10599 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 + 1)) = ((𝑃𝑛) · 𝑃))
198196, 197eqtr4d 2206 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 · (𝑃𝑛)) = (𝑃↑(𝑛 + 1)))
199198oveq2d 5867 . . . . . . . . . . . . . . . . . 18 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃 · (𝑃𝑛))) = (𝑘 · (𝑃↑(𝑛 + 1))))
200195, 199eqtrd 2203 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃𝑛)) = (𝑘 · (𝑃↑(𝑛 + 1))))
201200breq2d 3999 . . . . . . . . . . . . . . . 16 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝐷 ∥ ((𝑘 · 𝑃) · (𝑃𝑛)) ↔ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1)))))
202 nnm1nn0 9165 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ0)
203202ad2antrr 485 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑛 − 1) ∈ ℕ0)
204 zexpcl 10480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃 ∈ ℤ ∧ (𝑛 − 1) ∈ ℕ0) → (𝑃↑(𝑛 − 1)) ∈ ℤ)
205129, 203, 204syl2anc 409 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 − 1)) ∈ ℤ)
206205zcnd 9324 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑(𝑛 − 1)) ∈ ℂ)
207192, 193, 206mulassd 7932 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))) = (𝑘 · (𝑃 · (𝑃↑(𝑛 − 1)))))
208193, 206mulcomd 7930 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 · (𝑃↑(𝑛 − 1))) = ((𝑃↑(𝑛 − 1)) · 𝑃))
209 simpll 524 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑛 ∈ ℕ)
210 expm1t 10493 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃 ∈ ℂ ∧ 𝑛 ∈ ℕ) → (𝑃𝑛) = ((𝑃↑(𝑛 − 1)) · 𝑃))
211193, 209, 210syl2anc 409 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃𝑛) = ((𝑃↑(𝑛 − 1)) · 𝑃))
212208, 211eqtr4d 2206 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃 · (𝑃↑(𝑛 − 1))) = (𝑃𝑛))
213212oveq2d 5867 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃 · (𝑃↑(𝑛 − 1)))) = (𝑘 · (𝑃𝑛)))
214207, 213eqtrd 2203 . . . . . . . . . . . . . . . . . 18 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))) = (𝑘 · (𝑃𝑛)))
215214breq2d 3999 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃𝑛))))
216215notbid 662 . . . . . . . . . . . . . . . 16 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃𝑛))))
217201, 216anbi12d 470 . . . . . . . . . . . . . . 15 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃𝑛)))))
218217imbi1d 230 . . . . . . . . . . . . . 14 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) → (𝑃𝑛) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃𝑛))) → (𝑃𝑛) ∥ 𝐷)))
219 nncn 8875 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
220219ad2antrr 485 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → 𝑛 ∈ ℂ)
221 ax-1cn 7856 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℂ
222 pncan 8114 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 1) = 𝑛)
223220, 221, 222sylancl 411 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝑛 + 1) − 1) = 𝑛)
224223oveq2d 5867 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑃↑((𝑛 + 1) − 1)) = (𝑃𝑛))
225224oveq2d 5867 . . . . . . . . . . . . . . . . . 18 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝑘 · (𝑃↑((𝑛 + 1) − 1))) = (𝑘 · (𝑃𝑛)))
226225breq2d 3999 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1))) ↔ 𝐷 ∥ (𝑘 · (𝑃𝑛))))
227226notbid 662 . . . . . . . . . . . . . . . 16 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1))) ↔ ¬ 𝐷 ∥ (𝑘 · (𝑃𝑛))))
228227anbi2d 461 . . . . . . . . . . . . . . 15 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) ↔ (𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃𝑛)))))
229228imbi1d 230 . . . . . . . . . . . . . 14 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷) ↔ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃𝑛))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
230191, 218, 2293imtr4d 202 . . . . . . . . . . . . 13 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (((𝐷 ∥ ((𝑘 · 𝑃) · (𝑃𝑛)) ∧ ¬ 𝐷 ∥ ((𝑘 · 𝑃) · (𝑃↑(𝑛 − 1)))) → (𝑃𝑛) ∥ 𝐷) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
231139, 230syld 45 . . . . . . . . . . . 12 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ)) → (∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃𝑛) ∥ 𝐷) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
232231anassrs 398 . . . . . . . . . . 11 ((((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ ℤ) → (∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃𝑛) ∥ 𝐷) → ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
233232ralrimdva 2550 . . . . . . . . . 10 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ 𝑃 ∈ ℙ) → (∀𝑥 ∈ ℤ ((𝐷 ∥ (𝑥 · (𝑃𝑛)) ∧ ¬ 𝐷 ∥ (𝑥 · (𝑃↑(𝑛 − 1)))) → (𝑃𝑛) ∥ 𝐷) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
234127, 233syl5bi 151 . . . . . . . . 9 (((𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ) ∧ 𝑃 ∈ ℙ) → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃𝑛) ∥ 𝐷) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷)))
235234expl 376 . . . . . . . 8 (𝑛 ∈ ℕ → ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → (∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃𝑛) ∥ 𝐷) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷))))
236235a2d 26 . . . . . . 7 (𝑛 ∈ ℕ → (((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃𝑛)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑛 − 1)))) → (𝑃𝑛) ∥ 𝐷)) → ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃↑(𝑛 + 1))) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑((𝑛 + 1) − 1)))) → (𝑃↑(𝑛 + 1)) ∥ 𝐷))))
23720, 33, 46, 59, 119, 236nnind 8883 . . . . . 6 (𝑁 ∈ ℕ → ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃𝑁) ∥ 𝐷)))
238237com12 30 . . . . 5 ((𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ) → (𝑁 ∈ ℕ → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃𝑁) ∥ 𝐷)))
239238impr 377 . . . 4 ((𝐷 ∈ ℤ ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ)) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃𝑁) ∥ 𝐷))
240239adantll 473 . . 3 (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ)) → ∀𝑘 ∈ ℤ ((𝐷 ∥ (𝑘 · (𝑃𝑁)) ∧ ¬ 𝐷 ∥ (𝑘 · (𝑃↑(𝑁 − 1)))) → (𝑃𝑁) ∥ 𝐷))
241 simpll 524 . . 3 (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ)) → 𝐾 ∈ ℤ)
2427, 240, 241rspcdva 2839 . 2 (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ)) → ((𝐷 ∥ (𝐾 · (𝑃𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1)))) → (𝑃𝑁) ∥ 𝐷))
2432423impia 1195 1 (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) ∧ (𝐷 ∥ (𝐾 · (𝑃𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1))))) → (𝑃𝑁) ∥ 𝐷)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104  DECID wdc 829  w3a 973   = wceq 1348  wcel 2141  wne 2340  wral 2448  wrex 2449   class class class wbr 3987  (class class class)co 5851  cc 7761  0cc0 7763  1c1 7764   + caddc 7766   · cmul 7768  cmin 8079  cn 8867  0cn0 9124  cz 9201  cexp 10464  cdvds 11738   gcd cgcd 11886  cprime 12050
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4102  ax-sep 4105  ax-nul 4113  ax-pow 4158  ax-pr 4192  ax-un 4416  ax-setind 4519  ax-iinf 4570  ax-cnex 7854  ax-resscn 7855  ax-1cn 7856  ax-1re 7857  ax-icn 7858  ax-addcl 7859  ax-addrcl 7860  ax-mulcl 7861  ax-mulrcl 7862  ax-addcom 7863  ax-mulcom 7864  ax-addass 7865  ax-mulass 7866  ax-distr 7867  ax-i2m1 7868  ax-0lt1 7869  ax-1rid 7870  ax-0id 7871  ax-rnegex 7872  ax-precex 7873  ax-cnre 7874  ax-pre-ltirr 7875  ax-pre-ltwlin 7876  ax-pre-lttrn 7877  ax-pre-apti 7878  ax-pre-ltadd 7879  ax-pre-mulgt0 7880  ax-pre-mulext 7881  ax-arch 7882  ax-caucvg 7883
This theorem depends on definitions:  df-bi 116  df-stab 826  df-dc 830  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-nel 2436  df-ral 2453  df-rex 2454  df-reu 2455  df-rmo 2456  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-if 3526  df-pw 3566  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-int 3830  df-iun 3873  df-br 3988  df-opab 4049  df-mpt 4050  df-tr 4086  df-id 4276  df-po 4279  df-iso 4280  df-iord 4349  df-on 4351  df-ilim 4352  df-suc 4354  df-iom 4573  df-xp 4615  df-rel 4616  df-cnv 4617  df-co 4618  df-dm 4619  df-rn 4620  df-res 4621  df-ima 4622  df-iota 5158  df-fun 5198  df-fn 5199  df-f 5200  df-f1 5201  df-fo 5202  df-f1o 5203  df-fv 5204  df-riota 5807  df-ov 5854  df-oprab 5855  df-mpo 5856  df-1st 6117  df-2nd 6118  df-recs 6282  df-frec 6368  df-1o 6393  df-2o 6394  df-er 6510  df-en 6716  df-sup 6958  df-pnf 7945  df-mnf 7946  df-xr 7947  df-ltxr 7948  df-le 7949  df-sub 8081  df-neg 8082  df-reap 8483  df-ap 8490  df-div 8579  df-inn 8868  df-2 8926  df-3 8927  df-4 8928  df-n0 9125  df-z 9202  df-uz 9477  df-q 9568  df-rp 9600  df-fz 9955  df-fzo 10088  df-fl 10215  df-mod 10268  df-seqfrec 10391  df-exp 10465  df-cj 10795  df-re 10796  df-im 10797  df-rsqrt 10951  df-abs 10952  df-dvds 11739  df-gcd 11887  df-prm 12051
This theorem is referenced by:  pockthlem  12297
  Copyright terms: Public domain W3C validator