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 syl6bb ⊢ ( ( 𝑃 ∥ ( 𝐴 ↑ 𝑘 ) ↔ 𝑃 ∥ 𝐴 ) → ( ( 𝑃 ∥ ( 𝐴 ↑ 𝑘 ) ∨ 𝑃 ∥ 𝐴 ) ↔ 𝑃 ∥ 𝐴 ) )
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 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑃 ∥ ( 𝐴 ↑ 𝑁 ) ↔ 𝑃 ∥ 𝐴 ) )