Metamath Proof Explorer


Theorem prmdvdsexp

Description: A prime divides a positive power of an integer iff it divides the integer. (Contributed by Mario Carneiro, 24-Feb-2014) (Revised by Mario Carneiro, 17-Jul-2014)

Ref Expression
Assertion prmdvdsexp ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑃 ∥ ( 𝐴𝑁 ) ↔ 𝑃𝐴 ) )

Proof

Step Hyp Ref Expression
1 oveq2 ( 𝑚 = 1 → ( 𝐴𝑚 ) = ( 𝐴 ↑ 1 ) )
2 1 breq2d ( 𝑚 = 1 → ( 𝑃 ∥ ( 𝐴𝑚 ) ↔ 𝑃 ∥ ( 𝐴 ↑ 1 ) ) )
3 2 bibi1d ( 𝑚 = 1 → ( ( 𝑃 ∥ ( 𝐴𝑚 ) ↔ 𝑃𝐴 ) ↔ ( 𝑃 ∥ ( 𝐴 ↑ 1 ) ↔ 𝑃𝐴 ) ) )
4 3 imbi2d ( 𝑚 = 1 → ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 ∥ ( 𝐴𝑚 ) ↔ 𝑃𝐴 ) ) ↔ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 ∥ ( 𝐴 ↑ 1 ) ↔ 𝑃𝐴 ) ) ) )
5 oveq2 ( 𝑚 = 𝑘 → ( 𝐴𝑚 ) = ( 𝐴𝑘 ) )
6 5 breq2d ( 𝑚 = 𝑘 → ( 𝑃 ∥ ( 𝐴𝑚 ) ↔ 𝑃 ∥ ( 𝐴𝑘 ) ) )
7 6 bibi1d ( 𝑚 = 𝑘 → ( ( 𝑃 ∥ ( 𝐴𝑚 ) ↔ 𝑃𝐴 ) ↔ ( 𝑃 ∥ ( 𝐴𝑘 ) ↔ 𝑃𝐴 ) ) )
8 7 imbi2d ( 𝑚 = 𝑘 → ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 ∥ ( 𝐴𝑚 ) ↔ 𝑃𝐴 ) ) ↔ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 ∥ ( 𝐴𝑘 ) ↔ 𝑃𝐴 ) ) ) )
9 oveq2 ( 𝑚 = ( 𝑘 + 1 ) → ( 𝐴𝑚 ) = ( 𝐴 ↑ ( 𝑘 + 1 ) ) )
10 9 breq2d ( 𝑚 = ( 𝑘 + 1 ) → ( 𝑃 ∥ ( 𝐴𝑚 ) ↔ 𝑃 ∥ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) )
11 10 bibi1d ( 𝑚 = ( 𝑘 + 1 ) → ( ( 𝑃 ∥ ( 𝐴𝑚 ) ↔ 𝑃𝐴 ) ↔ ( 𝑃 ∥ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ↔ 𝑃𝐴 ) ) )
12 11 imbi2d ( 𝑚 = ( 𝑘 + 1 ) → ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 ∥ ( 𝐴𝑚 ) ↔ 𝑃𝐴 ) ) ↔ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 ∥ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ↔ 𝑃𝐴 ) ) ) )
13 oveq2 ( 𝑚 = 𝑁 → ( 𝐴𝑚 ) = ( 𝐴𝑁 ) )
14 13 breq2d ( 𝑚 = 𝑁 → ( 𝑃 ∥ ( 𝐴𝑚 ) ↔ 𝑃 ∥ ( 𝐴𝑁 ) ) )
15 14 bibi1d ( 𝑚 = 𝑁 → ( ( 𝑃 ∥ ( 𝐴𝑚 ) ↔ 𝑃𝐴 ) ↔ ( 𝑃 ∥ ( 𝐴𝑁 ) ↔ 𝑃𝐴 ) ) )
16 15 imbi2d ( 𝑚 = 𝑁 → ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 ∥ ( 𝐴𝑚 ) ↔ 𝑃𝐴 ) ) ↔ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 ∥ ( 𝐴𝑁 ) ↔ 𝑃𝐴 ) ) ) )
17 zcn ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
18 17 adantl ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → 𝐴 ∈ ℂ )
19 18 exp1d ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝐴 ↑ 1 ) = 𝐴 )
20 19 breq2d ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 ∥ ( 𝐴 ↑ 1 ) ↔ 𝑃𝐴 ) )
21 nnnn0 ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
22 expp1 ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐴𝑘 ) · 𝐴 ) )
23 18 21 22 syl2an ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐴𝑘 ) · 𝐴 ) )
24 23 breq2d ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑘 ∈ ℕ ) → ( 𝑃 ∥ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ↔ 𝑃 ∥ ( ( 𝐴𝑘 ) · 𝐴 ) ) )
25 simpll ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑘 ∈ ℕ ) → 𝑃 ∈ ℙ )
26 simpr ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → 𝐴 ∈ ℤ )
27 zexpcl ( ( 𝐴 ∈ ℤ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴𝑘 ) ∈ ℤ )
28 26 21 27 syl2an ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑘 ∈ ℕ ) → ( 𝐴𝑘 ) ∈ ℤ )
29 simplr ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ℤ )
30 euclemma ( ( 𝑃 ∈ ℙ ∧ ( 𝐴𝑘 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 ∥ ( ( 𝐴𝑘 ) · 𝐴 ) ↔ ( 𝑃 ∥ ( 𝐴𝑘 ) ∨ 𝑃𝐴 ) ) )
31 25 28 29 30 syl3anc ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑘 ∈ ℕ ) → ( 𝑃 ∥ ( ( 𝐴𝑘 ) · 𝐴 ) ↔ ( 𝑃 ∥ ( 𝐴𝑘 ) ∨ 𝑃𝐴 ) ) )
32 24 31 bitrd ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑘 ∈ ℕ ) → ( 𝑃 ∥ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ↔ ( 𝑃 ∥ ( 𝐴𝑘 ) ∨ 𝑃𝐴 ) ) )
33 orbi1 ( ( 𝑃 ∥ ( 𝐴𝑘 ) ↔ 𝑃𝐴 ) → ( ( 𝑃 ∥ ( 𝐴𝑘 ) ∨ 𝑃𝐴 ) ↔ ( 𝑃𝐴𝑃𝐴 ) ) )
34 oridm ( ( 𝑃𝐴𝑃𝐴 ) ↔ 𝑃𝐴 )
35 33 34 bitrdi ( ( 𝑃 ∥ ( 𝐴𝑘 ) ↔ 𝑃𝐴 ) → ( ( 𝑃 ∥ ( 𝐴𝑘 ) ∨ 𝑃𝐴 ) ↔ 𝑃𝐴 ) )
36 35 bibi2d ( ( 𝑃 ∥ ( 𝐴𝑘 ) ↔ 𝑃𝐴 ) → ( ( 𝑃 ∥ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ↔ ( 𝑃 ∥ ( 𝐴𝑘 ) ∨ 𝑃𝐴 ) ) ↔ ( 𝑃 ∥ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ↔ 𝑃𝐴 ) ) )
37 32 36 syl5ibcom ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑃 ∥ ( 𝐴𝑘 ) ↔ 𝑃𝐴 ) → ( 𝑃 ∥ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ↔ 𝑃𝐴 ) ) )
38 37 expcom ( 𝑘 ∈ ℕ → ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( ( 𝑃 ∥ ( 𝐴𝑘 ) ↔ 𝑃𝐴 ) → ( 𝑃 ∥ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ↔ 𝑃𝐴 ) ) ) )
39 38 a2d ( 𝑘 ∈ ℕ → ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 ∥ ( 𝐴𝑘 ) ↔ 𝑃𝐴 ) ) → ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 ∥ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ↔ 𝑃𝐴 ) ) ) )
40 4 8 12 16 20 39 nnind ( 𝑁 ∈ ℕ → ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 ∥ ( 𝐴𝑁 ) ↔ 𝑃𝐴 ) ) )
41 40 impcom ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) ∧ 𝑁 ∈ ℕ ) → ( 𝑃 ∥ ( 𝐴𝑁 ) ↔ 𝑃𝐴 ) )
42 41 3impa ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑃 ∥ ( 𝐴𝑁 ) ↔ 𝑃𝐴 ) )