Metamath Proof Explorer

Theorem isppw2

Description: Two ways to say that A is a prime power. (Contributed by Mario Carneiro, 7-Apr-2016)

Ref Expression
Assertion isppw2 ⊢ A ∈ ℕ → Λ ⁡ A ≠ 0 ↔ ∃ p ∈ ℙ ∃ k ∈ ℕ A = p k

Proof

Step Hyp Ref Expression
1 isppw ⊢ A ∈ ℕ → Λ ⁡ A ≠ 0 ↔ ∃! q ∈ ℙ q ∥ A
2 reu6 ⊢ ∃! q ∈ ℙ q ∥ A ↔ ∃ p ∈ ℙ ∀ q ∈ ℙ q ∥ A ↔ q = p
3 equid ⊢ p = p
4 breq1 ⊢ q = p → q ∥ A ↔ p ∥ A
5 equequ1 ⊢ q = p → q = p ↔ p = p
6 4 5 bibi12d ⊢ q = p → q ∥ A ↔ q = p ↔ p ∥ A ↔ p = p
7 6 rspcva ⊢ p ∈ ℙ ∧ ∀ q ∈ ℙ q ∥ A ↔ q = p → p ∥ A ↔ p = p
8 7 adantll ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ ∀ q ∈ ℙ q ∥ A ↔ q = p → p ∥ A ↔ p = p
9 3 8 mpbiri ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ ∀ q ∈ ℙ q ∥ A ↔ q = p → p ∥ A
10 simplr ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ ∀ q ∈ ℙ q ∥ A ↔ q = p → p ∈ ℙ
11 simpll ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ ∀ q ∈ ℙ q ∥ A ↔ q = p → A ∈ ℕ
12 pcelnn ⊢ p ∈ ℙ ∧ A ∈ ℕ → p pCnt A ∈ ℕ ↔ p ∥ A
13 10 11 12 syl2anc ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ ∀ q ∈ ℙ q ∥ A ↔ q = p → p pCnt A ∈ ℕ ↔ p ∥ A
14 9 13 mpbird ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ ∀ q ∈ ℙ q ∥ A ↔ q = p → p pCnt A ∈ ℕ
15 simpr ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ q ∈ ℙ ∧ q ∥ A ↔ q = p ∧ q = p → q = p
16 15 oveq1d ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ q ∈ ℙ ∧ q ∥ A ↔ q = p ∧ q = p → q pCnt A = p pCnt A
17 simpllr ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ q ∈ ℙ ∧ q ∥ A ↔ q = p ∧ q = p → p ∈ ℙ
18 pccl ⊢ p ∈ ℙ ∧ A ∈ ℕ → p pCnt A ∈ ℕ 0
19 18 ancoms ⊢ A ∈ ℕ ∧ p ∈ ℙ → p pCnt A ∈ ℕ 0
20 19 ad2antrr ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ q ∈ ℙ ∧ q ∥ A ↔ q = p ∧ q = p → p pCnt A ∈ ℕ 0
21 20 nn0zd ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ q ∈ ℙ ∧ q ∥ A ↔ q = p ∧ q = p → p pCnt A ∈ ℤ
22 pcid ⊢ p ∈ ℙ ∧ p pCnt A ∈ ℤ → p pCnt p p pCnt A = p pCnt A
23 17 21 22 syl2anc ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ q ∈ ℙ ∧ q ∥ A ↔ q = p ∧ q = p → p pCnt p p pCnt A = p pCnt A
24 16 23 eqtr4d ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ q ∈ ℙ ∧ q ∥ A ↔ q = p ∧ q = p → q pCnt A = p pCnt p p pCnt A
25 15 oveq1d ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ q ∈ ℙ ∧ q ∥ A ↔ q = p ∧ q = p → q pCnt p p pCnt A = p pCnt p p pCnt A
26 24 25 eqtr4d ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ q ∈ ℙ ∧ q ∥ A ↔ q = p ∧ q = p → q pCnt A = q pCnt p p pCnt A
27 simprr ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ q ∈ ℙ ∧ q ∥ A ↔ q = p → q ∥ A ↔ q = p
28 27 notbid ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ q ∈ ℙ ∧ q ∥ A ↔ q = p → ¬ q ∥ A ↔ ¬ q = p
29 28 biimpar ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ q ∈ ℙ ∧ q ∥ A ↔ q = p ∧ ¬ q = p → ¬ q ∥ A
30 simplrl ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ q ∈ ℙ ∧ q ∥ A ↔ q = p ∧ ¬ q = p → q ∈ ℙ
31 simplll ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ q ∈ ℙ ∧ q ∥ A ↔ q = p ∧ ¬ q = p → A ∈ ℕ
32 pceq0 ⊢ q ∈ ℙ ∧ A ∈ ℕ → q pCnt A = 0 ↔ ¬ q ∥ A
33 30 31 32 syl2anc ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ q ∈ ℙ ∧ q ∥ A ↔ q = p ∧ ¬ q = p → q pCnt A = 0 ↔ ¬ q ∥ A
34 29 33 mpbird ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ q ∈ ℙ ∧ q ∥ A ↔ q = p ∧ ¬ q = p → q pCnt A = 0
35 simprl ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ q ∈ ℙ ∧ q ∥ A ↔ q = p → q ∈ ℙ
36 simplr ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ q ∈ ℙ ∧ q ∥ A ↔ q = p → p ∈ ℙ
37 19 adantr ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ q ∈ ℙ ∧ q ∥ A ↔ q = p → p pCnt A ∈ ℕ 0
38 prmdvdsexpr ⊢ q ∈ ℙ ∧ p ∈ ℙ ∧ p pCnt A ∈ ℕ 0 → q ∥ p p pCnt A → q = p
39 35 36 37 38 syl3anc ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ q ∈ ℙ ∧ q ∥ A ↔ q = p → q ∥ p p pCnt A → q = p
40 39 con3dimp ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ q ∈ ℙ ∧ q ∥ A ↔ q = p ∧ ¬ q = p → ¬ q ∥ p p pCnt A
41 prmnn ⊢ p ∈ ℙ → p ∈ ℕ
42 41 adantl ⊢ A ∈ ℕ ∧ p ∈ ℙ → p ∈ ℕ
43 42 19 nnexpcld ⊢ A ∈ ℕ ∧ p ∈ ℙ → p p pCnt A ∈ ℕ
44 43 ad2antrr ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ q ∈ ℙ ∧ q ∥ A ↔ q = p ∧ ¬ q = p → p p pCnt A ∈ ℕ
45 pceq0 ⊢ q ∈ ℙ ∧ p p pCnt A ∈ ℕ → q pCnt p p pCnt A = 0 ↔ ¬ q ∥ p p pCnt A
46 30 44 45 syl2anc ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ q ∈ ℙ ∧ q ∥ A ↔ q = p ∧ ¬ q = p → q pCnt p p pCnt A = 0 ↔ ¬ q ∥ p p pCnt A
47 40 46 mpbird ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ q ∈ ℙ ∧ q ∥ A ↔ q = p ∧ ¬ q = p → q pCnt p p pCnt A = 0
48 34 47 eqtr4d ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ q ∈ ℙ ∧ q ∥ A ↔ q = p ∧ ¬ q = p → q pCnt A = q pCnt p p pCnt A
49 26 48 pm2.61dan ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ q ∈ ℙ ∧ q ∥ A ↔ q = p → q pCnt A = q pCnt p p pCnt A
50 49 expr ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ q ∈ ℙ → q ∥ A ↔ q = p → q pCnt A = q pCnt p p pCnt A
51 50 ralimdva ⊢ A ∈ ℕ ∧ p ∈ ℙ → ∀ q ∈ ℙ q ∥ A ↔ q = p → ∀ q ∈ ℙ q pCnt A = q pCnt p p pCnt A
52 51 imp ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ ∀ q ∈ ℙ q ∥ A ↔ q = p → ∀ q ∈ ℙ q pCnt A = q pCnt p p pCnt A
53 nnnn0 ⊢ A ∈ ℕ → A ∈ ℕ 0
54 53 ad2antrr ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ ∀ q ∈ ℙ q ∥ A ↔ q = p → A ∈ ℕ 0
55 43 adantr ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ ∀ q ∈ ℙ q ∥ A ↔ q = p → p p pCnt A ∈ ℕ
56 55 nnnn0d ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ ∀ q ∈ ℙ q ∥ A ↔ q = p → p p pCnt A ∈ ℕ 0
57 pc11 ⊢ A ∈ ℕ 0 ∧ p p pCnt A ∈ ℕ 0 → A = p p pCnt A ↔ ∀ q ∈ ℙ q pCnt A = q pCnt p p pCnt A
58 54 56 57 syl2anc ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ ∀ q ∈ ℙ q ∥ A ↔ q = p → A = p p pCnt A ↔ ∀ q ∈ ℙ q pCnt A = q pCnt p p pCnt A
59 52 58 mpbird ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ ∀ q ∈ ℙ q ∥ A ↔ q = p → A = p p pCnt A
60 oveq2 ⊢ k = p pCnt A → p k = p p pCnt A
61 60 rspceeqv ⊢ p pCnt A ∈ ℕ ∧ A = p p pCnt A → ∃ k ∈ ℕ A = p k
62 14 59 61 syl2anc ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ ∀ q ∈ ℙ q ∥ A ↔ q = p → ∃ k ∈ ℕ A = p k
63 62 ex ⊢ A ∈ ℕ ∧ p ∈ ℙ → ∀ q ∈ ℙ q ∥ A ↔ q = p → ∃ k ∈ ℕ A = p k
64 prmdvdsexpb ⊢ q ∈ ℙ ∧ p ∈ ℙ ∧ k ∈ ℕ → q ∥ p k ↔ q = p
65 64 3coml ⊢ p ∈ ℙ ∧ k ∈ ℕ ∧ q ∈ ℙ → q ∥ p k ↔ q = p
66 65 3expa ⊢ p ∈ ℙ ∧ k ∈ ℕ ∧ q ∈ ℙ → q ∥ p k ↔ q = p
67 66 ralrimiva ⊢ p ∈ ℙ ∧ k ∈ ℕ → ∀ q ∈ ℙ q ∥ p k ↔ q = p
68 67 adantll ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ k ∈ ℕ → ∀ q ∈ ℙ q ∥ p k ↔ q = p
69 breq2 ⊢ A = p k → q ∥ A ↔ q ∥ p k
70 69 bibi1d ⊢ A = p k → q ∥ A ↔ q = p ↔ q ∥ p k ↔ q = p
71 70 ralbidv ⊢ A = p k → ∀ q ∈ ℙ q ∥ A ↔ q = p ↔ ∀ q ∈ ℙ q ∥ p k ↔ q = p
72 68 71 syl5ibrcom ⊢ A ∈ ℕ ∧ p ∈ ℙ ∧ k ∈ ℕ → A = p k → ∀ q ∈ ℙ q ∥ A ↔ q = p
73 72 rexlimdva ⊢ A ∈ ℕ ∧ p ∈ ℙ → ∃ k ∈ ℕ A = p k → ∀ q ∈ ℙ q ∥ A ↔ q = p
74 63 73 impbid ⊢ A ∈ ℕ ∧ p ∈ ℙ → ∀ q ∈ ℙ q ∥ A ↔ q = p ↔ ∃ k ∈ ℕ A = p k
75 74 rexbidva ⊢ A ∈ ℕ → ∃ p ∈ ℙ ∀ q ∈ ℙ q ∥ A ↔ q = p ↔ ∃ p ∈ ℙ ∃ k ∈ ℕ A = p k
76 2 75 bitrid ⊢ A ∈ ℕ → ∃! q ∈ ℙ q ∥ A ↔ ∃ p ∈ ℙ ∃ k ∈ ℕ A = p k
77 1 76 bitrd ⊢ A ∈ ℕ → Λ ⁡ A ≠ 0 ↔ ∃ p ∈ ℙ ∃ k ∈ ℕ A = p k