emcllem7

Description: Lemma for emcl and harmonicbnd . Derive bounds on gamma as F ( 1 ) and G ( 1 ) . (Contributed by Mario Carneiro, 11-Jul-2014) (Revised by Mario Carneiro, 9-Apr-2016)

	Ref	Expression
Hypotheses	emcl.1	$⊢ F = (n \in ℕ ⟼ \sum_{m = 1}^{n} (\frac{1}{m}) - \log n)$
	emcl.2	$⊢ G = (n \in ℕ ⟼ \sum_{m = 1}^{n} (\frac{1}{m}) - \log (n + 1))$
	emcl.3	$⊢ H = (n \in ℕ ⟼ \log (1 + (\frac{1}{n})))$
	emcl.4	$⊢ T = (n \in ℕ ⟼ (\frac{1}{n}) - \log (1 + (\frac{1}{n})))$
Assertion	emcllem7	$⊢ (γ \in [1 - \log 2, 1] \land F : ℕ ⟶ [γ, 1] \land G : ℕ ⟶ [1 - \log 2, γ])$

Proof

Step	Hyp	Ref	Expression
1		emcl.1	$⊢ F = (n \in ℕ ⟼ \sum_{m = 1}^{n} (\frac{1}{m}) - \log n)$
2		emcl.2	$⊢ G = (n \in ℕ ⟼ \sum_{m = 1}^{n} (\frac{1}{m}) - \log (n + 1))$
3		emcl.3	$⊢ H = (n \in ℕ ⟼ \log (1 + (\frac{1}{n})))$
4		emcl.4	$⊢ T = (n \in ℕ ⟼ (\frac{1}{n}) - \log (1 + (\frac{1}{n})))$
5		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
6		1zzd	$⊢ ⊤ \to 1 \in ℤ$
7	1 2 3 4	emcllem6	$⊢ (F ⇝ γ \land G ⇝ γ)$
8	7	simpri	$⊢ G ⇝ γ$
9	8	a1i	$⊢ ⊤ \to G ⇝ γ$
10	1 2	emcllem1	$⊢ (F : ℕ ⟶ ℝ \land G : ℕ ⟶ ℝ)$
11	10	simpri	$⊢ G : ℕ ⟶ ℝ$
12	11	ffvelcdmi	$⊢ k \in ℕ \to G (k) \in ℝ$
13	12	adantl	$⊢ (⊤ \land k \in ℕ) \to G (k) \in ℝ$
14	5 6 9 13	climrecl	$⊢ ⊤ \to γ \in ℝ$
15		1nn	$⊢ 1 \in ℕ$
16		simpr	$⊢ (⊤ \land i \in ℕ) \to i \in ℕ$
17	8	a1i	$⊢ (⊤ \land i \in ℕ) \to G ⇝ γ$
18	12	adantl	$⊢ ((⊤ \land i \in ℕ) \land k \in ℕ) \to G (k) \in ℝ$
19	1 2	emcllem2	$⊢ k \in ℕ \to (F (k + 1) \leq F (k) \land G (k) \leq G (k + 1))$
20	19	simprd	$⊢ k \in ℕ \to G (k) \leq G (k + 1)$
21	20	adantl	$⊢ ((⊤ \land i \in ℕ) \land k \in ℕ) \to G (k) \leq G (k + 1)$
22	5 16 17 18 21	climub	$⊢ (⊤ \land i \in ℕ) \to G (i) \leq γ$
23	22	ralrimiva	$⊢ ⊤ \to \forall i \in ℕ G (i) \leq γ$
24		fveq2	$⊢ i = 1 \to G (i) = G (1)$
25		oveq2	$⊢ n = 1 \to (1 \dots n) = (1 \dots 1)$
26	25	sumeq1d	$⊢ n = 1 \to \sum_{m = 1}^{n} (\frac{1}{m}) = \sum_{m = 1}^{1} (\frac{1}{m})$
27		1z	$⊢ 1 \in ℤ$
28		ax-1cn	$⊢ 1 \in ℂ$
29		oveq2	$⊢ m = 1 \to \frac{1}{m} = \frac{1}{1}$
30		1div1e1	$⊢ \frac{1}{1} = 1$
31	29 30	eqtrdi	$⊢ m = 1 \to \frac{1}{m} = 1$
32	31	fsum1	$⊢ (1 \in ℤ \land 1 \in ℂ) \to \sum_{m = 1}^{1} (\frac{1}{m}) = 1$
33	27 28 32	mp2an	$⊢ \sum_{m = 1}^{1} (\frac{1}{m}) = 1$
34	26 33	eqtrdi	$⊢ n = 1 \to \sum_{m = 1}^{n} (\frac{1}{m}) = 1$
35		oveq1	$⊢ n = 1 \to n + 1 = 1 + 1$
36		df-2	$⊢ 2 = 1 + 1$
37	35 36	eqtr4di	$⊢ n = 1 \to n + 1 = 2$
38	37	fveq2d	$⊢ n = 1 \to \log (n + 1) = \log 2$
39	34 38	oveq12d	$⊢ n = 1 \to \sum_{m = 1}^{n} (\frac{1}{m}) - \log (n + 1) = 1 - \log 2$
40		1re	$⊢ 1 \in ℝ$
41		2rp	$⊢ 2 \in ℝ^{+}$
42		relogcl	$⊢ 2 \in ℝ^{+} \to \log 2 \in ℝ$
43	41 42	ax-mp	$⊢ \log 2 \in ℝ$
44	40 43	resubcli	$⊢ 1 - \log 2 \in ℝ$
45	44	elexi	$⊢ 1 - \log 2 \in V$
46	39 2 45	fvmpt	$⊢ 1 \in ℕ \to G (1) = 1 - \log 2$
47	15 46	ax-mp	$⊢ G (1) = 1 - \log 2$
48	24 47	eqtrdi	$⊢ i = 1 \to G (i) = 1 - \log 2$
49	48	breq1d	$⊢ i = 1 \to (G (i) \leq γ \leftrightarrow 1 - \log 2 \leq γ)$
50	49	rspcva	$⊢ (1 \in ℕ \land \forall i \in ℕ G (i) \leq γ) \to 1 - \log 2 \leq γ$
51	15 23 50	sylancr	$⊢ ⊤ \to 1 - \log 2 \leq γ$
52		fveq2	$⊢ x = i \to F (x) = F (i)$
53	52	negeqd	$⊢ x = i \to - F (x) = - F (i)$
54		eqid	$⊢ (x \in ℕ ⟼ - F (x)) = (x \in ℕ ⟼ - F (x))$
55		negex	$⊢ - F (i) \in V$
56	53 54 55	fvmpt	$⊢ i \in ℕ \to (x \in ℕ ⟼ - F (x)) (i) = - F (i)$
57	56	adantl	$⊢ (⊤ \land i \in ℕ) \to (x \in ℕ ⟼ - F (x)) (i) = - F (i)$
58	7	simpli	$⊢ F ⇝ γ$
59	58	a1i	$⊢ ⊤ \to F ⇝ γ$
60		0cnd	$⊢ ⊤ \to 0 \in ℂ$
61		nnex	$⊢ ℕ \in V$
62	61	mptex	$⊢ (x \in ℕ ⟼ - F (x)) \in V$
63	62	a1i	$⊢ ⊤ \to (x \in ℕ ⟼ - F (x)) \in V$
64	10	simpli	$⊢ F : ℕ ⟶ ℝ$
65	64	ffvelcdmi	$⊢ k \in ℕ \to F (k) \in ℝ$
66	65	adantl	$⊢ (⊤ \land k \in ℕ) \to F (k) \in ℝ$
67	66	recnd	$⊢ (⊤ \land k \in ℕ) \to F (k) \in ℂ$
68		fveq2	$⊢ x = k \to F (x) = F (k)$
69	68	negeqd	$⊢ x = k \to - F (x) = - F (k)$
70		negex	$⊢ - F (k) \in V$
71	69 54 70	fvmpt	$⊢ k \in ℕ \to (x \in ℕ ⟼ - F (x)) (k) = - F (k)$
72	71	adantl	$⊢ (⊤ \land k \in ℕ) \to (x \in ℕ ⟼ - F (x)) (k) = - F (k)$
73		df-neg	$⊢ - F (k) = 0 - F (k)$
74	72 73	eqtrdi	$⊢ (⊤ \land k \in ℕ) \to (x \in ℕ ⟼ - F (x)) (k) = 0 - F (k)$
75	5 6 59 60 63 67 74	climsubc2	$⊢ ⊤ \to (x \in ℕ ⟼ - F (x)) ⇝ (0 - γ)$
76	75	adantr	$⊢ (⊤ \land i \in ℕ) \to (x \in ℕ ⟼ - F (x)) ⇝ (0 - γ)$
77	66	renegcld	$⊢ (⊤ \land k \in ℕ) \to - F (k) \in ℝ$
78	72 77	eqeltrd	$⊢ (⊤ \land k \in ℕ) \to (x \in ℕ ⟼ - F (x)) (k) \in ℝ$
79	78	adantlr	$⊢ ((⊤ \land i \in ℕ) \land k \in ℕ) \to (x \in ℕ ⟼ - F (x)) (k) \in ℝ$
80	19	simpld	$⊢ k \in ℕ \to F (k + 1) \leq F (k)$
81	80	adantl	$⊢ (⊤ \land k \in ℕ) \to F (k + 1) \leq F (k)$
82		peano2nn	$⊢ k \in ℕ \to k + 1 \in ℕ$
83	82	adantl	$⊢ (⊤ \land k \in ℕ) \to k + 1 \in ℕ$
84	64	ffvelcdmi	$⊢ k + 1 \in ℕ \to F (k + 1) \in ℝ$
85	83 84	syl	$⊢ (⊤ \land k \in ℕ) \to F (k + 1) \in ℝ$
86	85 66	lenegd	$⊢ (⊤ \land k \in ℕ) \to (F (k + 1) \leq F (k) \leftrightarrow - F (k) \leq - F (k + 1))$
87	81 86	mpbid	$⊢ (⊤ \land k \in ℕ) \to - F (k) \leq - F (k + 1)$
88		fveq2	$⊢ x = k + 1 \to F (x) = F (k + 1)$
89	88	negeqd	$⊢ x = k + 1 \to - F (x) = - F (k + 1)$
90		negex	$⊢ - F (k + 1) \in V$
91	89 54 90	fvmpt	$⊢ k + 1 \in ℕ \to (x \in ℕ ⟼ - F (x)) (k + 1) = - F (k + 1)$
92	83 91	syl	$⊢ (⊤ \land k \in ℕ) \to (x \in ℕ ⟼ - F (x)) (k + 1) = - F (k + 1)$
93	87 72 92	3brtr4d	$⊢ (⊤ \land k \in ℕ) \to (x \in ℕ ⟼ - F (x)) (k) \leq (x \in ℕ ⟼ - F (x)) (k + 1)$
94	93	adantlr	$⊢ ((⊤ \land i \in ℕ) \land k \in ℕ) \to (x \in ℕ ⟼ - F (x)) (k) \leq (x \in ℕ ⟼ - F (x)) (k + 1)$
95	5 16 76 79 94	climub	$⊢ (⊤ \land i \in ℕ) \to (x \in ℕ ⟼ - F (x)) (i) \leq 0 - γ$
96	57 95	eqbrtrrd	$⊢ (⊤ \land i \in ℕ) \to - F (i) \leq 0 - γ$
97		df-neg	$⊢ - γ = 0 - γ$
98	96 97	breqtrrdi	$⊢ (⊤ \land i \in ℕ) \to - F (i) \leq - γ$
99	14	mptru	$⊢ γ \in ℝ$
100	64	ffvelcdmi	$⊢ i \in ℕ \to F (i) \in ℝ$
101	100	adantl	$⊢ (⊤ \land i \in ℕ) \to F (i) \in ℝ$
102		leneg	$⊢ (γ \in ℝ \land F (i) \in ℝ) \to (γ \leq F (i) \leftrightarrow - F (i) \leq - γ)$
103	99 101 102	sylancr	$⊢ (⊤ \land i \in ℕ) \to (γ \leq F (i) \leftrightarrow - F (i) \leq - γ)$
104	98 103	mpbird	$⊢ (⊤ \land i \in ℕ) \to γ \leq F (i)$
105	104	ralrimiva	$⊢ ⊤ \to \forall i \in ℕ γ \leq F (i)$
106		fveq2	$⊢ i = 1 \to F (i) = F (1)$
107		fveq2	$⊢ n = 1 \to \log n = \log 1$
108		log1	$⊢ \log 1 = 0$
109	107 108	eqtrdi	$⊢ n = 1 \to \log n = 0$
110	34 109	oveq12d	$⊢ n = 1 \to \sum_{m = 1}^{n} (\frac{1}{m}) - \log n = 1 - 0$
111		1m0e1	$⊢ 1 - 0 = 1$
112	110 111	eqtrdi	$⊢ n = 1 \to \sum_{m = 1}^{n} (\frac{1}{m}) - \log n = 1$
113	40	elexi	$⊢ 1 \in V$
114	112 1 113	fvmpt	$⊢ 1 \in ℕ \to F (1) = 1$
115	15 114	ax-mp	$⊢ F (1) = 1$
116	106 115	eqtrdi	$⊢ i = 1 \to F (i) = 1$
117	116	breq2d	$⊢ i = 1 \to (γ \leq F (i) \leftrightarrow γ \leq 1)$
118	117	rspcva	$⊢ (1 \in ℕ \land \forall i \in ℕ γ \leq F (i)) \to γ \leq 1$
119	15 105 118	sylancr	$⊢ ⊤ \to γ \leq 1$
120	44 40	elicc2i	$⊢ γ \in [1 - \log 2, 1] \leftrightarrow (γ \in ℝ \land 1 - \log 2 \leq γ \land γ \leq 1)$
121	14 51 119 120	syl3anbrc	$⊢ ⊤ \to γ \in [1 - \log 2, 1]$
122		ffn	$⊢ F : ℕ ⟶ ℝ \to F Fn ℕ$
123	64 122	mp1i	$⊢ ⊤ \to F Fn ℕ$
124	16 5	eleqtrdi	$⊢ (⊤ \land i \in ℕ) \to i \in ℤ_{\geq 1}$
125		elfznn	$⊢ k \in (1 \dots i) \to k \in ℕ$
126	125	adantl	$⊢ ((⊤ \land i \in ℕ) \land k \in (1 \dots i)) \to k \in ℕ$
127	126 65	syl	$⊢ ((⊤ \land i \in ℕ) \land k \in (1 \dots i)) \to F (k) \in ℝ$
128		elfznn	$⊢ k \in (1 \dots i - 1) \to k \in ℕ$
129	128	adantl	$⊢ ((⊤ \land i \in ℕ) \land k \in (1 \dots i - 1)) \to k \in ℕ$
130	129 80	syl	$⊢ ((⊤ \land i \in ℕ) \land k \in (1 \dots i - 1)) \to F (k + 1) \leq F (k)$
131	124 127 130	monoord2	$⊢ (⊤ \land i \in ℕ) \to F (i) \leq F (1)$
132	131 115	breqtrdi	$⊢ (⊤ \land i \in ℕ) \to F (i) \leq 1$
133	99 40	elicc2i	$⊢ F (i) \in [γ, 1] \leftrightarrow (F (i) \in ℝ \land γ \leq F (i) \land F (i) \leq 1)$
134	101 104 132 133	syl3anbrc	$⊢ (⊤ \land i \in ℕ) \to F (i) \in [γ, 1]$
135	134	ralrimiva	$⊢ ⊤ \to \forall i \in ℕ F (i) \in [γ, 1]$
136		ffnfv	$⊢ F : ℕ ⟶ [γ, 1] \leftrightarrow (F Fn ℕ \land \forall i \in ℕ F (i) \in [γ, 1])$
137	123 135 136	sylanbrc	$⊢ ⊤ \to F : ℕ ⟶ [γ, 1]$
138		ffn	$⊢ G : ℕ ⟶ ℝ \to G Fn ℕ$
139	11 138	mp1i	$⊢ ⊤ \to G Fn ℕ$
140	11	ffvelcdmi	$⊢ i \in ℕ \to G (i) \in ℝ$
141	140	adantl	$⊢ (⊤ \land i \in ℕ) \to G (i) \in ℝ$
142	126 12	syl	$⊢ ((⊤ \land i \in ℕ) \land k \in (1 \dots i)) \to G (k) \in ℝ$
143	129 20	syl	$⊢ ((⊤ \land i \in ℕ) \land k \in (1 \dots i - 1)) \to G (k) \leq G (k + 1)$
144	124 142 143	monoord	$⊢ (⊤ \land i \in ℕ) \to G (1) \leq G (i)$
145	47 144	eqbrtrrid	$⊢ (⊤ \land i \in ℕ) \to 1 - \log 2 \leq G (i)$
146	44 99	elicc2i	$⊢ G (i) \in [1 - \log 2, γ] \leftrightarrow (G (i) \in ℝ \land 1 - \log 2 \leq G (i) \land G (i) \leq γ)$
147	141 145 22 146	syl3anbrc	$⊢ (⊤ \land i \in ℕ) \to G (i) \in [1 - \log 2, γ]$
148	147	ralrimiva	$⊢ ⊤ \to \forall i \in ℕ G (i) \in [1 - \log 2, γ]$
149		ffnfv	$⊢ G : ℕ ⟶ [1 - \log 2, γ] \leftrightarrow (G Fn ℕ \land \forall i \in ℕ G (i) \in [1 - \log 2, γ])$
150	139 148 149	sylanbrc	$⊢ ⊤ \to G : ℕ ⟶ [1 - \log 2, γ]$
151	121 137 150	3jca	$⊢ ⊤ \to (γ \in [1 - \log 2, 1] \land F : ℕ ⟶ [γ, 1] \land G : ℕ ⟶ [1 - \log 2, γ])$
152	151	mptru	$⊢ (γ \in [1 - \log 2, 1] \land F : ℕ ⟶ [γ, 1] \land G : ℕ ⟶ [1 - \log 2, γ])$

Metamath Proof Explorer

Theorem emcllem7

Proof