Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  emcllem7 Structured version   Visualization version   GIF version

Theorem emcllem7 25596
 Description: Lemma for emcl 25597 and harmonicbnd 25598. Derive bounds on γ as 𝐹(1) and 𝐺(1). (Contributed by Mario Carneiro, 11-Jul-2014.) (Revised by Mario Carneiro, 9-Apr-2016.)
Hypotheses
Ref Expression
emcl.1 𝐹 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛)))
emcl.2 𝐺 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1))))
emcl.3 𝐻 = (𝑛 ∈ ℕ ↦ (log‘(1 + (1 / 𝑛))))
emcl.4 𝑇 = (𝑛 ∈ ℕ ↦ ((1 / 𝑛) − (log‘(1 + (1 / 𝑛)))))
Assertion
Ref Expression
emcllem7 (γ ∈ ((1 − (log‘2))[,]1) ∧ 𝐹:ℕ⟶(γ[,]1) ∧ 𝐺:ℕ⟶((1 − (log‘2))[,]γ))
Distinct variable groups:   𝑚,𝐻   𝑚,𝑛,𝑇
Allowed substitution hints:   𝐹(𝑚,𝑛)   𝐺(𝑚,𝑛)   𝐻(𝑛)

Proof of Theorem emcllem7
Dummy variables 𝑖 𝑘 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 12280 . . . . 5 ℕ = (ℤ‘1)
2 1zzd 12012 . . . . 5 (⊤ → 1 ∈ ℤ)
3 emcl.1 . . . . . . . 8 𝐹 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛)))
4 emcl.2 . . . . . . . 8 𝐺 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1))))
5 emcl.3 . . . . . . . 8 𝐻 = (𝑛 ∈ ℕ ↦ (log‘(1 + (1 / 𝑛))))
6 emcl.4 . . . . . . . 8 𝑇 = (𝑛 ∈ ℕ ↦ ((1 / 𝑛) − (log‘(1 + (1 / 𝑛)))))
73, 4, 5, 6emcllem6 25595 . . . . . . 7 (𝐹 ⇝ γ ∧ 𝐺 ⇝ γ)
87simpri 489 . . . . . 6 𝐺 ⇝ γ
98a1i 11 . . . . 5 (⊤ → 𝐺 ⇝ γ)
103, 4emcllem1 25590 . . . . . . . 8 (𝐹:ℕ⟶ℝ ∧ 𝐺:ℕ⟶ℝ)
1110simpri 489 . . . . . . 7 𝐺:ℕ⟶ℝ
1211ffvelrni 6843 . . . . . 6 (𝑘 ∈ ℕ → (𝐺𝑘) ∈ ℝ)
1312adantl 485 . . . . 5 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ℝ)
141, 2, 9, 13climrecl 14942 . . . 4 (⊤ → γ ∈ ℝ)
15 1nn 11647 . . . . 5 1 ∈ ℕ
16 simpr 488 . . . . . . 7 ((⊤ ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℕ)
178a1i 11 . . . . . . 7 ((⊤ ∧ 𝑖 ∈ ℕ) → 𝐺 ⇝ γ)
1812adantl 485 . . . . . . 7 (((⊤ ∧ 𝑖 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ℝ)
193, 4emcllem2 25591 . . . . . . . . 9 (𝑘 ∈ ℕ → ((𝐹‘(𝑘 + 1)) ≤ (𝐹𝑘) ∧ (𝐺𝑘) ≤ (𝐺‘(𝑘 + 1))))
2019simprd 499 . . . . . . . 8 (𝑘 ∈ ℕ → (𝐺𝑘) ≤ (𝐺‘(𝑘 + 1)))
2120adantl 485 . . . . . . 7 (((⊤ ∧ 𝑖 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) ≤ (𝐺‘(𝑘 + 1)))
221, 16, 17, 18, 21climub 15020 . . . . . 6 ((⊤ ∧ 𝑖 ∈ ℕ) → (𝐺𝑖) ≤ γ)
2322ralrimiva 3177 . . . . 5 (⊤ → ∀𝑖 ∈ ℕ (𝐺𝑖) ≤ γ)
24 fveq2 6663 . . . . . . . 8 (𝑖 = 1 → (𝐺𝑖) = (𝐺‘1))
25 oveq2 7159 . . . . . . . . . . . . 13 (𝑛 = 1 → (1...𝑛) = (1...1))
2625sumeq1d 15060 . . . . . . . . . . . 12 (𝑛 = 1 → Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) = Σ𝑚 ∈ (1...1)(1 / 𝑚))
27 1z 12011 . . . . . . . . . . . . 13 1 ∈ ℤ
28 ax-1cn 10595 . . . . . . . . . . . . 13 1 ∈ ℂ
29 oveq2 7159 . . . . . . . . . . . . . . 15 (𝑚 = 1 → (1 / 𝑚) = (1 / 1))
30 1div1e1 11330 . . . . . . . . . . . . . . 15 (1 / 1) = 1
3129, 30syl6eq 2875 . . . . . . . . . . . . . 14 (𝑚 = 1 → (1 / 𝑚) = 1)
3231fsum1 15104 . . . . . . . . . . . . 13 ((1 ∈ ℤ ∧ 1 ∈ ℂ) → Σ𝑚 ∈ (1...1)(1 / 𝑚) = 1)
3327, 28, 32mp2an 691 . . . . . . . . . . . 12 Σ𝑚 ∈ (1...1)(1 / 𝑚) = 1
3426, 33syl6eq 2875 . . . . . . . . . . 11 (𝑛 = 1 → Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) = 1)
35 oveq1 7158 . . . . . . . . . . . . 13 (𝑛 = 1 → (𝑛 + 1) = (1 + 1))
36 df-2 11699 . . . . . . . . . . . . 13 2 = (1 + 1)
3735, 36eqtr4di 2877 . . . . . . . . . . . 12 (𝑛 = 1 → (𝑛 + 1) = 2)
3837fveq2d 6667 . . . . . . . . . . 11 (𝑛 = 1 → (log‘(𝑛 + 1)) = (log‘2))
3934, 38oveq12d 7169 . . . . . . . . . 10 (𝑛 = 1 → (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1))) = (1 − (log‘2)))
40 1re 10641 . . . . . . . . . . . 12 1 ∈ ℝ
41 2rp 12393 . . . . . . . . . . . . 13 2 ∈ ℝ+
42 relogcl 25176 . . . . . . . . . . . . 13 (2 ∈ ℝ+ → (log‘2) ∈ ℝ)
4341, 42ax-mp 5 . . . . . . . . . . . 12 (log‘2) ∈ ℝ
4440, 43resubcli 10948 . . . . . . . . . . 11 (1 − (log‘2)) ∈ ℝ
4544elexi 3499 . . . . . . . . . 10 (1 − (log‘2)) ∈ V
4639, 4, 45fvmpt 6761 . . . . . . . . 9 (1 ∈ ℕ → (𝐺‘1) = (1 − (log‘2)))
4715, 46ax-mp 5 . . . . . . . 8 (𝐺‘1) = (1 − (log‘2))
4824, 47syl6eq 2875 . . . . . . 7 (𝑖 = 1 → (𝐺𝑖) = (1 − (log‘2)))
4948breq1d 5063 . . . . . 6 (𝑖 = 1 → ((𝐺𝑖) ≤ γ ↔ (1 − (log‘2)) ≤ γ))
5049rspcva 3607 . . . . 5 ((1 ∈ ℕ ∧ ∀𝑖 ∈ ℕ (𝐺𝑖) ≤ γ) → (1 − (log‘2)) ≤ γ)
5115, 23, 50sylancr 590 . . . 4 (⊤ → (1 − (log‘2)) ≤ γ)
52 fveq2 6663 . . . . . . . . . . . 12 (𝑥 = 𝑖 → (𝐹𝑥) = (𝐹𝑖))
5352negeqd 10880 . . . . . . . . . . 11 (𝑥 = 𝑖 → -(𝐹𝑥) = -(𝐹𝑖))
54 eqid 2824 . . . . . . . . . . 11 (𝑥 ∈ ℕ ↦ -(𝐹𝑥)) = (𝑥 ∈ ℕ ↦ -(𝐹𝑥))
55 negex 10884 . . . . . . . . . . 11 -(𝐹𝑖) ∈ V
5653, 54, 55fvmpt 6761 . . . . . . . . . 10 (𝑖 ∈ ℕ → ((𝑥 ∈ ℕ ↦ -(𝐹𝑥))‘𝑖) = -(𝐹𝑖))
5756adantl 485 . . . . . . . . 9 ((⊤ ∧ 𝑖 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ -(𝐹𝑥))‘𝑖) = -(𝐹𝑖))
587simpli 487 . . . . . . . . . . . . 13 𝐹 ⇝ γ
5958a1i 11 . . . . . . . . . . . 12 (⊤ → 𝐹 ⇝ γ)
60 0cnd 10634 . . . . . . . . . . . 12 (⊤ → 0 ∈ ℂ)
61 nnex 11642 . . . . . . . . . . . . . 14 ℕ ∈ V
6261mptex 6979 . . . . . . . . . . . . 13 (𝑥 ∈ ℕ ↦ -(𝐹𝑥)) ∈ V
6362a1i 11 . . . . . . . . . . . 12 (⊤ → (𝑥 ∈ ℕ ↦ -(𝐹𝑥)) ∈ V)
6410simpli 487 . . . . . . . . . . . . . . 15 𝐹:ℕ⟶ℝ
6564ffvelrni 6843 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → (𝐹𝑘) ∈ ℝ)
6665adantl 485 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℝ)
6766recnd 10669 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℂ)
68 fveq2 6663 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑘 → (𝐹𝑥) = (𝐹𝑘))
6968negeqd 10880 . . . . . . . . . . . . . . 15 (𝑥 = 𝑘 → -(𝐹𝑥) = -(𝐹𝑘))
70 negex 10884 . . . . . . . . . . . . . . 15 -(𝐹𝑘) ∈ V
7169, 54, 70fvmpt 6761 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → ((𝑥 ∈ ℕ ↦ -(𝐹𝑥))‘𝑘) = -(𝐹𝑘))
7271adantl 485 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ -(𝐹𝑥))‘𝑘) = -(𝐹𝑘))
73 df-neg 10873 . . . . . . . . . . . . 13 -(𝐹𝑘) = (0 − (𝐹𝑘))
7472, 73syl6eq 2875 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ -(𝐹𝑥))‘𝑘) = (0 − (𝐹𝑘)))
751, 2, 59, 60, 63, 67, 74climsubc2 14997 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ ℕ ↦ -(𝐹𝑥)) ⇝ (0 − γ))
7675adantr 484 . . . . . . . . . 10 ((⊤ ∧ 𝑖 ∈ ℕ) → (𝑥 ∈ ℕ ↦ -(𝐹𝑥)) ⇝ (0 − γ))
7766renegcld 11067 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ) → -(𝐹𝑘) ∈ ℝ)
7872, 77eqeltrd 2916 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ -(𝐹𝑥))‘𝑘) ∈ ℝ)
7978adantlr 714 . . . . . . . . . 10 (((⊤ ∧ 𝑖 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ -(𝐹𝑥))‘𝑘) ∈ ℝ)
8019simpld 498 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → (𝐹‘(𝑘 + 1)) ≤ (𝐹𝑘))
8180adantl 485 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ≤ (𝐹𝑘))
82 peano2nn 11648 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
8382adantl 485 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
8464ffvelrni 6843 . . . . . . . . . . . . . . 15 ((𝑘 + 1) ∈ ℕ → (𝐹‘(𝑘 + 1)) ∈ ℝ)
8583, 84syl 17 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ∈ ℝ)
8685, 66lenegd 11219 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝐹‘(𝑘 + 1)) ≤ (𝐹𝑘) ↔ -(𝐹𝑘) ≤ -(𝐹‘(𝑘 + 1))))
8781, 86mpbid 235 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ) → -(𝐹𝑘) ≤ -(𝐹‘(𝑘 + 1)))
88 fveq2 6663 . . . . . . . . . . . . . . 15 (𝑥 = (𝑘 + 1) → (𝐹𝑥) = (𝐹‘(𝑘 + 1)))
8988negeqd 10880 . . . . . . . . . . . . . 14 (𝑥 = (𝑘 + 1) → -(𝐹𝑥) = -(𝐹‘(𝑘 + 1)))
90 negex 10884 . . . . . . . . . . . . . 14 -(𝐹‘(𝑘 + 1)) ∈ V
9189, 54, 90fvmpt 6761 . . . . . . . . . . . . 13 ((𝑘 + 1) ∈ ℕ → ((𝑥 ∈ ℕ ↦ -(𝐹𝑥))‘(𝑘 + 1)) = -(𝐹‘(𝑘 + 1)))
9283, 91syl 17 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ -(𝐹𝑥))‘(𝑘 + 1)) = -(𝐹‘(𝑘 + 1)))
9387, 72, 923brtr4d 5085 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ -(𝐹𝑥))‘𝑘) ≤ ((𝑥 ∈ ℕ ↦ -(𝐹𝑥))‘(𝑘 + 1)))
9493adantlr 714 . . . . . . . . . 10 (((⊤ ∧ 𝑖 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ -(𝐹𝑥))‘𝑘) ≤ ((𝑥 ∈ ℕ ↦ -(𝐹𝑥))‘(𝑘 + 1)))
951, 16, 76, 79, 94climub 15020 . . . . . . . . 9 ((⊤ ∧ 𝑖 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ -(𝐹𝑥))‘𝑖) ≤ (0 − γ))
9657, 95eqbrtrrd 5077 . . . . . . . 8 ((⊤ ∧ 𝑖 ∈ ℕ) → -(𝐹𝑖) ≤ (0 − γ))
97 df-neg 10873 . . . . . . . 8 -γ = (0 − γ)
9896, 97breqtrrdi 5095 . . . . . . 7 ((⊤ ∧ 𝑖 ∈ ℕ) → -(𝐹𝑖) ≤ -γ)
9914mptru 1545 . . . . . . . 8 γ ∈ ℝ
10064ffvelrni 6843 . . . . . . . . 9 (𝑖 ∈ ℕ → (𝐹𝑖) ∈ ℝ)
101100adantl 485 . . . . . . . 8 ((⊤ ∧ 𝑖 ∈ ℕ) → (𝐹𝑖) ∈ ℝ)
102 leneg 11143 . . . . . . . 8 ((γ ∈ ℝ ∧ (𝐹𝑖) ∈ ℝ) → (γ ≤ (𝐹𝑖) ↔ -(𝐹𝑖) ≤ -γ))
10399, 101, 102sylancr 590 . . . . . . 7 ((⊤ ∧ 𝑖 ∈ ℕ) → (γ ≤ (𝐹𝑖) ↔ -(𝐹𝑖) ≤ -γ))
10498, 103mpbird 260 . . . . . 6 ((⊤ ∧ 𝑖 ∈ ℕ) → γ ≤ (𝐹𝑖))
105104ralrimiva 3177 . . . . 5 (⊤ → ∀𝑖 ∈ ℕ γ ≤ (𝐹𝑖))
106 fveq2 6663 . . . . . . . 8 (𝑖 = 1 → (𝐹𝑖) = (𝐹‘1))
107 fveq2 6663 . . . . . . . . . . . . 13 (𝑛 = 1 → (log‘𝑛) = (log‘1))
108 log1 25186 . . . . . . . . . . . . 13 (log‘1) = 0
109107, 108syl6eq 2875 . . . . . . . . . . . 12 (𝑛 = 1 → (log‘𝑛) = 0)
11034, 109oveq12d 7169 . . . . . . . . . . 11 (𝑛 = 1 → (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛)) = (1 − 0))
111 1m0e1 11757 . . . . . . . . . . 11 (1 − 0) = 1
112110, 111syl6eq 2875 . . . . . . . . . 10 (𝑛 = 1 → (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛)) = 1)
11340elexi 3499 . . . . . . . . . 10 1 ∈ V
114112, 3, 113fvmpt 6761 . . . . . . . . 9 (1 ∈ ℕ → (𝐹‘1) = 1)
11515, 114ax-mp 5 . . . . . . . 8 (𝐹‘1) = 1
116106, 115syl6eq 2875 . . . . . . 7 (𝑖 = 1 → (𝐹𝑖) = 1)
117116breq2d 5065 . . . . . 6 (𝑖 = 1 → (γ ≤ (𝐹𝑖) ↔ γ ≤ 1))
118117rspcva 3607 . . . . 5 ((1 ∈ ℕ ∧ ∀𝑖 ∈ ℕ γ ≤ (𝐹𝑖)) → γ ≤ 1)
11915, 105, 118sylancr 590 . . . 4 (⊤ → γ ≤ 1)
12044, 40elicc2i 12802 . . . 4 (γ ∈ ((1 − (log‘2))[,]1) ↔ (γ ∈ ℝ ∧ (1 − (log‘2)) ≤ γ ∧ γ ≤ 1))
12114, 51, 119, 120syl3anbrc 1340 . . 3 (⊤ → γ ∈ ((1 − (log‘2))[,]1))
122 ffn 6505 . . . . 5 (𝐹:ℕ⟶ℝ → 𝐹 Fn ℕ)
12364, 122mp1i 13 . . . 4 (⊤ → 𝐹 Fn ℕ)
12416, 1eleqtrdi 2926 . . . . . . . 8 ((⊤ ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ (ℤ‘1))
125 elfznn 12942 . . . . . . . . . 10 (𝑘 ∈ (1...𝑖) → 𝑘 ∈ ℕ)
126125adantl 485 . . . . . . . . 9 (((⊤ ∧ 𝑖 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑖)) → 𝑘 ∈ ℕ)
127126, 65syl 17 . . . . . . . 8 (((⊤ ∧ 𝑖 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑖)) → (𝐹𝑘) ∈ ℝ)
128 elfznn 12942 . . . . . . . . . 10 (𝑘 ∈ (1...(𝑖 − 1)) → 𝑘 ∈ ℕ)
129128adantl 485 . . . . . . . . 9 (((⊤ ∧ 𝑖 ∈ ℕ) ∧ 𝑘 ∈ (1...(𝑖 − 1))) → 𝑘 ∈ ℕ)
130129, 80syl 17 . . . . . . . 8 (((⊤ ∧ 𝑖 ∈ ℕ) ∧ 𝑘 ∈ (1...(𝑖 − 1))) → (𝐹‘(𝑘 + 1)) ≤ (𝐹𝑘))
131124, 127, 130monoord2 13408 . . . . . . 7 ((⊤ ∧ 𝑖 ∈ ℕ) → (𝐹𝑖) ≤ (𝐹‘1))
132131, 115breqtrdi 5094 . . . . . 6 ((⊤ ∧ 𝑖 ∈ ℕ) → (𝐹𝑖) ≤ 1)
13399, 40elicc2i 12802 . . . . . 6 ((𝐹𝑖) ∈ (γ[,]1) ↔ ((𝐹𝑖) ∈ ℝ ∧ γ ≤ (𝐹𝑖) ∧ (𝐹𝑖) ≤ 1))
134101, 104, 132, 133syl3anbrc 1340 . . . . 5 ((⊤ ∧ 𝑖 ∈ ℕ) → (𝐹𝑖) ∈ (γ[,]1))
135134ralrimiva 3177 . . . 4 (⊤ → ∀𝑖 ∈ ℕ (𝐹𝑖) ∈ (γ[,]1))
136 ffnfv 6875 . . . 4 (𝐹:ℕ⟶(γ[,]1) ↔ (𝐹 Fn ℕ ∧ ∀𝑖 ∈ ℕ (𝐹𝑖) ∈ (γ[,]1)))
137123, 135, 136sylanbrc 586 . . 3 (⊤ → 𝐹:ℕ⟶(γ[,]1))
138 ffn 6505 . . . . 5 (𝐺:ℕ⟶ℝ → 𝐺 Fn ℕ)
13911, 138mp1i 13 . . . 4 (⊤ → 𝐺 Fn ℕ)
14011ffvelrni 6843 . . . . . . 7 (𝑖 ∈ ℕ → (𝐺𝑖) ∈ ℝ)
141140adantl 485 . . . . . 6 ((⊤ ∧ 𝑖 ∈ ℕ) → (𝐺𝑖) ∈ ℝ)
142126, 12syl 17 . . . . . . . 8 (((⊤ ∧ 𝑖 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑖)) → (𝐺𝑘) ∈ ℝ)
143129, 20syl 17 . . . . . . . 8 (((⊤ ∧ 𝑖 ∈ ℕ) ∧ 𝑘 ∈ (1...(𝑖 − 1))) → (𝐺𝑘) ≤ (𝐺‘(𝑘 + 1)))
144124, 142, 143monoord 13407 . . . . . . 7 ((⊤ ∧ 𝑖 ∈ ℕ) → (𝐺‘1) ≤ (𝐺𝑖))
14547, 144eqbrtrrid 5089 . . . . . 6 ((⊤ ∧ 𝑖 ∈ ℕ) → (1 − (log‘2)) ≤ (𝐺𝑖))
14644, 99elicc2i 12802 . . . . . 6 ((𝐺𝑖) ∈ ((1 − (log‘2))[,]γ) ↔ ((𝐺𝑖) ∈ ℝ ∧ (1 − (log‘2)) ≤ (𝐺𝑖) ∧ (𝐺𝑖) ≤ γ))
147141, 145, 22, 146syl3anbrc 1340 . . . . 5 ((⊤ ∧ 𝑖 ∈ ℕ) → (𝐺𝑖) ∈ ((1 − (log‘2))[,]γ))
148147ralrimiva 3177 . . . 4 (⊤ → ∀𝑖 ∈ ℕ (𝐺𝑖) ∈ ((1 − (log‘2))[,]γ))
149 ffnfv 6875 . . . 4 (𝐺:ℕ⟶((1 − (log‘2))[,]γ) ↔ (𝐺 Fn ℕ ∧ ∀𝑖 ∈ ℕ (𝐺𝑖) ∈ ((1 − (log‘2))[,]γ)))
150139, 148, 149sylanbrc 586 . . 3 (⊤ → 𝐺:ℕ⟶((1 − (log‘2))[,]γ))
151121, 137, 1503jca 1125 . 2 (⊤ → (γ ∈ ((1 − (log‘2))[,]1) ∧ 𝐹:ℕ⟶(γ[,]1) ∧ 𝐺:ℕ⟶((1 − (log‘2))[,]γ)))
152151mptru 1545 1 (γ ∈ ((1 − (log‘2))[,]1) ∧ 𝐹:ℕ⟶(γ[,]1) ∧ 𝐺:ℕ⟶((1 − (log‘2))[,]γ))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ⊤wtru 1539   ∈ wcel 2115  ∀wral 3133  Vcvv 3480   class class class wbr 5053   ↦ cmpt 5133   Fn wfn 6340  ⟶wf 6341  ‘cfv 6345  (class class class)co 7151  ℂcc 10535  ℝcr 10536  0cc0 10537  1c1 10538   + caddc 10540   ≤ cle 10676   − cmin 10870  -cneg 10871   / cdiv 11297  ℕcn 11636  2c2 11691  ℤcz 11980  ℤ≥cuz 12242  ℝ+crp 12388  [,]cicc 12740  ...cfz 12896   ⇝ cli 14843  Σcsu 15044  logclog 25155  γcem 25586 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5177  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7457  ax-inf2 9103  ax-cnex 10593  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614  ax-pre-sup 10615  ax-addf 10616  ax-mulf 10617 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-int 4863  df-iun 4907  df-iin 4908  df-br 5054  df-opab 5116  df-mpt 5134  df-tr 5160  df-id 5448  df-eprel 5453  df-po 5462  df-so 5463  df-fr 5502  df-se 5503  df-we 5504  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556  df-pred 6137  df-ord 6183  df-on 6184  df-lim 6185  df-suc 6186  df-iota 6304  df-fun 6347  df-fn 6348  df-f 6349  df-f1 6350  df-fo 6351  df-f1o 6352  df-fv 6353  df-isom 6354  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-of 7405  df-om 7577  df-1st 7686  df-2nd 7687  df-supp 7829  df-wrecs 7945  df-recs 8006  df-rdg 8044  df-1o 8100  df-2o 8101  df-oadd 8104  df-er 8287  df-map 8406  df-pm 8407  df-ixp 8460  df-en 8508  df-dom 8509  df-sdom 8510  df-fin 8511  df-fsupp 8833  df-fi 8874  df-sup 8905  df-inf 8906  df-oi 8973  df-card 9367  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-div 11298  df-nn 11637  df-2 11699  df-3 11700  df-4 11701  df-5 11702  df-6 11703  df-7 11704  df-8 11705  df-9 11706  df-n0 11897  df-z 11981  df-dec 12098  df-uz 12243  df-q 12348  df-rp 12389  df-xneg 12506  df-xadd 12507  df-xmul 12508  df-ioo 12741  df-ioc 12742  df-ico 12743  df-icc 12744  df-fz 12897  df-fzo 13040  df-fl 13168  df-mod 13244  df-seq 13376  df-exp 13437  df-fac 13641  df-bc 13670  df-hash 13698  df-shft 14428  df-cj 14460  df-re 14461  df-im 14462  df-sqrt 14596  df-abs 14597  df-limsup 14830  df-clim 14847  df-rlim 14848  df-sum 15045  df-ef 15423  df-sin 15425  df-cos 15426  df-pi 15428  df-struct 16487  df-ndx 16488  df-slot 16489  df-base 16491  df-sets 16492  df-ress 16493  df-plusg 16580  df-mulr 16581  df-starv 16582  df-sca 16583  df-vsca 16584  df-ip 16585  df-tset 16586  df-ple 16587  df-ds 16589  df-unif 16590  df-hom 16591  df-cco 16592  df-rest 16698  df-topn 16699  df-0g 16717  df-gsum 16718  df-topgen 16719  df-pt 16720  df-prds 16723  df-xrs 16777  df-qtop 16782  df-imas 16783  df-xps 16785  df-mre 16859  df-mrc 16860  df-acs 16862  df-mgm 17854  df-sgrp 17903  df-mnd 17914  df-submnd 17959  df-mulg 18227  df-cntz 18449  df-cmn 18910  df-psmet 20092  df-xmet 20093  df-met 20094  df-bl 20095  df-mopn 20096  df-fbas 20097  df-fg 20098  df-cnfld 20101  df-top 21508  df-topon 21525  df-topsp 21547  df-bases 21560  df-cld 21633  df-ntr 21634  df-cls 21635  df-nei 21712  df-lp 21750  df-perf 21751  df-cn 21841  df-cnp 21842  df-haus 21929  df-tx 22176  df-hmeo 22369  df-fil 22460  df-fm 22552  df-flim 22553  df-flf 22554  df-xms 22936  df-ms 22937  df-tms 22938  df-cncf 23492  df-limc 24478  df-dv 24479  df-log 25157  df-em 25587 This theorem is referenced by:  emcl  25597  harmonicbnd  25598  harmonicbnd2  25599
 Copyright terms: Public domain W3C validator