Irrationality of the omega series in factorial base

Checked by the kernel — an outline of the attested proof below: attestations/000314.json, merge commit fee48729440a.

Outline of Proof.lean, extracted by the gate at 82834c4684b8 from the proof’s elaboration: each step is a claim the proof establishes and the goal it leaves. Open a step for what it uses and its Lean lines.

1. h_x3c9 (hω) have ∀ (n : ℕ), (ω : ℕ → ℕ) n = n.primeFactors.card

   Leaves Irrational (∑' (n : ℕ), (↑((ω : ℕ → ℕ) n) : ℝ) / (↑n.factorial : ℝ)), with hω : ∀ (n : ℕ), (ω : ℕ → ℕ) n = n.primeFactors.card.

   Uses library ArithmeticFunction.cardDistinctFactors_apply, List.card_toFinset.

   Lean, lines 18–19

     have hω : ∀ n : ℕ, ω n = n.primeFactors.card := fun n => by
       rw [ArithmeticFunction.cardDistinctFactors_apply, ← List.card_toFinset]; rfl

   targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, lines 18–19 at fee48729440a ↗

2. pow_le have ∀ (k : ℕ), (2 : ℕ) * k ≤ (2 : ℕ) ^ k

   Leaves Irrational (∑' (n : ℕ), (↑((ω : ℕ → ℕ) n) : ℝ) / (↑n.factorial : ℝ)), with pow_le : ∀ (k : ℕ), (2 : ℕ) * k ≤ (2 : ℕ) ^ k.

   Lean, lines 20–25

     have pow_le : ∀ k : ℕ, 2 * k ≤ 2 ^ k := by
       intro k
       rcases k with _ | m
       · simp
       · have := @Nat.lt_two_pow_self m
         rw [pow_succ]; omega

   targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, lines 20–25 at fee48729440a ↗

   1. pow_le.s1 case routine: simp

      Leaves (2 : ℕ) * (0 : ℕ) ≤ (2 : ℕ) ^ (0 : ℕ).

      Lean, line 23

          · simp

      targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 23 at fee48729440a ↗

   2. pow_le.s2 case

      Leaves (2 : ℕ) * (m + (1 : ℕ)) ≤ (2 : ℕ) ^ (m + (1 : ℕ)).

      Uses library pow_succ.

      Lean, lines 24–25

          · have := @Nat.lt_two_pow_self m
            rw [pow_succ]; omega

      targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, lines 24–25 at fee48729440a ↗

      1. pow_le.s2.this have m < (2 : ℕ) ^ m

         Leaves (2 : ℕ) * (m + (1 : ℕ)) ≤ (2 : ℕ) ^ (m + (1 : ℕ)), with this : m < (2 : ℕ) ^ m.

         Uses library Nat.lt_two_pow_self.

         Lean, line 24

             · have := @Nat.lt_two_pow_self m

         targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 24 at fee48729440a ↗

3. h_x3c92 (hω2) have ∀ (n : ℕ), (2 : ℕ) * (ω : ℕ → ℕ) n ≤ n

   Leaves Irrational (∑' (n : ℕ), (↑((ω : ℕ → ℕ) n) : ℝ) / (↑n.factorial : ℝ)), with hω2 : ∀ (n : ℕ), (2 : ℕ) * (ω : ℕ → ℕ) n ≤ n.

   Uses library Nat.eq_zero_or_pos.

   Lean, lines 26–34

     have hω2 : ∀ n : ℕ, 2 * ω n ≤ n := by
       intro n
       rcases Nat.eq_zero_or_pos n with h0 | hpos
       · subst h0; rw [hω]; simp
       · have h1 : 2 ^ n.primeFactors.card ≤ ∏ p ∈ n.primeFactors, p :=
           Finset.pow_card_le_prod _ _ _ (fun p hp => (Nat.prime_of_mem_primeFactors hp).two_le)
         have h2 : ∏ p ∈ n.primeFactors, p ≤ n := Nat.le_of_dvd hpos (Nat.prod_primeFactors_dvd n)
         rw [hω]
         exact (pow_le _).trans (h1.trans h2)

   targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, lines 26–34 at fee48729440a ↗

   1. h_x3c92.s1 case

      Leaves (2 : ℕ) * (ω : ℕ → ℕ) n ≤ n.

      Lean, line 29

          · subst h0; rw [hω]; simp

      targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 29 at fee48729440a ↗

   2. h_x3c92.s2 case

      Leaves (2 : ℕ) * (ω : ℕ → ℕ) n ≤ n.

      Lean, lines 30–34

          · have h1 : 2 ^ n.primeFactors.card ≤ ∏ p ∈ n.primeFactors, p :=
              Finset.pow_card_le_prod _ _ _ (fun p hp => (Nat.prime_of_mem_primeFactors hp).two_le)
            have h2 : ∏ p ∈ n.primeFactors, p ≤ n := Nat.le_of_dvd hpos (Nat.prod_primeFactors_dvd n)
            rw [hω]
            exact (pow_le _).trans (h1.trans h2)

      targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, lines 30–34 at fee48729440a ↗

      1. h_x3c92.s2.h1 have (2 : ℕ) ^ n.primeFactors.card ≤ ∏ p ∈ n.primeFactors, p

         Leaves (2 : ℕ) * (ω : ℕ → ℕ) n ≤ n, with h1 : (2 : ℕ) ^ n.primeFactors.card ≤ ∏ p ∈ n.primeFactors, p.

         Uses library Finset.pow_card_le_prod, Nat.prime_of_mem_primeFactors.

         Lean, lines 30–31

             · have h1 : 2 ^ n.primeFactors.card ≤ ∏ p ∈ n.primeFactors, p :=
                 Finset.pow_card_le_prod _ _ _ (fun p hp => (Nat.prime_of_mem_primeFactors hp).two_le)

         targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, lines 30–31 at fee48729440a ↗

      2. h_x3c92.s2.h2 have ∏ p ∈ n.primeFactors, p ≤ n

         Leaves (2 : ℕ) * (ω : ℕ → ℕ) n ≤ n, with h2 : ∏ p ∈ n.primeFactors, p ≤ n.

         Uses library Nat.le_of_dvd, Nat.prod_primeFactors_dvd.

         Lean, line 32

               have h2 : ∏ p ∈ n.primeFactors, p ≤ n := Nat.le_of_dvd hpos (Nat.prod_primeFactors_dvd n)

         targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 32 at fee48729440a ↗

4. s4 obtain ∃ (a : ℕ → ℝ), a = fun (n : ℕ) => (↑((ω : ℕ → ℕ) n) : ℝ) / (↑n.factorial : ℝ)

   Leaves Irrational (∑' (n : ℕ), (↑((ω : ℕ → ℕ) n) : ℝ) / (↑n.factorial : ℝ)), with a : ℕ → ℝ, ha : a = fun (n : ℕ) => (↑((ω : ℕ → ℕ) n) : ℝ) / (↑n.factorial : ℝ).

   Uses library Exists.intro Existential introduction. , rfl rfl : a = a is the unique constructor of the equality type. .

   Lean, line 35

     obtain ⟨a, ha⟩ : ∃ a : ℕ → ℝ, a = fun n => (ω n : ℝ) / n.factorial := ⟨_, rfl⟩

   targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 35 at fee48729440a ↗

5. fpos have ∀ (n : ℕ), (0 : ℝ) < (↑n.factorial : ℝ)

   Leaves Irrational (∑' (n : ℕ), a n), with fpos : ∀ (n : ℕ), (0 : ℝ) < (↑n.factorial : ℝ).

   Uses library Nat.factorial_pos.

   Lean, line 37

     have fpos : ∀ n : ℕ, (0 : ℝ) < n.factorial := fun n => by exact_mod_cast Nat.factorial_pos n

   targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 37 at fee48729440a ↗

6. a_nonneg have ∀ (n : ℕ), (0 : ℝ) ≤ a n

   Leaves Irrational (∑' (n : ℕ), a n), with a_nonneg : ∀ (n : ℕ), (0 : ℝ) ≤ a n.

   Uses library div_nonneg, Nat.cast_nonneg Specialisation of Nat.cast_nonneg', which seems to be easier for Lean to use. .

   Lean, lines 38–39

     have a_nonneg : ∀ n, 0 ≤ a n := fun n => by
       simp only [ha]; exact div_nonneg (Nat.cast_nonneg _) (fpos n).le

   targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, lines 38–39 at fee48729440a ↗

7. a_le have ∀ (n : ℕ), a n ≤ (2 : ℝ) ^ n / (↑n.factorial : ℝ)

   Leaves Irrational (∑' (n : ℕ), a n), with a_le : ∀ (n : ℕ), a n ≤ (2 : ℝ) ^ n / (↑n.factorial : ℝ).

   Uses library div_le_div_iff_of_pos_right.

   Lean, lines 40–44

     have a_le : ∀ n, a n ≤ (2 : ℝ) ^ n / n.factorial := fun n => by
       simp only [ha]
       rw [div_le_div_iff_of_pos_right (fpos n)]
       have h : ω n ≤ 2 ^ n := by have := hω2 n; have := @Nat.lt_two_pow_self n; omega
       exact_mod_cast h

   targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, lines 40–44 at fee48729440a ↗

   1. a_le.h have (ω : ℕ → ℕ) n ≤ (2 : ℕ) ^ n

      Leaves (↑((ω : ℕ → ℕ) n) : ℝ) ≤ (2 : ℝ) ^ n, with h : (ω : ℕ → ℕ) n ≤ (2 : ℕ) ^ n.

      Lean, line 43

          have h : ω n ≤ 2 ^ n := by have := hω2 n; have := @Nat.lt_two_pow_self n; omega

      targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 43 at fee48729440a ↗

      1. a_le.h.s1 have (2 : ℕ) * (ω : ℕ → ℕ) n ≤ n

         Leaves (ω : ℕ → ℕ) n ≤ (2 : ℕ) ^ n, with this : (2 : ℕ) * (ω : ℕ → ℕ) n ≤ n.

         Lean, line 43

             have h : ω n ≤ 2 ^ n := by have := hω2 n; have := @Nat.lt_two_pow_self n; omega

         targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 43 at fee48729440a ↗

      2. a_le.h.s2 have n < (2 : ℕ) ^ n

         Leaves (ω : ℕ → ℕ) n ≤ (2 : ℕ) ^ n, with this : n < (2 : ℕ) ^ n.

         Uses library Nat.lt_two_pow_self.

         Lean, line 43

             have h : ω n ≤ 2 ^ n := by have := hω2 n; have := @Nat.lt_two_pow_self n; omega

         targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 43 at fee48729440a ↗

8. hs have Summable a

   Leaves Irrational (∑' (n : ℕ), a n), with hs : Summable a.

   Uses library Summable Summable f means that f has some (infinite) sum with respect to L. , Summable.of_nonneg_of_le Comparison test of convergence of series of non-negative real numbers. , Real.summable_pow_div_factorial The series ∑' n, x ^ n / n! is summable of any x : ℝ. .

   Lean, lines 45–46

     have hs : Summable a :=
       Summable.of_nonneg_of_le a_nonneg a_le (Real.summable_pow_div_factorial 2)

   targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, lines 45–46 at fee48729440a ↗

9. s9 obtain ∃ (N : ℕ), N = q.den + (2 : ℕ)

   Leaves False, with N : ℕ, hN : N = q.den + (2 : ℕ).

   Uses library Exists.intro Existential introduction. , rfl rfl : a = a is the unique constructor of the equality type. .

   Lean, line 48

     obtain ⟨N, hN⟩ : ∃ N, N = q.den + 2 := ⟨_, rfl⟩

   targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 48 at fee48729440a ↗

10. hN2 have (2 : ℝ) ≤ (↑N : ℝ)

    Leaves False, with hN2 : (2 : ℝ) ≤ (↑N : ℝ).

    Lean, lines 49–50

      have hN2 : (2 : ℝ) ≤ N := by have : 2 ≤ N := by omega
                                   exact_mod_cast this

    targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, lines 49–50 at fee48729440a ↗

    1. hN2.this have (2 : ℕ) ≤ N routine: omega

       Leaves (2 : ℝ) ≤ (↑N : ℝ), with this : (2 : ℕ) ≤ N.

       Lean, line 49

         have hN2 : (2 : ℝ) ≤ N := by have : 2 ≤ N := by omega

       targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 49 at fee48729440a ↗

11. split have ∑ i ∈ Finset.range (N + (1 : ℕ)), a i + ∑' (i : ℕ), a (i + (N + (1 : ℕ))) = ∑' (i : ℕ), a i

    Leaves False, with split : ∑ i ∈ Finset.range (N + (1 : ℕ)), a i + ∑' (i : ℕ), a (i + (N + (1 : ℕ))) = ∑' (i : ℕ), a i.

    Uses library Summable.sum_add_tsum_nat_add.

    Lean, line 51

      have split := Summable.sum_add_tsum_nat_add (N + 1) hs

    targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 51 at fee48729440a ↗

12. s12 obtain ∃ (T : ℝ), T = ∑' (i : ℕ), a (i + (N + (1 : ℕ)))

    Leaves False, with T : ℝ, hT : T = ∑' (i : ℕ), a (i + (N + (1 : ℕ))).

    Uses library Exists.intro Existential introduction. , rfl rfl : a = a is the unique constructor of the equality type. .

    Lean, line 52

      obtain ⟨T, hT⟩ : ∃ T, T = ∑' i, a (i + (N + 1)) := ⟨_, rfl⟩

    targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 52 at fee48729440a ↗

13. hg have Summable fun (i : ℕ) => a (i + (N + (1 : ℕ)))

    Leaves False, with hg : Summable fun (i : ℕ) => a (i + (N + (1 : ℕ))).

    Uses library Summable Summable f means that f has some (infinite) sum with respect to L. , summable_nat_add_iff.

    Lean, line 53

      have hg : Summable (fun i => a (i + (N + 1))) := (summable_nat_add_iff (N + 1)).mpr hs

    targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 53 at fee48729440a ↗

14. hNF have (0 : ℝ) < (↑N.factorial : ℝ)

    Leaves False, with hNF : (0 : ℝ) < (↑N.factorial : ℝ).

    Lean, line 54

      have hNF : (0 : ℝ) < N.factorial := fpos N

    targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 54 at fee48729440a ↗

15. s15 obtain ∃ (r : ℝ), r = (1 : ℝ) / ((↑N : ℝ) + (1 : ℝ))

    Leaves False, with r : ℝ, hr : r = (1 : ℝ) / ((↑N : ℝ) + (1 : ℝ)).

    Uses library Exists.intro Existential introduction. , rfl rfl : a = a is the unique constructor of the equality type. .

    Lean, line 55

      obtain ⟨r, hr⟩ : ∃ r : ℝ, r = 1 / ((N : ℝ) + 1) := ⟨_, rfl⟩

    targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 55 at fee48729440a ↗

16. r0 have (0 : ℝ) ≤ r

    Leaves False, with r0 : (0 : ℝ) ≤ r.

    Lean, line 56

      have r0 : 0 ≤ r := by rw [hr]; positivity

    targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 56 at fee48729440a ↗

17. r3 have r ≤ (1 / 3 : ℝ)

    Leaves False, with r3 : r ≤ (1 / 3 : ℝ).

    Uses library one_div_le_one_div_of_le.

    Lean, line 57

      have r3 : r ≤ 1 / 3 := by rw [hr]; exact one_div_le_one_div_of_le (by norm_num) (by linarith)

    targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 57 at fee48729440a ↗

18. r1 have r < (1 : ℝ) routine: linarith

    Leaves False, with r1 : r < (1 : ℝ).

    Lean, line 58

      have r1 : r < 1 := by linarith

    targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 58 at fee48729440a ↗

19. term have ∀ (i : ℕ), (↑N.factorial : ℝ) * a (i + (N + (1 : ℕ))) ≤ (1 / 2 : ℝ) * r ^ i

    Leaves False, with term : ∀ (i : ℕ), (↑N.factorial : ℝ) * a (i + (N + (1 : ℕ))) ≤ (1 / 2 : ℝ) * r ^ i.

    Uses library one_div_pow, one_div_mul_one_div, mul_div_assoc', div_le_div_iff₀, one_mul.

    Lean, lines 60–76

      have term : ∀ i, (N.factorial : ℝ) * a (i + (N + 1)) ≤ (1 / 2) * r ^ i := by
        intro i
        have hnat : N.factorial * ω (i + (N + 1)) * (2 * (N + 1) ^ i) ≤ (i + (N + 1)).factorial := by
          have h1 : 2 * ω (i + (N + 1)) ≤ N + i + 1 := by have := hω2 (i + (N + 1)); omega
          have h2 : N.factorial * (N + 1) ^ i ≤ (N + i).factorial := Nat.factorial_mul_pow_le_factorial
          have h3 : (i + (N + 1)).factorial = (N + i + 1) * (N + i).factorial := by
            rw [show i + (N + 1) = (N + i) + 1 by ring]; exact Nat.factorial_succ _
          rw [h3]
          calc N.factorial * ω (i + (N + 1)) * (2 * (N + 1) ^ i)
              = (2 * ω (i + (N + 1))) * (N.factorial * (N + 1) ^ i) := by ring
            _ ≤ (N + i + 1) * (N + i).factorial := Nat.mul_le_mul h1 h2
        have hreal : (N.factorial : ℝ) * ω (i + (N + 1)) * (2 * ((N : ℝ) + 1) ^ i)
            ≤ (i + (N + 1)).factorial := by exact_mod_cast hnat
        simp only [ha]
        rw [hr, one_div_pow, one_div_mul_one_div, mul_div_assoc',
          div_le_div_iff₀ (fpos _) (by positivity), one_mul]
        exact hreal

    targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, lines 60–76 at fee48729440a ↗

    1. term.hnat have N.factorial * (ω : ℕ → ℕ) (i + (N + (1 : ℕ))) * ((2 : ℕ) * (N + (1 : ℕ)) ^ i) ≤ (i + (N + (1 : ℕ))).factorial

       Leaves (↑N.factorial : ℝ) * a (i + (N + (1 : ℕ))) ≤ (1 / 2 : ℝ) * r ^ i, with hnat : N.factorial * (ω : ℕ → ℕ) (i + (N + (1 : ℕ))) * ((2 : ℕ) * (N + (1 : ℕ)) ^ i) ≤ (i + (N + (1 : ℕ))).factorial.

       Lean, lines 62–70

           have hnat : N.factorial * ω (i + (N + 1)) * (2 * (N + 1) ^ i) ≤ (i + (N + 1)).factorial := by
             have h1 : 2 * ω (i + (N + 1)) ≤ N + i + 1 := by have := hω2 (i + (N + 1)); omega
             have h2 : N.factorial * (N + 1) ^ i ≤ (N + i).factorial := Nat.factorial_mul_pow_le_factorial
             have h3 : (i + (N + 1)).factorial = (N + i + 1) * (N + i).factorial := by
               rw [show i + (N + 1) = (N + i) + 1 by ring]; exact Nat.factorial_succ _
             rw [h3]
             calc N.factorial * ω (i + (N + 1)) * (2 * (N + 1) ^ i)
                 = (2 * ω (i + (N + 1))) * (N.factorial * (N + 1) ^ i) := by ring
               _ ≤ (N + i + 1) * (N + i).factorial := Nat.mul_le_mul h1 h2

       targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, lines 62–70 at fee48729440a ↗

       1. term.hnat.h1 have (2 : ℕ) * (ω : ℕ → ℕ) (i + (N + (1 : ℕ))) ≤ N + i + (1 : ℕ)

          Leaves N.factorial * (ω : ℕ → ℕ) (i + (N + (1 : ℕ))) * ((2 : ℕ) * (N + (1 : ℕ)) ^ i) ≤ (i + (N + (1 : ℕ))).factorial, with h1 : (2 : ℕ) * (ω : ℕ → ℕ) (i + (N + (1 : ℕ))) ≤ N + i + (1 : ℕ).

          Lean, line 63

                have h1 : 2 * ω (i + (N + 1)) ≤ N + i + 1 := by have := hω2 (i + (N + 1)); omega

          targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 63 at fee48729440a ↗

          1. term.hnat.h1.this have (2 : ℕ) * (ω : ℕ → ℕ) (i + (N + (1 : ℕ))) ≤ i + (N + (1 : ℕ))

             Leaves (2 : ℕ) * (ω : ℕ → ℕ) (i + (N + (1 : ℕ))) ≤ N + i + (1 : ℕ), with this : (2 : ℕ) * (ω : ℕ → ℕ) (i + (N + (1 : ℕ))) ≤ i + (N + (1 : ℕ)).

             Lean, line 63

                   have h1 : 2 * ω (i + (N + 1)) ≤ N + i + 1 := by have := hω2 (i + (N + 1)); omega

             targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 63 at fee48729440a ↗

       2. term.hnat.h2 have N.factorial * (N + (1 : ℕ)) ^ i ≤ (N + i).factorial

          Leaves N.factorial * (ω : ℕ → ℕ) (i + (N + (1 : ℕ))) * ((2 : ℕ) * (N + (1 : ℕ)) ^ i) ≤ (i + (N + (1 : ℕ))).factorial, with h2 : N.factorial * (N + (1 : ℕ)) ^ i ≤ (N + i).factorial.

          Uses library Nat.factorial_mul_pow_le_factorial.

          Lean, line 64

                have h2 : N.factorial * (N + 1) ^ i ≤ (N + i).factorial := Nat.factorial_mul_pow_le_factorial

          targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 64 at fee48729440a ↗

       3. term.hnat.h3 have (i + (N + (1 : ℕ))).factorial = (N + i + (1 : ℕ)) * (N + i).factorial

          Leaves N.factorial * (ω : ℕ → ℕ) (i + (N + (1 : ℕ))) * ((2 : ℕ) * (N + (1 : ℕ)) ^ i) ≤ (i + (N + (1 : ℕ))).factorial, with h3 : (i + (N + (1 : ℕ))).factorial = (N + i + (1 : ℕ)) * (N + i).factorial.

          Uses library Nat.factorial_succ.

          Lean, lines 65–66

                have h3 : (i + (N + 1)).factorial = (N + i + 1) * (N + i).factorial := by
                  rw [show i + (N + 1) = (N + i) + 1 by ring]; exact Nat.factorial_succ _

          targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, lines 65–66 at fee48729440a ↗

       4. term.hnat.s4 calc N.factorial * (ω : ℕ → ℕ) (i + (N + (1 : ℕ))) * ((2 : ℕ) * (N + (1 : ℕ)) ^ i) = (2 : ℕ) * (ω : ℕ → ℕ) (i + (N + (1 : ℕ))) * (N.factorial * (N + (1 : ℕ)) ^ i) routine: ring

          Closes the goal.

          Lean, lines 68–69

                calc N.factorial * ω (i + (N + 1)) * (2 * (N + 1) ^ i)
                    = (2 * ω (i + (N + 1))) * (N.factorial * (N + 1) ^ i) := by ring

          targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, lines 68–69 at fee48729440a ↗

       5. term.hnat.s5 calc (2 : ℕ) * (ω : ℕ → ℕ) (i + (N + (1 : ℕ))) * (N.factorial * (N + (1 : ℕ)) ^ i) ≤ (N + i + (1 : ℕ)) * (N + i).factorial

          Closes the goal.

          Uses library Nat.mul_le_mul.

          Lean, line 70

                  _ ≤ (N + i + 1) * (N + i).factorial := Nat.mul_le_mul h1 h2

          targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 70 at fee48729440a ↗

    2. term.hreal have (↑N.factorial : ℝ) * (↑((ω : ℕ → ℕ) (i + (N + (1 : ℕ)))) : ℝ) * ((2 : ℝ) * ((↑N : ℝ) + (1 : ℝ)) ^ i) ≤ (↑(i + (N + (1 : ℕ))).factorial : ℝ)

       Leaves (↑N.factorial : ℝ) * a (i + (N + (1 : ℕ))) ≤ (1 / 2 : ℝ) * r ^ i, with hreal : (↑N.factorial : ℝ) * (↑((ω : ℕ → ℕ) (i + (N + (1 : ℕ)))) : ℝ) * ((2 : ℝ) * ((↑N : ℝ) + (1 : ℝ)) ^ i) ≤ (↑(i + (N + (1 : ℕ))).factorial : ℝ).

       Lean, lines 71–72

           have hreal : (N.factorial : ℝ) * ω (i + (N + 1)) * (2 * ((N : ℝ) + 1) ^ i)
               ≤ (i + (N + 1)).factorial := by exact_mod_cast hnat

       targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, lines 71–72 at fee48729440a ↗

20. geo have Summable fun (i : ℕ) => (1 / 2 : ℝ) * r ^ i

    Leaves False, with geo : Summable fun (i : ℕ) => (1 / 2 : ℝ) * r ^ i.

    Uses library Summable Summable f means that f has some (infinite) sum with respect to L. , summable_geometric_of_lt_one.

    Lean, lines 77–78

      have geo : Summable (fun i : ℕ => (1 / 2 : ℝ) * r ^ i) :=
        (summable_geometric_of_lt_one r0 r1).mul_left _

    targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, lines 77–78 at fee48729440a ↗

21. hTle have (↑N.factorial : ℝ) * T ≤ (1 / 2 : ℝ) * ((1 : ℝ) - r)⁻¹

    Leaves False, with hTle : (↑N.factorial : ℝ) * T ≤ (1 / 2 : ℝ) * ((1 : ℝ) - r)⁻¹.

    Uses library tsum_mul_left, tsum_geometric_of_lt_one, Summable.tsum_le_tsum.

    Lean, lines 79–81

      have hTle : (N.factorial : ℝ) * T ≤ (1 / 2) * (1 - r)⁻¹ := by
        rw [hT, ← tsum_mul_left, ← tsum_geometric_of_lt_one r0 r1, ← tsum_mul_left]
        exact Summable.tsum_le_tsum term (hg.mul_left _) geo

    targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, lines 79–81 at fee48729440a ↗

22. hlt have (1 / 2 : ℝ) * ((1 : ℝ) - r)⁻¹ < (1 : ℝ)

    Leaves False, with hlt : (1 / 2 : ℝ) * ((1 : ℝ) - r)⁻¹ < (1 : ℝ).

    Lean, lines 82–87

      have hlt : (1 / 2 : ℝ) * (1 - r)⁻¹ < 1 := by
        have h1 : (2 / 3 : ℝ) ≤ 1 - r := by linarith
        have h2 : (1 - r)⁻¹ ≤ (2 / 3 : ℝ)⁻¹ := inv_anti₀ (by norm_num) h1
        calc (1 / 2 : ℝ) * (1 - r)⁻¹ ≤ 1 / 2 * (2 / 3 : ℝ)⁻¹ :=
              mul_le_mul_of_nonneg_left h2 (by norm_num)
          _ < 1 := by norm_num

    targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, lines 82–87 at fee48729440a ↗

    1. hlt.h1 have (2 / 3 : ℝ) ≤ (1 : ℝ) - r routine: linarith

       Leaves (1 / 2 : ℝ) * ((1 : ℝ) - r)⁻¹ < (1 : ℝ), with h1 : (2 / 3 : ℝ) ≤ (1 : ℝ) - r.

       Lean, line 83

           have h1 : (2 / 3 : ℝ) ≤ 1 - r := by linarith

       targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 83 at fee48729440a ↗

    2. hlt.h2 have ((1 : ℝ) - r)⁻¹ ≤ (2 / 3 : ℝ)⁻¹

       Leaves (1 / 2 : ℝ) * ((1 : ℝ) - r)⁻¹ < (1 : ℝ), with h2 : ((1 : ℝ) - r)⁻¹ ≤ (2 / 3 : ℝ)⁻¹.

       Uses library inv_anti₀.

       Lean, line 84

           have h2 : (1 - r)⁻¹ ≤ (2 / 3 : ℝ)⁻¹ := inv_anti₀ (by norm_num) h1

       targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 84 at fee48729440a ↗

    3. hlt.s3 calc (1 / 2 : ℝ) * ((1 : ℝ) - r)⁻¹ ≤ (1 / 2 : ℝ) * (2 / 3 : ℝ)⁻¹

       Closes the goal.

       Uses library mul_le_mul_of_nonneg_left.

       Lean, lines 85–86

           calc (1 / 2 : ℝ) * (1 - r)⁻¹ ≤ 1 / 2 * (2 / 3 : ℝ)⁻¹ :=
                 mul_le_mul_of_nonneg_left h2 (by norm_num)

       targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, lines 85–86 at fee48729440a ↗

    4. hlt.s4 calc routine: norm_num

       Closes the goal.

       Lean, line 87

             _ < 1 := by norm_num

       targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 87 at fee48729440a ↗

23. hTpos have (0 : ℝ) < T

    Leaves False, with hTpos : (0 : ℝ) < T.

    Uses library zero_add, div_pos.

    Lean, lines 89–95

      have hTpos : 0 < T := by
        rw [hT]
        refine hg.tsum_pos (fun i => a_nonneg _) 0 ?_
        simp only [ha, zero_add]
        apply div_pos _ (fpos _)
        have : 0 < ω (N + 1) := ArithmeticFunction.cardDistinctFactors_pos.mpr (by omega)
        exact_mod_cast this

    targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, lines 89–95 at fee48729440a ↗

    1. hTpos.this have (0 : ℕ) < (ω : ℕ → ℕ) (N + (1 : ℕ))

       Leaves (0 : ℝ) < (↑((ω : ℕ → ℕ) (N + (1 : ℕ))) : ℝ), with this : (0 : ℕ) < (ω : ℕ → ℕ) (N + (1 : ℕ)).

       Uses library ArithmeticFunction.cardDistinctFactors_pos.

       Lean, line 94

           have : 0 < ω (N + 1) := ArithmeticFunction.cardDistinctFactors_pos.mpr (by omega)

       targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 94 at fee48729440a ↗

24. s24 obtain ∃ (Z : ℕ), Z = ∑ i ∈ Finset.range (N + (1 : ℕ)), (ω : ℕ → ℕ) i * (N.factorial / i.factorial)

    Leaves False, with Z : ℕ, hZ : Z = ∑ i ∈ Finset.range (N + (1 : ℕ)), (ω : ℕ → ℕ) i * (N.factorial / i.factorial).

    Uses library Finset.range range n is the set of natural numbers less than n. , Exists.intro Existential introduction. , rfl rfl : a = a is the unique constructor of the equality type. .

    Lean, lines 97–98

      obtain ⟨Z, hZ⟩ : ∃ Z : ℕ,
          Z = ∑ i ∈ Finset.range (N + 1), ω i * (N.factorial / i.factorial) := ⟨_, rfl⟩

    targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, lines 97–98 at fee48729440a ↗

25. hZ' have (↑N.factorial : ℝ) * ∑ i ∈ Finset.range (N + (1 : ℕ)), a i = (↑Z : ℝ)

    Leaves False, with hZ' : (↑N.factorial : ℝ) * ∑ i ∈ Finset.range (N + (1 : ℕ)), a i = (↑Z : ℝ).

    Uses library Finset.range range n is the set of natural numbers less than n. , Finset.mul_sum, Nat.cast_sum, Finset.sum_congr, rfl rfl : a = a is the unique constructor of the equality type. , Nat.cast_mul, Nat.cast_div, Nat.factorial_dvd_factorial.

    Lean, lines 99–105

      have hZ' : (N.factorial : ℝ) * ∑ i ∈ Finset.range (N + 1), a i = Z := by
        rw [hZ, Finset.mul_sum, Nat.cast_sum]
        apply Finset.sum_congr rfl
        intro i hi
        have hi' : i ≤ N := Nat.lt_succ_iff.mp (Finset.mem_range.mp hi)
        rw [Nat.cast_mul, Nat.cast_div (Nat.factorial_dvd_factorial hi') (fpos i).ne']
        simp only [ha]; ring

    targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, lines 99–105 at fee48729440a ↗

    1. hZ'.hi' have i ≤ N

       Leaves (↑N.factorial : ℝ) * a i = (↑((ω : ℕ → ℕ) i * (N.factorial / i.factorial)) : ℝ), with hi' : i ≤ N.

       Uses library Nat.lt_succ_iff, Finset.mem_range.

       Lean, line 103

           have hi' : i ≤ N := Nat.lt_succ_iff.mp (Finset.mem_range.mp hi)

       targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 103 at fee48729440a ↗

26. hden have q.den ∣ N.factorial

    Leaves False, with hden : q.den ∣ N.factorial.

    Uses library Nat.dvd_factorial.

    Lean, line 107

      have hden : q.den ∣ N.factorial := Nat.dvd_factorial q.den_pos (by omega)

    targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 107 at fee48729440a ↗

27. hM have (↑N.factorial : ℝ) * (↑q : ℝ) = (↑(q.num * (↑(N.factorial / q.den) : ℤ)) : ℝ)

    Leaves False, with hM : (↑N.factorial : ℝ) * (↑q : ℝ) = (↑(q.num * (↑(N.factorial / q.den) : ℤ)) : ℝ).

    Uses library Int.cast_mul, Int.cast_natCast, Nat.cast_div, Nat.cast_ne_zero, Rat.cast_def.

    Lean, lines 108–111

      have hM : (N.factorial : ℝ) * q = ((q.num * ((N.factorial / q.den : ℕ) : ℤ) : ℤ) : ℝ) := by
        rw [Int.cast_mul, Int.cast_natCast, Nat.cast_div hden (Nat.cast_ne_zero.mpr q.den_nz),
          Rat.cast_def]
        ring

    targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, lines 108–111 at fee48729440a ↗

28. key have (↑N.factorial : ℝ) * T = (↑(q.num * (↑(N.factorial / q.den) : ℤ) - (↑Z : ℤ)) : ℝ)

    Leaves False, with key : (↑N.factorial : ℝ) * T = (↑(q.num * (↑(N.factorial / q.den) : ℤ) - (↑Z : ℤ)) : ℝ).

    Uses library Int.cast_sub, mul_add Alias of left_distrib. .

    Lean, lines 112–115

      have key : (N.factorial : ℝ) * T
          = (((q.num * ((N.factorial / q.den : ℕ) : ℤ)) - Z : ℤ) : ℝ) := by
        rw [Int.cast_sub, ← hM, hq, ← split, ← hT, mul_add, hZ']
        push_cast; ring

    targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, lines 112–115 at fee48729440a ↗

29. i1 have (0 : ℤ) < q.num * (↑(N.factorial / q.den) : ℤ) - (↑Z : ℤ)

    Leaves False, with i1 : (0 : ℤ) < q.num * (↑(N.factorial / q.den) : ℤ) - (↑Z : ℤ).

    Lean, lines 116–118

      have i1 : (0 : ℤ) < q.num * ((N.factorial / q.den : ℕ) : ℤ) - Z := by
        have h : (0 : ℝ) < (N.factorial : ℝ) * T := mul_pos hNF hTpos
        rw [key] at h; exact_mod_cast h

    targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, lines 116–118 at fee48729440a ↗

    1. i1.h have (0 : ℝ) < (↑N.factorial : ℝ) * T

       Leaves (0 : ℤ) < q.num * (↑(N.factorial / q.den) : ℤ) - (↑Z : ℤ), with h : (0 : ℝ) < (↑N.factorial : ℝ) * T.

       Uses library mul_pos Alias of Left.mul_pos. .

       Lean, line 117

           have h : (0 : ℝ) < (N.factorial : ℝ) * T := mul_pos hNF hTpos

       targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 117 at fee48729440a ↗

30. i2 have q.num * (↑(N.factorial / q.den) : ℤ) - (↑Z : ℤ) < (1 : ℤ)

    Leaves False, with i2 : q.num * (↑(N.factorial / q.den) : ℤ) - (↑Z : ℤ) < (1 : ℤ).

    Lean, lines 119–121

      have i2 : q.num * ((N.factorial / q.den : ℕ) : ℤ) - Z < 1 := by
        have h : (N.factorial : ℝ) * T < 1 := lt_of_le_of_lt hTle hlt
        rw [key] at h; exact_mod_cast h

    targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, lines 119–121 at fee48729440a ↗

    1. i2.h have (↑N.factorial : ℝ) * T < (1 : ℝ)

       Leaves q.num * (↑(N.factorial / q.den) : ℤ) - (↑Z : ℤ) < (1 : ℤ), with h : (↑N.factorial : ℝ) * T < (1 : ℝ).

       Uses library lt_of_le_of_lt.

       Lean, line 120

           have h : (N.factorial : ℝ) * T < 1 := lt_of_le_of_lt hTle hlt

       targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean, line 120 at fee48729440a ↗