Metamath Proof Explorer

Theorem ppip1le

Description: The prime-counting function ppi cannot locally increase faster than the identity function. (Contributed by Mario Carneiro, 21-Sep-2014)

Ref Expression
Assertion ppip1le ⊢ A ∈ ℝ → π _ ⁡ A + 1 ≤ π _ ⁡ A + 1

Proof

Step Hyp Ref Expression
1 flcl ⊢ A ∈ ℝ → A ∈ ℤ
2 zre ⊢ A ∈ ℤ → A ∈ ℝ
3 peano2re ⊢ A ∈ ℝ → A + 1 ∈ ℝ
4 2 3 syl ⊢ A ∈ ℤ → A + 1 ∈ ℝ
5 4 adantr ⊢ A ∈ ℤ ∧ A + 1 ∈ ℙ → A + 1 ∈ ℝ
6 ppicl ⊢ A + 1 ∈ ℝ → π _ ⁡ A + 1 ∈ ℕ 0
7 5 6 syl ⊢ A ∈ ℤ ∧ A + 1 ∈ ℙ → π _ ⁡ A + 1 ∈ ℕ 0
8 7 nn0red ⊢ A ∈ ℤ ∧ A + 1 ∈ ℙ → π _ ⁡ A + 1 ∈ ℝ
9 ppiprm ⊢ A ∈ ℤ ∧ A + 1 ∈ ℙ → π _ ⁡ A + 1 = π _ ⁡ A + 1
10 8 9 eqled ⊢ A ∈ ℤ ∧ A + 1 ∈ ℙ → π _ ⁡ A + 1 ≤ π _ ⁡ A + 1
11 ppinprm ⊢ A ∈ ℤ ∧ ¬ A + 1 ∈ ℙ → π _ ⁡ A + 1 = π _ ⁡ A
12 ppicl ⊢ A ∈ ℝ → π _ ⁡ A ∈ ℕ 0
13 2 12 syl ⊢ A ∈ ℤ → π _ ⁡ A ∈ ℕ 0
14 13 nn0red ⊢ A ∈ ℤ → π _ ⁡ A ∈ ℝ
15 14 adantr ⊢ A ∈ ℤ ∧ ¬ A + 1 ∈ ℙ → π _ ⁡ A ∈ ℝ
16 15 lep1d ⊢ A ∈ ℤ ∧ ¬ A + 1 ∈ ℙ → π _ ⁡ A ≤ π _ ⁡ A + 1
17 11 16 eqbrtrd ⊢ A ∈ ℤ ∧ ¬ A + 1 ∈ ℙ → π _ ⁡ A + 1 ≤ π _ ⁡ A + 1
18 10 17 pm2.61dan ⊢ A ∈ ℤ → π _ ⁡ A + 1 ≤ π _ ⁡ A + 1
19 1 18 syl ⊢ A ∈ ℝ → π _ ⁡ A + 1 ≤ π _ ⁡ A + 1
20 1z ⊢ 1 ∈ ℤ
21 fladdz ⊢ A ∈ ℝ ∧ 1 ∈ ℤ → A + 1 = A + 1
22 20 21 mpan2 ⊢ A ∈ ℝ → A + 1 = A + 1
23 22 fveq2d ⊢ A ∈ ℝ → π _ ⁡ A + 1 = π _ ⁡ A + 1
24 peano2re ⊢ A ∈ ℝ → A + 1 ∈ ℝ
25 ppifl ⊢ A + 1 ∈ ℝ → π _ ⁡ A + 1 = π _ ⁡ A + 1
26 24 25 syl ⊢ A ∈ ℝ → π _ ⁡ A + 1 = π _ ⁡ A + 1
27 23 26 eqtr3d ⊢ A ∈ ℝ → π _ ⁡ A + 1 = π _ ⁡ A + 1
28 ppifl ⊢ A ∈ ℝ → π _ ⁡ A = π _ ⁡ A
29 28 oveq1d ⊢ A ∈ ℝ → π _ ⁡ A + 1 = π _ ⁡ A + 1
30 19 27 29 3brtr3d ⊢ A ∈ ℝ → π _ ⁡ A + 1 ≤ π _ ⁡ A + 1