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 ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ N ∈ ℕ → P ∥ A N ↔ P ∥ A

Proof

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