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∈ℙppCntA=ppCntB

Proof

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