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

Theorem emcllem7 27022
Description: Lemma for emcl 27023 and harmonicbnd 27024. 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 12912 . . . . 5 ℕ = (ℤ‘1)
2 1zzd 12640 . . . . 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 27021 . . . . . . 7 (𝐹 ⇝ γ ∧ 𝐺 ⇝ γ)
87simpri 484 . . . . . 6 𝐺 ⇝ γ
98a1i 11 . . . . 5 (⊤ → 𝐺 ⇝ γ)
103, 4emcllem1 27016 . . . . . . . 8 (𝐹:ℕ⟶ℝ ∧ 𝐺:ℕ⟶ℝ)
1110simpri 484 . . . . . . 7 𝐺:ℕ⟶ℝ
1211ffvelcdmi 7096 . . . . . 6 (𝑘 ∈ ℕ → (𝐺𝑘) ∈ ℝ)
1312adantl 480 . . . . 5 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ℝ)
141, 2, 9, 13climrecl 15580 . . . 4 (⊤ → γ ∈ ℝ)
15 1nn 12270 . . . . 5 1 ∈ ℕ
16 simpr 483 . . . . . . 7 ((⊤ ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℕ)
178a1i 11 . . . . . . 7 ((⊤ ∧ 𝑖 ∈ ℕ) → 𝐺 ⇝ γ)
1812adantl 480 . . . . . . 7 (((⊤ ∧ 𝑖 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ℝ)
193, 4emcllem2 27017 . . . . . . . . 9 (𝑘 ∈ ℕ → ((𝐹‘(𝑘 + 1)) ≤ (𝐹𝑘) ∧ (𝐺𝑘) ≤ (𝐺‘(𝑘 + 1))))
2019simprd 494 . . . . . . . 8 (𝑘 ∈ ℕ → (𝐺𝑘) ≤ (𝐺‘(𝑘 + 1)))
2120adantl 480 . . . . . . 7 (((⊤ ∧ 𝑖 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) ≤ (𝐺‘(𝑘 + 1)))
221, 16, 17, 18, 21climub 15661 . . . . . 6 ((⊤ ∧ 𝑖 ∈ ℕ) → (𝐺𝑖) ≤ γ)
2322ralrimiva 3135 . . . . 5 (⊤ → ∀𝑖 ∈ ℕ (𝐺𝑖) ≤ γ)
24 fveq2 6900 . . . . . . . 8 (𝑖 = 1 → (𝐺𝑖) = (𝐺‘1))
25 oveq2 7431 . . . . . . . . . . . . 13 (𝑛 = 1 → (1...𝑛) = (1...1))
2625sumeq1d 15700 . . . . . . . . . . . 12 (𝑛 = 1 → Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) = Σ𝑚 ∈ (1...1)(1 / 𝑚))
27 1z 12639 . . . . . . . . . . . . 13 1 ∈ ℤ
28 ax-1cn 11212 . . . . . . . . . . . . 13 1 ∈ ℂ
29 oveq2 7431 . . . . . . . . . . . . . . 15 (𝑚 = 1 → (1 / 𝑚) = (1 / 1))
30 1div1e1 11951 . . . . . . . . . . . . . . 15 (1 / 1) = 1
3129, 30eqtrdi 2781 . . . . . . . . . . . . . 14 (𝑚 = 1 → (1 / 𝑚) = 1)
3231fsum1 15746 . . . . . . . . . . . . 13 ((1 ∈ ℤ ∧ 1 ∈ ℂ) → Σ𝑚 ∈ (1...1)(1 / 𝑚) = 1)
3327, 28, 32mp2an 690 . . . . . . . . . . . 12 Σ𝑚 ∈ (1...1)(1 / 𝑚) = 1
3426, 33eqtrdi 2781 . . . . . . . . . . 11 (𝑛 = 1 → Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) = 1)
35 oveq1 7430 . . . . . . . . . . . . 13 (𝑛 = 1 → (𝑛 + 1) = (1 + 1))
36 df-2 12322 . . . . . . . . . . . . 13 2 = (1 + 1)
3735, 36eqtr4di 2783 . . . . . . . . . . . 12 (𝑛 = 1 → (𝑛 + 1) = 2)
3837fveq2d 6904 . . . . . . . . . . 11 (𝑛 = 1 → (log‘(𝑛 + 1)) = (log‘2))
3934, 38oveq12d 7441 . . . . . . . . . 10 (𝑛 = 1 → (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1))) = (1 − (log‘2)))
40 1re 11260 . . . . . . . . . . . 12 1 ∈ ℝ
41 2rp 13028 . . . . . . . . . . . . 13 2 ∈ ℝ+
42 relogcl 26594 . . . . . . . . . . . . 13 (2 ∈ ℝ+ → (log‘2) ∈ ℝ)
4341, 42ax-mp 5 . . . . . . . . . . . 12 (log‘2) ∈ ℝ
4440, 43resubcli 11568 . . . . . . . . . . 11 (1 − (log‘2)) ∈ ℝ
4544elexi 3483 . . . . . . . . . 10 (1 − (log‘2)) ∈ V
4639, 4, 45fvmpt 7008 . . . . . . . . 9 (1 ∈ ℕ → (𝐺‘1) = (1 − (log‘2)))
4715, 46ax-mp 5 . . . . . . . 8 (𝐺‘1) = (1 − (log‘2))
4824, 47eqtrdi 2781 . . . . . . 7 (𝑖 = 1 → (𝐺𝑖) = (1 − (log‘2)))
4948breq1d 5162 . . . . . 6 (𝑖 = 1 → ((𝐺𝑖) ≤ γ ↔ (1 − (log‘2)) ≤ γ))
5049rspcva 3605 . . . . 5 ((1 ∈ ℕ ∧ ∀𝑖 ∈ ℕ (𝐺𝑖) ≤ γ) → (1 − (log‘2)) ≤ γ)
5115, 23, 50sylancr 585 . . . 4 (⊤ → (1 − (log‘2)) ≤ γ)
52 fveq2 6900 . . . . . . . . . . . 12 (𝑥 = 𝑖 → (𝐹𝑥) = (𝐹𝑖))
5352negeqd 11500 . . . . . . . . . . 11 (𝑥 = 𝑖 → -(𝐹𝑥) = -(𝐹𝑖))
54 eqid 2725 . . . . . . . . . . 11 (𝑥 ∈ ℕ ↦ -(𝐹𝑥)) = (𝑥 ∈ ℕ ↦ -(𝐹𝑥))
55 negex 11504 . . . . . . . . . . 11 -(𝐹𝑖) ∈ V
5653, 54, 55fvmpt 7008 . . . . . . . . . 10 (𝑖 ∈ ℕ → ((𝑥 ∈ ℕ ↦ -(𝐹𝑥))‘𝑖) = -(𝐹𝑖))
5756adantl 480 . . . . . . . . 9 ((⊤ ∧ 𝑖 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ -(𝐹𝑥))‘𝑖) = -(𝐹𝑖))
587simpli 482 . . . . . . . . . . . . 13 𝐹 ⇝ γ
5958a1i 11 . . . . . . . . . . . 12 (⊤ → 𝐹 ⇝ γ)
60 0cnd 11253 . . . . . . . . . . . 12 (⊤ → 0 ∈ ℂ)
61 nnex 12265 . . . . . . . . . . . . . 14 ℕ ∈ V
6261mptex 7239 . . . . . . . . . . . . 13 (𝑥 ∈ ℕ ↦ -(𝐹𝑥)) ∈ V
6362a1i 11 . . . . . . . . . . . 12 (⊤ → (𝑥 ∈ ℕ ↦ -(𝐹𝑥)) ∈ V)
6410simpli 482 . . . . . . . . . . . . . . 15 𝐹:ℕ⟶ℝ
6564ffvelcdmi 7096 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → (𝐹𝑘) ∈ ℝ)
6665adantl 480 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℝ)
6766recnd 11288 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℂ)
68 fveq2 6900 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑘 → (𝐹𝑥) = (𝐹𝑘))
6968negeqd 11500 . . . . . . . . . . . . . . 15 (𝑥 = 𝑘 → -(𝐹𝑥) = -(𝐹𝑘))
70 negex 11504 . . . . . . . . . . . . . . 15 -(𝐹𝑘) ∈ V
7169, 54, 70fvmpt 7008 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → ((𝑥 ∈ ℕ ↦ -(𝐹𝑥))‘𝑘) = -(𝐹𝑘))
7271adantl 480 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ -(𝐹𝑥))‘𝑘) = -(𝐹𝑘))
73 df-neg 11493 . . . . . . . . . . . . 13 -(𝐹𝑘) = (0 − (𝐹𝑘))
7472, 73eqtrdi 2781 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ -(𝐹𝑥))‘𝑘) = (0 − (𝐹𝑘)))
751, 2, 59, 60, 63, 67, 74climsubc2 15636 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ ℕ ↦ -(𝐹𝑥)) ⇝ (0 − γ))
7675adantr 479 . . . . . . . . . 10 ((⊤ ∧ 𝑖 ∈ ℕ) → (𝑥 ∈ ℕ ↦ -(𝐹𝑥)) ⇝ (0 − γ))
7766renegcld 11687 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ) → -(𝐹𝑘) ∈ ℝ)
7872, 77eqeltrd 2825 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ -(𝐹𝑥))‘𝑘) ∈ ℝ)
7978adantlr 713 . . . . . . . . . 10 (((⊤ ∧ 𝑖 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ -(𝐹𝑥))‘𝑘) ∈ ℝ)
8019simpld 493 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → (𝐹‘(𝑘 + 1)) ≤ (𝐹𝑘))
8180adantl 480 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ≤ (𝐹𝑘))
82 peano2nn 12271 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
8382adantl 480 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
8464ffvelcdmi 7096 . . . . . . . . . . . . . . 15 ((𝑘 + 1) ∈ ℕ → (𝐹‘(𝑘 + 1)) ∈ ℝ)
8583, 84syl 17 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ∈ ℝ)
8685, 66lenegd 11839 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝐹‘(𝑘 + 1)) ≤ (𝐹𝑘) ↔ -(𝐹𝑘) ≤ -(𝐹‘(𝑘 + 1))))
8781, 86mpbid 231 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ) → -(𝐹𝑘) ≤ -(𝐹‘(𝑘 + 1)))
88 fveq2 6900 . . . . . . . . . . . . . . 15 (𝑥 = (𝑘 + 1) → (𝐹𝑥) = (𝐹‘(𝑘 + 1)))
8988negeqd 11500 . . . . . . . . . . . . . 14 (𝑥 = (𝑘 + 1) → -(𝐹𝑥) = -(𝐹‘(𝑘 + 1)))
90 negex 11504 . . . . . . . . . . . . . 14 -(𝐹‘(𝑘 + 1)) ∈ V
9189, 54, 90fvmpt 7008 . . . . . . . . . . . . 13 ((𝑘 + 1) ∈ ℕ → ((𝑥 ∈ ℕ ↦ -(𝐹𝑥))‘(𝑘 + 1)) = -(𝐹‘(𝑘 + 1)))
9283, 91syl 17 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ -(𝐹𝑥))‘(𝑘 + 1)) = -(𝐹‘(𝑘 + 1)))
9387, 72, 923brtr4d 5184 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ -(𝐹𝑥))‘𝑘) ≤ ((𝑥 ∈ ℕ ↦ -(𝐹𝑥))‘(𝑘 + 1)))
9493adantlr 713 . . . . . . . . . 10 (((⊤ ∧ 𝑖 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ -(𝐹𝑥))‘𝑘) ≤ ((𝑥 ∈ ℕ ↦ -(𝐹𝑥))‘(𝑘 + 1)))
951, 16, 76, 79, 94climub 15661 . . . . . . . . 9 ((⊤ ∧ 𝑖 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ -(𝐹𝑥))‘𝑖) ≤ (0 − γ))
9657, 95eqbrtrrd 5176 . . . . . . . 8 ((⊤ ∧ 𝑖 ∈ ℕ) → -(𝐹𝑖) ≤ (0 − γ))
97 df-neg 11493 . . . . . . . 8 -γ = (0 − γ)
9896, 97breqtrrdi 5194 . . . . . . 7 ((⊤ ∧ 𝑖 ∈ ℕ) → -(𝐹𝑖) ≤ -γ)
9914mptru 1540 . . . . . . . 8 γ ∈ ℝ
10064ffvelcdmi 7096 . . . . . . . . 9 (𝑖 ∈ ℕ → (𝐹𝑖) ∈ ℝ)
101100adantl 480 . . . . . . . 8 ((⊤ ∧ 𝑖 ∈ ℕ) → (𝐹𝑖) ∈ ℝ)
102 leneg 11763 . . . . . . . 8 ((γ ∈ ℝ ∧ (𝐹𝑖) ∈ ℝ) → (γ ≤ (𝐹𝑖) ↔ -(𝐹𝑖) ≤ -γ))
10399, 101, 102sylancr 585 . . . . . . 7 ((⊤ ∧ 𝑖 ∈ ℕ) → (γ ≤ (𝐹𝑖) ↔ -(𝐹𝑖) ≤ -γ))
10498, 103mpbird 256 . . . . . 6 ((⊤ ∧ 𝑖 ∈ ℕ) → γ ≤ (𝐹𝑖))
105104ralrimiva 3135 . . . . 5 (⊤ → ∀𝑖 ∈ ℕ γ ≤ (𝐹𝑖))
106 fveq2 6900 . . . . . . . 8 (𝑖 = 1 → (𝐹𝑖) = (𝐹‘1))
107 fveq2 6900 . . . . . . . . . . . . 13 (𝑛 = 1 → (log‘𝑛) = (log‘1))
108 log1 26604 . . . . . . . . . . . . 13 (log‘1) = 0
109107, 108eqtrdi 2781 . . . . . . . . . . . 12 (𝑛 = 1 → (log‘𝑛) = 0)
11034, 109oveq12d 7441 . . . . . . . . . . 11 (𝑛 = 1 → (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛)) = (1 − 0))
111 1m0e1 12380 . . . . . . . . . . 11 (1 − 0) = 1
112110, 111eqtrdi 2781 . . . . . . . . . 10 (𝑛 = 1 → (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛)) = 1)
11340elexi 3483 . . . . . . . . . 10 1 ∈ V
114112, 3, 113fvmpt 7008 . . . . . . . . 9 (1 ∈ ℕ → (𝐹‘1) = 1)
11515, 114ax-mp 5 . . . . . . . 8 (𝐹‘1) = 1
116106, 115eqtrdi 2781 . . . . . . 7 (𝑖 = 1 → (𝐹𝑖) = 1)
117116breq2d 5164 . . . . . 6 (𝑖 = 1 → (γ ≤ (𝐹𝑖) ↔ γ ≤ 1))
118117rspcva 3605 . . . . 5 ((1 ∈ ℕ ∧ ∀𝑖 ∈ ℕ γ ≤ (𝐹𝑖)) → γ ≤ 1)
11915, 105, 118sylancr 585 . . . 4 (⊤ → γ ≤ 1)
12044, 40elicc2i 13439 . . . 4 (γ ∈ ((1 − (log‘2))[,]1) ↔ (γ ∈ ℝ ∧ (1 − (log‘2)) ≤ γ ∧ γ ≤ 1))
12114, 51, 119, 120syl3anbrc 1340 . . 3 (⊤ → γ ∈ ((1 − (log‘2))[,]1))
122 ffn 6727 . . . . 5 (𝐹:ℕ⟶ℝ → 𝐹 Fn ℕ)
12364, 122mp1i 13 . . . 4 (⊤ → 𝐹 Fn ℕ)
12416, 1eleqtrdi 2835 . . . . . . . 8 ((⊤ ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ (ℤ‘1))
125 elfznn 13579 . . . . . . . . . 10 (𝑘 ∈ (1...𝑖) → 𝑘 ∈ ℕ)
126125adantl 480 . . . . . . . . 9 (((⊤ ∧ 𝑖 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑖)) → 𝑘 ∈ ℕ)
127126, 65syl 17 . . . . . . . 8 (((⊤ ∧ 𝑖 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑖)) → (𝐹𝑘) ∈ ℝ)
128 elfznn 13579 . . . . . . . . . 10 (𝑘 ∈ (1...(𝑖 − 1)) → 𝑘 ∈ ℕ)
129128adantl 480 . . . . . . . . 9 (((⊤ ∧ 𝑖 ∈ ℕ) ∧ 𝑘 ∈ (1...(𝑖 − 1))) → 𝑘 ∈ ℕ)
130129, 80syl 17 . . . . . . . 8 (((⊤ ∧ 𝑖 ∈ ℕ) ∧ 𝑘 ∈ (1...(𝑖 − 1))) → (𝐹‘(𝑘 + 1)) ≤ (𝐹𝑘))
131124, 127, 130monoord2 14048 . . . . . . 7 ((⊤ ∧ 𝑖 ∈ ℕ) → (𝐹𝑖) ≤ (𝐹‘1))
132131, 115breqtrdi 5193 . . . . . 6 ((⊤ ∧ 𝑖 ∈ ℕ) → (𝐹𝑖) ≤ 1)
13399, 40elicc2i 13439 . . . . . 6 ((𝐹𝑖) ∈ (γ[,]1) ↔ ((𝐹𝑖) ∈ ℝ ∧ γ ≤ (𝐹𝑖) ∧ (𝐹𝑖) ≤ 1))
134101, 104, 132, 133syl3anbrc 1340 . . . . 5 ((⊤ ∧ 𝑖 ∈ ℕ) → (𝐹𝑖) ∈ (γ[,]1))
135134ralrimiva 3135 . . . 4 (⊤ → ∀𝑖 ∈ ℕ (𝐹𝑖) ∈ (γ[,]1))
136 ffnfv 7132 . . . 4 (𝐹:ℕ⟶(γ[,]1) ↔ (𝐹 Fn ℕ ∧ ∀𝑖 ∈ ℕ (𝐹𝑖) ∈ (γ[,]1)))
137123, 135, 136sylanbrc 581 . . 3 (⊤ → 𝐹:ℕ⟶(γ[,]1))
138 ffn 6727 . . . . 5 (𝐺:ℕ⟶ℝ → 𝐺 Fn ℕ)
13911, 138mp1i 13 . . . 4 (⊤ → 𝐺 Fn ℕ)
14011ffvelcdmi 7096 . . . . . . 7 (𝑖 ∈ ℕ → (𝐺𝑖) ∈ ℝ)
141140adantl 480 . . . . . 6 ((⊤ ∧ 𝑖 ∈ ℕ) → (𝐺𝑖) ∈ ℝ)
142126, 12syl 17 . . . . . . . 8 (((⊤ ∧ 𝑖 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑖)) → (𝐺𝑘) ∈ ℝ)
143129, 20syl 17 . . . . . . . 8 (((⊤ ∧ 𝑖 ∈ ℕ) ∧ 𝑘 ∈ (1...(𝑖 − 1))) → (𝐺𝑘) ≤ (𝐺‘(𝑘 + 1)))
144124, 142, 143monoord 14047 . . . . . . 7 ((⊤ ∧ 𝑖 ∈ ℕ) → (𝐺‘1) ≤ (𝐺𝑖))
14547, 144eqbrtrrid 5188 . . . . . 6 ((⊤ ∧ 𝑖 ∈ ℕ) → (1 − (log‘2)) ≤ (𝐺𝑖))
14644, 99elicc2i 13439 . . . . . 6 ((𝐺𝑖) ∈ ((1 − (log‘2))[,]γ) ↔ ((𝐺𝑖) ∈ ℝ ∧ (1 − (log‘2)) ≤ (𝐺𝑖) ∧ (𝐺𝑖) ≤ γ))
147141, 145, 22, 146syl3anbrc 1340 . . . . 5 ((⊤ ∧ 𝑖 ∈ ℕ) → (𝐺𝑖) ∈ ((1 − (log‘2))[,]γ))
148147ralrimiva 3135 . . . 4 (⊤ → ∀𝑖 ∈ ℕ (𝐺𝑖) ∈ ((1 − (log‘2))[,]γ))
149 ffnfv 7132 . . . 4 (𝐺:ℕ⟶((1 − (log‘2))[,]γ) ↔ (𝐺 Fn ℕ ∧ ∀𝑖 ∈ ℕ (𝐺𝑖) ∈ ((1 − (log‘2))[,]γ)))
150139, 148, 149sylanbrc 581 . . 3 (⊤ → 𝐺:ℕ⟶((1 − (log‘2))[,]γ))
151121, 137, 1503jca 1125 . 2 (⊤ → (γ ∈ ((1 − (log‘2))[,]1) ∧ 𝐹:ℕ⟶(γ[,]1) ∧ 𝐺:ℕ⟶((1 − (log‘2))[,]γ)))
152151mptru 1540 1 (γ ∈ ((1 − (log‘2))[,]1) ∧ 𝐹:ℕ⟶(γ[,]1) ∧ 𝐺:ℕ⟶((1 − (log‘2))[,]γ))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 394  w3a 1084   = wceq 1533  wtru 1534  wcel 2098  wral 3050  Vcvv 3461   class class class wbr 5152  cmpt 5235   Fn wfn 6548  wf 6549  cfv 6553  (class class class)co 7423  cc 11152  cr 11153  0cc0 11154  1c1 11155   + caddc 11157  cle 11295  cmin 11490  -cneg 11491   / cdiv 11917  cn 12259  2c2 12314  cz 12605  cuz 12869  +crp 13023  [,]cicc 13376  ...cfz 13533  cli 15481  Σcsu 15685  logclog 26573  γcem 27012
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5368  ax-pr 5432  ax-un 7745  ax-inf2 9680  ax-cnex 11210  ax-resscn 11211  ax-1cn 11212  ax-icn 11213  ax-addcl 11214  ax-addrcl 11215  ax-mulcl 11216  ax-mulrcl 11217  ax-mulcom 11218  ax-addass 11219  ax-mulass 11220  ax-distr 11221  ax-i2m1 11222  ax-1ne0 11223  ax-1rid 11224  ax-rnegex 11225  ax-rrecex 11226  ax-cnre 11227  ax-pre-lttri 11228  ax-pre-lttrn 11229  ax-pre-ltadd 11230  ax-pre-mulgt0 11231  ax-pre-sup 11232  ax-addf 11233
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4325  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-tp 4637  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-iin 5003  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5579  df-eprel 5585  df-po 5593  df-so 5594  df-fr 5636  df-se 5637  df-we 5638  df-xp 5687  df-rel 5688  df-cnv 5689  df-co 5690  df-dm 5691  df-rn 5692  df-res 5693  df-ima 5694  df-pred 6311  df-ord 6378  df-on 6379  df-lim 6380  df-suc 6381  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-isom 6562  df-riota 7379  df-ov 7426  df-oprab 7427  df-mpo 7428  df-of 7689  df-om 7876  df-1st 8002  df-2nd 8003  df-supp 8174  df-frecs 8295  df-wrecs 8326  df-recs 8400  df-rdg 8439  df-1o 8495  df-2o 8496  df-er 8733  df-map 8856  df-pm 8857  df-ixp 8926  df-en 8974  df-dom 8975  df-sdom 8976  df-fin 8977  df-fsupp 9402  df-fi 9450  df-sup 9481  df-inf 9482  df-oi 9549  df-card 9978  df-pnf 11296  df-mnf 11297  df-xr 11298  df-ltxr 11299  df-le 11300  df-sub 11492  df-neg 11493  df-div 11918  df-nn 12260  df-2 12322  df-3 12323  df-4 12324  df-5 12325  df-6 12326  df-7 12327  df-8 12328  df-9 12329  df-n0 12520  df-z 12606  df-dec 12725  df-uz 12870  df-q 12980  df-rp 13024  df-xneg 13141  df-xadd 13142  df-xmul 13143  df-ioo 13377  df-ioc 13378  df-ico 13379  df-icc 13380  df-fz 13534  df-fzo 13677  df-fl 13807  df-mod 13885  df-seq 14017  df-exp 14077  df-fac 14286  df-bc 14315  df-hash 14343  df-shft 15067  df-cj 15099  df-re 15100  df-im 15101  df-sqrt 15235  df-abs 15236  df-limsup 15468  df-clim 15485  df-rlim 15486  df-sum 15686  df-ef 16064  df-sin 16066  df-cos 16067  df-pi 16069  df-struct 17144  df-sets 17161  df-slot 17179  df-ndx 17191  df-base 17209  df-ress 17238  df-plusg 17274  df-mulr 17275  df-starv 17276  df-sca 17277  df-vsca 17278  df-ip 17279  df-tset 17280  df-ple 17281  df-ds 17283  df-unif 17284  df-hom 17285  df-cco 17286  df-rest 17432  df-topn 17433  df-0g 17451  df-gsum 17452  df-topgen 17453  df-pt 17454  df-prds 17457  df-xrs 17512  df-qtop 17517  df-imas 17518  df-xps 17520  df-mre 17594  df-mrc 17595  df-acs 17597  df-mgm 18628  df-sgrp 18707  df-mnd 18723  df-submnd 18769  df-mulg 19057  df-cntz 19306  df-cmn 19775  df-psmet 21327  df-xmet 21328  df-met 21329  df-bl 21330  df-mopn 21331  df-fbas 21332  df-fg 21333  df-cnfld 21336  df-top 22879  df-topon 22896  df-topsp 22918  df-bases 22932  df-cld 23006  df-ntr 23007  df-cls 23008  df-nei 23085  df-lp 23123  df-perf 23124  df-cn 23214  df-cnp 23215  df-haus 23302  df-tx 23549  df-hmeo 23742  df-fil 23833  df-fm 23925  df-flim 23926  df-flf 23927  df-xms 24309  df-ms 24310  df-tms 24311  df-cncf 24881  df-limc 25878  df-dv 25879  df-log 26575  df-em 27013
This theorem is referenced by:  emcl  27023  harmonicbnd  27024  harmonicbnd2  27025
  Copyright terms: Public domain W3C validator