Metamath Proof Explorer

Theorem pc11

Description: The prime count function, viewed as a function from NN to ( NN ^m Prime ) , is one-to-one. (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Assertion pc11 ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ 0 → A = B ↔ ∀ p ∈ ℙ p pCnt A = p pCnt B

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ A = B → p pCnt A = p pCnt B
2 1 ralrimivw ⊢ A = B → ∀ p ∈ ℙ p pCnt A = p pCnt B
3 nn0z ⊢ A ∈ ℕ 0 → A ∈ ℤ
4 nn0z ⊢ B ∈ ℕ 0 → B ∈ ℤ
5 zq ⊢ A ∈ ℤ → A ∈ ℚ
6 pcxcl ⊢ p ∈ ℙ ∧ A ∈ ℚ → p pCnt A ∈ ℝ *
7 5 6 sylan2 ⊢ p ∈ ℙ ∧ A ∈ ℤ → p pCnt A ∈ ℝ *
8 zq ⊢ B ∈ ℤ → B ∈ ℚ
9 pcxcl ⊢ p ∈ ℙ ∧ B ∈ ℚ → p pCnt B ∈ ℝ *
10 8 9 sylan2 ⊢ p ∈ ℙ ∧ B ∈ ℤ → p pCnt B ∈ ℝ *
11 7 10 anim12dan ⊢ p ∈ ℙ ∧ A ∈ ℤ ∧ B ∈ ℤ → p pCnt A ∈ ℝ * ∧ p pCnt B ∈ ℝ *
12 xrletri3 ⊢ p pCnt A ∈ ℝ * ∧ p pCnt B ∈ ℝ * → p pCnt A = p pCnt B ↔ p pCnt A ≤ p pCnt B ∧ p pCnt B ≤ p pCnt A
13 11 12 syl ⊢ p ∈ ℙ ∧ A ∈ ℤ ∧ B ∈ ℤ → p pCnt A = p pCnt B ↔ p pCnt A ≤ p pCnt B ∧ p pCnt B ≤ p pCnt A
14 13 ancoms ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ p ∈ ℙ → p pCnt A = p pCnt B ↔ p pCnt A ≤ p pCnt B ∧ p pCnt B ≤ p pCnt A
15 14 ralbidva ⊢ A ∈ ℤ ∧ B ∈ ℤ → ∀ p ∈ ℙ p pCnt A = p pCnt B ↔ ∀ p ∈ ℙ p pCnt A ≤ p pCnt B ∧ p pCnt B ≤ p pCnt A
16 r19.26 ⊢ ∀ p ∈ ℙ p pCnt A ≤ p pCnt B ∧ p pCnt B ≤ p pCnt A ↔ ∀ p ∈ ℙ p pCnt A ≤ p pCnt B ∧ ∀ p ∈ ℙ p pCnt B ≤ p pCnt A
17 15 16 bitrdi ⊢ A ∈ ℤ ∧ B ∈ ℤ → ∀ p ∈ ℙ p pCnt A = p pCnt B ↔ ∀ p ∈ ℙ p pCnt A ≤ p pCnt B ∧ ∀ p ∈ ℙ p pCnt B ≤ p pCnt A
18 pc2dvds ⊢ A ∈ ℤ ∧ B ∈ ℤ → A ∥ B ↔ ∀ p ∈ ℙ p pCnt A ≤ p pCnt B
19 pc2dvds ⊢ B ∈ ℤ ∧ A ∈ ℤ → B ∥ A ↔ ∀ p ∈ ℙ p pCnt B ≤ p pCnt A
20 19 ancoms ⊢ A ∈ ℤ ∧ B ∈ ℤ → B ∥ A ↔ ∀ p ∈ ℙ p pCnt B ≤ p pCnt A
21 18 20 anbi12d ⊢ A ∈ ℤ ∧ B ∈ ℤ → A ∥ B ∧ B ∥ A ↔ ∀ p ∈ ℙ p pCnt A ≤ p pCnt B ∧ ∀ p ∈ ℙ p pCnt B ≤ p pCnt A
22 17 21 bitr4d ⊢ A ∈ ℤ ∧ B ∈ ℤ → ∀ p ∈ ℙ p pCnt A = p pCnt B ↔ A ∥ B ∧ B ∥ A
23 3 4 22 syl2an ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ 0 → ∀ p ∈ ℙ p pCnt A = p pCnt B ↔ A ∥ B ∧ B ∥ A
24 dvdseq ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ 0 ∧ A ∥ B ∧ B ∥ A → A = B
25 24 ex ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ 0 → A ∥ B ∧ B ∥ A → A = B
26 23 25 sylbid ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ 0 → ∀ p ∈ ℙ p pCnt A = p pCnt B → A = B
27 2 26 impbid2 ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ 0 → A = B ↔ ∀ p ∈ ℙ p pCnt A = p pCnt B