climcndslem2

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

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

Metamath Proof Explorer

Theorem climcndslem2

Proof