This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 74 78 gcdcomd ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 gcd 𝑥 ) = ( 𝑥 gcd 𝑃 ) )
80 79 eqeq1d ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑃 gcd 𝑥 ) = 1 ↔ ( 𝑥 gcd 𝑃 ) = 1 ) )
81 77 80 anbi12d ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑥 ∥ ( 𝑘 · 𝑃 ) ∧ ( 𝑃 gcd 𝑥 ) = 1 ) ↔ ( 𝑥 ∥ ( 𝑃 · 𝑘 ) ∧ ( 𝑥 gcd 𝑃 ) = 1 ) ) )
82 simprr ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑘 ∈ ℤ )
83 coprmdvds ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑥 ∥ ( 𝑃 · 𝑘 ) ∧ ( 𝑥 gcd 𝑃 ) = 1 ) → 𝑥 ∥ 𝑘 ) )
84 78 74 82 83 syl3anc ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑥 ∥ ( 𝑃 · 𝑘 ) ∧ ( 𝑥 gcd 𝑃 ) = 1 ) → 𝑥 ∥ 𝑘 ) )
85 81 84 sylbid ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑥 ∥ ( 𝑘 · 𝑃 ) ∧ ( 𝑃 gcd 𝑥 ) = 1 ) → 𝑥 ∥ 𝑘 ) )
86 85 expdimp ⊢ ( ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) ∧ 𝑥 ∥ ( 𝑘 · 𝑃 ) ) → ( ( 𝑃 gcd 𝑥 ) = 1 → 𝑥 ∥ 𝑘 ) )
87 70 86 sylbid ⊢ ( ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) ∧ 𝑥 ∥ ( 𝑘 · 𝑃 ) ) → ( ¬ 𝑃 ∥ 𝑥 → 𝑥 ∥ 𝑘 ) )
88 87 con1d ⊢ ( ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) ∧ 𝑥 ∥ ( 𝑘 · 𝑃 ) ) → ( ¬ 𝑥 ∥ 𝑘 → 𝑃 ∥ 𝑥 ) )
89 88 expimpd ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑥 ∥ ( 𝑘 · 𝑃 ) ∧ ¬ 𝑥 ∥ 𝑘 ) → 𝑃 ∥ 𝑥 ) )
90 89 ex ⊢ ( 𝑥 ∈ ℤ → ( ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑥 ∥ ( 𝑘 · 𝑃 ) ∧ ¬ 𝑥 ∥ 𝑘 ) → 𝑃 ∥ 𝑥 ) ) )
91 66 90 vtoclga ⊢ ( 𝐷 ∈ ℤ → ( ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) → ( ( 𝐷 ∥ ( 𝑘 · 𝑃 ) ∧ ¬ 𝐷 ∥ 𝑘 ) → 𝑃 ∥ 𝐷 ) ) )
92 91 impl ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝐷 ∥ ( 𝑘 · 𝑃 ) ∧ ¬ 𝐷 ∥ 𝑘 ) → 𝑃 ∥ 𝐷 ) )
93 73 zcnd ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℂ )
94 93 exp1d ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ↑ 1 ) = 𝑃 )
95 94 ad2antlr ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( 𝑃 ↑ 1 ) = 𝑃 )
96 95 oveq2d ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( 𝑘 · ( 𝑃 ↑ 1 ) ) = ( 𝑘 · 𝑃 ) )
97 96 breq2d ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 1 ) ) ↔ 𝐷 ∥ ( 𝑘 · 𝑃 ) ) )
98 1m1e0 ⊢ ( 1 − 1 ) = 0
99 98 oveq2i ⊢ ( 𝑃 ↑ ( 1 − 1 ) ) = ( 𝑃 ↑ 0 )
100 73 ad2antlr ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → 𝑃 ∈ ℤ )
101 100 zcnd ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → 𝑃 ∈ ℂ )
102 101 exp0d ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( 𝑃 ↑ 0 ) = 1 )
103 99 102 eqtrid ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( 𝑃 ↑ ( 1 − 1 ) ) = 1 )
104 103 oveq2d ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( 𝑘 · ( 𝑃 ↑ ( 1 − 1 ) ) ) = ( 𝑘 · 1 ) )
105 71 adantl ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → 𝑘 ∈ ℂ )
106 105 mulridd ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( 𝑘 · 1 ) = 𝑘 )
107 104 106 eqtrd ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( 𝑘 · ( 𝑃 ↑ ( 1 − 1 ) ) ) = 𝑘 )
108 107 breq2d ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 1 − 1 ) ) ) ↔ 𝐷 ∥ 𝑘 ) )
109 108 notbid ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 1 − 1 ) ) ) ↔ ¬ 𝐷 ∥ 𝑘 ) )
110 97 109 anbi12d ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 1 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 1 − 1 ) ) ) ) ↔ ( 𝐷 ∥ ( 𝑘 · 𝑃 ) ∧ ¬ 𝐷 ∥ 𝑘 ) ) )
111 101 exp1d ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( 𝑃 ↑ 1 ) = 𝑃 )
112 111 breq1d ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝑃 ↑ 1 ) ∥ 𝐷 ↔ 𝑃 ∥ 𝐷 ) )
113 92 110 112 3imtr4d ⊢ ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 1 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 1 − 1 ) ) ) ) → ( 𝑃 ↑ 1 ) ∥ 𝐷 ) )
114 113 ralrimiva ⊢ ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 1 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 1 − 1 ) ) ) ) → ( 𝑃 ↑ 1 ) ∥ 𝐷 ) )
115 oveq1 ⊢ ( 𝑘 = 𝑥 → ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) = ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) )
116 115 breq2d ⊢ ( 𝑘 = 𝑥 → ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ↔ 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ) )
117 oveq1 ⊢ ( 𝑘 = 𝑥 → ( 𝑘 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) = ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) )
118 117 breq2d ⊢ ( 𝑘 = 𝑥 → ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ↔ 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) )
119 118 notbid ⊢ ( 𝑘 = 𝑥 → ( ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ↔ ¬ 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) )
120 116 119 anbi12d ⊢ ( 𝑘 = 𝑥 → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) ↔ ( 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) ) )
121 120 imbi1d ⊢ ( 𝑘 = 𝑥 → ( ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) ↔ ( ( 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) ) )
122 121 cbvralvw ⊢ ( ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) ↔ ∀ 𝑥 ∈ ℤ ( ( 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) )
123 simprr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑘 ∈ ℤ )
124 73 ad2antrl ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑃 ∈ ℤ )
125 123 124 zmulcld ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑘 · 𝑃 ) ∈ ℤ )
126 oveq1 ⊢ ( 𝑥 = ( 𝑘 · 𝑃 ) → ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) = ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) )
127 126 breq2d ⊢ ( 𝑥 = ( 𝑘 · 𝑃 ) → ( 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ↔ 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) ) )
128 oveq1 ⊢ ( 𝑥 = ( 𝑘 · 𝑃 ) → ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) = ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) )
129 128 breq2d ⊢ ( 𝑥 = ( 𝑘 · 𝑃 ) → ( 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ↔ 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) )
130 129 notbid ⊢ ( 𝑥 = ( 𝑘 · 𝑃 ) → ( ¬ 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ↔ ¬ 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) )
131 127 130 anbi12d ⊢ ( 𝑥 = ( 𝑘 · 𝑃 ) → ( ( 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) ↔ ( 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) ) )
132 131 imbi1d ⊢ ( 𝑥 = ( 𝑘 · 𝑃 ) → ( ( ( 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) ↔ ( ( 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) ) )
133 132 rspcv ⊢ ( ( 𝑘 · 𝑃 ) ∈ ℤ → ( ∀ 𝑥 ∈ ℤ ( ( 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) → ( ( 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) ) )
134 125 133 syl ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ∀ 𝑥 ∈ ℤ ( ( 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) → ( ( 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) ) )
135 nnnn0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
136 135 ad2antrr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑛 ∈ ℕ0 )
137 zexpcl ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑛 ∈ ℕ0 ) → ( 𝑃 ↑ 𝑛 ) ∈ ℤ )
138 124 136 137 syl2anc ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 ↑ 𝑛 ) ∈ ℤ )
139 simplr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝐷 ∈ ℤ )
140 divides ⊢ ( ( ( 𝑃 ↑ 𝑛 ) ∈ ℤ ∧ 𝐷 ∈ ℤ ) → ( ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ↔ ∃ 𝑥 ∈ ℤ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) = 𝐷 ) )
141 138 139 140 syl2anc ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ↔ ∃ 𝑥 ∈ ℤ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) = 𝐷 ) )
142 89 adantll ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑥 ∥ ( 𝑘 · 𝑃 ) ∧ ¬ 𝑥 ∥ 𝑘 ) → 𝑃 ∥ 𝑥 ) )
143 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
144 143 ad2antrl ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑃 ∈ ℕ )
145 144 nncnd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑃 ∈ ℂ )
146 135 ad2antrr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑛 ∈ ℕ0 )
147 145 146 expp1d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) = ( ( 𝑃 ↑ 𝑛 ) · 𝑃 ) )
148 144 146 nnexpcld ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 ↑ 𝑛 ) ∈ ℕ )
149 148 nncnd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 ↑ 𝑛 ) ∈ ℂ )
150 149 145 mulcomd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑃 ↑ 𝑛 ) · 𝑃 ) = ( 𝑃 · ( 𝑃 ↑ 𝑛 ) ) )
151 147 150 eqtrd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) = ( 𝑃 · ( 𝑃 ↑ 𝑛 ) ) )
152 151 oveq2d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) = ( 𝑘 · ( 𝑃 · ( 𝑃 ↑ 𝑛 ) ) ) )
153 71 ad2antll ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑘 ∈ ℂ )
154 153 145 149 mulassd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) = ( 𝑘 · ( 𝑃 · ( 𝑃 ↑ 𝑛 ) ) ) )
155 152 154 eqtr4d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) = ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) )
156 155 breq2d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ↔ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) ) )
157 simplr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑥 ∈ ℤ )
158 simprr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑘 ∈ ℤ )
159 144 nnzd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑃 ∈ ℤ )
160 158 159 zmulcld ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑘 · 𝑃 ) ∈ ℤ )
161 148 nnzd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 ↑ 𝑛 ) ∈ ℤ )
162 148 nnne0d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 ↑ 𝑛 ) ≠ 0 )
163 dvdsmulcr ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑘 · 𝑃 ) ∈ ℤ ∧ ( ( 𝑃 ↑ 𝑛 ) ∈ ℤ ∧ ( 𝑃 ↑ 𝑛 ) ≠ 0 ) ) → ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) ↔ 𝑥 ∥ ( 𝑘 · 𝑃 ) ) )
164 157 160 161 162 163 syl112anc ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) ↔ 𝑥 ∥ ( 𝑘 · 𝑃 ) ) )
165 156 164 bitrd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ↔ 𝑥 ∥ ( 𝑘 · 𝑃 ) ) )
166 dvdsmulcr ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ ( ( 𝑃 ↑ 𝑛 ) ∈ ℤ ∧ ( 𝑃 ↑ 𝑛 ) ≠ 0 ) ) → ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ↔ 𝑥 ∥ 𝑘 ) )
167 157 158 161 162 166 syl112anc ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ↔ 𝑥 ∥ 𝑘 ) )
168 167 notbid ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ¬ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ↔ ¬ 𝑥 ∥ 𝑘 ) )
169 165 168 anbi12d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) ↔ ( 𝑥 ∥ ( 𝑘 · 𝑃 ) ∧ ¬ 𝑥 ∥ 𝑘 ) ) )
170 151 breq1d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ↔ ( 𝑃 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ) )
171 dvdsmulcr ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ ( ( 𝑃 ↑ 𝑛 ) ∈ ℤ ∧ ( 𝑃 ↑ 𝑛 ) ≠ 0 ) ) → ( ( 𝑃 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ↔ 𝑃 ∥ 𝑥 ) )
172 159 157 161 162 171 syl112anc ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑃 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ↔ 𝑃 ∥ 𝑥 ) )
173 170 172 bitrd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ↔ 𝑃 ∥ 𝑥 ) )
174 142 169 173 3imtr4d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ) )
175 174 an32s ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) ∧ 𝑥 ∈ ℤ ) → ( ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ) )
176 breq1 ⊢ ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) = 𝐷 → ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ↔ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ) )
177 breq1 ⊢ ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) = 𝐷 → ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ↔ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) )
178 177 notbid ⊢ ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) = 𝐷 → ( ¬ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ↔ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) )
179 176 178 anbi12d ⊢ ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) = 𝐷 → ( ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) ↔ ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) ) )
180 breq2 ⊢ ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) = 𝐷 → ( ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ↔ ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) )
181 179 180 imbi12d ⊢ ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) = 𝐷 → ( ( ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ) ↔ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) )
182 175 181 syl5ibcom ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) = 𝐷 → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) )
183 182 rexlimdva ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ∃ 𝑥 ∈ ℤ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) = 𝐷 → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) )
184 183 adantlr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ∃ 𝑥 ∈ ℤ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) = 𝐷 → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) )
185 141 184 sylbid ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) )
186 185 com23 ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) → ( ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) )
187 186 a2d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) )
188 71 ad2antll ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑘 ∈ ℂ )
189 124 zcnd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑃 ∈ ℂ )
190 138 zcnd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 ↑ 𝑛 ) ∈ ℂ )
191 188 189 190 mulassd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) = ( 𝑘 · ( 𝑃 · ( 𝑃 ↑ 𝑛 ) ) ) )
192 189 190 mulcomd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 · ( 𝑃 ↑ 𝑛 ) ) = ( ( 𝑃 ↑ 𝑛 ) · 𝑃 ) )
193 189 136 expp1d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) = ( ( 𝑃 ↑ 𝑛 ) · 𝑃 ) )
194 192 193 eqtr4d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 · ( 𝑃 ↑ 𝑛 ) ) = ( 𝑃 ↑ ( 𝑛 + 1 ) ) )
195 194 oveq2d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑘 · ( 𝑃 · ( 𝑃 ↑ 𝑛 ) ) ) = ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) )
196 191 195 eqtrd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) = ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) )
197 196 breq2d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) ↔ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ) )
198 nnm1nn0 ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 − 1 ) ∈ ℕ0 )
199 198 ad2antrr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑛 − 1 ) ∈ ℕ0 )
200 zexpcl ⊢ ( ( 𝑃 ∈ ℤ ∧ ( 𝑛 − 1 ) ∈ ℕ0 ) → ( 𝑃 ↑ ( 𝑛 − 1 ) ) ∈ ℤ )
201 124 199 200 syl2anc ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 ↑ ( 𝑛 − 1 ) ) ∈ ℤ )
202 201 zcnd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 ↑ ( 𝑛 − 1 ) ) ∈ ℂ )
203 188 189 202 mulassd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) = ( 𝑘 · ( 𝑃 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) )
204 189 202 mulcomd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) = ( ( 𝑃 ↑ ( 𝑛 − 1 ) ) · 𝑃 ) )
205 simpll ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑛 ∈ ℕ )
206 expm1t ⊢ ( ( 𝑃 ∈ ℂ ∧ 𝑛 ∈ ℕ ) → ( 𝑃 ↑ 𝑛 ) = ( ( 𝑃 ↑ ( 𝑛 − 1 ) ) · 𝑃 ) )
207 189 205 206 syl2anc ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 ↑ 𝑛 ) = ( ( 𝑃 ↑ ( 𝑛 − 1 ) ) · 𝑃 ) )
208 204 207 eqtr4d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) = ( 𝑃 ↑ 𝑛 ) )
209 208 oveq2d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑘 · ( 𝑃 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) = ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) )
210 203 209 eqtrd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) = ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) )
211 210 breq2d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ↔ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) )
212 211 notbid ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ¬ 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ↔ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) )
213 197 212 anbi12d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) ↔ ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) ) )
214 213 imbi1d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( ( 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) ↔ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) ) )
215 nncn ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
216 215 ad2antrr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → 𝑛 ∈ ℂ )
217 ax-1cn ⊢ 1 ∈ ℂ
218 pncan ⊢ ( ( 𝑛 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑛 + 1 ) − 1 ) = 𝑛 )
219 216 217 218 sylancl ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑛 + 1 ) − 1 ) = 𝑛 )
220 219 oveq2d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) = ( 𝑃 ↑ 𝑛 ) )
221 220 oveq2d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) = ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) )
222 221 breq2d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) ↔ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) )
223 222 notbid ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) ↔ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) )
224 223 anbi2d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) ) ↔ ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) ) )
225 224 imbi1d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ↔ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) )
226 187 214 225 3imtr4d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ( ( 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( ( 𝑘 · 𝑃 ) · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) )
227 134 226 syld ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ℤ ) ) → ( ∀ 𝑥 ∈ ℤ ( ( 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) )
228 227 anassrs ⊢ ( ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ 𝑃 ∈ ℙ ) ∧ 𝑘 ∈ ℤ ) → ( ∀ 𝑥 ∈ ℤ ( ( 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) → ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) )
229 228 ralrimdva ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ 𝑃 ∈ ℙ ) → ( ∀ 𝑥 ∈ ℤ ( ( 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑥 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) → ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) )
230 122 229 biimtrid ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝐷 ∈ ℤ ) ∧ 𝑃 ∈ ℙ ) → ( ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) → ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) )
231 230 expl ⊢ ( 𝑛 ∈ ℕ → ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ( ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) → ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) ) )
232 231 a2d ⊢ ( 𝑛 ∈ ℕ → ( ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑛 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑛 ) ∥ 𝐷 ) ) → ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑛 + 1 ) ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( ( 𝑛 + 1 ) − 1 ) ) ) ) → ( 𝑃 ↑ ( 𝑛 + 1 ) ) ∥ 𝐷 ) ) ) )
233 20 33 46 59 114 232 nnind ⊢ ( 𝑁 ∈ ℕ → ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑁 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑁 ) ∥ 𝐷 ) ) )
234 233 com12 ⊢ ( ( 𝐷 ∈ ℤ ∧ 𝑃 ∈ ℙ ) → ( 𝑁 ∈ ℕ → ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑁 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑁 ) ∥ 𝐷 ) ) )
235 234 impr ⊢ ( ( 𝐷 ∈ ℤ ∧ ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) ) → ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑁 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑁 ) ∥ 𝐷 ) )
236 235 adantll ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) ) → ∀ 𝑘 ∈ ℤ ( ( 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ 𝑁 ) ) ∧ ¬ 𝐷 ∥ ( 𝑘 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑁 ) ∥ 𝐷 ) )
237 simpll ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) ) → 𝐾 ∈ ℤ )
238 7 236 237 rspcdva ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) ) → ( ( 𝐷 ∥ ( 𝐾 · ( 𝑃 ↑ 𝑁 ) ) ∧ ¬ 𝐷 ∥ ( 𝐾 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) ) → ( 𝑃 ↑ 𝑁 ) ∥ 𝐷 ) )
239 238 3impia ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐷 ∥ ( 𝐾 · ( 𝑃 ↑ 𝑁 ) ) ∧ ¬ 𝐷 ∥ ( 𝐾 · ( 𝑃 ↑ ( 𝑁 − 1 ) ) ) ) ) → ( 𝑃 ↑ 𝑁 ) ∥ 𝐷 )