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 ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝐴 ) = ( 𝑝 pCnt 𝐵 ) ) )

Proof

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