Metamath Proof Explorer

Theorem pcdiv

Description: Division property of the prime power function. (Contributed by Mario Carneiro, 1-Mar-2014)

Ref Expression
Assertion pcdiv ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ A ≠ 0 ∧ B ∈ ℕ → P pCnt A B = P pCnt A − P pCnt B

Proof

Step Hyp Ref Expression
1 simp1 ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ A ≠ 0 ∧ B ∈ ℕ → P ∈ ℙ
2 simp2l ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ A ≠ 0 ∧ B ∈ ℕ → A ∈ ℤ
3 simp3 ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ A ≠ 0 ∧ B ∈ ℕ → B ∈ ℕ
4 znq ⊢ A ∈ ℤ ∧ B ∈ ℕ → A B ∈ ℚ
5 2 3 4 syl2anc ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ A ≠ 0 ∧ B ∈ ℕ → A B ∈ ℚ
6 2 zcnd ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ A ≠ 0 ∧ B ∈ ℕ → A ∈ ℂ
7 3 nncnd ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ A ≠ 0 ∧ B ∈ ℕ → B ∈ ℂ
8 simp2r ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ A ≠ 0 ∧ B ∈ ℕ → A ≠ 0
9 3 nnne0d ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ A ≠ 0 ∧ B ∈ ℕ → B ≠ 0
10 6 7 8 9 divne0d ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ A ≠ 0 ∧ B ∈ ℕ → A B ≠ 0
11 eqid ⊢ sup n ∈ ℕ 0 | P n ∥ x ℝ < = sup n ∈ ℕ 0 | P n ∥ x ℝ <
12 eqid ⊢ sup n ∈ ℕ 0 | P n ∥ y ℝ < = sup n ∈ ℕ 0 | P n ∥ y ℝ <
13 11 12 pcval ⊢ P ∈ ℙ ∧ A B ∈ ℚ ∧ A B ≠ 0 → P pCnt A B = ι z | ∃ x ∈ ℤ ∃ y ∈ ℕ A B = x y ∧ z = sup n ∈ ℕ 0 | P n ∥ x ℝ < − sup n ∈ ℕ 0 | P n ∥ y ℝ <
14 1 5 10 13 syl12anc ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ A ≠ 0 ∧ B ∈ ℕ → P pCnt A B = ι z | ∃ x ∈ ℤ ∃ y ∈ ℕ A B = x y ∧ z = sup n ∈ ℕ 0 | P n ∥ x ℝ < − sup n ∈ ℕ 0 | P n ∥ y ℝ <
15 eqid ⊢ sup n ∈ ℕ 0 | P n ∥ A ℝ < = sup n ∈ ℕ 0 | P n ∥ A ℝ <
16 15 pczpre ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ A ≠ 0 → P pCnt A = sup n ∈ ℕ 0 | P n ∥ A ℝ <
17 16 3adant3 ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ A ≠ 0 ∧ B ∈ ℕ → P pCnt A = sup n ∈ ℕ 0 | P n ∥ A ℝ <
18 nnz ⊢ B ∈ ℕ → B ∈ ℤ
19 nnne0 ⊢ B ∈ ℕ → B ≠ 0
20 18 19 jca ⊢ B ∈ ℕ → B ∈ ℤ ∧ B ≠ 0
21 eqid ⊢ sup n ∈ ℕ 0 | P n ∥ B ℝ < = sup n ∈ ℕ 0 | P n ∥ B ℝ <
22 21 pczpre ⊢ P ∈ ℙ ∧ B ∈ ℤ ∧ B ≠ 0 → P pCnt B = sup n ∈ ℕ 0 | P n ∥ B ℝ <
23 20 22 sylan2 ⊢ P ∈ ℙ ∧ B ∈ ℕ → P pCnt B = sup n ∈ ℕ 0 | P n ∥ B ℝ <
24 23 3adant2 ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ A ≠ 0 ∧ B ∈ ℕ → P pCnt B = sup n ∈ ℕ 0 | P n ∥ B ℝ <
25 17 24 oveq12d ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ A ≠ 0 ∧ B ∈ ℕ → P pCnt A − P pCnt B = sup n ∈ ℕ 0 | P n ∥ A ℝ < − sup n ∈ ℕ 0 | P n ∥ B ℝ <
26 eqid ⊢ A B = A B
27 25 26 jctil ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ A ≠ 0 ∧ B ∈ ℕ → A B = A B ∧ P pCnt A − P pCnt B = sup n ∈ ℕ 0 | P n ∥ A ℝ < − sup n ∈ ℕ 0 | P n ∥ B ℝ <
28 oveq1 ⊢ x = A → x y = A y
29 28 eqeq2d ⊢ x = A → A B = x y ↔ A B = A y
30 breq2 ⊢ x = A → P n ∥ x ↔ P n ∥ A
31 30 rabbidv ⊢ x = A → n ∈ ℕ 0 | P n ∥ x = n ∈ ℕ 0 | P n ∥ A
32 31 supeq1d ⊢ x = A → sup n ∈ ℕ 0 | P n ∥ x ℝ < = sup n ∈ ℕ 0 | P n ∥ A ℝ <
33 32 oveq1d ⊢ x = A → sup n ∈ ℕ 0 | P n ∥ x ℝ < − sup n ∈ ℕ 0 | P n ∥ y ℝ < = sup n ∈ ℕ 0 | P n ∥ A ℝ < − sup n ∈ ℕ 0 | P n ∥ y ℝ <
34 33 eqeq2d ⊢ x = A → P pCnt A − P pCnt B = sup n ∈ ℕ 0 | P n ∥ x ℝ < − sup n ∈ ℕ 0 | P n ∥ y ℝ < ↔ P pCnt A − P pCnt B = sup n ∈ ℕ 0 | P n ∥ A ℝ < − sup n ∈ ℕ 0 | P n ∥ y ℝ <
35 29 34 anbi12d ⊢ x = A → A B = x y ∧ P pCnt A − P pCnt B = sup n ∈ ℕ 0 | P n ∥ x ℝ < − sup n ∈ ℕ 0 | P n ∥ y ℝ < ↔ A B = A y ∧ P pCnt A − P pCnt B = sup n ∈ ℕ 0 | P n ∥ A ℝ < − sup n ∈ ℕ 0 | P n ∥ y ℝ <
36 oveq2 ⊢ y = B → A y = A B
37 36 eqeq2d ⊢ y = B → A B = A y ↔ A B = A B
38 breq2 ⊢ y = B → P n ∥ y ↔ P n ∥ B
39 38 rabbidv ⊢ y = B → n ∈ ℕ 0 | P n ∥ y = n ∈ ℕ 0 | P n ∥ B
40 39 supeq1d ⊢ y = B → sup n ∈ ℕ 0 | P n ∥ y ℝ < = sup n ∈ ℕ 0 | P n ∥ B ℝ <
41 40 oveq2d ⊢ y = B → sup n ∈ ℕ 0 | P n ∥ A ℝ < − sup n ∈ ℕ 0 | P n ∥ y ℝ < = sup n ∈ ℕ 0 | P n ∥ A ℝ < − sup n ∈ ℕ 0 | P n ∥ B ℝ <
42 41 eqeq2d ⊢ y = B → P pCnt A − P pCnt B = sup n ∈ ℕ 0 | P n ∥ A ℝ < − sup n ∈ ℕ 0 | P n ∥ y ℝ < ↔ P pCnt A − P pCnt B = sup n ∈ ℕ 0 | P n ∥ A ℝ < − sup n ∈ ℕ 0 | P n ∥ B ℝ <
43 37 42 anbi12d ⊢ y = B → A B = A y ∧ P pCnt A − P pCnt B = sup n ∈ ℕ 0 | P n ∥ A ℝ < − sup n ∈ ℕ 0 | P n ∥ y ℝ < ↔ A B = A B ∧ P pCnt A − P pCnt B = sup n ∈ ℕ 0 | P n ∥ A ℝ < − sup n ∈ ℕ 0 | P n ∥ B ℝ <
44 35 43 rspc2ev ⊢ A ∈ ℤ ∧ B ∈ ℕ ∧ A B = A B ∧ P pCnt A − P pCnt B = sup n ∈ ℕ 0 | P n ∥ A ℝ < − sup n ∈ ℕ 0 | P n ∥ B ℝ < → ∃ x ∈ ℤ ∃ y ∈ ℕ A B = x y ∧ P pCnt A − P pCnt B = sup n ∈ ℕ 0 | P n ∥ x ℝ < − sup n ∈ ℕ 0 | P n ∥ y ℝ <
45 2 3 27 44 syl3anc ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ A ≠ 0 ∧ B ∈ ℕ → ∃ x ∈ ℤ ∃ y ∈ ℕ A B = x y ∧ P pCnt A − P pCnt B = sup n ∈ ℕ 0 | P n ∥ x ℝ < − sup n ∈ ℕ 0 | P n ∥ y ℝ <
46 ovex ⊢ P pCnt A − P pCnt B ∈ V
47 11 12 pceu ⊢ P ∈ ℙ ∧ A B ∈ ℚ ∧ A B ≠ 0 → ∃! z ∃ x ∈ ℤ ∃ y ∈ ℕ A B = x y ∧ z = sup n ∈ ℕ 0 | P n ∥ x ℝ < − sup n ∈ ℕ 0 | P n ∥ y ℝ <
48 1 5 10 47 syl12anc ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ A ≠ 0 ∧ B ∈ ℕ → ∃! z ∃ x ∈ ℤ ∃ y ∈ ℕ A B = x y ∧ z = sup n ∈ ℕ 0 | P n ∥ x ℝ < − sup n ∈ ℕ 0 | P n ∥ y ℝ <
49 eqeq1 ⊢ z = P pCnt A − P pCnt B → z = sup n ∈ ℕ 0 | P n ∥ x ℝ < − sup n ∈ ℕ 0 | P n ∥ y ℝ < ↔ P pCnt A − P pCnt B = sup n ∈ ℕ 0 | P n ∥ x ℝ < − sup n ∈ ℕ 0 | P n ∥ y ℝ <
50 49 anbi2d ⊢ z = P pCnt A − P pCnt B → A B = x y ∧ z = sup n ∈ ℕ 0 | P n ∥ x ℝ < − sup n ∈ ℕ 0 | P n ∥ y ℝ < ↔ A B = x y ∧ P pCnt A − P pCnt B = sup n ∈ ℕ 0 | P n ∥ x ℝ < − sup n ∈ ℕ 0 | P n ∥ y ℝ <
51 50 2rexbidv ⊢ z = P pCnt A − P pCnt B → ∃ x ∈ ℤ ∃ y ∈ ℕ A B = x y ∧ z = sup n ∈ ℕ 0 | P n ∥ x ℝ < − sup n ∈ ℕ 0 | P n ∥ y ℝ < ↔ ∃ x ∈ ℤ ∃ y ∈ ℕ A B = x y ∧ P pCnt A − P pCnt B = sup n ∈ ℕ 0 | P n ∥ x ℝ < − sup n ∈ ℕ 0 | P n ∥ y ℝ <
52 51 iota2 ⊢ P pCnt A − P pCnt B ∈ V ∧ ∃! z ∃ x ∈ ℤ ∃ y ∈ ℕ A B = x y ∧ z = sup n ∈ ℕ 0 | P n ∥ x ℝ < − sup n ∈ ℕ 0 | P n ∥ y ℝ < → ∃ x ∈ ℤ ∃ y ∈ ℕ A B = x y ∧ P pCnt A − P pCnt B = sup n ∈ ℕ 0 | P n ∥ x ℝ < − sup n ∈ ℕ 0 | P n ∥ y ℝ < ↔ ι z | ∃ x ∈ ℤ ∃ y ∈ ℕ A B = x y ∧ z = sup n ∈ ℕ 0 | P n ∥ x ℝ < − sup n ∈ ℕ 0 | P n ∥ y ℝ < = P pCnt A − P pCnt B
53 46 48 52 sylancr ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ A ≠ 0 ∧ B ∈ ℕ → ∃ x ∈ ℤ ∃ y ∈ ℕ A B = x y ∧ P pCnt A − P pCnt B = sup n ∈ ℕ 0 | P n ∥ x ℝ < − sup n ∈ ℕ 0 | P n ∥ y ℝ < ↔ ι z | ∃ x ∈ ℤ ∃ y ∈ ℕ A B = x y ∧ z = sup n ∈ ℕ 0 | P n ∥ x ℝ < − sup n ∈ ℕ 0 | P n ∥ y ℝ < = P pCnt A − P pCnt B
54 45 53 mpbid ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ A ≠ 0 ∧ B ∈ ℕ → ι z | ∃ x ∈ ℤ ∃ y ∈ ℕ A B = x y ∧ z = sup n ∈ ℕ 0 | P n ∥ x ℝ < − sup n ∈ ℕ 0 | P n ∥ y ℝ < = P pCnt A − P pCnt B
55 14 54 eqtrd ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ A ≠ 0 ∧ B ∈ ℕ → P pCnt A B = P pCnt A − P pCnt B