From c1fe97648737a03b36ab393fb4ad4383ee37efc1 Mon Sep 17 00:00:00 2001
From: Ralf Stephan <gtrwst9@gmail.com>
Date: Sat, 4 May 2024 09:44:19 +0200
Subject: [PATCH] Ch01: add lemma for proof 4 (#53)
* add lemma for proof 4
Co-authored-by: Moritz Firsching <firsching@google.com>
---
..._Six_proofs_of_the_infinity_of_primes.lean | 22 ++++++++++++++++++-
1 file changed, 21 insertions(+), 1 deletion(-)
diff --git a/FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean b/FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean
index a7ddfc7..65d9fa8 100644
--- a/FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean
+++ b/FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean
@@ -13,7 +13,7 @@ WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-Authors: Moritz Firsching
+Authors: Moritz Firsching, Ralf Stephan
-/
import Mathlib.NumberTheory.LucasLehmer
import Mathlib.NumberTheory.PrimeCounting
@@ -224,6 +224,26 @@ lemma H_P4_1 {k p: ℝ} (hk: k > 0) (hp: p ≥ k + 1): p / (p - 1) ≤ (k + 1) /
one_div_le_one_div h_p_pred_pos hk, @le_sub_iff_add_le]
exact hp
+lemma prod_Icc_succ_div (n : ℕ) (hn : 2 ≤ n) : (∏ x in Icc 1 n, ((x + 1) : ℝ) / x) = n + 1 := by
+ rw [← Nat.Ico_succ_right]
+ induction' n with n h
+ · simp
+ · rw [Finset.prod_Ico_succ_top <| Nat.le_add_left 1 n]
+ norm_num
+ cases' lt_or_ge n 2 with _ h2
+ · interval_cases n
+ · tauto
+ · norm_num
+ specialize h h2
+ field_simp [Finset.prod_eq_zero_iff] at h ⊢
+ rw [h]
+ ring
+
+lemma H_P4_2 (hx : x ≥ 3) (hpi3 : (π 3) = 2) : (∏ x in Icc 1 (π x), ((x + 1) : ℝ) / x) = (π x) + 1 := by
+ rw [prod_Icc_succ_div]
+ rw [← hpi3]
+ refine Monotone.imp monotone_primeCounting ?h
+ linarith
/-!
### Fifth proof