Metamath Proof Explorer

Theorem ppiwordi

Description: The prime-counting function ppi is weakly increasing. (Contributed by Mario Carneiro, 19-Sep-2014)

Ref Expression
Assertion ppiwordi ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( π ‘ 𝐴 ) ≤ ( π ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simp2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ℝ )
2 ppifi ⊢ ( 𝐵 ∈ ℝ → ( ( 0 [,] 𝐵 ) ∩ ℙ ) ∈ Fin )
3 1 2 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ( 0 [,] 𝐵 ) ∩ ℙ ) ∈ Fin )
4 0red ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 0 ∈ ℝ )
5 0le0 ⊢ 0 ≤ 0
6 5 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 0 ≤ 0 )
7 simp3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ≤ 𝐵 )
8 iccss ⊢ ( ( ( 0 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 0 ∧ 𝐴 ≤ 𝐵 ) ) → ( 0 [,] 𝐴 ) ⊆ ( 0 [,] 𝐵 ) )
9 4 1 6 7 8 syl22anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( 0 [,] 𝐴 ) ⊆ ( 0 [,] 𝐵 ) )
10 9 ssrind ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ⊆ ( ( 0 [,] 𝐵 ) ∩ ℙ ) )
11 ssdomg ⊢ ( ( ( 0 [,] 𝐵 ) ∩ ℙ ) ∈ Fin → ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ⊆ ( ( 0 [,] 𝐵 ) ∩ ℙ ) → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ≼ ( ( 0 [,] 𝐵 ) ∩ ℙ ) ) )
12 3 10 11 sylc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ≼ ( ( 0 [,] 𝐵 ) ∩ ℙ ) )
13 ppifi ⊢ ( 𝐴 ∈ ℝ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∈ Fin )
14 13 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∈ Fin )
15 hashdom ⊢ ( ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∈ Fin ∧ ( ( 0 [,] 𝐵 ) ∩ ℙ ) ∈ Fin ) → ( ( ♯ ‘ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ≤ ( ♯ ‘ ( ( 0 [,] 𝐵 ) ∩ ℙ ) ) ↔ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ≼ ( ( 0 [,] 𝐵 ) ∩ ℙ ) ) )
16 14 3 15 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ( ♯ ‘ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ≤ ( ♯ ‘ ( ( 0 [,] 𝐵 ) ∩ ℙ ) ) ↔ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ≼ ( ( 0 [,] 𝐵 ) ∩ ℙ ) ) )
17 12 16 mpbird ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( ♯ ‘ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ≤ ( ♯ ‘ ( ( 0 [,] 𝐵 ) ∩ ℙ ) ) )
18 ppival ⊢ ( 𝐴 ∈ ℝ → ( π ‘ 𝐴 ) = ( ♯ ‘ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) )
19 18 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( π ‘ 𝐴 ) = ( ♯ ‘ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) )
20 ppival ⊢ ( 𝐵 ∈ ℝ → ( π ‘ 𝐵 ) = ( ♯ ‘ ( ( 0 [,] 𝐵 ) ∩ ℙ ) ) )
21 1 20 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( π ‘ 𝐵 ) = ( ♯ ‘ ( ( 0 [,] 𝐵 ) ∩ ℙ ) ) )
22 17 19 21 3brtr4d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( π ‘ 𝐴 ) ≤ ( π ‘ 𝐵 ) )