Theorem: prodPrimesRealLePowFour (FromTheBook/Ch02/Bertrand/ProdPrimes.lean)

State before:
x : ℝ
hx : 1 ≤ x
⊢ ↑(prodPrimes ⌊x⌋₊) ≤ ↑(4 ^ (⌊x⌋₊ - 1))
Tactic:
norm_cast
State after:
x : ℝ
hx : 1 ≤ x
⊢ prodPrimes ⌊x⌋₊ ≤ 4 ^ (⌊x⌋₊ - 1)

State before:
x : ℝ
hx : 1 ≤ x
⊢ prodPrimes ⌊x⌋₊ ≤ 4 ^ (⌊x⌋₊ - 1)
Tactic:
apply prodPrimesLePowFour
State after:
no goals

State before:
x : ℝ
hx : 1 ≤ x
⊢ ↑(4 ^ (⌊x⌋₊ - 1)) = 4 ^ ↑(⌊x⌋₊ - 1)
Tactic:
norm_cast
State after:
no goals

State before:
x : ℝ
hx : 1 ≤ x
⊢ 4 ^ ↑(⌊x⌋₊ - 1) ≤ 4 ^ (x - 1)
Tactic:
rw [Real.rpow_le_rpow_left_iff (by norm_num)]
State after:
x : ℝ
hx : 1 ≤ x
⊢ ↑(⌊x⌋₊ - 1) ≤ x - 1

State before:
x : ℝ
hx : 1 ≤ x
⊢ ↑(⌊x⌋₊ - 1) ≤ x - 1
Tactic:
rw [← Nat.floor_sub_one]
State after:
x : ℝ
hx : 1 ≤ x
⊢ ↑⌊x - 1⌋₊ ≤ x - 1

State before:
x : ℝ
hx : 1 ≤ x
⊢ ↑⌊x - 1⌋₊ ≤ x - 1
Tactic:
apply Nat.floor_le
State after:
case ha
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ x - 1

State before:
case ha
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ x - 1
Tactic:
linarith
State after:
no goals

State before:
x : ℝ
hx : 1 ≤ x
⊢ 1 < 4
Tactic:
norm_num
State after:
no goals