Metamath Proof Explorer

Theorem prmpwdvds

Description: A relation involving divisibility by a prime power. (Contributed by Mario Carneiro, 2-Mar-2014)

Ref Expression
Assertion prmpwdvds ( ( ( 𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐷 ∥ ( 𝐾 · ( 𝑃 ↑ 𝑁 ) ) ∧ ¬ 𝐷 ∥ ( 𝐾 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) ) ) → ( 𝑃 ↑ 𝑁 ) ∥ 𝐷 )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑘 = 𝐾 → ( 𝑘 · ( 𝑃 ↑ 𝑁 ) ) = ( 𝐾 · ( 𝑃 ↑ 𝑁 ) ) )
2 1 breq2d ⊢ ( 𝑘 = 𝐾 → ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑁 ) ) ↔ 𝐷 ∥ ( 𝐾 · ( 𝑃 ↑ 𝑁 ) ) ) )
3 oveq1 ⊢ ( 𝑘 = 𝐾 → ( 𝑘 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) = ( 𝐾 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) )
4 3 breq2d ⊢ ( 𝑘 = 𝐾 → ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) ↔ 𝐷 ∥ ( 𝐾 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) ) )
5 4 notbid ⊢ ( 𝑘 = 𝐾 → ( ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) ↔ ¬ 𝐷 ∥ ( 𝐾 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) ) )
6 2 5 anbi12d ⊢ ( 𝑘 = 𝐾 → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑁 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) ) ↔ ( 𝐷 ∥ ( 𝐾 · ( 𝑃 ↑ 𝑁 ) ) ∧ ¬ 𝐷 ∥ ( 𝐾 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) ) ) )
7 6 imbi1d ⊢ ( 𝑘 = 𝐾 → ( ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑁 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑁 ) ∥ 𝐷 ) ↔ ( ( 𝐷 ∥ ( 𝐾 · ( 𝑃 ↑ 𝑁 ) ) ∧ ¬ 𝐷 ∥ ( 𝐾 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑁 ) ∥ 𝐷 ) ) )
8 oveq2 ⊢ ( 𝑥 = 1 → ( 𝑃 ↑ 𝑥 ) = ( 𝑃 ↑ 1 ) )
9 8 oveq2d ⊢ ( 𝑥 = 1 → ( 𝑘 · ( 𝑃 ↑ 𝑥 ) ) = ( 𝑘 · ( 𝑃 ↑ 1 ) ) )
10 9 breq2d ⊢ ( 𝑥 = 1 → ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑥 ) ) ↔ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 1 ) ) ) )
11 oveq1 ⊢ ( 𝑥 = 1 → ( 𝑥 − 1 ) = ( 1 − 1 ) )
12 11 oveq2d ⊢ ( 𝑥 = 1 → ( 𝑃 ↑ ( 𝑥 − 1 ) ) = ( 𝑃 ↑ ( 1 − 1 ) ) )
13 12 oveq2d ⊢ ( 𝑥 = 1 → ( 𝑘 · ( 𝑃 ↑ ( 𝑥 − 1 ) ) ) = ( 𝑘 · ( 𝑃 ↑ ( 1 − 1 ) ) ) )
14 13 breq2d ⊢ ( 𝑥 = 1 → ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑥 − 1 ) ) ) ↔ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 1 − 1 ) ) ) ) )
15 14 notbid ⊢ ( 𝑥 = 1 → ( ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑥 − 1 ) ) ) ↔ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 1 − 1 ) ) ) ) )
16 10 15 anbi12d ⊢ ( 𝑥 = 1 → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑥 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑥 − 1 ) ) ) ) ↔ ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 1 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 1 − 1 ) ) ) ) ) )
17 8 breq1d ⊢ ( 𝑥 = 1 → ( ( 𝑃 ↑ 𝑥 ) ∥ 𝐷 ↔ ( 𝑃 ↑ 1 ) ∥ 𝐷 ) )
18 16 17 imbi12d ⊢ ( 𝑥 = 1 → ( ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑥 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑥 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑥 ) ∥ 𝐷 ) ↔ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 1 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 1 − 1 ) ) ) ) → ( 𝑃 ↑ 1 ) ∥ 𝐷 ) ) )
19 18 ralbidv ⊢ ( 𝑥 = 1 → ( ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑥 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑥 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑥 ) ∥ 𝐷 ) ↔ ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 1 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 1 − 1 ) ) ) ) → ( 𝑃 ↑ 1 ) ∥ 𝐷 ) ) )
20 19 imbi2d ⊢ ( 𝑥 = 1 → ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑥 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑥 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑥 ) ∥ 𝐷 ) ) ↔ ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 1 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 1 − 1 ) ) ) ) → ( 𝑃 ↑ 1 ) ∥ 𝐷 ) ) ) )
21 oveq2 ⊢ ( 𝑥 = 𝑛 → ( 𝑃 ↑ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) )
22 21 oveq2d ⊢ ( 𝑥 = 𝑛 → ( 𝑘 · ( 𝑃 ↑ 𝑥 ) ) = ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) )
23 22 breq2d ⊢ ( 𝑥 = 𝑛 → ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑥 ) ) ↔ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) )
24 oveq1 ⊢ ( 𝑥 = 𝑛 → ( 𝑥 − 1 ) = ( 𝑛 − 1 ) )
25 24 oveq2d ⊢ ( 𝑥 = 𝑛 → ( 𝑃 ↑ ( 𝑥 − 1 ) ) = ( 𝑃 ↑ ( 𝑛 − 1 ) ) )
26 25 oveq2d ⊢ ( 𝑥 = 𝑛 → ( 𝑘 · ( 𝑃 ↑ ( 𝑥 − 1 ) ) ) = ( 𝑘 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) )
27 26 breq2d ⊢ ( 𝑥 = 𝑛 → ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑥 − 1 ) ) ) ↔ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) )
28 27 notbid ⊢ ( 𝑥 = 𝑛 → ( ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑥 − 1 ) ) ) ↔ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) )
29 23 28 anbi12d ⊢ ( 𝑥 = 𝑛 → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑥 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑥 − 1 ) ) ) ) ↔ ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) ) )
30 21 breq1d ⊢ ( 𝑥 = 𝑛 → ( ( 𝑃 ↑ 𝑥 ) ∥ 𝐷 ↔ ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) )
31 29 30 imbi12d ⊢ ( 𝑥 = 𝑛 → ( ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑥 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑥 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑥 ) ∥ 𝐷 ) ↔ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) ) )
32 31 ralbidv ⊢ ( 𝑥 = 𝑛 → ( ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑥 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑥 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑥 ) ∥ 𝐷 ) ↔ ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) ) )
33 32 imbi2d ⊢ ( 𝑥 = 𝑛 → ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑥 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑥 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑥 ) ∥ 𝐷 ) ) ↔ ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) ) ) )
34 oveq2 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑃 ↑ 𝑥 ) = ( 𝑃 ↑ ( 𝑛 + 1 ) ) )
35 34 oveq2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑘 · ( 𝑃 ↑ 𝑥 ) ) = ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) )
36 35 breq2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑥 ) ) ↔ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ) )
37 oveq1 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑥 − 1 ) = ( ( 𝑛 + 1 ) − 1 ) )
38 37 oveq2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑃 ↑ ( 𝑥 − 1 ) ) = ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) )
39 38 oveq2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑘 · ( 𝑃 ↑ ( 𝑥 − 1 ) ) ) = ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) )
40 39 breq2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑥 − 1 ) ) ) ↔ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) ) )
41 40 notbid ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑥 − 1 ) ) ) ↔ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) ) )
42 36 41 anbi12d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑥 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑥 − 1 ) ) ) ) ↔ ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) ) ) )
43 34 breq1d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝑃 ↑ 𝑥 ) ∥ 𝐷 ↔ ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) )
44 42 43 imbi12d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑥 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑥 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑥 ) ∥ 𝐷 ) ↔ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) )
45 44 ralbidv ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑥 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑥 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑥 ) ∥ 𝐷 ) ↔ ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) )
46 45 imbi2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑥 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑥 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑥 ) ∥ 𝐷 ) ) ↔ ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) ) )
47 oveq2 ⊢ ( 𝑥 = 𝑁 → ( 𝑃 ↑ 𝑥 ) = ( 𝑃 ↑ 𝑁 ) )
48 47 oveq2d ⊢ ( 𝑥 = 𝑁 → ( 𝑘 · ( 𝑃 ↑ 𝑥 ) ) = ( 𝑘 · ( 𝑃 ↑ 𝑁 ) ) )
49 48 breq2d ⊢ ( 𝑥 = 𝑁 → ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑥 ) ) ↔ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑁 ) ) ) )
50 oveq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 − 1 ) = ( 𝑁 − 1 ) )
51 50 oveq2d ⊢ ( 𝑥 = 𝑁 → ( 𝑃 ↑ ( 𝑥 − 1 ) ) = ( 𝑃 ↑ ( 𝑁 − 1 ) ) )
52 51 oveq2d ⊢ ( 𝑥 = 𝑁 → ( 𝑘 · ( 𝑃 ↑ ( 𝑥 − 1 ) ) ) = ( 𝑘 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) )
53 52 breq2d ⊢ ( 𝑥 = 𝑁 → ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑥 − 1 ) ) ) ↔ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) ) )
54 53 notbid ⊢ ( 𝑥 = 𝑁 → ( ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑥 − 1 ) ) ) ↔ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) ) )
55 49 54 anbi12d ⊢ ( 𝑥 = 𝑁 → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑥 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑥 − 1 ) ) ) ) ↔ ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑁 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) ) ) )
56 47 breq1d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑃 ↑ 𝑥 ) ∥ 𝐷 ↔ ( 𝑃 ↑ 𝑁 ) ∥ 𝐷 ) )
57 55 56 imbi12d ⊢ ( 𝑥 = 𝑁 → ( ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑥 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑥 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑥 ) ∥ 𝐷 ) ↔ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑁 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑁 ) ∥ 𝐷 ) ) )
58 57 ralbidv ⊢ ( 𝑥 = 𝑁 → ( ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑥 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑥 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑥 ) ∥ 𝐷 ) ↔ ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑁 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑁 ) ∥ 𝐷 ) ) )
59 58 imbi2d ⊢ ( 𝑥 = 𝑁 → ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑥 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑥 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑥 ) ∥ 𝐷 ) ) ↔ ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑁 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑁 ) ∥ 𝐷 ) ) ) )
60 breq1 ⊢ ( 𝑥 = 𝐷 → ( 𝑥 ∥ ( 𝑘 · 𝑃 ) ↔ 𝐷 ∥ ( 𝑘 · 𝑃 ) ) )
61 breq1 ⊢ ( 𝑥 = 𝐷 → ( 𝑥 ∥ 𝑘 ↔ 𝐷 ∥ 𝑘 ) )
62 61 notbid ⊢ ( 𝑥 = 𝐷 → ( ¬ 𝑥 ∥ 𝑘 ↔ ¬ 𝐷 ∥ 𝑘 ) )
63 60 62 anbi12d ⊢ ( 𝑥 = 𝐷 → ( ( 𝑥 ∥ ( 𝑘 · 𝑃 ) ∧ ¬ 𝑥 ∥ 𝑘 ) ↔ ( 𝐷 ∥ ( 𝑘 · 𝑃 ) ∧ ¬ 𝐷 ∥ 𝑘 ) ) )
64 breq2 ⊢ ( 𝑥 = 𝐷 → ( 𝑃 ∥ 𝑥 ↔ 𝑃 ∥ 𝐷 ) )
65 63 64 imbi12d ⊢ ( 𝑥 = 𝐷 → ( ( ( 𝑥 ∥ ( 𝑘 · 𝑃 ) ∧ ¬ 𝑥 ∥ 𝑘 ) → 𝑃 ∥ 𝑥 ) ↔ ( ( 𝐷 ∥ ( 𝑘 · 𝑃 ) ∧ ¬ 𝐷 ∥ 𝑘 ) → 𝑃 ∥ 𝐷 ) ) )
66 65 imbi2d ⊢ ( 𝑥 = 𝐷 → ( ( ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑥 ∥ ( 𝑘 · 𝑃 ) ∧ ¬ 𝑥 ∥ 𝑘 ) → 𝑃 ∥ 𝑥 ) ) ↔ ( ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) → ( ( 𝐷 ∥ ( 𝑘 · 𝑃 ) ∧ ¬ 𝐷 ∥ 𝑘 ) → 𝑃 ∥ 𝐷 ) ) ) )
67 simplrl ⊢ ( ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) ∧ 𝑥 ∥ ( 𝑘 · 𝑃 ) ) → 𝑃 ∈ ℙ )
68 simpll ⊢ ( ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) ∧ 𝑥 ∥ ( 𝑘 · 𝑃 ) ) → 𝑥 ∈ ℤ )
69 coprm ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ ) → ( ¬ 𝑃 ∥ 𝑥 ↔ ( 𝑃 gcd 𝑥 ) = 1 ) )
70 67 68 69 syl2anc ⊢ ( ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) ∧ 𝑥 ∥ ( 𝑘 · 𝑃 ) ) → ( ¬ 𝑃 ∥ 𝑥 ↔ ( 𝑃 gcd 𝑥 ) = 1 ) )
71 zcn ⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℂ )
72 71 ad2antll ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑘 ∈ ℂ )
73 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
74 73 ad2antrl ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑃 ∈ ℤ )
75 74 zcnd ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑃 ∈ ℂ )
76 72 75 mulcomd ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑘 · 𝑃 ) = ( 𝑃 · 𝑘 ) )
77 76 breq2d ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑥 ∥ ( 𝑘 · 𝑃 ) ↔ 𝑥 ∥ ( 𝑃 · 𝑘 ) ) )
78 simpl ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑥 ∈ ℤ )
79 gcdcom ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( 𝑃 gcd 𝑥 ) = ( 𝑥 gcd 𝑃 ) )
80 74 78 79 syl2anc ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 gcd 𝑥 ) = ( 𝑥 gcd 𝑃 ) )
81 80 eqeq1d ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑃 gcd 𝑥 ) = 1 ↔ ( 𝑥 gcd 𝑃 ) = 1 ) )
82 77 81 anbi12d ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑥 ∥ ( 𝑘 · 𝑃 ) ∧ ( 𝑃 gcd 𝑥 ) = 1 ) ↔ ( 𝑥 ∥ ( 𝑃 · 𝑘 ) ∧ ( 𝑥 gcd 𝑃 ) = 1 ) ) )
83 simprr ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑘 ∈ ℤ )
84 coprmdvds ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑥 ∥ ( 𝑃 · 𝑘 ) ∧ ( 𝑥 gcd 𝑃 ) = 1 ) → 𝑥 ∥ 𝑘 ) )
85 78 74 83 84 syl3anc ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑥 ∥ ( 𝑃 · 𝑘 ) ∧ ( 𝑥 gcd 𝑃 ) = 1 ) → 𝑥 ∥ 𝑘 ) )
86 82 85 sylbid ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑥 ∥ ( 𝑘 · 𝑃 ) ∧ ( 𝑃 gcd 𝑥 ) = 1 ) → 𝑥 ∥ 𝑘 ) )
87 86 expdimp ⊢ ( ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) ∧ 𝑥 ∥ ( 𝑘 · 𝑃 ) ) → ( ( 𝑃 gcd 𝑥 ) = 1 → 𝑥 ∥ 𝑘 ) )
88 70 87 sylbid ⊢ ( ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) ∧ 𝑥 ∥ ( 𝑘 · 𝑃 ) ) → ( ¬ 𝑃 ∥ 𝑥 → 𝑥 ∥ 𝑘 ) )
89 88 con1d ⊢ ( ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) ∧ 𝑥 ∥ ( 𝑘 · 𝑃 ) ) → ( ¬ 𝑥 ∥ 𝑘 → 𝑃 ∥ 𝑥 ) )
90 89 expimpd ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑥 ∥ ( 𝑘 · 𝑃 ) ∧ ¬ 𝑥 ∥ 𝑘 ) → 𝑃 ∥ 𝑥 ) )
91 90 ex ⊢ ( 𝑥 ∈ ℤ → ( ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑥 ∥ ( 𝑘 · 𝑃 ) ∧ ¬ 𝑥 ∥ 𝑘 ) → 𝑃 ∥ 𝑥 ) ) )
92 66 91 vtoclga ⊢ ( 𝐷 ∈ ℤ → ( ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) → ( ( 𝐷 ∥ ( 𝑘 · 𝑃 ) ∧ ¬ 𝐷 ∥ 𝑘 ) → 𝑃 ∥ 𝐷 ) ) )
93 92 impl ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝐷 ∥ ( 𝑘 · 𝑃 ) ∧ ¬ 𝐷 ∥ 𝑘 ) → 𝑃 ∥ 𝐷 ) )
94 73 zcnd ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℂ )
95 94 exp1d ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ↑ 1 ) = 𝑃 )
96 95 ad2antlr ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( 𝑃 ↑ 1 ) = 𝑃 )
97 96 oveq2d ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( 𝑘 · ( 𝑃 ↑ 1 ) ) = ( 𝑘 · 𝑃 ) )
98 97 breq2d ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 1 ) ) ↔ 𝐷 ∥ ( 𝑘 · 𝑃 ) ) )
99 1m1e0 ⊢ ( 1 − 1 ) = 0
100 99 oveq2i ⊢ ( 𝑃 ↑ ( 1 − 1 ) ) = ( 𝑃 ↑ 0 )
101 73 ad2antlr ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → 𝑃 ∈ ℤ )
102 101 zcnd ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → 𝑃 ∈ ℂ )
103 102 exp0d ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( 𝑃 ↑ 0 ) = 1 )
104 100 103 syl5eq ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( 𝑃 ↑ ( 1 − 1 ) ) = 1 )
105 104 oveq2d ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( 𝑘 · ( 𝑃 ↑ ( 1 − 1 ) ) ) = ( 𝑘 · 1 ) )
106 71 adantl ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → 𝑘 ∈ ℂ )
107 106 mulid1d ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( 𝑘 · 1 ) = 𝑘 )
108 105 107 eqtrd ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( 𝑘 · ( 𝑃 ↑ ( 1 − 1 ) ) ) = 𝑘 )
109 108 breq2d ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 1 − 1 ) ) ) ↔ 𝐷 ∥ 𝑘 ) )
110 109 notbid ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 1 − 1 ) ) ) ↔ ¬ 𝐷 ∥ 𝑘 ) )
111 98 110 anbi12d ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 1 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 1 − 1 ) ) ) ) ↔ ( 𝐷 ∥ ( 𝑘 · 𝑃 ) ∧ ¬ 𝐷 ∥ 𝑘 ) ) )
112 102 exp1d ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( 𝑃 ↑ 1 ) = 𝑃 )
113 112 breq1d ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝑃 ↑ 1 ) ∥ 𝐷 ↔ 𝑃 ∥ 𝐷 ) )
114 93 111 113 3imtr4d ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 1 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 1 − 1 ) ) ) ) → ( 𝑃 ↑ 1 ) ∥ 𝐷 ) )
115 114 ralrimiva ⊢ ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 1 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 1 − 1 ) ) ) ) → ( 𝑃 ↑ 1 ) ∥ 𝐷 ) )
116 oveq1 ⊢ ( 𝑘 = 𝑥 → ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) = ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) )
117 116 breq2d ⊢ ( 𝑘 = 𝑥 → ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ↔ 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ) )
118 oveq1 ⊢ ( 𝑘 = 𝑥 → ( 𝑘 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) = ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) )
119 118 breq2d ⊢ ( 𝑘 = 𝑥 → ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ↔ 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) )
120 119 notbid ⊢ ( 𝑘 = 𝑥 → ( ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ↔ ¬ 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) )
121 117 120 anbi12d ⊢ ( 𝑘 = 𝑥 → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) ↔ ( 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) ) )
122 121 imbi1d ⊢ ( 𝑘 = 𝑥 → ( ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) ↔ ( ( 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) ) )
123 122 cbvralvw ⊢ ( ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) ↔ ∀ 𝑥 ∈ ℤ ( ( 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) )
124 simprr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑘 ∈ ℤ )
125 73 ad2antrl ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑃 ∈ ℤ )
126 124 125 zmulcld ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑘 · 𝑃 ) ∈ ℤ )
127 oveq1 ⊢ ( 𝑥 = ( 𝑘 · 𝑃 ) → ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) = ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) )
128 127 breq2d ⊢ ( 𝑥 = ( 𝑘 · 𝑃 ) → ( 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ↔ 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) ) )
129 oveq1 ⊢ ( 𝑥 = ( 𝑘 · 𝑃 ) → ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) = ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) )
130 129 breq2d ⊢ ( 𝑥 = ( 𝑘 · 𝑃 ) → ( 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ↔ 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) )
131 130 notbid ⊢ ( 𝑥 = ( 𝑘 · 𝑃 ) → ( ¬ 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ↔ ¬ 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) )
132 128 131 anbi12d ⊢ ( 𝑥 = ( 𝑘 · 𝑃 ) → ( ( 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) ↔ ( 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) ) )
133 132 imbi1d ⊢ ( 𝑥 = ( 𝑘 · 𝑃 ) → ( ( ( 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) ↔ ( ( 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) ) )
134 133 rspcv ⊢ ( ( 𝑘 · 𝑃 ) ∈ ℤ → ( ∀ 𝑥 ∈ ℤ ( ( 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) → ( ( 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) ) )
135 126 134 syl ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ∀ 𝑥 ∈ ℤ ( ( 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) → ( ( 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) ) )
136 nnnn0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
137 136 ad2antrr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑛 ∈ ℕ0 )
138 zexpcl ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑛 ∈ ℕ0 ) → ( 𝑃 ↑ 𝑛 ) ∈ ℤ )
139 125 137 138 syl2anc ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 ↑ 𝑛 ) ∈ ℤ )
140 simplr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝐷 ∈ ℤ )
141 divides ⊢ ( ( ( 𝑃 ↑ 𝑛 ) ∈ ℤ ∧ 𝐷 ∈ ℤ ) → ( ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ↔ ∃ 𝑥 ∈ ℤ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) = 𝐷 ) )
142 139 140 141 syl2anc ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ↔ ∃ 𝑥 ∈ ℤ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) = 𝐷 ) )
143 90 adantll ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑥 ∥ ( 𝑘 · 𝑃 ) ∧ ¬ 𝑥 ∥ 𝑘 ) → 𝑃 ∥ 𝑥 ) )
144 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
145 144 ad2antrl ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑃 ∈ ℕ )
146 145 nncnd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑃 ∈ ℂ )
147 136 ad2antrr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑛 ∈ ℕ0 )
148 146 147 expp1d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) = ( ( 𝑃 ↑ 𝑛 ) · 𝑃 ) )
149 145 147 nnexpcld ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 ↑ 𝑛 ) ∈ ℕ )
150 149 nncnd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 ↑ 𝑛 ) ∈ ℂ )
151 150 146 mulcomd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑃 ↑ 𝑛 ) · 𝑃 ) = ( 𝑃 · ( 𝑃 ↑ 𝑛 ) ) )
152 148 151 eqtrd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) = ( 𝑃 · ( 𝑃 ↑ 𝑛 ) ) )
153 152 oveq2d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) = ( 𝑘 · ( 𝑃 · ( 𝑃 ↑ 𝑛 ) ) ) )
154 71 ad2antll ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑘 ∈ ℂ )
155 154 146 150 mulassd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) = ( 𝑘 · ( 𝑃 · ( 𝑃 ↑ 𝑛 ) ) ) )
156 153 155 eqtr4d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) = ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) )
157 156 breq2d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ↔ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) ) )
158 simplr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑥 ∈ ℤ )
159 simprr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑘 ∈ ℤ )
160 145 nnzd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑃 ∈ ℤ )
161 159 160 zmulcld ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑘 · 𝑃 ) ∈ ℤ )
162 149 nnzd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 ↑ 𝑛 ) ∈ ℤ )
163 149 nnne0d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 ↑ 𝑛 ) ≠ 0 )
164 dvdsmulcr ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑘 · 𝑃 ) ∈ ℤ ∧ ( ( 𝑃 ↑ 𝑛 ) ∈ ℤ ∧ ( 𝑃 ↑ 𝑛 ) ≠ 0 ) ) → ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) ↔ 𝑥 ∥ ( 𝑘 · 𝑃 ) ) )
165 158 161 162 163 164 syl112anc ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) ↔ 𝑥 ∥ ( 𝑘 · 𝑃 ) ) )
166 157 165 bitrd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ↔ 𝑥 ∥ ( 𝑘 · 𝑃 ) ) )
167 dvdsmulcr ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ ( ( 𝑃 ↑ 𝑛 ) ∈ ℤ ∧ ( 𝑃 ↑ 𝑛 ) ≠ 0 ) ) → ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ↔ 𝑥 ∥ 𝑘 ) )
168 158 159 162 163 167 syl112anc ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ↔ 𝑥 ∥ 𝑘 ) )
169 168 notbid ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ¬ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ↔ ¬ 𝑥 ∥ 𝑘 ) )
170 166 169 anbi12d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) ↔ ( 𝑥 ∥ ( 𝑘 · 𝑃 ) ∧ ¬ 𝑥 ∥ 𝑘 ) ) )
171 152 breq1d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ↔ ( 𝑃 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ) )
172 dvdsmulcr ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ ( ( 𝑃 ↑ 𝑛 ) ∈ ℤ ∧ ( 𝑃 ↑ 𝑛 ) ≠ 0 ) ) → ( ( 𝑃 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ↔ 𝑃 ∥ 𝑥 ) )
173 160 158 162 163 172 syl112anc ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑃 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ↔ 𝑃 ∥ 𝑥 ) )
174 171 173 bitrd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ↔ 𝑃 ∥ 𝑥 ) )
175 143 170 174 3imtr4d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ) )
176 175 an32s ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) ∧ 𝑥 ∈ ℤ ) → ( ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ) )
177 breq1 ⊢ ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) = 𝐷 → ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ↔ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ) )
178 breq1 ⊢ ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) = 𝐷 → ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ↔ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) )
179 178 notbid ⊢ ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) = 𝐷 → ( ¬ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ↔ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) )
180 177 179 anbi12d ⊢ ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) = 𝐷 → ( ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) ↔ ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) ) )
181 breq2 ⊢ ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) = 𝐷 → ( ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ↔ ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) )
182 180 181 imbi12d ⊢ ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) = 𝐷 → ( ( ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ) ↔ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) )
183 176 182 syl5ibcom ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) = 𝐷 → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) )
184 183 rexlimdva ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ∃ 𝑥 ∈ ℤ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) = 𝐷 → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) )
185 184 adantlr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ∃ 𝑥 ∈ ℤ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) = 𝐷 → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) )
186 142 185 sylbid ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) )
187 186 com23 ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) → ( ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) )
188 187 a2d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) )
189 71 ad2antll ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑘 ∈ ℂ )
190 125 zcnd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑃 ∈ ℂ )
191 139 zcnd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 ↑ 𝑛 ) ∈ ℂ )
192 189 190 191 mulassd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) = ( 𝑘 · ( 𝑃 · ( 𝑃 ↑ 𝑛 ) ) ) )
193 190 191 mulcomd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 · ( 𝑃 ↑ 𝑛 ) ) = ( ( 𝑃 ↑ 𝑛 ) · 𝑃 ) )
194 190 137 expp1d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) = ( ( 𝑃 ↑ 𝑛 ) · 𝑃 ) )
195 193 194 eqtr4d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 · ( 𝑃 ↑ 𝑛 ) ) = ( 𝑃 ↑ ( 𝑛 + 1 ) ) )
196 195 oveq2d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑘 · ( 𝑃 · ( 𝑃 ↑ 𝑛 ) ) ) = ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) )
197 192 196 eqtrd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) = ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) )
198 197 breq2d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) ↔ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ) )
199 nnm1nn0 ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 − 1 ) ∈ ℕ0 )
200 199 ad2antrr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑛 − 1 ) ∈ ℕ0 )
201 zexpcl ⊢ ( ( 𝑃 ∈ ℤ ∧ ( 𝑛 − 1 ) ∈ ℕ0 ) → ( 𝑃 ↑ ( 𝑛 − 1 ) ) ∈ ℤ )
202 125 200 201 syl2anc ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 ↑ ( 𝑛 − 1 ) ) ∈ ℤ )
203 202 zcnd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 ↑ ( 𝑛 − 1 ) ) ∈ ℂ )
204 189 190 203 mulassd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) = ( 𝑘 · ( 𝑃 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) )
205 190 203 mulcomd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) = ( ( 𝑃 ↑ ( 𝑛 − 1 ) ) · 𝑃 ) )
206 simpll ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑛 ∈ ℕ )
207 expm1t ⊢ ( ( 𝑃 ∈ ℂ ∧ 𝑛 ∈ ℕ ) → ( 𝑃 ↑ 𝑛 ) = ( ( 𝑃 ↑ ( 𝑛 − 1 ) ) · 𝑃 ) )
208 190 206 207 syl2anc ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 ↑ 𝑛 ) = ( ( 𝑃 ↑ ( 𝑛 − 1 ) ) · 𝑃 ) )
209 205 208 eqtr4d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) = ( 𝑃 ↑ 𝑛 ) )
210 209 oveq2d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑘 · ( 𝑃 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) = ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) )
211 204 210 eqtrd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) = ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) )
212 211 breq2d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ↔ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) )
213 212 notbid ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ¬ 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ↔ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) )
214 198 213 anbi12d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) ↔ ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) ) )
215 214 imbi1d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( ( 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) ↔ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) ) )
216 nncn ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
217 216 ad2antrr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑛 ∈ ℂ )
218 ax-1cn ⊢ 1 ∈ ℂ
219 pncan ⊢ ( ( 𝑛 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑛 + 1 ) − 1 ) = 𝑛 )
220 217 218 219 sylancl ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑛 + 1 ) − 1 ) = 𝑛 )
221 220 oveq2d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) = ( 𝑃 ↑ 𝑛 ) )
222 221 oveq2d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) = ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) )
223 222 breq2d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) ↔ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) )
224 223 notbid ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) ↔ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) )
225 224 anbi2d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) ) ↔ ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) ) )
226 225 imbi1d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ↔ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) )
227 188 215 226 3imtr4d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( ( 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) )
228 135 227 syld ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ∀ 𝑥 ∈ ℤ ( ( 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) )
229 228 anassrs ⊢ ( ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( ∀ 𝑥 ∈ ℤ ( ( 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) )
230 229 ralrimdva ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ 𝑃 ∈ ℙ ) → ( ∀ 𝑥 ∈ ℤ ( ( 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) → ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) )
231 123 230 syl5bi ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ 𝑃 ∈ ℙ ) → ( ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) → ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) )
232 231 expl ⊢ ( 𝑛 ∈ ℕ → ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ( ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) → ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) ) )
233 232 a2d ⊢ ( 𝑛 ∈ ℕ → ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) ) → ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) ) )
234 20 33 46 59 115 233 nnind ⊢ ( 𝑁 ∈ ℕ → ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑁 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑁 ) ∥ 𝐷 ) ) )
235 234 com12 ⊢ ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ( 𝑁 ∈ ℕ → ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑁 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑁 ) ∥ 𝐷 ) ) )
236 235 impr ⊢ ( ( 𝐷 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) ) → ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑁 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑁 ) ∥ 𝐷 ) )
237 236 adantll ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) ) → ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑁 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑁 ) ∥ 𝐷 ) )
238 simpll ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) ) → 𝐾 ∈ ℤ )
239 7 237 238 rspcdva ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) ) → ( ( 𝐷 ∥ ( 𝐾 · ( 𝑃 ↑ 𝑁 ) ) ∧ ¬ 𝐷 ∥ ( 𝐾 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑁 ) ∥ 𝐷 ) )
240 239 3impia ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐷 ∥ ( 𝐾 · ( 𝑃 ↑ 𝑁 ) ) ∧ ¬ 𝐷 ∥ ( 𝐾 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) ) ) → ( 𝑃 ↑ 𝑁 ) ∥ 𝐷 )