climcnds

Description: The Cauchy condensation test. If a ( k ) is a decreasing sequence of nonnegative terms, then sum_ k e. NN a ( k ) converges iff sum_ n e. NN0 2 ^ n x. a ( 2 ^ n ) converges. (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	climcnds	$⊢ φ \to (seq 1 (+ F) \in dom ⇝ \leftrightarrow seq 0 (+ G) \in dom ⇝)$

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		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
6		1zzd	$⊢ (φ \land seq 1 (+ F) \in dom ⇝) \to 1 \in ℤ$
7		1zzd	$⊢ φ \to 1 \in ℤ$
8		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
9		2nn	$⊢ 2 \in ℕ$
10		simpr	$⊢ (φ \land n \in ℕ_{0}) \to n \in ℕ_{0}$
11		nnexpcl	$⊢ (2 \in ℕ \land n \in ℕ_{0}) \to 2^{n} \in ℕ$
12	9 10 11	sylancr	$⊢ (φ \land n \in ℕ_{0}) \to 2^{n} \in ℕ$
13	12	nnred	$⊢ (φ \land n \in ℕ_{0}) \to 2^{n} \in ℝ$
14		fveq2	$⊢ k = 2^{n} \to F (k) = F (2^{n})$
15	14	eleq1d	$⊢ k = 2^{n} \to (F (k) \in ℝ \leftrightarrow F (2^{n}) \in ℝ)$
16	1	ralrimiva	$⊢ φ \to \forall k \in ℕ F (k) \in ℝ$
17	16	adantr	$⊢ (φ \land n \in ℕ_{0}) \to \forall k \in ℕ F (k) \in ℝ$
18	15 17 12	rspcdva	$⊢ (φ \land n \in ℕ_{0}) \to F (2^{n}) \in ℝ$
19	13 18	remulcld	$⊢ (φ \land n \in ℕ_{0}) \to 2^{n} F (2^{n}) \in ℝ$
20	4 19	eqeltrd	$⊢ (φ \land n \in ℕ_{0}) \to G (n) \in ℝ$
21	8 20	sylan2	$⊢ (φ \land n \in ℕ) \to G (n) \in ℝ$
22	5 7 21	serfre	$⊢ φ \to seq 1 (+ G) : ℕ ⟶ ℝ$
23	22	adantr	$⊢ (φ \land seq 1 (+ F) \in dom ⇝) \to seq 1 (+ G) : ℕ ⟶ ℝ$
24		simpr	$⊢ (φ \land j \in ℕ) \to j \in ℕ$
25	24 5	eleqtrdi	$⊢ (φ \land j \in ℕ) \to j \in ℤ_{\geq 1}$
26		nnz	$⊢ j \in ℕ \to j \in ℤ$
27	26	adantl	$⊢ (φ \land j \in ℕ) \to j \in ℤ$
28		uzid	$⊢ j \in ℤ \to j \in ℤ_{\geq j}$
29		peano2uz	$⊢ j \in ℤ_{\geq j} \to j + 1 \in ℤ_{\geq j}$
30	27 28 29	3syl	$⊢ (φ \land j \in ℕ) \to j + 1 \in ℤ_{\geq j}$
31		simpl	$⊢ (φ \land j \in ℕ) \to φ$
32		elfznn	$⊢ n \in (1 \dots j + 1) \to n \in ℕ$
33	31 32 21	syl2an	$⊢ ((φ \land j \in ℕ) \land n \in (1 \dots j + 1)) \to G (n) \in ℝ$
34		simpll	$⊢ ((φ \land j \in ℕ) \land n \in (j + 1 \dots j + 1)) \to φ$
35		elfz1eq	$⊢ n \in (j + 1 \dots j + 1) \to n = j + 1$
36	35	adantl	$⊢ ((φ \land j \in ℕ) \land n \in (j + 1 \dots j + 1)) \to n = j + 1$
37		nnnn0	$⊢ j \in ℕ \to j \in ℕ_{0}$
38		peano2nn0	$⊢ j \in ℕ_{0} \to j + 1 \in ℕ_{0}$
39	37 38	syl	$⊢ j \in ℕ \to j + 1 \in ℕ_{0}$
40	39	ad2antlr	$⊢ ((φ \land j \in ℕ) \land n \in (j + 1 \dots j + 1)) \to j + 1 \in ℕ_{0}$
41	36 40	eqeltrd	$⊢ ((φ \land j \in ℕ) \land n \in (j + 1 \dots j + 1)) \to n \in ℕ_{0}$
42	12	nnnn0d	$⊢ (φ \land n \in ℕ_{0}) \to 2^{n} \in ℕ_{0}$
43	42	nn0ge0d	$⊢ (φ \land n \in ℕ_{0}) \to 0 \leq 2^{n}$
44	14	breq2d	$⊢ k = 2^{n} \to (0 \leq F (k) \leftrightarrow 0 \leq F (2^{n}))$
45	2	ralrimiva	$⊢ φ \to \forall k \in ℕ 0 \leq F (k)$
46	45	adantr	$⊢ (φ \land n \in ℕ_{0}) \to \forall k \in ℕ 0 \leq F (k)$
47	44 46 12	rspcdva	$⊢ (φ \land n \in ℕ_{0}) \to 0 \leq F (2^{n})$
48	13 18 43 47	mulge0d	$⊢ (φ \land n \in ℕ_{0}) \to 0 \leq 2^{n} F (2^{n})$
49	48 4	breqtrrd	$⊢ (φ \land n \in ℕ_{0}) \to 0 \leq G (n)$
50	34 41 49	syl2anc	$⊢ ((φ \land j \in ℕ) \land n \in (j + 1 \dots j + 1)) \to 0 \leq G (n)$
51	25 30 33 50	sermono	$⊢ (φ \land j \in ℕ) \to seq 1 (+ G) (j) \leq seq 1 (+ G) (j + 1)$
52	51	adantlr	$⊢ ((φ \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \to seq 1 (+ G) (j) \leq seq 1 (+ G) (j + 1)$
53		2re	$⊢ 2 \in ℝ$
54		eqidd	$⊢ ((φ \land seq 1 (+ F) \in dom ⇝) \land k \in ℕ) \to F (k) = F (k)$
55	1	adantlr	$⊢ ((φ \land seq 1 (+ F) \in dom ⇝) \land k \in ℕ) \to F (k) \in ℝ$
56		simpr	$⊢ (φ \land seq 1 (+ F) \in dom ⇝) \to seq 1 (+ F) \in dom ⇝$
57	5 6 54 55 56	isumrecl	$⊢ (φ \land seq 1 (+ F) \in dom ⇝) \to \sum_{k \in ℕ} F (k) \in ℝ$
58		remulcl	$⊢ (2 \in ℝ \land \sum_{k \in ℕ} F (k) \in ℝ) \to 2 \sum_{k \in ℕ} F (k) \in ℝ$
59	53 57 58	sylancr	$⊢ (φ \land seq 1 (+ F) \in dom ⇝) \to 2 \sum_{k \in ℕ} F (k) \in ℝ$
60	23	ffvelcdmda	$⊢ ((φ \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \to seq 1 (+ G) (j) \in ℝ$
61	5 7 1	serfre	$⊢ φ \to seq 1 (+ F) : ℕ ⟶ ℝ$
62	61	ad2antrr	$⊢ ((φ \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \to seq 1 (+ F) : ℕ ⟶ ℝ$
63	37	adantl	$⊢ ((φ \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \to j \in ℕ_{0}$
64		nnexpcl	$⊢ (2 \in ℕ \land j \in ℕ_{0}) \to 2^{j} \in ℕ$
65	9 63 64	sylancr	$⊢ ((φ \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \to 2^{j} \in ℕ$
66	62 65	ffvelcdmd	$⊢ ((φ \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \to seq 1 (+ F) (2^{j}) \in ℝ$
67		remulcl	$⊢ (2 \in ℝ \land seq 1 (+ F) (2^{j}) \in ℝ) \to 2 seq 1 (+ F) (2^{j}) \in ℝ$
68	53 66 67	sylancr	$⊢ ((φ \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \to 2 seq 1 (+ F) (2^{j}) \in ℝ$
69	59	adantr	$⊢ ((φ \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \to 2 \sum_{k \in ℕ} F (k) \in ℝ$
70	1 2 3 4	climcndslem2	$⊢ (φ \land j \in ℕ) \to seq 1 (+ G) (j) \leq 2 seq 1 (+ F) (2^{j})$
71	70	adantlr	$⊢ ((φ \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \to seq 1 (+ G) (j) \leq 2 seq 1 (+ F) (2^{j})$
72		eqidd	$⊢ (((φ \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \land k \in (1 \dots 2^{j})) \to F (k) = F (k)$
73	65 5	eleqtrdi	$⊢ ((φ \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \to 2^{j} \in ℤ_{\geq 1}$
74		simpll	$⊢ ((φ \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \to φ$
75		elfznn	$⊢ k \in (1 \dots 2^{j}) \to k \in ℕ$
76	1	recnd	$⊢ (φ \land k \in ℕ) \to F (k) \in ℂ$
77	74 75 76	syl2an	$⊢ (((φ \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \land k \in (1 \dots 2^{j})) \to F (k) \in ℂ$
78	72 73 77	fsumser	$⊢ ((φ \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \to \sum_{k = 1}^{2^{j}} F (k) = seq 1 (+ F) (2^{j})$
79		1zzd	$⊢ ((φ \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \to 1 \in ℤ$
80		fzfid	$⊢ ((φ \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \to (1 \dots 2^{j}) \in Fin$
81	75	ssriv	$⊢ (1 \dots 2^{j}) \subseteq ℕ$
82	81	a1i	$⊢ ((φ \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \to (1 \dots 2^{j}) \subseteq ℕ$
83		eqidd	$⊢ (((φ \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \land k \in ℕ) \to F (k) = F (k)$
84	1	ad4ant14	$⊢ (((φ \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \land k \in ℕ) \to F (k) \in ℝ$
85	2	ad4ant14	$⊢ (((φ \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \land k \in ℕ) \to 0 \leq F (k)$
86		simplr	$⊢ ((φ \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \to seq 1 (+ F) \in dom ⇝$
87	5 79 80 82 83 84 85 86	isumless	$⊢ ((φ \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \to \sum_{k = 1}^{2^{j}} F (k) \leq \sum_{k \in ℕ} F (k)$
88	78 87	eqbrtrrd	$⊢ ((φ \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \to seq 1 (+ F) (2^{j}) \leq \sum_{k \in ℕ} F (k)$
89	57	adantr	$⊢ ((φ \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \to \sum_{k \in ℕ} F (k) \in ℝ$
90		2rp	$⊢ 2 \in ℝ^{+}$
91	90	a1i	$⊢ ((φ \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \to 2 \in ℝ^{+}$
92	66 89 91	lemul2d	$⊢ ((φ \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \to (seq 1 (+ F) (2^{j}) \leq \sum_{k \in ℕ} F (k) \leftrightarrow 2 seq 1 (+ F) (2^{j}) \leq 2 \sum_{k \in ℕ} F (k))$
93	88 92	mpbid	$⊢ ((φ \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \to 2 seq 1 (+ F) (2^{j}) \leq 2 \sum_{k \in ℕ} F (k)$
94	60 68 69 71 93	letrd	$⊢ ((φ \land seq 1 (+ F) \in dom ⇝) \land j \in ℕ) \to seq 1 (+ G) (j) \leq 2 \sum_{k \in ℕ} F (k)$
95	94	ralrimiva	$⊢ (φ \land seq 1 (+ F) \in dom ⇝) \to \forall j \in ℕ seq 1 (+ G) (j) \leq 2 \sum_{k \in ℕ} F (k)$
96		brralrspcev	$⊢ (2 \sum_{k \in ℕ} F (k) \in ℝ \land \forall j \in ℕ seq 1 (+ G) (j) \leq 2 \sum_{k \in ℕ} F (k)) \to \exists x \in ℝ \forall j \in ℕ seq 1 (+ G) (j) \leq x$
97	59 95 96	syl2anc	$⊢ (φ \land seq 1 (+ F) \in dom ⇝) \to \exists x \in ℝ \forall j \in ℕ seq 1 (+ G) (j) \leq x$
98	5 6 23 52 97	climsup	$⊢ (φ \land seq 1 (+ F) \in dom ⇝) \to seq 1 (+ G) ⇝ sup (ran seq 1 (+ G) ℝ <)$
99		climrel	$⊢ Rel ⇝$
100	99	releldmi	$⊢ seq 1 (+ G) ⇝ sup (ran seq 1 (+ G) ℝ <) \to seq 1 (+ G) \in dom ⇝$
101	98 100	syl	$⊢ (φ \land seq 1 (+ F) \in dom ⇝) \to seq 1 (+ G) \in dom ⇝$
102		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
103		1nn0	$⊢ 1 \in ℕ_{0}$
104	103	a1i	$⊢ φ \to 1 \in ℕ_{0}$
105	20	recnd	$⊢ (φ \land n \in ℕ_{0}) \to G (n) \in ℂ$
106	102 104 105	iserex	$⊢ φ \to (seq 0 (+ G) \in dom ⇝ \leftrightarrow seq 1 (+ G) \in dom ⇝)$
107	106	biimpar	$⊢ (φ \land seq 1 (+ G) \in dom ⇝) \to seq 0 (+ G) \in dom ⇝$
108	101 107	syldan	$⊢ (φ \land seq 1 (+ F) \in dom ⇝) \to seq 0 (+ G) \in dom ⇝$
109		1zzd	$⊢ (φ \land seq 0 (+ G) \in dom ⇝) \to 1 \in ℤ$
110	61	adantr	$⊢ (φ \land seq 0 (+ G) \in dom ⇝) \to seq 1 (+ F) : ℕ ⟶ ℝ$
111		elfznn	$⊢ k \in (1 \dots j + 1) \to k \in ℕ$
112	31 111 1	syl2an	$⊢ ((φ \land j \in ℕ) \land k \in (1 \dots j + 1)) \to F (k) \in ℝ$
113		simpll	$⊢ ((φ \land j \in ℕ) \land k \in (j + 1 \dots j + 1)) \to φ$
114		peano2nn	$⊢ j \in ℕ \to j + 1 \in ℕ$
115	114	adantl	$⊢ (φ \land j \in ℕ) \to j + 1 \in ℕ$
116		elfz1eq	$⊢ k \in (j + 1 \dots j + 1) \to k = j + 1$
117		eleq1	$⊢ k = j + 1 \to (k \in ℕ \leftrightarrow j + 1 \in ℕ)$
118	117	biimparc	$⊢ (j + 1 \in ℕ \land k = j + 1) \to k \in ℕ$
119	115 116 118	syl2an	$⊢ ((φ \land j \in ℕ) \land k \in (j + 1 \dots j + 1)) \to k \in ℕ$
120	113 119 2	syl2anc	$⊢ ((φ \land j \in ℕ) \land k \in (j + 1 \dots j + 1)) \to 0 \leq F (k)$
121	25 30 112 120	sermono	$⊢ (φ \land j \in ℕ) \to seq 1 (+ F) (j) \leq seq 1 (+ F) (j + 1)$
122	121	adantlr	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to seq 1 (+ F) (j) \leq seq 1 (+ F) (j + 1)$
123		0zd	$⊢ (φ \land seq 0 (+ G) \in dom ⇝) \to 0 \in ℤ$
124		eqidd	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land n \in ℕ_{0}) \to G (n) = G (n)$
125	20	adantlr	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land n \in ℕ_{0}) \to G (n) \in ℝ$
126		simpr	$⊢ (φ \land seq 0 (+ G) \in dom ⇝) \to seq 0 (+ G) \in dom ⇝$
127	102 123 124 125 126	isumrecl	$⊢ (φ \land seq 0 (+ G) \in dom ⇝) \to \sum_{n \in ℕ_{0}} G (n) \in ℝ$
128	110	ffvelcdmda	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to seq 1 (+ F) (j) \in ℝ$
129		0zd	$⊢ φ \to 0 \in ℤ$
130	102 129 20	serfre	$⊢ φ \to seq 0 (+ G) : ℕ_{0} ⟶ ℝ$
131	130	adantr	$⊢ (φ \land seq 0 (+ G) \in dom ⇝) \to seq 0 (+ G) : ℕ_{0} ⟶ ℝ$
132		ffvelcdm	$⊢ (seq 0 (+ G) : ℕ_{0} ⟶ ℝ \land j \in ℕ_{0}) \to seq 0 (+ G) (j) \in ℝ$
133	131 37 132	syl2an	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to seq 0 (+ G) (j) \in ℝ$
134	127	adantr	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to \sum_{n \in ℕ_{0}} G (n) \in ℝ$
135	110	adantr	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to seq 1 (+ F) : ℕ ⟶ ℝ$
136		simpr	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to j \in ℕ$
137	26	adantl	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to j \in ℤ$
138	39	adantl	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to j + 1 \in ℕ_{0}$
139	138	nn0red	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to j + 1 \in ℝ$
140		nnexpcl	$⊢ (2 \in ℕ \land j + 1 \in ℕ_{0}) \to 2^{j + 1} \in ℕ$
141	9 138 140	sylancr	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to 2^{j + 1} \in ℕ$
142	141	nnred	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to 2^{j + 1} \in ℝ$
143		2z	$⊢ 2 \in ℤ$
144		uzid	$⊢ 2 \in ℤ \to 2 \in ℤ_{\geq 2}$
145	143 144	ax-mp	$⊢ 2 \in ℤ_{\geq 2}$
146		bernneq3	$⊢ (2 \in ℤ_{\geq 2} \land j + 1 \in ℕ_{0}) \to j + 1 < 2^{j + 1}$
147	145 138 146	sylancr	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to j + 1 < 2^{j + 1}$
148	139 142 147	ltled	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to j + 1 \leq 2^{j + 1}$
149	137	peano2zd	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to j + 1 \in ℤ$
150	141	nnzd	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to 2^{j + 1} \in ℤ$
151		eluz	$⊢ (j + 1 \in ℤ \land 2^{j + 1} \in ℤ) \to (2^{j + 1} \in ℤ_{\geq (j + 1)} \leftrightarrow j + 1 \leq 2^{j + 1})$
152	149 150 151	syl2anc	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to (2^{j + 1} \in ℤ_{\geq (j + 1)} \leftrightarrow j + 1 \leq 2^{j + 1})$
153	148 152	mpbird	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to 2^{j + 1} \in ℤ_{\geq (j + 1)}$
154		eluzp1m1	$⊢ (j \in ℤ \land 2^{j + 1} \in ℤ_{\geq (j + 1)}) \to 2^{j + 1} - 1 \in ℤ_{\geq j}$
155	137 153 154	syl2anc	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to 2^{j + 1} - 1 \in ℤ_{\geq j}$
156		eluznn	$⊢ (j \in ℕ \land 2^{j + 1} - 1 \in ℤ_{\geq j}) \to 2^{j + 1} - 1 \in ℕ$
157	136 155 156	syl2anc	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to 2^{j + 1} - 1 \in ℕ$
158	135 157	ffvelcdmd	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to seq 1 (+ F) (2^{j + 1} - 1) \in ℝ$
159	25	adantlr	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to j \in ℤ_{\geq 1}$
160		simpll	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to φ$
161		elfznn	$⊢ k \in (1 \dots 2^{j + 1} - 1) \to k \in ℕ$
162	160 161 1	syl2an	$⊢ (((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \land k \in (1 \dots 2^{j + 1} - 1)) \to F (k) \in ℝ$
163	114	adantl	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to j + 1 \in ℕ$
164		elfzuz	$⊢ k \in (j + 1 \dots 2^{j + 1} - 1) \to k \in ℤ_{\geq (j + 1)}$
165		eluznn	$⊢ (j + 1 \in ℕ \land k \in ℤ_{\geq (j + 1)}) \to k \in ℕ$
166	163 164 165	syl2an	$⊢ (((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \land k \in (j + 1 \dots 2^{j + 1} - 1)) \to k \in ℕ$
167	160 166 2	syl2an2r	$⊢ (((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \land k \in (j + 1 \dots 2^{j + 1} - 1)) \to 0 \leq F (k)$
168	159 155 162 167	sermono	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to seq 1 (+ F) (j) \leq seq 1 (+ F) (2^{j + 1} - 1)$
169	37	adantl	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to j \in ℕ_{0}$
170	1 2 3 4	climcndslem1	$⊢ (φ \land j \in ℕ_{0}) \to seq 1 (+ F) (2^{j + 1} - 1) \leq seq 0 (+ G) (j)$
171	160 169 170	syl2anc	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to seq 1 (+ F) (2^{j + 1} - 1) \leq seq 0 (+ G) (j)$
172	128 158 133 168 171	letrd	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to seq 1 (+ F) (j) \leq seq 0 (+ G) (j)$
173		eqidd	$⊢ (((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \land n \in (0 \dots j)) \to G (n) = G (n)$
174	169 102	eleqtrdi	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to j \in ℤ_{\geq 0}$
175		elfznn0	$⊢ n \in (0 \dots j) \to n \in ℕ_{0}$
176	160 175 105	syl2an	$⊢ (((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \land n \in (0 \dots j)) \to G (n) \in ℂ$
177	173 174 176	fsumser	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to \sum_{n = 0}^{j} G (n) = seq 0 (+ G) (j)$
178		0zd	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to 0 \in ℤ$
179		fzfid	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to (0 \dots j) \in Fin$
180	175	ssriv	$⊢ (0 \dots j) \subseteq ℕ_{0}$
181	180	a1i	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to (0 \dots j) \subseteq ℕ_{0}$
182		eqidd	$⊢ (((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \land n \in ℕ_{0}) \to G (n) = G (n)$
183	20	ad4ant14	$⊢ (((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \land n \in ℕ_{0}) \to G (n) \in ℝ$
184	49	ad4ant14	$⊢ (((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \land n \in ℕ_{0}) \to 0 \leq G (n)$
185		simplr	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to seq 0 (+ G) \in dom ⇝$
186	102 178 179 181 182 183 184 185	isumless	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to \sum_{n = 0}^{j} G (n) \leq \sum_{n \in ℕ_{0}} G (n)$
187	177 186	eqbrtrrd	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to seq 0 (+ G) (j) \leq \sum_{n \in ℕ_{0}} G (n)$
188	128 133 134 172 187	letrd	$⊢ ((φ \land seq 0 (+ G) \in dom ⇝) \land j \in ℕ) \to seq 1 (+ F) (j) \leq \sum_{n \in ℕ_{0}} G (n)$
189	188	ralrimiva	$⊢ (φ \land seq 0 (+ G) \in dom ⇝) \to \forall j \in ℕ seq 1 (+ F) (j) \leq \sum_{n \in ℕ_{0}} G (n)$
190		brralrspcev	$⊢ (\sum_{n \in ℕ_{0}} G (n) \in ℝ \land \forall j \in ℕ seq 1 (+ F) (j) \leq \sum_{n \in ℕ_{0}} G (n)) \to \exists x \in ℝ \forall j \in ℕ seq 1 (+ F) (j) \leq x$
191	127 189 190	syl2anc	$⊢ (φ \land seq 0 (+ G) \in dom ⇝) \to \exists x \in ℝ \forall j \in ℕ seq 1 (+ F) (j) \leq x$
192	5 109 110 122 191	climsup	$⊢ (φ \land seq 0 (+ G) \in dom ⇝) \to seq 1 (+ F) ⇝ sup (ran seq 1 (+ F) ℝ <)$
193	99	releldmi	$⊢ seq 1 (+ F) ⇝ sup (ran seq 1 (+ F) ℝ <) \to seq 1 (+ F) \in dom ⇝$
194	192 193	syl	$⊢ (φ \land seq 0 (+ G) \in dom ⇝) \to seq 1 (+ F) \in dom ⇝$
195	108 194	impbida	$⊢ φ \to (seq 1 (+ F) \in dom ⇝ \leftrightarrow seq 0 (+ G) \in dom ⇝)$

Metamath Proof Explorer

Theorem climcnds

Proof