climcndslem1

Description: Lemma for climcnds : bound the original series by the condensed series. (Contributed by Mario Carneiro, 18-Jul-2014)

	Ref	Expression
Hypotheses	climcnds.1	$⊢ (φ \land k \in ℕ) \to F (k) \in ℝ$
	climcnds.2	$⊢ (φ \land k \in ℕ) \to 0 \leq F (k)$
	climcnds.3	$⊢ (φ \land k \in ℕ) \to F (k + 1) \leq F (k)$
	climcnds.4	$⊢ (φ \land n \in ℕ_{0}) \to G (n) = 2^{n} F (2^{n})$
Assertion	climcndslem1	$⊢ (φ \land N \in ℕ_{0}) \to seq 1 (+ F) (2^{N + 1} - 1) \leq seq 0 (+ G) (N)$

Proof

Step	Hyp	Ref	Expression
1		climcnds.1	$⊢ (φ \land k \in ℕ) \to F (k) \in ℝ$
2		climcnds.2	$⊢ (φ \land k \in ℕ) \to 0 \leq F (k)$
3		climcnds.3	$⊢ (φ \land k \in ℕ) \to F (k + 1) \leq F (k)$
4		climcnds.4	$⊢ (φ \land n \in ℕ_{0}) \to G (n) = 2^{n} F (2^{n})$
5		oveq1	$⊢ x = 0 \to x + 1 = 0 + 1$
6		0p1e1	$⊢ 0 + 1 = 1$
7	5 6	eqtrdi	$⊢ x = 0 \to x + 1 = 1$
8	7	oveq2d	$⊢ x = 0 \to 2^{x + 1} = 2^{1}$
9		2cn	$⊢ 2 \in ℂ$
10		exp1	$⊢ 2 \in ℂ \to 2^{1} = 2$
11	9 10	ax-mp	$⊢ 2^{1} = 2$
12		df-2	$⊢ 2 = 1 + 1$
13	11 12	eqtri	$⊢ 2^{1} = 1 + 1$
14	8 13	eqtrdi	$⊢ x = 0 \to 2^{x + 1} = 1 + 1$
15	14	oveq1d	$⊢ x = 0 \to 2^{x + 1} - 1 = 1 + 1 - 1$
16		ax-1cn	$⊢ 1 \in ℂ$
17	16 16	pncan3oi	$⊢ 1 + 1 - 1 = 1$
18	15 17	eqtrdi	$⊢ x = 0 \to 2^{x + 1} - 1 = 1$
19	18	fveq2d	$⊢ x = 0 \to seq 1 (+ F) (2^{x + 1} - 1) = seq 1 (+ F) (1)$
20		fveq2	$⊢ x = 0 \to seq 0 (+ G) (x) = seq 0 (+ G) (0)$
21	19 20	breq12d	$⊢ x = 0 \to (seq 1 (+ F) (2^{x + 1} - 1) \leq seq 0 (+ G) (x) \leftrightarrow seq 1 (+ F) (1) \leq seq 0 (+ G) (0))$
22	21	imbi2d	$⊢ x = 0 \to ((φ \to seq 1 (+ F) (2^{x + 1} - 1) \leq seq 0 (+ G) (x)) \leftrightarrow (φ \to seq 1 (+ F) (1) \leq seq 0 (+ G) (0)))$
23		oveq1	$⊢ x = j \to x + 1 = j + 1$
24	23	oveq2d	$⊢ x = j \to 2^{x + 1} = 2^{j + 1}$
25	24	fvoveq1d	$⊢ x = j \to seq 1 (+ F) (2^{x + 1} - 1) = seq 1 (+ F) (2^{j + 1} - 1)$
26		fveq2	$⊢ x = j \to seq 0 (+ G) (x) = seq 0 (+ G) (j)$
27	25 26	breq12d	$⊢ x = j \to (seq 1 (+ F) (2^{x + 1} - 1) \leq seq 0 (+ G) (x) \leftrightarrow seq 1 (+ F) (2^{j + 1} - 1) \leq seq 0 (+ G) (j))$
28	27	imbi2d	$⊢ x = j \to ((φ \to seq 1 (+ F) (2^{x + 1} - 1) \leq seq 0 (+ G) (x)) \leftrightarrow (φ \to seq 1 (+ F) (2^{j + 1} - 1) \leq seq 0 (+ G) (j)))$
29		oveq1	$⊢ x = j + 1 \to x + 1 = j + 1 + 1$
30	29	oveq2d	$⊢ x = j + 1 \to 2^{x + 1} = 2^{j + 1 + 1}$
31	30	fvoveq1d	$⊢ x = j + 1 \to seq 1 (+ F) (2^{x + 1} - 1) = seq 1 (+ F) (2^{j + 1 + 1} - 1)$
32		fveq2	$⊢ x = j + 1 \to seq 0 (+ G) (x) = seq 0 (+ G) (j + 1)$
33	31 32	breq12d	$⊢ x = j + 1 \to (seq 1 (+ F) (2^{x + 1} - 1) \leq seq 0 (+ G) (x) \leftrightarrow seq 1 (+ F) (2^{j + 1 + 1} - 1) \leq seq 0 (+ G) (j + 1))$
34	33	imbi2d	$⊢ x = j + 1 \to ((φ \to seq 1 (+ F) (2^{x + 1} - 1) \leq seq 0 (+ G) (x)) \leftrightarrow (φ \to seq 1 (+ F) (2^{j + 1 + 1} - 1) \leq seq 0 (+ G) (j + 1)))$
35		oveq1	$⊢ x = N \to x + 1 = N + 1$
36	35	oveq2d	$⊢ x = N \to 2^{x + 1} = 2^{N + 1}$
37	36	fvoveq1d	$⊢ x = N \to seq 1 (+ F) (2^{x + 1} - 1) = seq 1 (+ F) (2^{N + 1} - 1)$
38		fveq2	$⊢ x = N \to seq 0 (+ G) (x) = seq 0 (+ G) (N)$
39	37 38	breq12d	$⊢ x = N \to (seq 1 (+ F) (2^{x + 1} - 1) \leq seq 0 (+ G) (x) \leftrightarrow seq 1 (+ F) (2^{N + 1} - 1) \leq seq 0 (+ G) (N))$
40	39	imbi2d	$⊢ x = N \to ((φ \to seq 1 (+ F) (2^{x + 1} - 1) \leq seq 0 (+ G) (x)) \leftrightarrow (φ \to seq 1 (+ F) (2^{N + 1} - 1) \leq seq 0 (+ G) (N)))$
41		fveq2	$⊢ k = 1 \to F (k) = F (1)$
42	41	eleq1d	$⊢ k = 1 \to (F (k) \in ℝ \leftrightarrow F (1) \in ℝ)$
43	1	ralrimiva	$⊢ φ \to \forall k \in ℕ F (k) \in ℝ$
44		1nn	$⊢ 1 \in ℕ$
45	44	a1i	$⊢ φ \to 1 \in ℕ$
46	42 43 45	rspcdva	$⊢ φ \to F (1) \in ℝ$
47	46	leidd	$⊢ φ \to F (1) \leq F (1)$
48	46	recnd	$⊢ φ \to F (1) \in ℂ$
49	48	mulid2d	$⊢ φ \to 1 F (1) = F (1)$
50	47 49	breqtrrd	$⊢ φ \to F (1) \leq 1 F (1)$
51		1z	$⊢ 1 \in ℤ$
52		eqidd	$⊢ φ \to F (1) = F (1)$
53	51 52	seq1i	$⊢ φ \to seq 1 (+ F) (1) = F (1)$
54		0z	$⊢ 0 \in ℤ$
55		fveq2	$⊢ n = 0 \to G (n) = G (0)$
56		oveq2	$⊢ n = 0 \to 2^{n} = 2^{0}$
57		exp0	$⊢ 2 \in ℂ \to 2^{0} = 1$
58	9 57	ax-mp	$⊢ 2^{0} = 1$
59	56 58	eqtrdi	$⊢ n = 0 \to 2^{n} = 1$
60	59	fveq2d	$⊢ n = 0 \to F (2^{n}) = F (1)$
61	59 60	oveq12d	$⊢ n = 0 \to 2^{n} F (2^{n}) = 1 F (1)$
62	55 61	eqeq12d	$⊢ n = 0 \to (G (n) = 2^{n} F (2^{n}) \leftrightarrow G (0) = 1 F (1))$
63	4	ralrimiva	$⊢ φ \to \forall n \in ℕ_{0} G (n) = 2^{n} F (2^{n})$
64		0nn0	$⊢ 0 \in ℕ_{0}$
65	64	a1i	$⊢ φ \to 0 \in ℕ_{0}$
66	62 63 65	rspcdva	$⊢ φ \to G (0) = 1 F (1)$
67	54 66	seq1i	$⊢ φ \to seq 0 (+ G) (0) = 1 F (1)$
68	50 53 67	3brtr4d	$⊢ φ \to seq 1 (+ F) (1) \leq seq 0 (+ G) (0)$
69		fzfid	$⊢ (φ \land j \in ℕ_{0}) \to (2^{j + 1} \dots 2^{j + 1 + 1} - 1) \in Fin$
70		simpl	$⊢ (φ \land j \in ℕ_{0}) \to φ$
71		2nn	$⊢ 2 \in ℕ$
72		peano2nn0	$⊢ j \in ℕ_{0} \to j + 1 \in ℕ_{0}$
73	72	adantl	$⊢ (φ \land j \in ℕ_{0}) \to j + 1 \in ℕ_{0}$
74		nnexpcl	$⊢ (2 \in ℕ \land j + 1 \in ℕ_{0}) \to 2^{j + 1} \in ℕ$
75	71 73 74	sylancr	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1} \in ℕ$
76		elfzuz	$⊢ k \in (2^{j + 1} \dots 2^{j + 1 + 1} - 1) \to k \in ℤ_{\geq 2^{j + 1}}$
77		eluznn	$⊢ (2^{j + 1} \in ℕ \land k \in ℤ_{\geq 2^{j + 1}}) \to k \in ℕ$
78	75 76 77	syl2an	$⊢ ((φ \land j \in ℕ_{0}) \land k \in (2^{j + 1} \dots 2^{j + 1 + 1} - 1)) \to k \in ℕ$
79	70 78 1	syl2an2r	$⊢ ((φ \land j \in ℕ_{0}) \land k \in (2^{j + 1} \dots 2^{j + 1 + 1} - 1)) \to F (k) \in ℝ$
80		fveq2	$⊢ k = 2^{j + 1} \to F (k) = F (2^{j + 1})$
81	80	eleq1d	$⊢ k = 2^{j + 1} \to (F (k) \in ℝ \leftrightarrow F (2^{j + 1}) \in ℝ)$
82	43	adantr	$⊢ (φ \land j \in ℕ_{0}) \to \forall k \in ℕ F (k) \in ℝ$
83	81 82 75	rspcdva	$⊢ (φ \land j \in ℕ_{0}) \to F (2^{j + 1}) \in ℝ$
84	83	adantr	$⊢ ((φ \land j \in ℕ_{0}) \land k \in (2^{j + 1} \dots 2^{j + 1 + 1} - 1)) \to F (2^{j + 1}) \in ℝ$
85		simpr	$⊢ ((φ \land j \in ℕ_{0}) \land n \in ℤ_{\geq 2^{j + 1}}) \to n \in ℤ_{\geq 2^{j + 1}}$
86		simplll	$⊢ (((φ \land j \in ℕ_{0}) \land n \in ℤ_{\geq 2^{j + 1}}) \land k \in (2^{j + 1} \dots n)) \to φ$
87	75	adantr	$⊢ ((φ \land j \in ℕ_{0}) \land n \in ℤ_{\geq 2^{j + 1}}) \to 2^{j + 1} \in ℕ$
88		elfzuz	$⊢ k \in (2^{j + 1} \dots n) \to k \in ℤ_{\geq 2^{j + 1}}$
89	87 88 77	syl2an	$⊢ (((φ \land j \in ℕ_{0}) \land n \in ℤ_{\geq 2^{j + 1}}) \land k \in (2^{j + 1} \dots n)) \to k \in ℕ$
90	86 89 1	syl2anc	$⊢ (((φ \land j \in ℕ_{0}) \land n \in ℤ_{\geq 2^{j + 1}}) \land k \in (2^{j + 1} \dots n)) \to F (k) \in ℝ$
91		simplll	$⊢ (((φ \land j \in ℕ_{0}) \land n \in ℤ_{\geq 2^{j + 1}}) \land k \in (2^{j + 1} \dots n - 1)) \to φ$
92		elfzuz	$⊢ k \in (2^{j + 1} \dots n - 1) \to k \in ℤ_{\geq 2^{j + 1}}$
93	87 92 77	syl2an	$⊢ (((φ \land j \in ℕ_{0}) \land n \in ℤ_{\geq 2^{j + 1}}) \land k \in (2^{j + 1} \dots n - 1)) \to k \in ℕ$
94	91 93 3	syl2anc	$⊢ (((φ \land j \in ℕ_{0}) \land n \in ℤ_{\geq 2^{j + 1}}) \land k \in (2^{j + 1} \dots n - 1)) \to F (k + 1) \leq F (k)$
95	85 90 94	monoord2	$⊢ ((φ \land j \in ℕ_{0}) \land n \in ℤ_{\geq 2^{j + 1}}) \to F (n) \leq F (2^{j + 1})$
96	95	ralrimiva	$⊢ (φ \land j \in ℕ_{0}) \to \forall n \in ℤ_{\geq 2^{j + 1}} F (n) \leq F (2^{j + 1})$
97		fveq2	$⊢ n = k \to F (n) = F (k)$
98	97	breq1d	$⊢ n = k \to (F (n) \leq F (2^{j + 1}) \leftrightarrow F (k) \leq F (2^{j + 1}))$
99	98	rspccva	$⊢ (\forall n \in ℤ_{\geq 2^{j + 1}} F (n) \leq F (2^{j + 1}) \land k \in ℤ_{\geq 2^{j + 1}}) \to F (k) \leq F (2^{j + 1})$
100	96 76 99	syl2an	$⊢ ((φ \land j \in ℕ_{0}) \land k \in (2^{j + 1} \dots 2^{j + 1 + 1} - 1)) \to F (k) \leq F (2^{j + 1})$
101	69 79 84 100	fsumle	$⊢ (φ \land j \in ℕ_{0}) \to \sum_{k = 2^{j + 1}}^{2^{j + 1 + 1} - 1} F (k) \leq \sum_{k = 2^{j + 1}}^{2^{j + 1 + 1} - 1} F (2^{j + 1})$
102		fzfid	$⊢ (φ \land j \in ℕ_{0}) \to (1 \dots 2^{j + 1} - 1) \in Fin$
103		hashcl	$⊢ (1 \dots 2^{j + 1} - 1) \in Fin \to \|(1 \dots 2^{j + 1} - 1)\| \in ℕ_{0}$
104	102 103	syl	$⊢ (φ \land j \in ℕ_{0}) \to \|(1 \dots 2^{j + 1} - 1)\| \in ℕ_{0}$
105	104	nn0cnd	$⊢ (φ \land j \in ℕ_{0}) \to \|(1 \dots 2^{j + 1} - 1)\| \in ℂ$
106	75	nnred	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1} \in ℝ$
107	106	recnd	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1} \in ℂ$
108		hashcl	$⊢ (2^{j + 1} \dots 2^{j + 1 + 1} - 1) \in Fin \to \|(2^{j + 1} \dots 2^{j + 1 + 1} - 1)\| \in ℕ_{0}$
109	69 108	syl	$⊢ (φ \land j \in ℕ_{0}) \to \|(2^{j + 1} \dots 2^{j + 1 + 1} - 1)\| \in ℕ_{0}$
110	109	nn0cnd	$⊢ (φ \land j \in ℕ_{0}) \to \|(2^{j + 1} \dots 2^{j + 1 + 1} - 1)\| \in ℂ$
111		2z	$⊢ 2 \in ℤ$
112		zexpcl	$⊢ (2 \in ℤ \land j + 1 \in ℕ_{0}) \to 2^{j + 1} \in ℤ$
113	111 73 112	sylancr	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1} \in ℤ$
114		2re	$⊢ 2 \in ℝ$
115		1le2	$⊢ 1 \leq 2$
116		nn0p1nn	$⊢ j \in ℕ_{0} \to j + 1 \in ℕ$
117	116	adantl	$⊢ (φ \land j \in ℕ_{0}) \to j + 1 \in ℕ$
118		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
119	117 118	eleqtrdi	$⊢ (φ \land j \in ℕ_{0}) \to j + 1 \in ℤ_{\geq 1}$
120		leexp2a	$⊢ (2 \in ℝ \land 1 \leq 2 \land j + 1 \in ℤ_{\geq 1}) \to 2^{1} \leq 2^{j + 1}$
121	114 115 119 120	mp3an12i	$⊢ (φ \land j \in ℕ_{0}) \to 2^{1} \leq 2^{j + 1}$
122	11 121	eqbrtrrid	$⊢ (φ \land j \in ℕ_{0}) \to 2 \leq 2^{j + 1}$
123	111	eluz1i	$⊢ 2^{j + 1} \in ℤ_{\geq 2} \leftrightarrow (2^{j + 1} \in ℤ \land 2 \leq 2^{j + 1})$
124	113 122 123	sylanbrc	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1} \in ℤ_{\geq 2}$
125		uz2m1nn	$⊢ 2^{j + 1} \in ℤ_{\geq 2} \to 2^{j + 1} - 1 \in ℕ$
126	124 125	syl	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1} - 1 \in ℕ$
127	126 118	eleqtrdi	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1} - 1 \in ℤ_{\geq 1}$
128		peano2zm	$⊢ 2^{j + 1} \in ℤ \to 2^{j + 1} - 1 \in ℤ$
129	113 128	syl	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1} - 1 \in ℤ$
130		peano2nn0	$⊢ j + 1 \in ℕ_{0} \to j + 1 + 1 \in ℕ_{0}$
131	73 130	syl	$⊢ (φ \land j \in ℕ_{0}) \to j + 1 + 1 \in ℕ_{0}$
132		zexpcl	$⊢ (2 \in ℤ \land j + 1 + 1 \in ℕ_{0}) \to 2^{j + 1 + 1} \in ℤ$
133	111 131 132	sylancr	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1 + 1} \in ℤ$
134		peano2zm	$⊢ 2^{j + 1 + 1} \in ℤ \to 2^{j + 1 + 1} - 1 \in ℤ$
135	133 134	syl	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1 + 1} - 1 \in ℤ$
136	113	zred	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1} \in ℝ$
137	133	zred	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1 + 1} \in ℝ$
138		1red	$⊢ (φ \land j \in ℕ_{0}) \to 1 \in ℝ$
139	73	nn0zd	$⊢ (φ \land j \in ℕ_{0}) \to j + 1 \in ℤ$
140		uzid	$⊢ j + 1 \in ℤ \to j + 1 \in ℤ_{\geq (j + 1)}$
141		peano2uz	$⊢ j + 1 \in ℤ_{\geq (j + 1)} \to j + 1 + 1 \in ℤ_{\geq (j + 1)}$
142		leexp2a	$⊢ (2 \in ℝ \land 1 \leq 2 \land j + 1 + 1 \in ℤ_{\geq (j + 1)}) \to 2^{j + 1} \leq 2^{j + 1 + 1}$
143	114 115 142	mp3an12	$⊢ j + 1 + 1 \in ℤ_{\geq (j + 1)} \to 2^{j + 1} \leq 2^{j + 1 + 1}$
144	139 140 141 143	4syl	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1} \leq 2^{j + 1 + 1}$
145	136 137 138 144	lesub1dd	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1} - 1 \leq 2^{j + 1 + 1} - 1$
146		eluz2	$⊢ 2^{j + 1 + 1} - 1 \in ℤ_{\geq (2^{j + 1} - 1)} \leftrightarrow (2^{j + 1} - 1 \in ℤ \land 2^{j + 1 + 1} - 1 \in ℤ \land 2^{j + 1} - 1 \leq 2^{j + 1 + 1} - 1)$
147	129 135 145 146	syl3anbrc	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1 + 1} - 1 \in ℤ_{\geq (2^{j + 1} - 1)}$
148		elfzuzb	$⊢ 2^{j + 1} - 1 \in (1 \dots 2^{j + 1 + 1} - 1) \leftrightarrow (2^{j + 1} - 1 \in ℤ_{\geq 1} \land 2^{j + 1 + 1} - 1 \in ℤ_{\geq (2^{j + 1} - 1)})$
149	127 147 148	sylanbrc	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1} - 1 \in (1 \dots 2^{j + 1 + 1} - 1)$
150		fzsplit	$⊢ 2^{j + 1} - 1 \in (1 \dots 2^{j + 1 + 1} - 1) \to (1 \dots 2^{j + 1 + 1} - 1) = (1 \dots 2^{j + 1} - 1) \cup (2^{j + 1} - 1 + 1 \dots 2^{j + 1 + 1} - 1)$
151	149 150	syl	$⊢ (φ \land j \in ℕ_{0}) \to (1 \dots 2^{j + 1 + 1} - 1) = (1 \dots 2^{j + 1} - 1) \cup (2^{j + 1} - 1 + 1 \dots 2^{j + 1 + 1} - 1)$
152		npcan	$⊢ (2^{j + 1} \in ℂ \land 1 \in ℂ) \to 2^{j + 1} - 1 + 1 = 2^{j + 1}$
153	107 16 152	sylancl	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1} - 1 + 1 = 2^{j + 1}$
154	153	oveq1d	$⊢ (φ \land j \in ℕ_{0}) \to (2^{j + 1} - 1 + 1 \dots 2^{j + 1 + 1} - 1) = (2^{j + 1} \dots 2^{j + 1 + 1} - 1)$
155	154	uneq2d	$⊢ (φ \land j \in ℕ_{0}) \to (1 \dots 2^{j + 1} - 1) \cup (2^{j + 1} - 1 + 1 \dots 2^{j + 1 + 1} - 1) = (1 \dots 2^{j + 1} - 1) \cup (2^{j + 1} \dots 2^{j + 1 + 1} - 1)$
156	151 155	eqtrd	$⊢ (φ \land j \in ℕ_{0}) \to (1 \dots 2^{j + 1 + 1} - 1) = (1 \dots 2^{j + 1} - 1) \cup (2^{j + 1} \dots 2^{j + 1 + 1} - 1)$
157	156	fveq2d	$⊢ (φ \land j \in ℕ_{0}) \to \|(1 \dots 2^{j + 1 + 1} - 1)\| = \|(1 \dots 2^{j + 1} - 1) \cup (2^{j + 1} \dots 2^{j + 1 + 1} - 1)\|$
158		expp1	$⊢ (2 \in ℂ \land j + 1 \in ℕ_{0}) \to 2^{j + 1 + 1} = 2^{j + 1} \cdot 2$
159	9 73 158	sylancr	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1 + 1} = 2^{j + 1} \cdot 2$
160	107	times2d	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1} \cdot 2 = 2^{j + 1} + 2^{j + 1}$
161	159 160	eqtrd	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1 + 1} = 2^{j + 1} + 2^{j + 1}$
162	161	oveq1d	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1 + 1} - 1 = 2^{j + 1} + 2^{j + 1} - 1$
163		1cnd	$⊢ (φ \land j \in ℕ_{0}) \to 1 \in ℂ$
164	107 107 163	addsubd	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1} + 2^{j + 1} - 1 = 2^{j + 1} - 1 + 2^{j + 1}$
165	162 164	eqtrd	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1 + 1} - 1 = 2^{j + 1} - 1 + 2^{j + 1}$
166		uztrn	$⊢ (2^{j + 1 + 1} - 1 \in ℤ_{\geq (2^{j + 1} - 1)} \land 2^{j + 1} - 1 \in ℤ_{\geq 1}) \to 2^{j + 1 + 1} - 1 \in ℤ_{\geq 1}$
167	147 127 166	syl2anc	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1 + 1} - 1 \in ℤ_{\geq 1}$
168	167 118	eleqtrrdi	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1 + 1} - 1 \in ℕ$
169	168	nnnn0d	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1 + 1} - 1 \in ℕ_{0}$
170		hashfz1	$⊢ 2^{j + 1 + 1} - 1 \in ℕ_{0} \to \|(1 \dots 2^{j + 1 + 1} - 1)\| = 2^{j + 1 + 1} - 1$
171	169 170	syl	$⊢ (φ \land j \in ℕ_{0}) \to \|(1 \dots 2^{j + 1 + 1} - 1)\| = 2^{j + 1 + 1} - 1$
172	126	nnnn0d	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1} - 1 \in ℕ_{0}$
173		hashfz1	$⊢ 2^{j + 1} - 1 \in ℕ_{0} \to \|(1 \dots 2^{j + 1} - 1)\| = 2^{j + 1} - 1$
174	172 173	syl	$⊢ (φ \land j \in ℕ_{0}) \to \|(1 \dots 2^{j + 1} - 1)\| = 2^{j + 1} - 1$
175	174	oveq1d	$⊢ (φ \land j \in ℕ_{0}) \to \|(1 \dots 2^{j + 1} - 1)\| + 2^{j + 1} = 2^{j + 1} - 1 + 2^{j + 1}$
176	165 171 175	3eqtr4d	$⊢ (φ \land j \in ℕ_{0}) \to \|(1 \dots 2^{j + 1 + 1} - 1)\| = \|(1 \dots 2^{j + 1} - 1)\| + 2^{j + 1}$
177	106	ltm1d	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1} - 1 < 2^{j + 1}$
178		fzdisj	$⊢ 2^{j + 1} - 1 < 2^{j + 1} \to (1 \dots 2^{j + 1} - 1) \cap (2^{j + 1} \dots 2^{j + 1 + 1} - 1) = \emptyset$
179	177 178	syl	$⊢ (φ \land j \in ℕ_{0}) \to (1 \dots 2^{j + 1} - 1) \cap (2^{j + 1} \dots 2^{j + 1 + 1} - 1) = \emptyset$
180		hashun	$⊢ ((1 \dots 2^{j + 1} - 1) \in Fin \land (2^{j + 1} \dots 2^{j + 1 + 1} - 1) \in Fin \land (1 \dots 2^{j + 1} - 1) \cap (2^{j + 1} \dots 2^{j + 1 + 1} - 1) = \emptyset) \to \|(1 \dots 2^{j + 1} - 1) \cup (2^{j + 1} \dots 2^{j + 1 + 1} - 1)\| = \|(1 \dots 2^{j + 1} - 1)\| + \|(2^{j + 1} \dots 2^{j + 1 + 1} - 1)\|$
181	102 69 179 180	syl3anc	$⊢ (φ \land j \in ℕ_{0}) \to \|(1 \dots 2^{j + 1} - 1) \cup (2^{j + 1} \dots 2^{j + 1 + 1} - 1)\| = \|(1 \dots 2^{j + 1} - 1)\| + \|(2^{j + 1} \dots 2^{j + 1 + 1} - 1)\|$
182	157 176 181	3eqtr3d	$⊢ (φ \land j \in ℕ_{0}) \to \|(1 \dots 2^{j + 1} - 1)\| + 2^{j + 1} = \|(1 \dots 2^{j + 1} - 1)\| + \|(2^{j + 1} \dots 2^{j + 1 + 1} - 1)\|$
183	105 107 110 182	addcanad	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1} = \|(2^{j + 1} \dots 2^{j + 1 + 1} - 1)\|$
184	183	oveq1d	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1} F (2^{j + 1}) = \|(2^{j + 1} \dots 2^{j + 1 + 1} - 1)\| F (2^{j + 1})$
185		fveq2	$⊢ n = j + 1 \to G (n) = G (j + 1)$
186		oveq2	$⊢ n = j + 1 \to 2^{n} = 2^{j + 1}$
187	186	fveq2d	$⊢ n = j + 1 \to F (2^{n}) = F (2^{j + 1})$
188	186 187	oveq12d	$⊢ n = j + 1 \to 2^{n} F (2^{n}) = 2^{j + 1} F (2^{j + 1})$
189	185 188	eqeq12d	$⊢ n = j + 1 \to (G (n) = 2^{n} F (2^{n}) \leftrightarrow G (j + 1) = 2^{j + 1} F (2^{j + 1}))$
190	63	adantr	$⊢ (φ \land j \in ℕ_{0}) \to \forall n \in ℕ_{0} G (n) = 2^{n} F (2^{n})$
191	189 190 73	rspcdva	$⊢ (φ \land j \in ℕ_{0}) \to G (j + 1) = 2^{j + 1} F (2^{j + 1})$
192	83	recnd	$⊢ (φ \land j \in ℕ_{0}) \to F (2^{j + 1}) \in ℂ$
193		fsumconst	$⊢ ((2^{j + 1} \dots 2^{j + 1 + 1} - 1) \in Fin \land F (2^{j + 1}) \in ℂ) \to \sum_{k = 2^{j + 1}}^{2^{j + 1 + 1} - 1} F (2^{j + 1}) = \|(2^{j + 1} \dots 2^{j + 1 + 1} - 1)\| F (2^{j + 1})$
194	69 192 193	syl2anc	$⊢ (φ \land j \in ℕ_{0}) \to \sum_{k = 2^{j + 1}}^{2^{j + 1 + 1} - 1} F (2^{j + 1}) = \|(2^{j + 1} \dots 2^{j + 1 + 1} - 1)\| F (2^{j + 1})$
195	184 191 194	3eqtr4d	$⊢ (φ \land j \in ℕ_{0}) \to G (j + 1) = \sum_{k = 2^{j + 1}}^{2^{j + 1 + 1} - 1} F (2^{j + 1})$
196	101 195	breqtrrd	$⊢ (φ \land j \in ℕ_{0}) \to \sum_{k = 2^{j + 1}}^{2^{j + 1 + 1} - 1} F (k) \leq G (j + 1)$
197		elfznn	$⊢ k \in (1 \dots 2^{j + 1} - 1) \to k \in ℕ$
198	70 197 1	syl2an	$⊢ ((φ \land j \in ℕ_{0}) \land k \in (1 \dots 2^{j + 1} - 1)) \to F (k) \in ℝ$
199	102 198	fsumrecl	$⊢ (φ \land j \in ℕ_{0}) \to \sum_{k = 1}^{2^{j + 1} - 1} F (k) \in ℝ$
200	69 79	fsumrecl	$⊢ (φ \land j \in ℕ_{0}) \to \sum_{k = 2^{j + 1}}^{2^{j + 1 + 1} - 1} F (k) \in ℝ$
201		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
202		0zd	$⊢ φ \to 0 \in ℤ$
203		simpr	$⊢ (φ \land n \in ℕ_{0}) \to n \in ℕ_{0}$
204		nnexpcl	$⊢ (2 \in ℕ \land n \in ℕ_{0}) \to 2^{n} \in ℕ$
205	71 203 204	sylancr	$⊢ (φ \land n \in ℕ_{0}) \to 2^{n} \in ℕ$
206	205	nnred	$⊢ (φ \land n \in ℕ_{0}) \to 2^{n} \in ℝ$
207		fveq2	$⊢ k = 2^{n} \to F (k) = F (2^{n})$
208	207	eleq1d	$⊢ k = 2^{n} \to (F (k) \in ℝ \leftrightarrow F (2^{n}) \in ℝ)$
209	43	adantr	$⊢ (φ \land n \in ℕ_{0}) \to \forall k \in ℕ F (k) \in ℝ$
210	208 209 205	rspcdva	$⊢ (φ \land n \in ℕ_{0}) \to F (2^{n}) \in ℝ$
211	206 210	remulcld	$⊢ (φ \land n \in ℕ_{0}) \to 2^{n} F (2^{n}) \in ℝ$
212	4 211	eqeltrd	$⊢ (φ \land n \in ℕ_{0}) \to G (n) \in ℝ$
213	201 202 212	serfre	$⊢ φ \to seq 0 (+ G) : ℕ_{0} ⟶ ℝ$
214	213	ffvelrnda	$⊢ (φ \land j \in ℕ_{0}) \to seq 0 (+ G) (j) \in ℝ$
215	136 83	remulcld	$⊢ (φ \land j \in ℕ_{0}) \to 2^{j + 1} F (2^{j + 1}) \in ℝ$
216	191 215	eqeltrd	$⊢ (φ \land j \in ℕ_{0}) \to G (j + 1) \in ℝ$
217		le2add	$⊢ ((\sum_{k = 1}^{2^{j + 1} - 1} F (k) \in ℝ \land \sum_{k = 2^{j + 1}}^{2^{j + 1 + 1} - 1} F (k) \in ℝ) \land (seq 0 (+ G) (j) \in ℝ \land G (j + 1) \in ℝ)) \to ((\sum_{k = 1}^{2^{j + 1} - 1} F (k) \leq seq 0 (+ G) (j) \land \sum_{k = 2^{j + 1}}^{2^{j + 1 + 1} - 1} F (k) \leq G (j + 1)) \to \sum_{k = 1}^{2^{j + 1} - 1} F (k) + \sum_{k = 2^{j + 1}}^{2^{j + 1 + 1} - 1} F (k) \leq seq 0 (+ G) (j) + G (j + 1))$
218	199 200 214 216 217	syl22anc	$⊢ (φ \land j \in ℕ_{0}) \to ((\sum_{k = 1}^{2^{j + 1} - 1} F (k) \leq seq 0 (+ G) (j) \land \sum_{k = 2^{j + 1}}^{2^{j + 1 + 1} - 1} F (k) \leq G (j + 1)) \to \sum_{k = 1}^{2^{j + 1} - 1} F (k) + \sum_{k = 2^{j + 1}}^{2^{j + 1 + 1} - 1} F (k) \leq seq 0 (+ G) (j) + G (j + 1))$
219	196 218	mpan2d	$⊢ (φ \land j \in ℕ_{0}) \to (\sum_{k = 1}^{2^{j + 1} - 1} F (k) \leq seq 0 (+ G) (j) \to \sum_{k = 1}^{2^{j + 1} - 1} F (k) + \sum_{k = 2^{j + 1}}^{2^{j + 1 + 1} - 1} F (k) \leq seq 0 (+ G) (j) + G (j + 1))$
220		eqidd	$⊢ ((φ \land j \in ℕ_{0}) \land k \in (1 \dots 2^{j + 1} - 1)) \to F (k) = F (k)$
221	1	recnd	$⊢ (φ \land k \in ℕ) \to F (k) \in ℂ$
222	70 197 221	syl2an	$⊢ ((φ \land j \in ℕ_{0}) \land k \in (1 \dots 2^{j + 1} - 1)) \to F (k) \in ℂ$
223	220 127 222	fsumser	$⊢ (φ \land j \in ℕ_{0}) \to \sum_{k = 1}^{2^{j + 1} - 1} F (k) = seq 1 (+ F) (2^{j + 1} - 1)$
224	223	eqcomd	$⊢ (φ \land j \in ℕ_{0}) \to seq 1 (+ F) (2^{j + 1} - 1) = \sum_{k = 1}^{2^{j + 1} - 1} F (k)$
225	224	breq1d	$⊢ (φ \land j \in ℕ_{0}) \to (seq 1 (+ F) (2^{j + 1} - 1) \leq seq 0 (+ G) (j) \leftrightarrow \sum_{k = 1}^{2^{j + 1} - 1} F (k) \leq seq 0 (+ G) (j))$
226		eqidd	$⊢ ((φ \land j \in ℕ_{0}) \land k \in (1 \dots 2^{j + 1 + 1} - 1)) \to F (k) = F (k)$
227		elfznn	$⊢ k \in (1 \dots 2^{j + 1 + 1} - 1) \to k \in ℕ$
228	70 227 221	syl2an	$⊢ ((φ \land j \in ℕ_{0}) \land k \in (1 \dots 2^{j + 1 + 1} - 1)) \to F (k) \in ℂ$
229	226 167 228	fsumser	$⊢ (φ \land j \in ℕ_{0}) \to \sum_{k = 1}^{2^{j + 1 + 1} - 1} F (k) = seq 1 (+ F) (2^{j + 1 + 1} - 1)$
230		fzfid	$⊢ (φ \land j \in ℕ_{0}) \to (1 \dots 2^{j + 1 + 1} - 1) \in Fin$
231	179 156 230 228	fsumsplit	$⊢ (φ \land j \in ℕ_{0}) \to \sum_{k = 1}^{2^{j + 1 + 1} - 1} F (k) = \sum_{k = 1}^{2^{j + 1} - 1} F (k) + \sum_{k = 2^{j + 1}}^{2^{j + 1 + 1} - 1} F (k)$
232	229 231	eqtr3d	$⊢ (φ \land j \in ℕ_{0}) \to seq 1 (+ F) (2^{j + 1 + 1} - 1) = \sum_{k = 1}^{2^{j + 1} - 1} F (k) + \sum_{k = 2^{j + 1}}^{2^{j + 1 + 1} - 1} F (k)$
233		simpr	$⊢ (φ \land j \in ℕ_{0}) \to j \in ℕ_{0}$
234	233 201	eleqtrdi	$⊢ (φ \land j \in ℕ_{0}) \to j \in ℤ_{\geq 0}$
235		seqp1	$⊢ j \in ℤ_{\geq 0} \to seq 0 (+ G) (j + 1) = seq 0 (+ G) (j) + G (j + 1)$
236	234 235	syl	$⊢ (φ \land j \in ℕ_{0}) \to seq 0 (+ G) (j + 1) = seq 0 (+ G) (j) + G (j + 1)$
237	232 236	breq12d	$⊢ (φ \land j \in ℕ_{0}) \to (seq 1 (+ F) (2^{j + 1 + 1} - 1) \leq seq 0 (+ G) (j + 1) \leftrightarrow \sum_{k = 1}^{2^{j + 1} - 1} F (k) + \sum_{k = 2^{j + 1}}^{2^{j + 1 + 1} - 1} F (k) \leq seq 0 (+ G) (j) + G (j + 1))$
238	219 225 237	3imtr4d	$⊢ (φ \land j \in ℕ_{0}) \to (seq 1 (+ F) (2^{j + 1} - 1) \leq seq 0 (+ G) (j) \to seq 1 (+ F) (2^{j + 1 + 1} - 1) \leq seq 0 (+ G) (j + 1))$
239	238	expcom	$⊢ j \in ℕ_{0} \to (φ \to (seq 1 (+ F) (2^{j + 1} - 1) \leq seq 0 (+ G) (j) \to seq 1 (+ F) (2^{j + 1 + 1} - 1) \leq seq 0 (+ G) (j + 1)))$
240	239	a2d	$⊢ j \in ℕ_{0} \to ((φ \to seq 1 (+ F) (2^{j + 1} - 1) \leq seq 0 (+ G) (j)) \to (φ \to seq 1 (+ F) (2^{j + 1 + 1} - 1) \leq seq 0 (+ G) (j + 1)))$
241	22 28 34 40 68 240	nn0ind	$⊢ N \in ℕ_{0} \to (φ \to seq 1 (+ F) (2^{N + 1} - 1) \leq seq 0 (+ G) (N))$
242	241	impcom	$⊢ (φ \land N \in ℕ_{0}) \to seq 1 (+ F) (2^{N + 1} - 1) \leq seq 0 (+ G) (N)$

Metamath Proof Explorer

Theorem climcndslem1

Proof