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 ( 𝐴 ∈ ℝ → ( π ‘ ( 𝐴 + 1 ) ) ≤ ( ( π ‘ 𝐴 ) + 1 ) )

Proof

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