Theorem cntrsetlem 14999

Description: Lemma for cntrset 15000.

Hypothesis

Ref	Expression
cntrsetlem.1	|- C = {x | E.f e. ({0, 2} ^m NN)x = sum_k e. NN ((f` k) / (3^k))}

Assertion

Ref	Expression
cntrsetlem	|- C C_ (0[,]1)

Distinct variable groups:   x,C   f,k,x

Proof of Theorem cntrsetlem

Step	Hyp	Ref	Expression
1		dfss2 2610	. 2 |- (C C_ (0[,]1) <-> A.x(x e. C -> x e. (0[,]1)))
2		abid 1873	. . . 4 |- (x e. {x | E.f e. ({0, 2} ^m NN)x = sum_k e. NN ((f` k) / (3^k))} <-> E.f e. ({0, 2} ^m NN)x = sum_k e. NN ((f` k) / (3^k)))
3		eleq1 1957	. . . . . . 7 |- (x = sum_k e. NN ((f` k) / (3^k)) -> (x e. RR* <-> sum_k e. NN ((f` k) / (3^k)) e. RR*))
4		breq2 3342	. . . . . . 7 |- (x = sum_k e. NN ((f` k) / (3^k)) -> (0 <_ x <-> 0 <_ sum_k e. NN ((f` k) / (3^k))))
5		breq1 3341	. . . . . . 7 |- (x = sum_k e. NN ((f` k) / (3^k)) -> (x <_ 1 <-> sum_k e. NN ((f` k) / (3^k)) <_ 1))
6	3, 4, 5	3anbi123d 1168	. . . . . 6 |- (x = sum_k e. NN ((f` k) / (3^k)) -> ((x e. RR* /\ 0 <_ x /\ x <_ 1) <-> (sum_k e. NN ((f` k) / (3^k)) e. RR* /\ 0 <_ sum_k e. NN ((f` k) / (3^k)) /\ sum_k e. NN ((f` k) / (3^k)) <_ 1)))
7		1z 7368	. . . . . . . . . 10 |- 1 e. ZZ
8	7	a1i 8	. . . . . . . . 9 |- (f e. ({0, 2} ^m NN) -> 1 e. ZZ)
9		simpr 350	. . . . . . . . . . . . 13 |- ((f e. ({0, 2} ^m NN) /\ k e. (ZZ>=` 1)) -> k e. (ZZ>=` 1))
10		prex 3526	. . . . . . . . . . . . . . . . . 18 |- {0, 2} e. _V
11		nnex 7116	. . . . . . . . . . . . . . . . . 18 |- NN e. _V
12	10, 11	elmap 5393	. . . . . . . . . . . . . . . . 17 |- (f e. ({0, 2} ^m NN) <-> f:NN-->{0, 2})
13		nnuz 7608	. . . . . . . . . . . . . . . . . . . . . 22 |- NN = (ZZ>=` 1)
14	13	eqcomi 1888	. . . . . . . . . . . . . . . . . . . . 21 |- (ZZ>=` 1) = NN
15	14	eleq2i 1961	. . . . . . . . . . . . . . . . . . . 20 |- (k e. (ZZ>=` 1) <-> k e. NN)
16		ffvelrn 4787	. . . . . . . . . . . . . . . . . . . . . 22 |- ((f:NN-->{0, 2} /\ k e. NN) -> (f` k) e. {0, 2})
17		fvex 4689	. . . . . . . . . . . . . . . . . . . . . . 23 |- (f` k) e. _V
18	17	elpr 3061	. . . . . . . . . . . . . . . . . . . . . 22 |- ((f` k) e. {0, 2} <-> ((f` k) = 0 \/ (f` k) = 2))
19	16, 18	sylib 215	. . . . . . . . . . . . . . . . . . . . 21 |- ((f:NN-->{0, 2} /\ k e. NN) -> ((f` k) = 0 \/ (f` k) = 2))
20	19	expcom 403	. . . . . . . . . . . . . . . . . . . 20 |- (k e. NN -> (f:NN-->{0, 2} -> ((f` k) = 0 \/ (f` k) = 2)))
21	15, 20	sylbi 216	. . . . . . . . . . . . . . . . . . 19 |- (k e. (ZZ>=` 1) -> (f:NN-->{0, 2} -> ((f` k) = 0 \/ (f` k) = 2)))
22	21	anc2ri 327	. . . . . . . . . . . . . . . . . 18 |- (k e. (ZZ>=` 1) -> (f:NN-->{0, 2} -> (((f` k) = 0 \/ (f` k) = 2) /\ k e. (ZZ>=` 1))))
23	22	com12 14	. . . . . . . . . . . . . . . . 17 |- (f:NN-->{0, 2} -> (k e. (ZZ>=` 1) -> (((f` k) = 0 \/ (f` k) = 2) /\ k e. (ZZ>=` 1))))
24	12, 23	sylbi 216	. . . . . . . . . . . . . . . 16 |- (f e. ({0, 2} ^m NN) -> (k e. (ZZ>=` 1) -> (((f` k) = 0 \/ (f` k) = 2) /\ k e. (ZZ>=` 1))))
25	24	imp 377	. . . . . . . . . . . . . . 15 |- ((f e. ({0, 2} ^m NN) /\ k e. (ZZ>=` 1)) -> (((f` k) = 0 \/ (f` k) = 2) /\ k e. (ZZ>=` 1)))
26		0re 6603	. . . . . . . . . . . . . . . . . 18 |- 0 e. RR
27		eleq1 1957	. . . . . . . . . . . . . . . . . 18 |- ((f` k) = 0 -> ((f` k) e. RR <-> 0 e. RR))
28	26, 27	mpbiri 211	. . . . . . . . . . . . . . . . 17 |- ((f` k) = 0 -> (f` k) e. RR)
29		2re 7163	. . . . . . . . . . . . . . . . . 18 |- 2 e. RR
30		eleq1 1957	. . . . . . . . . . . . . . . . . 18 |- ((f` k) = 2 -> ((f` k) e. RR <-> 2 e. RR))
31	29, 30	mpbiri 211	. . . . . . . . . . . . . . . . 17 |- ((f` k) = 2 -> (f` k) e. RR)
32	28, 31	jaoi 368	. . . . . . . . . . . . . . . 16 |- (((f` k) = 0 \/ (f` k) = 2) -> (f` k) e. RR)
33	32	adantr 425	. . . . . . . . . . . . . . 15 |- ((((f` k) = 0 \/ (f` k) = 2) /\ k e. (ZZ>=` 1)) -> (f` k) e. RR)
34	25, 33	syl 12	. . . . . . . . . . . . . 14 |- ((f e. ({0, 2} ^m NN) /\ k e. (ZZ>=` 1)) -> (f` k) e. RR)
35		reexpcl 7823	. . . . . . . . . . . . . . . 16 |- ((3 e. RR /\ k e. NN0) -> (3^k) e. RR)
36		3re 7165	. . . . . . . . . . . . . . . 16 |- 3 e. RR
37		elnnuz 7609	. . . . . . . . . . . . . . . . 17 |- (k e. NN <-> k e. (ZZ>=` 1))
38		nnnn0 7315	. . . . . . . . . . . . . . . . 17 |- (k e. NN -> k e. NN0)
39	37, 38	sylbir 218	. . . . . . . . . . . . . . . 16 |- (k e. (ZZ>=` 1) -> k e. NN0)
40	35, 36, 39	sylancr 526	. . . . . . . . . . . . . . 15 |- (k e. (ZZ>=` 1) -> (3^k) e. RR)
41	40	adantl 424	. . . . . . . . . . . . . 14 |- ((f e. ({0, 2} ^m NN) /\ k e. (ZZ>=` 1)) -> (3^k) e. RR)
42		3cn 14525	. . . . . . . . . . . . . . . . 17 |- 3 e. CC
43	42	a1i 8	. . . . . . . . . . . . . . . 16 |- (k e. (ZZ>=` 1) -> 3 e. CC)
44		3ne0 14524	. . . . . . . . . . . . . . . . 17 |- 3 =/= 0
45	44	a1i 8	. . . . . . . . . . . . . . . 16 |- (k e. (ZZ>=` 1) -> 3 =/= 0)
46		expne0i 7830	. . . . . . . . . . . . . . . 16 |- ((3 e. CC /\ 3 =/= 0 /\ k e. NN0) -> (3^k) =/= 0)
47	43, 45, 39, 46	syl111anc 1100	. . . . . . . . . . . . . . 15 |- (k e. (ZZ>=` 1) -> (3^k) =/= 0)
48	47	adantl 424	. . . . . . . . . . . . . 14 |- ((f e. ({0, 2} ^m NN) /\ k e. (ZZ>=` 1)) -> (3^k) =/= 0)
49		redivcl 6978	. . . . . . . . . . . . . 14 |- (((f` k) e. RR /\ (3^k) e. RR /\ (3^k) =/= 0) -> ((f` k) / (3^k)) e. RR)
50	34, 41, 48, 49	syl111anc 1100	. . . . . . . . . . . . 13 |- ((f e. ({0, 2} ^m NN) /\ k e. (ZZ>=` 1)) -> ((f` k) / (3^k)) e. RR)
51		fveq2 4681	. . . . . . . . . . . . . . 15 |- (x = k -> (f` x) = (f` k))
52		opreq2 4890	. . . . . . . . . . . . . . 15 |- (x = k -> (3^x) = (3^k))
53	51, 52	opreq12d 4900	. . . . . . . . . . . . . 14 |- (x = k -> ((f` x) / (3^x)) = ((f` k) / (3^k)))
54		eqid 1884	. . . . . . . . . . . . . 14 |- {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))} = {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}
55	53, 54	fvopab4g 4742	. . . . . . . . . . . . 13 |- ((k e. (ZZ>=` 1) /\ ((f` k) / (3^k)) e. RR) -> ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` k) = ((f` k) / (3^k)))
56	9, 50, 55	syl11anc 524	. . . . . . . . . . . 12 |- ((f e. ({0, 2} ^m NN) /\ k e. (ZZ>=` 1)) -> ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` k) = ((f` k) / (3^k)))
57	56, 50	eqeltrd 1971	. . . . . . . . . . 11 |- ((f e. ({0, 2} ^m NN) /\ k e. (ZZ>=` 1)) -> ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` k) e. RR)
58	57	ex 402	. . . . . . . . . 10 |- (f e. ({0, 2} ^m NN) -> (k e. (ZZ>=` 1) -> ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` k) e. RR))
59	58	r19.21aiv 2175	. . . . . . . . 9 |- (f e. ({0, 2} ^m NN) -> A.k e. (ZZ>=` 1)({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` k) e. RR)
60		oprex 4907	. . . . . . . . . . . 12 |- (1 / 2) e. _V
61	60	cvgcmp3ce 8451	. . . . . . . . . . 11 |- ((1 e. NN /\ ((({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}:NN-->RR /\ A.l e. NN 0 <_ ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}` l)) /\ ( + seq1 {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}) ~~> (1 / 2)) /\ ((2 e. RR /\ 0 <_ 2) /\ ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}:NN-->CC /\ A.l e. NN (1 < l -> (abs` ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` l)) <_ (2 x. ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}` l))))))) -> E.a( + seq1 {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}) ~~> a)
62		1nn 7117	. . . . . . . . . . 11 |- 1 e. NN
63		oprex 4907	. . . . . . . . . . . . . . . 16 |- ((1 / 3)^l) e. _V
64		elnnuz 7609	. . . . . . . . . . . . . . . . 17 |- (l e. NN <-> l e. (ZZ>=` 1))
65	36, 44	rereccli 6979	. . . . . . . . . . . . . . . . . . . . 21 |- (1 / 3) e. RR
66	65	a1i 8	. . . . . . . . . . . . . . . . . . . 20 |- ((l e. (ZZ>=` 1) /\ ((1 / 3)^l) e. _V) -> (1 / 3) e. RR)
67		nnnn0 7315	. . . . . . . . . . . . . . . . . . . . . 22 |- (l e. NN -> l e. NN0)
68	64, 67	sylbir 218	. . . . . . . . . . . . . . . . . . . . 21 |- (l e. (ZZ>=` 1) -> l e. NN0)
69	68	adantr 425	. . . . . . . . . . . . . . . . . . . 20 |- ((l e. (ZZ>=` 1) /\ ((1 / 3)^l) e. _V) -> l e. NN0)
70		1re 6598	. . . . . . . . . . . . . . . . . . . . . . 23 |- 1 e. RR
71		lt01 6871	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 0 < 1
72	26, 70, 71	ltleii 6756	. . . . . . . . . . . . . . . . . . . . . . 23 |- 0 <_ 1
73	70, 72	pm3.2i 307	. . . . . . . . . . . . . . . . . . . . . 22 |- (1 e. RR /\ 0 <_ 1)
74		3pos 7175	. . . . . . . . . . . . . . . . . . . . . . 23 |- 0 < 3
75	36, 74	pm3.2i 307	. . . . . . . . . . . . . . . . . . . . . 22 |- (3 e. RR /\ 0 < 3)
76		divge0 7038	. . . . . . . . . . . . . . . . . . . . . 22 |- (((1 e. RR /\ 0 <_ 1) /\ (3 e. RR /\ 0 < 3)) -> 0 <_ (1 / 3))
77	73, 75, 76	mp2an 761	. . . . . . . . . . . . . . . . . . . . 21 |- 0 <_ (1 / 3)
78	77	a1i 8	. . . . . . . . . . . . . . . . . . . 20 |- ((l e. (ZZ>=` 1) /\ ((1 / 3)^l) e. _V) -> 0 <_ (1 / 3))
79		expge0 7833	. . . . . . . . . . . . . . . . . . . 20 |- (((1 / 3) e. RR /\ l e. NN0 /\ 0 <_ (1 / 3)) -> 0 <_ ((1 / 3)^l))
80	66, 69, 78, 79	syl111anc 1100	. . . . . . . . . . . . . . . . . . 19 |- ((l e. (ZZ>=` 1) /\ ((1 / 3)^l) e. _V) -> 0 <_ ((1 / 3)^l))
81		opreq2 4890	. . . . . . . . . . . . . . . . . . . 20 |- (x = l -> ((1 / 3)^x) = ((1 / 3)^l))
82		eqid 1884	. . . . . . . . . . . . . . . . . . . 20 |- {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))} = {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}
83	81, 82	fvopab4g 4742	. . . . . . . . . . . . . . . . . . 19 |- ((l e. (ZZ>=` 1) /\ ((1 / 3)^l) e. _V) -> ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}` l) = ((1 / 3)^l))
84	80, 83	breqtrrd 3363	. . . . . . . . . . . . . . . . . 18 |- ((l e. (ZZ>=` 1) /\ ((1 / 3)^l) e. _V) -> 0 <_ ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}` l))
85	84	ex 402	. . . . . . . . . . . . . . . . 17 |- (l e. (ZZ>=` 1) -> (((1 / 3)^l) e. _V -> 0 <_ ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}` l)))
86	64, 85	sylbi 216	. . . . . . . . . . . . . . . 16 |- (l e. NN -> (((1 / 3)^l) e. _V -> 0 <_ ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}` l)))
87	63, 86	mpi 55	. . . . . . . . . . . . . . 15 |- (l e. NN -> 0 <_ ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}` l))
88	87	rgen 2159	. . . . . . . . . . . . . 14 |- A.l e. NN 0 <_ ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}` l)
89	88	a1i 8	. . . . . . . . . . . . 13 |- (f e. ({0, 2} ^m NN) -> A.l e. NN 0 <_ ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}` l))
90		reexpcl 7823	. . . . . . . . . . . . . . . . . 18 |- (((1 / 3) e. RR /\ l e. NN0) -> ((1 / 3)^l) e. RR)
91	90, 65, 68	sylancr 526	. . . . . . . . . . . . . . . . 17 |- (l e. (ZZ>=` 1) -> ((1 / 3)^l) e. RR)
92	91	rgen 2159	. . . . . . . . . . . . . . . 16 |- A.l e. (ZZ>=` 1)((1 / 3)^l) e. RR
93		eqid 1884	. . . . . . . . . . . . . . . . 17 |- {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))} = {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}
94	93	fopab2 4796	. . . . . . . . . . . . . . . 16 |- (A.l e. (ZZ>=` 1)((1 / 3)^l) e. RR <-> {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}:(ZZ>=` 1)-->RR)
95	92, 94	mpbi 206	. . . . . . . . . . . . . . 15 |- {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}:(ZZ>=` 1)-->RR
96	13	feq2i 4559	. . . . . . . . . . . . . . 15 |- ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}:NN-->RR <-> {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}:(ZZ>=` 1)-->RR)
97	95, 96	mpbir 207	. . . . . . . . . . . . . 14 |- {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}:NN-->RR
98		eleq1 1957	. . . . . . . . . . . . . . . . 17 |- (x = l -> (x e. (ZZ>=` 1) <-> l e. (ZZ>=` 1)))
99	81	eqeq2d 1895	. . . . . . . . . . . . . . . . 17 |- (x = l -> (y = ((1 / 3)^x) <-> y = ((1 / 3)^l)))
100	98, 99	anbi12d 690	. . . . . . . . . . . . . . . 16 |- (x = l -> ((x e. (ZZ>=` 1) /\ y = ((1 / 3)^x)) <-> (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))))
101	100	cbvopab1v 3407	. . . . . . . . . . . . . . 15 |- {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))} = {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}
102	101	feq1i 4558	. . . . . . . . . . . . . 14 |- ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}:NN-->RR <-> {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}:NN-->RR)
103	97, 102	mpbir 207	. . . . . . . . . . . . 13 |- {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}:NN-->RR
104	89, 103	jctil 316	. . . . . . . . . . . 12 |- (f e. ({0, 2} ^m NN) -> ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}:NN-->RR /\ A.l e. NN 0 <_ ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}` l)))
105		eqid 1884	. . . . . . . . . . . . . . 15 |- {<.l, y>. | (l e. NN /\ y = ((1 / 3)^l))} = {<.l, y>. | (l e. NN /\ y = ((1 / 3)^l))}
106	42, 44	reccli 6902	. . . . . . . . . . . . . . 15 |- (1 / 3) e. CC
107	65, 70	abslti 8127	. . . . . . . . . . . . . . . 16 |- ((abs` (1 / 3)) < 1 <-> (-u1 < (1 / 3) /\ (1 / 3) < 1))
108	70	renegcli 6576	. . . . . . . . . . . . . . . . . 18 |- -u1 e. RR
109	108, 26, 65	3pm3.2i 1048	. . . . . . . . . . . . . . . . 17 |- (-u1 e. RR /\ 0 e. RR /\ (1 / 3) e. RR)
110		lt0neg2 6858	. . . . . . . . . . . . . . . . . . . . 21 |- (1 e. RR -> (0 < 1 <-> -u1 < 0))
111	110	bicomd 580	. . . . . . . . . . . . . . . . . . . 20 |- (1 e. RR -> (-u1 < 0 <-> 0 < 1))
112	70, 111	ax-mp 7	. . . . . . . . . . . . . . . . . . 19 |- (-u1 < 0 <-> 0 < 1)
113	71, 112	mpbir 207	. . . . . . . . . . . . . . . . . 18 |- -u1 < 0
114	36, 74	recgt0ii 6992	. . . . . . . . . . . . . . . . . 18 |- 0 < (1 / 3)
115	113, 114	pm3.2i 307	. . . . . . . . . . . . . . . . 17 |- (-u1 < 0 /\ 0 < (1 / 3))
116		axlttrn 6673	. . . . . . . . . . . . . . . . 17 |- ((-u1 e. RR /\ 0 e. RR /\ (1 / 3) e. RR) -> ((-u1 < 0 /\ 0 < (1 / 3)) -> -u1 < (1 / 3)))
117	109, 115, 116	mp2 54	. . . . . . . . . . . . . . . 16 |- -u1 < (1 / 3)
118		1lt3 7214	. . . . . . . . . . . . . . . . 17 |- 1 < 3
119		recgt1 7082	. . . . . . . . . . . . . . . . . . 19 |- ((3 e. RR /\ 0 < 3) -> (1 < 3 <-> (1 / 3) < 1))
120	119	bicomd 580	. . . . . . . . . . . . . . . . . 18 |- ((3 e. RR /\ 0 < 3) -> ((1 / 3) < 1 <-> 1 < 3))
121	36, 74, 120	mp2an 761	. . . . . . . . . . . . . . . . 17 |- ((1 / 3) < 1 <-> 1 < 3)
122	118, 121	mpbir 207	. . . . . . . . . . . . . . . 16 |- (1 / 3) < 1
123	107, 117, 122	mpbir2an 800	. . . . . . . . . . . . . . 15 |- (abs` (1 / 3)) < 1
124	105, 106, 123	geolim1i 8500	. . . . . . . . . . . . . 14 |- ( + seq1 {<.l, y>. | (l e. NN /\ y = ((1 / 3)^l))}) ~~> ((1 / 3) / (1 - (1 / 3)))
125		id 73	. . . . . . . . . . . . . . . . . 18 |- (x = l -> x = l)
126	14	a1i 8	. . . . . . . . . . . . . . . . . 18 |- (x = l -> (ZZ>=` 1) = NN)
127	125, 126	eleq12d 1965	. . . . . . . . . . . . . . . . 17 |- (x = l -> (x e. (ZZ>=` 1) <-> l e. NN))
128	127, 99	anbi12d 690	. . . . . . . . . . . . . . . 16 |- (x = l -> ((x e. (ZZ>=` 1) /\ y = ((1 / 3)^x)) <-> (l e. NN /\ y = ((1 / 3)^l))))
129	128	cbvopab1v 3407	. . . . . . . . . . . . . . 15 |- {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))} = {<.l, y>. | (l e. NN /\ y = ((1 / 3)^l))}
130	129	opreq2i 4893	. . . . . . . . . . . . . 14 |- ( + seq1 {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}) = ( + seq1 {<.l, y>. | (l e. NN /\ y = ((1 / 3)^l))})
131		ax1cn 6422	. . . . . . . . . . . . . . . . 17 |- 1 e. CC
132		2cn 7164	. . . . . . . . . . . . . . . . 17 |- 2 e. CC
133		2ne0 7174	. . . . . . . . . . . . . . . . 17 |- 2 =/= 0
134	131, 42, 132, 42, 44, 44, 133	divdivdivi 6966	. . . . . . . . . . . . . . . 16 |- ((1 / 3) / (2 / 3)) = ((1 x. 3) / (3 x. 2))
135	131, 42	mulcomi 6476	. . . . . . . . . . . . . . . . 17 |- (1 x. 3) = (3 x. 1)
136	135	opreq1i 4892	. . . . . . . . . . . . . . . 16 |- ((1 x. 3) / (3 x. 2)) = ((3 x. 1) / (3 x. 2))
137	132, 133	pm3.2i 307	. . . . . . . . . . . . . . . . 17 |- (2 e. CC /\ 2 =/= 0)
138	42, 44	pm3.2i 307	. . . . . . . . . . . . . . . . 17 |- (3 e. CC /\ 3 =/= 0)
139		divcan5 6957	. . . . . . . . . . . . . . . . 17 |- ((1 e. CC /\ (2 e. CC /\ 2 =/= 0) /\ (3 e. CC /\ 3 =/= 0)) -> ((3 x. 1) / (3 x. 2)) = (1 / 2))
140	131, 137, 138, 139	mp3an 1191	. . . . . . . . . . . . . . . 16 |- ((3 x. 1) / (3 x. 2)) = (1 / 2)
141	134, 136, 140	3eqtrri 1913	. . . . . . . . . . . . . . 15 |- (1 / 2) = ((1 / 3) / (2 / 3))
142		2eq3m1 14526	. . . . . . . . . . . . . . . . . 18 |- 2 = (3 - 1)
143	142	opreq1i 4892	. . . . . . . . . . . . . . . . 17 |- (2 / 3) = ((3 - 1) / 3)
144		divsubdir 6951	. . . . . . . . . . . . . . . . . 18 |- ((3 e. CC /\ 1 e. CC /\ (3 e. CC /\ 3 =/= 0)) -> ((3 - 1) / 3) = ((3 / 3) - (1 / 3)))
145	42, 131, 138, 144	mp3an 1191	. . . . . . . . . . . . . . . . 17 |- ((3 - 1) / 3) = ((3 / 3) - (1 / 3))
146	42, 44	dividi 6946	. . . . . . . . . . . . . . . . . 18 |- (3 / 3) = 1
147	146	opreq1i 4892	. . . . . . . . . . . . . . . . 17 |- ((3 / 3) - (1 / 3)) = (1 - (1 / 3))
148	143, 145, 147	3eqtri 1912	. . . . . . . . . . . . . . . 16 |- (2 / 3) = (1 - (1 / 3))
149	148	opreq2i 4893	. . . . . . . . . . . . . . 15 |- ((1 / 3) / (2 / 3)) = ((1 / 3) / (1 - (1 / 3)))
150	141, 149	eqtri 1908	. . . . . . . . . . . . . 14 |- (1 / 2) = ((1 / 3) / (1 - (1 / 3)))
151	124, 130, 150	3brtr4i 3365	. . . . . . . . . . . . 13 |- ( + seq1 {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}) ~~> (1 / 2)
152	151	a1i 8	. . . . . . . . . . . 12 |- (f e. ({0, 2} ^m NN) -> ( + seq1 {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}) ~~> (1 / 2))
153		2nn 7183	. . . . . . . . . . . . . . . 16 |- 2 e. NN
154		nnrp 7238	. . . . . . . . . . . . . . . . 17 |- (2 e. NN -> 2 e. RR+)
155		rpge0 7241	. . . . . . . . . . . . . . . . 17 |- (2 e. RR+ -> 0 <_ 2)
156	154, 155	syl 12	. . . . . . . . . . . . . . . 16 |- (2 e. NN -> 0 <_ 2)
157	153, 156	ax-mp 7	. . . . . . . . . . . . . . 15 |- 0 <_ 2
158	29, 157	pm3.2i 307	. . . . . . . . . . . . . 14 |- (2 e. RR /\ 0 <_ 2)
159	158	a1i 8	. . . . . . . . . . . . 13 |- (f e. ({0, 2} ^m NN) -> (2 e. RR /\ 0 <_ 2))
160		ffvelrn 4787	. . . . . . . . . . . . . . . . . . 19 |- ((f:NN-->{0, 2} /\ l e. NN) -> (f` l) e. {0, 2})
161		simpr 350	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((l e. NN /\ (f` l) e. CC) -> (f` l) e. CC)
162		expcl 7824	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((3 e. CC /\ l e. NN0) -> (3^l) e. CC)
163	162, 42, 67	sylancr 526	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (l e. NN -> (3^l) e. CC)
164	163	adantr 425	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((l e. NN /\ (f` l) e. CC) -> (3^l) e. CC)
165		df-ne 2019	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (3 =/= 0 <-> -. 3 = 0)
166	44, 165	mpbi 206	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- -. 3 = 0
167		expeq0 7828	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((3 e. CC /\ l e. NN) -> ((3^l) = 0 <-> 3 = 0))
168	42, 167	mpan 759	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (l e. NN -> ((3^l) = 0 <-> 3 = 0))
169	168	necon3abid 2033	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (l e. NN -> ((3^l) =/= 0 <-> -. 3 = 0))
170	166, 169	mpbiri 211	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (l e. NN -> (3^l) =/= 0)
171	170	adantr 425	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((l e. NN /\ (f` l) e. CC) -> (3^l) =/= 0)
172		divcl 6901	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((f` l) e. CC /\ (3^l) e. CC /\ (3^l) =/= 0) -> ((f` l) / (3^l)) e. CC)
173	161, 164, 171, 172	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . 22 |- ((l e. NN /\ (f` l) e. CC) -> ((f` l) / (3^l)) e. CC)
174	173	ex 402	. . . . . . . . . . . . . . . . . . . . 21 |- (l e. NN -> ((f` l) e. CC -> ((f` l) / (3^l)) e. CC))
175	174	adantl 424	. . . . . . . . . . . . . . . . . . . 20 |- ((f:NN-->{0, 2} /\ l e. NN) -> ((f` l) e. CC -> ((f` l) / (3^l)) e. CC))
176		fvex 4689	. . . . . . . . . . . . . . . . . . . . . 22 |- (f` l) e. _V
177	176	elpr 3061	. . . . . . . . . . . . . . . . . . . . 21 |- ((f` l) e. {0, 2} <-> ((f` l) = 0 \/ (f` l) = 2))
178		0cn 6481	. . . . . . . . . . . . . . . . . . . . . . 23 |- 0 e. CC
179		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((f` l) = 0 -> ((f` l) e. CC <-> 0 e. CC))
180	178, 179	mpbiri 211	. . . . . . . . . . . . . . . . . . . . . 22 |- ((f` l) = 0 -> (f` l) e. CC)
181		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((f` l) = 2 -> ((f` l) e. CC <-> 2 e. CC))
182	132, 181	mpbiri 211	. . . . . . . . . . . . . . . . . . . . . 22 |- ((f` l) = 2 -> (f` l) e. CC)
183	180, 182	jaoi 368	. . . . . . . . . . . . . . . . . . . . 21 |- (((f` l) = 0 \/ (f` l) = 2) -> (f` l) e. CC)
184	177, 183	sylbi 216	. . . . . . . . . . . . . . . . . . . 20 |- ((f` l) e. {0, 2} -> (f` l) e. CC)
185	175, 184	syl5com 63	. . . . . . . . . . . . . . . . . . 19 |- ((f` l) e. {0, 2} -> ((f:NN-->{0, 2} /\ l e. NN) -> ((f` l) / (3^l)) e. CC))
186	160, 185	mpcom 60	. . . . . . . . . . . . . . . . . 18 |- ((f:NN-->{0, 2} /\ l e. NN) -> ((f` l) / (3^l)) e. CC)
187	186	ex 402	. . . . . . . . . . . . . . . . 17 |- (f:NN-->{0, 2} -> (l e. NN -> ((f` l) / (3^l)) e. CC))
188	12, 187	sylbi 216	. . . . . . . . . . . . . . . 16 |- (f e. ({0, 2} ^m NN) -> (l e. NN -> ((f` l) / (3^l)) e. CC))
189	188	r19.21aiv 2175	. . . . . . . . . . . . . . 15 |- (f e. ({0, 2} ^m NN) -> A.l e. NN ((f` l) / (3^l)) e. CC)
190		fveq2 4681	. . . . . . . . . . . . . . . . . 18 |- (x = l -> (f` x) = (f` l))
191		opreq2 4890	. . . . . . . . . . . . . . . . . 18 |- (x = l -> (3^x) = (3^l))
192	190, 191	opreq12d 4900	. . . . . . . . . . . . . . . . 17 |- (x = l -> ((f` x) / (3^x)) = ((f` l) / (3^l)))
193	192	eleq1d 1963	. . . . . . . . . . . . . . . 16 |- (x = l -> (((f` x) / (3^x)) e. CC <-> ((f` l) / (3^l)) e. CC))
194	193	cbvralv 2280	. . . . . . . . . . . . . . 15 |- (A.x e. NN ((f` x) / (3^x)) e. CC <-> A.l e. NN ((f` l) / (3^l)) e. CC)
195	189, 194	sylibr 217	. . . . . . . . . . . . . 14 |- (f e. ({0, 2} ^m NN) -> A.x e. NN ((f` x) / (3^x)) e. CC)
196	14	eleq2i 1961	. . . . . . . . . . . . . . . . 17 |- (x e. (ZZ>=` 1) <-> x e. NN)
197	196	anbi1i 539	. . . . . . . . . . . . . . . 16 |- ((x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x))) <-> (x e. NN /\ y = ((f` x) / (3^x))))
198	197	opabbii 3402	. . . . . . . . . . . . . . 15 |- {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))} = {<.x, y>. | (x e. NN /\ y = ((f` x) / (3^x)))}
199	198	fopab2 4796	. . . . . . . . . . . . . 14 |- (A.x e. NN ((f` x) / (3^x)) e. CC <-> {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}:NN-->CC)
200	195, 199	sylib 215	. . . . . . . . . . . . 13 |- (f e. ({0, 2} ^m NN) -> {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}:NN-->CC)
201		ffvelrn 4787	. . . . . . . . . . . . . . . . . . . . 21 |- ((f:NN-->{0, 2} /\ x e. NN) -> (f` x) e. {0, 2})
202		fvex 4689	. . . . . . . . . . . . . . . . . . . . . 22 |- (f` x) e. _V
203	202	elpr 3061	. . . . . . . . . . . . . . . . . . . . 21 |- ((f` x) e. {0, 2} <-> ((f` x) = 0 \/ (f` x) = 2))
204	201, 203	sylib 215	. . . . . . . . . . . . . . . . . . . 20 |- ((f:NN-->{0, 2} /\ x e. NN) -> ((f` x) = 0 \/ (f` x) = 2))
205		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((f` x) = 0 -> ((f` x) e. RR <-> 0 e. RR))
206	26, 205	mpbiri 211	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((f` x) = 0 -> (f` x) e. RR)
207		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((f` x) = 2 -> ((f` x) e. RR <-> 2 e. RR))
208	29, 207	mpbiri 211	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((f` x) = 2 -> (f` x) e. RR)
209	206, 208	jaoi 368	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((f` x) = 0 \/ (f` x) = 2) -> (f` x) e. RR)
210	204, 209	syl 12	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((f:NN-->{0, 2} /\ x e. NN) -> (f` x) e. RR)
211	29	a1i 8	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((f:NN-->{0, 2} /\ x e. NN) -> 2 e. RR)
212		reexpcl 7823	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((3 e. RR /\ x e. NN0) -> (3^x) e. RR)
213		nnnn0 7315	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x e. NN -> x e. NN0)
214	212, 36, 213	sylancr 526	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x e. NN -> (3^x) e. RR)
215		3nn 7184	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- 3 e. NN
216	213, 215	jctil 316	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x e. NN -> (3 e. NN /\ x e. NN0))
217		nnexpcl 7819	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((3 e. NN /\ x e. NN0) -> (3^x) e. NN)
218		nngt0 7129	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((3^x) e. NN -> 0 < (3^x))
219	216, 217, 218	3syl 24	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x e. NN -> 0 < (3^x))
220	214, 219	jca 310	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x e. NN -> ((3^x) e. RR /\ 0 < (3^x)))
221	220	adantl 424	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((f:NN-->{0, 2} /\ x e. NN) -> ((3^x) e. RR /\ 0 < (3^x)))
222		lediv1 7033	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((f` x) e. RR /\ 2 e. RR /\ ((3^x) e. RR /\ 0 < (3^x))) -> ((f` x) <_ 2 <-> ((f` x) / (3^x)) <_ (2 / (3^x))))
223	222	biimpd 170	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((f` x) e. RR /\ 2 e. RR /\ ((3^x) e. RR /\ 0 < (3^x))) -> ((f` x) <_ 2 -> ((f` x) / (3^x)) <_ (2 / (3^x))))
224	210, 211, 221, 223	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . 22 |- ((f:NN-->{0, 2} /\ x e. NN) -> ((f` x) <_ 2 -> ((f` x) / (3^x)) <_ (2 / (3^x))))
225	26	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((3 e. RR /\ x e. NN0) -> 0 e. RR)
226		recn 6466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (3 e. RR -> 3 e. CC)
227	226	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((3 e. RR /\ x e. NN0) -> 3 e. CC)
228	44	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((3 e. RR /\ x e. NN0) -> 3 =/= 0)
229		simpr 350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((3 e. RR /\ x e. NN0) -> x e. NN0)
230		expne0i 7830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((3 e. CC /\ 3 =/= 0 /\ x e. NN0) -> (3^x) =/= 0)
231	227, 228, 229, 230	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((3 e. RR /\ x e. NN0) -> (3^x) =/= 0)
232	225, 212, 231	3jca 1050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((3 e. RR /\ x e. NN0) -> (0 e. RR /\ (3^x) e. RR /\ (3^x) =/= 0))
233	232, 36, 213	sylancr 526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (x e. NN -> (0 e. RR /\ (3^x) e. RR /\ (3^x) =/= 0))
234	233	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((f` x) = 0 /\ x e. NN) -> (0 e. RR /\ (3^x) e. RR /\ (3^x) =/= 0))
235		redivcl 6978	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((0 e. RR /\ (3^x) e. RR /\ (3^x) =/= 0) -> (0 / (3^x)) e. RR)
236	234, 235	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((f` x) = 0 /\ x e. NN) -> (0 / (3^x)) e. RR)
237		opreq1 4889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((f` x) = 0 -> ((f` x) / (3^x)) = (0 / (3^x)))
238	237	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((f` x) = 0 -> (((f` x) / (3^x)) e. RR <-> (0 / (3^x)) e. RR))
239	238	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((f` x) = 0 /\ x e. NN) -> (((f` x) / (3^x)) e. RR <-> (0 / (3^x)) e. RR))
240	236, 239	mpbird 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((f` x) = 0 /\ x e. NN) -> ((f` x) / (3^x)) e. RR)
241	240	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((f` x) = 0 -> (x e. NN -> ((f` x) / (3^x)) e. RR))
242		opreq1 4889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((f` x) = 2 -> ((f` x) / (3^x)) = (2 / (3^x)))
243	242	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((f` x) = 2 -> (((f` x) / (3^x)) e. RR <-> (2 / (3^x)) e. RR))
244	29	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (x e. NN -> 2 e. RR)
245	42	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (x e. NN -> 3 e. CC)
246	44	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (x e. NN -> 3 =/= 0)
247	245, 246, 213, 230	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (x e. NN -> (3^x) =/= 0)
248		redivcl 6978	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((2 e. RR /\ (3^x) e. RR /\ (3^x) =/= 0) -> (2 / (3^x)) e. RR)
249	244, 214, 247, 248	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (x e. NN -> (2 / (3^x)) e. RR)
250	243, 249	syl5bir 227	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((f` x) = 2 -> (x e. NN -> ((f` x) / (3^x)) e. RR))
251	241, 250	jaoi 368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((f` x) = 0 \/ (f` x) = 2) -> (x e. NN -> ((f` x) / (3^x)) e. RR))
252	251	impcom 378	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((x e. NN /\ ((f` x) = 0 \/ (f` x) = 2)) -> ((f` x) / (3^x)) e. RR)
253	237	breq2d 3350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((f` x) = 0 -> (0 <_ ((f` x) / (3^x)) <-> 0 <_ (0 / (3^x))))
254	26	leidi 6790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- 0 <_ 0
255	26	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (x e. NN -> 0 e. RR)
256		ge0div 7036	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((0 e. RR /\ (3^x) e. RR /\ 0 < (3^x)) -> (0 <_ 0 <-> 0 <_ (0 / (3^x))))
257	255, 214, 219, 256	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (x e. NN -> (0 <_ 0 <-> 0 <_ (0 / (3^x))))
258	254, 257	mpbii 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (x e. NN -> 0 <_ (0 / (3^x)))
259	253, 258	syl5bir 227	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((f` x) = 0 -> (x e. NN -> 0 <_ ((f` x) / (3^x))))
260		ge0div 7036	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((2 e. RR /\ (3^x) e. RR /\ 0 < (3^x)) -> (0 <_ 2 <-> 0 <_ (2 / (3^x))))
261	157, 260	mpbii 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((2 e. RR /\ (3^x) e. RR /\ 0 < (3^x)) -> 0 <_ (2 / (3^x)))
262	244, 214, 219, 261	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (x e. NN -> 0 <_ (2 / (3^x)))
263	262	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((f` x) = 2 /\ x e. NN) -> 0 <_ (2 / (3^x)))
264		simpl 346	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((f` x) = 2 /\ x e. NN) -> (f` x) = 2)
265	264	opreq1d 4897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((f` x) = 2 /\ x e. NN) -> ((f` x) / (3^x)) = (2 / (3^x)))
266	263, 265	breqtrrd 3363	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((f` x) = 2 /\ x e. NN) -> 0 <_ ((f` x) / (3^x)))
267	266	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((f` x) = 2 -> (x e. NN -> 0 <_ ((f` x) / (3^x))))
268	259, 267	jaoi 368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((f` x) = 0 \/ (f` x) = 2) -> (x e. NN -> 0 <_ ((f` x) / (3^x))))
269	268	impcom 378	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((x e. NN /\ ((f` x) = 0 \/ (f` x) = 2)) -> 0 <_ ((f` x) / (3^x)))
270	252, 269	jca 310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((x e. NN /\ ((f` x) = 0 \/ (f` x) = 2)) -> (((f` x) / (3^x)) e. RR /\ 0 <_ ((f` x) / (3^x))))
271	270	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (x e. NN -> (((f` x) = 0 \/ (f` x) = 2) -> (((f` x) / (3^x)) e. RR /\ 0 <_ ((f` x) / (3^x)))))
272	271	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((f:NN-->{0, 2} /\ x e. NN) -> (((f` x) = 0 \/ (f` x) = 2) -> (((f` x) / (3^x)) e. RR /\ 0 <_ ((f` x) / (3^x)))))
273	204, 272	mpd 29	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((f:NN-->{0, 2} /\ x e. NN) -> (((f` x) / (3^x)) e. RR /\ 0 <_ ((f` x) / (3^x))))
274		absid 8113	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((f` x) / (3^x)) e. RR /\ 0 <_ ((f` x) / (3^x))) -> (abs` ((f` x) / (3^x))) = ((f` x) / (3^x)))
275	273, 274	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((f:NN-->{0, 2} /\ x e. NN) -> (abs` ((f` x) / (3^x))) = ((f` x) / (3^x)))
276	275	eqcomd 1889	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((f:NN-->{0, 2} /\ x e. NN) -> ((f` x) / (3^x)) = (abs` ((f` x) / (3^x))))
277	276	breq1d 3348	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((f:NN-->{0, 2} /\ x e. NN) -> (((f` x) / (3^x)) <_ (2 / (3^x)) <-> (abs` ((f` x) / (3^x))) <_ (2 / (3^x))))
278	277	biimpd 170	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((f:NN-->{0, 2} /\ x e. NN) -> (((f` x) / (3^x)) <_ (2 / (3^x)) -> (abs` ((f` x) / (3^x))) <_ (2 / (3^x))))
279	132	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x e. NN -> 2 e. CC)
280		expcl 7824	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((3 e. CC /\ x e. NN0) -> (3^x) e. CC)
281	280, 42, 213	sylancr 526	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x e. NN -> (3^x) e. CC)
282		divrec 6922	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((2 e. CC /\ (3^x) e. CC /\ (3^x) =/= 0) -> (2 / (3^x)) = (2 x. (1 / (3^x))))
283	279, 281, 247, 282	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x e. NN -> (2 / (3^x)) = (2 x. (1 / (3^x))))
284		exprec 7837	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((3 e. CC /\ 3 =/= 0 /\ x e. NN0) -> ((1 / 3)^x) = (1 / (3^x)))
285	245, 246, 213, 284	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x e. NN -> ((1 / 3)^x) = (1 / (3^x)))
286	285	eqcomd 1889	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x e. NN -> (1 / (3^x)) = ((1 / 3)^x))
287	286	opreq2d 4898	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x e. NN -> (2 x. (1 / (3^x))) = (2 x. ((1 / 3)^x)))
288	283, 287	eqtrd 1925	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x e. NN -> (2 / (3^x)) = (2 x. ((1 / 3)^x)))
289	288	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((f:NN-->{0, 2} /\ x e. NN) -> (2 / (3^x)) = (2 x. ((1 / 3)^x)))
290	289	breq2d 3350	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((f:NN-->{0, 2} /\ x e. NN) -> ((abs` ((f` x) / (3^x))) <_ (2 / (3^x)) <-> (abs` ((f` x) / (3^x))) <_ (2 x. ((1 / 3)^x))))
291	278, 290	sylibd 219	. . . . . . . . . . . . . . . . . . . . . 22 |- ((f:NN-->{0, 2} /\ x e. NN) -> (((f` x) / (3^x)) <_ (2 / (3^x)) -> (abs` ((f` x) / (3^x))) <_ (2 x. ((1 / 3)^x))))
292	224, 291	syld 30	. . . . . . . . . . . . . . . . . . . . 21 |- ((f:NN-->{0, 2} /\ x e. NN) -> ((f` x) <_ 2 -> (abs` ((f` x) / (3^x))) <_ (2 x. ((1 / 3)^x))))
293		breq1 3341	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((f` x) = 0 -> ((f` x) <_ 2 <-> 0 <_ 2))
294	157, 293	mpbiri 211	. . . . . . . . . . . . . . . . . . . . . 22 |- ((f` x) = 0 -> (f` x) <_ 2)
295	29	leidi 6790	. . . . . . . . . . . . . . . . . . . . . . 23 |- 2 <_ 2
296		breq1 3341	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((f` x) = 2 -> ((f` x) <_ 2 <-> 2 <_ 2))
297	295, 296	mpbiri 211	. . . . . . . . . . . . . . . . . . . . . 22 |- ((f` x) = 2 -> (f` x) <_ 2)
298	294, 297	jaoi 368	. . . . . . . . . . . . . . . . . . . . 21 |- (((f` x) = 0 \/ (f` x) = 2) -> (f` x) <_ 2)
299	292, 298	syl5com 63	. . . . . . . . . . . . . . . . . . . 20 |- (((f` x) = 0 \/ (f` x) = 2) -> ((f:NN-->{0, 2} /\ x e. NN) -> (abs` ((f` x) / (3^x))) <_ (2 x. ((1 / 3)^x))))
300	204, 299	mpcom 60	. . . . . . . . . . . . . . . . . . 19 |- ((f:NN-->{0, 2} /\ x e. NN) -> (abs` ((f` x) / (3^x))) <_ (2 x. ((1 / 3)^x)))
301	300, 12	sylanb 498	. . . . . . . . . . . . . . . . . 18 |- ((f e. ({0, 2} ^m NN) /\ x e. NN) -> (abs` ((f` x) / (3^x))) <_ (2 x. ((1 / 3)^x)))
302		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . 22 |- (l = x -> (f` l) = (f` x))
303		opreq2 4890	. . . . . . . . . . . . . . . . . . . . . 22 |- (l = x -> (3^l) = (3^x))
304	302, 303	opreq12d 4900	. . . . . . . . . . . . . . . . . . . . 21 |- (l = x -> ((f` l) / (3^l)) = ((f` x) / (3^x)))
305		eqid 1884	. . . . . . . . . . . . . . . . . . . . 21 |- {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))} = {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}
306	304, 305	fvopab4g 4742	. . . . . . . . . . . . . . . . . . . 20 |- ((x e. (ZZ>=` 1) /\ ((f` x) / (3^x)) e. _V) -> ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` x) = ((f` x) / (3^x)))
307		elnnuz 7609	. . . . . . . . . . . . . . . . . . . . . 22 |- (x e. NN <-> x e. (ZZ>=` 1))
308	307	biimpi 168	. . . . . . . . . . . . . . . . . . . . 21 |- (x e. NN -> x e. (ZZ>=` 1))
309	308	adantl 424	. . . . . . . . . . . . . . . . . . . 20 |- ((f e. ({0, 2} ^m NN) /\ x e. NN) -> x e. (ZZ>=` 1))
310		oprex 4907	. . . . . . . . . . . . . . . . . . . 20 |- ((f` x) / (3^x)) e. _V
311	306, 309, 310	sylancl 525	. . . . . . . . . . . . . . . . . . 19 |- ((f e. ({0, 2} ^m NN) /\ x e. NN) -> ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` x) = ((f` x) / (3^x)))
312	311	fveq2d 4685	. . . . . . . . . . . . . . . . . 18 |- ((f e. ({0, 2} ^m NN) /\ x e. NN) -> (abs` ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` x)) = (abs` ((f` x) / (3^x))))
313		oprex 4907	. . . . . . . . . . . . . . . . . . . . . 22 |- ((1 / 3)^x) e. _V
314		opreq2 4890	. . . . . . . . . . . . . . . . . . . . . . 23 |- (l = x -> ((1 / 3)^l) = ((1 / 3)^x))
315	314, 93	fvopab4g 4742	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x e. (ZZ>=` 1) /\ ((1 / 3)^x) e. _V) -> ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x) = ((1 / 3)^x))
316	313, 315	mpan2 760	. . . . . . . . . . . . . . . . . . . . 21 |- (x e. (ZZ>=` 1) -> ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x) = ((1 / 3)^x))
317	196, 316	sylbir 218	. . . . . . . . . . . . . . . . . . . 20 |- (x e. NN -> ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x) = ((1 / 3)^x))
318	317	adantl 424	. . . . . . . . . . . . . . . . . . 19 |- ((f e. ({0, 2} ^m NN) /\ x e. NN) -> ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x) = ((1 / 3)^x))
319	318	opreq2d 4898	. . . . . . . . . . . . . . . . . 18 |- ((f e. ({0, 2} ^m NN) /\ x e. NN) -> (2 x. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x)) = (2 x. ((1 / 3)^x)))
320	301, 312, 319	3brtr4d 3367	. . . . . . . . . . . . . . . . 17 |- ((f e. ({0, 2} ^m NN) /\ x e. NN) -> (abs` ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` x)) <_ (2 x. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x)))
321	320	ex 402	. . . . . . . . . . . . . . . 16 |- (f e. ({0, 2} ^m NN) -> (x e. NN -> (abs` ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` x)) <_ (2 x. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x))))
322	321	a1dd 53	. . . . . . . . . . . . . . 15 |- (f e. ({0, 2} ^m NN) -> (x e. NN -> (1 < x -> (abs` ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` x)) <_ (2 x. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x)))))
323	322	r19.21aiv 2175	. . . . . . . . . . . . . 14 |- (f e. ({0, 2} ^m NN) -> A.x e. NN (1 < x -> (abs` ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` x)) <_ (2 x. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x))))
324		ax-17 1317	. . . . . . . . . . . . . . . 16 |- (1 < l -> A.x1 < l)
325		ax-17 1317	. . . . . . . . . . . . . . . . . 18 |- (u e. abs -> A.x u e. abs)
326		hbopab1 3562	. . . . . . . . . . . . . . . . . . 19 |- (u e. {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))} -> A.x u e. {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))})
327		ax-17 1317	. . . . . . . . . . . . . . . . . . 19 |- (u e. l -> A.x u e. l)
328	326, 327	hbfv 4686	. . . . . . . . . . . . . . . . . 18 |- (u e. ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` l) -> A.x u e. ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` l))
329	325, 328	hbfv 4686	. . . . . . . . . . . . . . . . 17 |- (u e. (abs` ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` l)) -> A.x u e. (abs` ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` l)))
330		ax-17 1317	. . . . . . . . . . . . . . . . 17 |- (u e. <_ -> A.x u e. <_ )
331		ax-17 1317	. . . . . . . . . . . . . . . . . 18 |- (u e. 2 -> A.x u e. 2)
332		ax-17 1317	. . . . . . . . . . . . . . . . . 18 |- (u e. x. -> A.x u e. x. )
333		hbopab1 3562	. . . . . . . . . . . . . . . . . . 19 |- (u e. {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))} -> A.x u e. {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))})
334	333, 327	hbfv 4686	. . . . . . . . . . . . . . . . . 18 |- (u e. ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}` l) -> A.x u e. ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}` l))
335	331, 332, 334	hbopr 4904	. . . . . . . . . . . . . . . . 17 |- (u e. (2 x. ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}` l)) -> A.x u e. (2 x. ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}` l)))
336	329, 330, 335	hbbr 3381	. . . . . . . . . . . . . . . 16 |- ((abs` ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` l)) <_ (2 x. ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}` l)) -> A.x(abs` ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` l)) <_ (2 x. ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}` l)))
337	324, 336	hbim 1354	. . . . . . . . . . . . . . 15 |- ((1 < l -> (abs` ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` l)) <_ (2 x. ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}` l))) -> A.x(1 < l -> (abs` ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` l)) <_ (2 x. ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}` l))))
338		ax-17 1317	. . . . . . . . . . . . . . . 16 |- (1 < x -> A.l1 < x)
339		ax-17 1317	. . . . . . . . . . . . . . . . . 18 |- (u e. abs -> A.l u e. abs)
340		hbopab1 3562	. . . . . . . . . . . . . . . . . . 19 |- (u e. {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))} -> A.l u e. {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))})
341		ax-17 1317	. . . . . . . . . . . . . . . . . . 19 |- (u e. x -> A.l u e. x)
342	340, 341	hbfv 4686	. . . . . . . . . . . . . . . . . 18 |- (u e. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` x) -> A.l u e. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` x))
343	339, 342	hbfv 4686	. . . . . . . . . . . . . . . . 17 |- (u e. (abs` ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` x)) -> A.l u e. (abs` ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` x)))
344		ax-17 1317	. . . . . . . . . . . . . . . . 17 |- (u e. <_ -> A.l u e. <_ )
345		ax-17 1317	. . . . . . . . . . . . . . . . . 18 |- (u e. 2 -> A.l u e. 2)
346		ax-17 1317	. . . . . . . . . . . . . . . . . 18 |- (u e. x. -> A.l u e. x. )
347		hbopab1 3562	. . . . . . . . . . . . . . . . . . 19 |- (u e. {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))} -> A.l u e. {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))})
348	347, 341	hbfv 4686	. . . . . . . . . . . . . . . . . 18 |- (u e. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x) -> A.l u e. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x))
349	345, 346, 348	hbopr 4904	. . . . . . . . . . . . . . . . 17 |- (u e. (2 x. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x)) -> A.l u e. (2 x. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x)))
350	343, 344, 349	hbbr 3381	. . . . . . . . . . . . . . . 16 |- ((abs` ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` x)) <_ (2 x. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x)) -> A.l(abs` ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` x)) <_ (2 x. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x)))
351	338, 350	hbim 1354	. . . . . . . . . . . . . . 15 |- ((1 < x -> (abs` ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` x)) <_ (2 x. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x))) -> A.l(1 < x -> (abs` ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` x)) <_ (2 x. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x))))
352		breq2 3342	. . . . . . . . . . . . . . . 16 |- (l = x -> (1 < l <-> 1 < x))
353	192	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = l -> (y = ((f` x) / (3^x)) <-> y = ((f` l) / (3^l))))
354	98, 353	anbi12d 690	. . . . . . . . . . . . . . . . . . . . 21 |- (x = l -> ((x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x))) <-> (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))))
355	354	cbvopab1v 3407	. . . . . . . . . . . . . . . . . . . 20 |- {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))} = {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}
356	355	a1i 8	. . . . . . . . . . . . . . . . . . 19 |- (l = x -> {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))} = {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))})
357		id 73	. . . . . . . . . . . . . . . . . . 19 |- (l = x -> l = x)
358	356, 357	fveq12d 10152	. . . . . . . . . . . . . . . . . 18 |- (l = x -> ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` l) = ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` x))
359	358	fveq2d 4685	. . . . . . . . . . . . . . . . 17 |- (l = x -> (abs` ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` l)) = (abs` ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` x)))
360	101	a1i 8	. . . . . . . . . . . . . . . . . . 19 |- (l = x -> {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))} = {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))})
361	360, 357	fveq12d 10152	. . . . . . . . . . . . . . . . . 18 |- (l = x -> ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}` l) = ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x))
362	361	opreq2d 4898	. . . . . . . . . . . . . . . . 17 |- (l = x -> (2 x. ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}` l)) = (2 x. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x)))
363	359, 362	breq12d 3351	. . . . . . . . . . . . . . . 16 |- (l = x -> ((abs` ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` l)) <_ (2 x. ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}` l)) <-> (abs` ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` x)) <_ (2 x. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x))))
364	352, 363	imbi12d 688	. . . . . . . . . . . . . . 15 |- (l = x -> ((1 < l -> (abs` ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` l)) <_ (2 x. ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}` l))) <-> (1 < x -> (abs` ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` x)) <_ (2 x. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x)))))
365	337, 351, 364	cbvral 2278	. . . . . . . . . . . . . 14 |- (A.l e. NN (1 < l -> (abs` ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` l)) <_ (2 x. ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}` l))) <-> A.x e. NN (1 < x -> (abs` ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` x)) <_ (2 x. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x))))
366	323, 365	sylibr 217	. . . . . . . . . . . . 13 |- (f e. ({0, 2} ^m NN) -> A.l e. NN (1 < l -> (abs` ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` l)) <_ (2 x. ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}` l))))
367	159, 200, 366	jca32 312	. . . . . . . . . . . 12 |- (f e. ({0, 2} ^m NN) -> ((2 e. RR /\ 0 <_ 2) /\ ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}:NN-->CC /\ A.l e. NN (1 < l -> (abs` ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` l)) <_ (2 x. ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}` l))))))
368	104, 152, 367	jca31 311	. . . . . . . . . . 11 |- (f e. ({0, 2} ^m NN) -> ((({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}:NN-->RR /\ A.l e. NN 0 <_ ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}` l)) /\ ( + seq1 {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}) ~~> (1 / 2)) /\ ((2 e. RR /\ 0 <_ 2) /\ ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}:NN-->CC /\ A.l e. NN (1 < l -> (abs` ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` l)) <_ (2 x. ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((1 / 3)^x))}` l)))))))
369	61, 62, 368	sylancr 526	. . . . . . . . . 10 |- (f e. ({0, 2} ^m NN) -> E.a( + seq1 {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}) ~~> a)
370		addex 6470	. . . . . . . . . . . . . 14 |- + e. _V
371		fvex 4689	. . . . . . . . . . . . . . 15 |- (ZZ>=` 1) e. _V
372	371	opabex2 4539	. . . . . . . . . . . . . 14 |- {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))} e. _V
373	370, 372	seq1seqz 7784	. . . . . . . . . . . . 13 |- ( + seq1 {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}) = (<.1, + >. seq {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))})
374	373	eqcomi 1888	. . . . . . . . . . . 12 |- (<.1, + >. seq {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}) = ( + seq1 {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))})
375	374	breq1i 3345	. . . . . . . . . . 11 |- ((<.1, + >. seq {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}) ~~> a <-> ( + seq1 {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}) ~~> a)
376	375	exbii 1398	. . . . . . . . . 10 |- (E.a(<.1, + >. seq {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}) ~~> a <-> E.a( + seq1 {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}) ~~> a)
377	369, 376	sylibr 217	. . . . . . . . 9 |- (f e. ({0, 2} ^m NN) -> E.a(<.1, + >. seq {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}) ~~> a)
378	8, 59, 377	3jca 1050	. . . . . . . 8 |- (f e. ({0, 2} ^m NN) -> (1 e. ZZ /\ A.k e. (ZZ>=` 1)({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` k) e. RR /\ E.a(<.1, + >. seq {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}) ~~> a))
379	372	isumrecl 8471	. . . . . . . . 9 |- ((1 e. ZZ /\ A.k e. (ZZ>=` 1)({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` k) e. RR /\ E.a(<.1, + >. seq {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}) ~~> a) -> sum_k e. (ZZ>=` 1)({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` k) e. RR)
380	53, 54	fvopab4g 4742	. . . . . . . . . . . 12 |- ((k e. (ZZ>=` 1) /\ ((f` k) / (3^k)) e. _V) -> ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` k) = ((f` k) / (3^k)))
381	380	eqcomd 1889	. . . . . . . . . . 11 |- ((k e. (ZZ>=` 1) /\ ((f` k) / (3^k)) e. _V) -> ((f` k) / (3^k)) = ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` k))
382	37	biimpi 168	. . . . . . . . . . 11 |- (k e. NN -> k e. (ZZ>=` 1))
383		oprex 4907	. . . . . . . . . . 11 |- ((f` k) / (3^k)) e. _V
384	381, 382, 383	sylancl 525	. . . . . . . . . 10 |- (k e. NN -> ((f` k) / (3^k)) = ({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` k))
385	13, 384	sumeq12i 8249	. . . . . . . . 9 |- sum_k e. NN ((f` k) / (3^k)) = sum_k e. (ZZ>=` 1)({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` k)
386	379, 385	syl5eqel 1975	. . . . . . . 8 |- ((1 e. ZZ /\ A.k e. (ZZ>=` 1)({<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}` k) e. RR /\ E.a(<.1, + >. seq {<.x, y>. | (x e. (ZZ>=` 1) /\ y = ((f` x) / (3^x)))}) ~~> a) -> sum_k e. NN ((f` k) / (3^k)) e. RR)
387		rexr 6668	. . . . . . . 8 |- (sum_k e. NN ((f` k) / (3^k)) e. RR -> sum_k e. NN ((f` k) / (3^k)) e. RR*)
388	378, 386, 387	3syl 24	. . . . . . 7 |- (f e. ({0, 2} ^m NN) -> sum_k e. NN ((f` k) / (3^k)) e. RR*)
389		oprex 4907	. . . . . . . . . . 11 |- ((f` l) / (3^l)) e. _V
390	389, 305	isumclim3 8461	. . . . . . . . . 10 |- ((1 e. ZZ /\ E.a(<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}) ~~> a) -> (<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}) ~~> sum_l e. (ZZ>=` 1)((f` l) / (3^l)))
391		ax-17 1317	. . . . . . . . . . . 12 |- (u e. ((f` k) / (3^k)) -> A.l u e. ((f` k) / (3^k)))
392		ax-17 1317	. . . . . . . . . . . 12 |- (u e. ((f` l) / (3^l)) -> A.k u e. ((f` l) / (3^l)))
393		fveq2 4681	. . . . . . . . . . . . 13 |- (k = l -> (f` k) = (f` l))
394		opreq2 4890	. . . . . . . . . . . . 13 |- (k = l -> (3^k) = (3^l))
395	393, 394	opreq12d 4900	. . . . . . . . . . . 12 |- (k = l -> ((f` k) / (3^k)) = ((f` l) / (3^l)))
396	391, 392, 395	cbvsumi 8246	. . . . . . . . . . 11 |- sum_k e. NN ((f` k) / (3^k)) = sum_l e. NN ((f` l) / (3^l))
397	13	sumeq1i 8247	. . . . . . . . . . 11 |- sum_l e. NN ((f` l) / (3^l)) = sum_l e. (ZZ>=` 1)((f` l) / (3^l))
398	396, 397	eqtri 1908	. . . . . . . . . 10 |- sum_k e. NN ((f` k) / (3^k)) = sum_l e. (ZZ>=` 1)((f` l) / (3^l))
399	390, 398	syl6breqr 3377	. . . . . . . . 9 |- ((1 e. ZZ /\ E.a(<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}) ~~> a) -> (<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}) ~~> sum_k e. NN ((f` k) / (3^k)))
400	62	a1i 8	. . . . . . . . . . 11 |- (f e. ({0, 2} ^m NN) -> 1 e. NN)
401	65	a1i 8	. . . . . . . . . . . . . . . . 17 |- (x e. NN -> (1 / 3) e. RR)
402	77	a1i 8	. . . . . . . . . . . . . . . . 17 |- (x e. NN -> 0 <_ (1 / 3))
403		expge0 7833	. . . . . . . . . . . . . . . . 17 |- (((1 / 3) e. RR /\ x e. NN0 /\ 0 <_ (1 / 3)) -> 0 <_ ((1 / 3)^x))
404	401, 213, 402, 403	syl111anc 1100	. . . . . . . . . . . . . . . 16 |- (x e. NN -> 0 <_ ((1 / 3)^x))
405	404, 317	breqtrrd 3363	. . . . . . . . . . . . . . 15 |- (x e. NN -> 0 <_ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x))
406	405	rgen 2159	. . . . . . . . . . . . . 14 |- A.x e. NN 0 <_ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x)
407	97, 406	pm3.2i 307	. . . . . . . . . . . . 13 |- ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}:NN-->RR /\ A.x e. NN 0 <_ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x))
408	64	bicomi 189	. . . . . . . . . . . . . . . . 17 |- (l e. (ZZ>=` 1) <-> l e. NN)
409	408	anbi1i 539	. . . . . . . . . . . . . . . 16 |- ((l e. (ZZ>=` 1) /\ y = ((1 / 3)^l)) <-> (l e. NN /\ y = ((1 / 3)^l)))
410	409	opabbii 3402	. . . . . . . . . . . . . . 15 |- {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))} = {<.l, y>. | (l e. NN /\ y = ((1 / 3)^l))}
411	410	opreq2i 4893	. . . . . . . . . . . . . 14 |- ( + seq1 {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}) = ( + seq1 {<.l, y>. | (l e. NN /\ y = ((1 / 3)^l))})
412	124, 411, 150	3brtr4i 3365	. . . . . . . . . . . . 13 |- ( + seq1 {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}) ~~> (1 / 2)
413	407, 412	pm3.2i 307	. . . . . . . . . . . 12 |- (({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}:NN-->RR /\ A.x e. NN 0 <_ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x)) /\ ( + seq1 {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}) ~~> (1 / 2))
414	413	a1i 8	. . . . . . . . . . 11 |- (f e. ({0, 2} ^m NN) -> (({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}:NN-->RR /\ A.x e. NN 0 <_ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x)) /\ ( + seq1 {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}) ~~> (1 / 2)))
415	408	anbi1i 539	. . . . . . . . . . . . . . 15 |- ((l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l))) <-> (l e. NN /\ y = ((f` l) / (3^l))))
416	415	opabbii 3402	. . . . . . . . . . . . . 14 |- {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))} = {<.l, y>. | (l e. NN /\ y = ((f` l) / (3^l)))}
417	416	fopab2 4796	. . . . . . . . . . . . 13 |- (A.l e. NN ((f` l) / (3^l)) e. CC <-> {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}:NN-->CC)
418	189, 417	sylib 215	. . . . . . . . . . . 12 |- (f e. ({0, 2} ^m NN) -> {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}:NN-->CC)
419	159, 418, 323	jca32 312	. . . . . . . . . . 11 |- (f e. ({0, 2} ^m NN) -> ((2 e. RR /\ 0 <_ 2) /\ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}:NN-->CC /\ A.x e. NN (1 < x -> (abs` ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` x)) <_ (2 x. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x))))))
420	60	cvgcmp3ce 8451	. . . . . . . . . . 11 |- ((1 e. NN /\ ((({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}:NN-->RR /\ A.x e. NN 0 <_ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x)) /\ ( + seq1 {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}) ~~> (1 / 2)) /\ ((2 e. RR /\ 0 <_ 2) /\ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}:NN-->CC /\ A.x e. NN (1 < x -> (abs` ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` x)) <_ (2 x. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((1 / 3)^l))}` x))))))) -> E.a( + seq1 {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}) ~~> a)
421	400, 414, 419, 420	syl12anc 1098	. . . . . . . . . 10 |- (f e. ({0, 2} ^m NN) -> E.a( + seq1 {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}) ~~> a)
422	371	opabex2 4539	. . . . . . . . . . . . . . 15 |- {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))} e. _V
423	370, 422	seq1seqz 7784	. . . . . . . . . . . . . 14 |- ( + seq1 {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}) = (<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))})
424	423	eqcomi 1888	. . . . . . . . . . . . 13 |- (<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}) = ( + seq1 {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))})
425	424	a1i 8	. . . . . . . . . . . 12 |- (f e. ({0, 2} ^m NN) -> (<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}) = ( + seq1 {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}))
426	425	breq1d 3348	. . . . . . . . . . 11 |- (f e. ({0, 2} ^m NN) -> ((<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}) ~~> a <-> ( + seq1 {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}) ~~> a))
427	426	exbidv 1657	. . . . . . . . . 10 |- (f e. ({0, 2} ^m NN) -> (E.a(<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}) ~~> a <-> E.a( + seq1 {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}) ~~> a))
428	421, 427	mpbird 213	. . . . . . . . 9 |- (f e. ({0, 2} ^m NN) -> E.a(<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}) ~~> a)
429	399, 7, 428	sylancr 526	. . . . . . . 8 |- (f e. ({0, 2} ^m NN) -> (<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}) ~~> sum_k e. NN ((f` k) / (3^k)))
430		fveq2 4681	. . . . . . . . . . . . . 14 |- (l = k -> (f` l) = (f` k))
431		opreq2 4890	. . . . . . . . . . . . . 14 |- (l = k -> (3^l) = (3^k))
432	430, 431	opreq12d 4900	. . . . . . . . . . . . 13 |- (l = k -> ((f` l) / (3^l)) = ((f` k) / (3^k)))
433	432, 305	fvopab4g 4742	. . . . . . . . . . . 12 |- ((k e. (ZZ>=` 1) /\ ((f` k) / (3^k)) e. _V) -> ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` k) = ((f` k) / (3^k)))
434	433, 9, 383	sylancl 525	. . . . . . . . . . 11 |- ((f e. ({0, 2} ^m NN) /\ k e. (ZZ>=` 1)) -> ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` k) = ((f` k) / (3^k)))
435	434, 50	eqeltrd 1971	. . . . . . . . . 10 |- ((f e. ({0, 2} ^m NN) /\ k e. (ZZ>=` 1)) -> ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` k) e. RR)
436	15	biimpi 168	. . . . . . . . . . . . . . 15 |- (k e. (ZZ>=` 1) -> k e. NN)
437	436	anim2i 362	. . . . . . . . . . . . . 14 |- ((f:NN-->{0, 2} /\ k e. (ZZ>=` 1)) -> (f:NN-->{0, 2} /\ k e. NN))
438	26, 254	pm3.2i 307	. . . . . . . . . . . . . . . . . . . . 21 |- (0 e. RR /\ 0 <_ 0)
439		breq2 3342	. . . . . . . . . . . . . . . . . . . . . 22 |- ((f` k) = 0 -> (0 <_ (f` k) <-> 0 <_ 0))
440	27, 439	anbi12d 690	. . . . . . . . . . . . . . . . . . . . 21 |- ((f` k) = 0 -> (((f` k) e. RR /\ 0 <_ (f` k)) <-> (0 e. RR /\ 0 <_ 0)))
441	438, 440	mpbiri 211	. . . . . . . . . . . . . . . . . . . 20 |- ((f` k) = 0 -> ((f` k) e. RR /\ 0 <_ (f` k)))
442	36	a1i 8	. . . . . . . . . . . . . . . . . . . . . 22 |- (k e. (ZZ>=` 1) -> 3 e. RR)
443	74	a1i 8	. . . . . . . . . . . . . . . . . . . . . 22 |- (k e. (ZZ>=` 1) -> 0 < 3)
444		expgt0 7831	. . . . . . . . . . . . . . . . . . . . . 22 |- ((3 e. RR /\ k e. NN0 /\ 0 < 3) -> 0 < (3^k))
445	442, 39, 443, 444	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . 21 |- (k e. (ZZ>=` 1) -> 0 < (3^k))
446	40, 445	jca 310	. . . . . . . . . . . . . . . . . . . 20 |- (k e. (ZZ>=` 1) -> ((3^k) e. RR /\ 0 < (3^k)))
447	441, 446	anim12i 360	. . . . . . . . . . . . . . . . . . 19 |- (((f` k) = 0 /\ k e. (ZZ>=` 1)) -> (((f` k) e. RR /\ 0 <_ (f` k)) /\ ((3^k) e. RR /\ 0 < (3^k))))
448	447	ex 402	. . . . . . . . . . . . . . . . . 18 |- ((f` k) = 0 -> (k e. (ZZ>=` 1) -> (((f` k) e. RR /\ 0 <_ (f` k)) /\ ((3^k) e. RR /\ 0 < (3^k)))))
449		divge0 7038	. . . . . . . . . . . . . . . . . 18 |- ((((f` k) e. RR /\ 0 <_ (f` k)) /\ ((3^k) e. RR /\ 0 < (3^k))) -> 0 <_ ((f` k) / (3^k)))
450	448, 449	syl6 25	. . . . . . . . . . . . . . . . 17 |- ((f` k) = 0 -> (k e. (ZZ>=` 1) -> 0 <_ ((f` k) / (3^k))))
451	31	adantr 425	. . . . . . . . . . . . . . . . . . . 20 |- (((f` k) = 2 /\ k e. (ZZ>=` 1)) -> (f` k) e. RR)
452		breq2 3342	. . . . . . . . . . . . . . . . . . . . . 22 |- ((f` k) = 2 -> (0 <_ (f` k) <-> 0 <_ 2))
453	157, 452	mpbiri 211	. . . . . . . . . . . . . . . . . . . . 21 |- ((f` k) = 2 -> 0 <_ (f` k))
454	453	adantr 425	. . . . . . . . . . . . . . . . . . . 20 |- (((f` k) = 2 /\ k e. (ZZ>=` 1)) -> 0 <_ (f` k))
455	446	adantl 424	. . . . . . . . . . . . . . . . . . . 20 |- (((f` k) = 2 /\ k e. (ZZ>=` 1)) -> ((3^k) e. RR /\ 0 < (3^k)))
456	451, 454, 455	jca31 311	. . . . . . . . . . . . . . . . . . 19 |- (((f` k) = 2 /\ k e. (ZZ>=` 1)) -> (((f` k) e. RR /\ 0 <_ (f` k)) /\ ((3^k) e. RR /\ 0 < (3^k))))
457	456	ex 402	. . . . . . . . . . . . . . . . . 18 |- ((f` k) = 2 -> (k e. (ZZ>=` 1) -> (((f` k) e. RR /\ 0 <_ (f` k)) /\ ((3^k) e. RR /\ 0 < (3^k)))))
458	457, 449	syl6 25	. . . . . . . . . . . . . . . . 17 |- ((f` k) = 2 -> (k e. (ZZ>=` 1) -> 0 <_ ((f` k) / (3^k))))
459	450, 458	jaoi 368	. . . . . . . . . . . . . . . 16 |- (((f` k) = 0 \/ (f` k) = 2) -> (k e. (ZZ>=` 1) -> 0 <_ ((f` k) / (3^k))))
460	459	adantld 426	. . . . . . . . . . . . . . 15 |- (((f` k) = 0 \/ (f` k) = 2) -> ((f:NN-->{0, 2} /\ k e. (ZZ>=` 1)) -> 0 <_ ((f` k) / (3^k))))
461	18, 460	sylbi 216	. . . . . . . . . . . . . 14 |- ((f` k) e. {0, 2} -> ((f:NN-->{0, 2} /\ k e. (ZZ>=` 1)) -> 0 <_ ((f` k) / (3^k))))
462	437, 16, 461	3syl 24	. . . . . . . . . . . . 13 |- ((f:NN-->{0, 2} /\ k e. (ZZ>=` 1)) -> ((f:NN-->{0, 2} /\ k e. (ZZ>=` 1)) -> 0 <_ ((f` k) / (3^k))))
463	462	pm2.43i 78	. . . . . . . . . . . 12 |- ((f:NN-->{0, 2} /\ k e. (ZZ>=` 1)) -> 0 <_ ((f` k) / (3^k)))
464	463, 12	sylanb 498	. . . . . . . . . . 11 |- ((f e. ({0, 2} ^m NN) /\ k e. (ZZ>=` 1)) -> 0 <_ ((f` k) / (3^k)))
465	464, 434	breqtrrd 3363	. . . . . . . . . 10 |- ((f e. ({0, 2} ^m NN) /\ k e. (ZZ>=` 1)) -> 0 <_ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` k))
466	435, 465	jca 310	. . . . . . . . 9 |- ((f e. ({0, 2} ^m NN) /\ k e. (ZZ>=` 1)) -> (({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` k) e. RR /\ 0 <_ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` k)))
467	466	r19.21aiva 2176	. . . . . . . 8 |- (f e. ({0, 2} ^m NN) -> A.k e. (ZZ>=` 1)(({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` k) e. RR /\ 0 <_ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` k)))
468		sumex 8241	. . . . . . . . 9 |- sum_k e. NN ((f` k) / (3^k)) e. _V
469	468, 422	iserzcmp0 8403	. . . . . . . 8 |- ((1 e. ZZ /\ (<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}) ~~> sum_k e. NN ((f` k) / (3^k)) /\ A.k e. (ZZ>=` 1)(({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` k) e. RR /\ 0 <_ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` k))) -> 0 <_ sum_k e. NN ((f` k) / (3^k)))
470	8, 429, 467, 469	syl111anc 1100	. . . . . . 7 |- (f e. ({0, 2} ^m NN) -> 0 <_ sum_k e. NN ((f` k) / (3^k)))
471		eleq1 1957	. . . . . . . . . . . . . 14 |- (l = k -> (l e. (ZZ>=` 1) <-> k e. (ZZ>=` 1)))
472	432	eqeq2d 1895	. . . . . . . . . . . . . 14 |- (l = k -> (y = ((f` l) / (3^l)) <-> y = ((f` k) / (3^k))))
473	471, 472	anbi12d 690	. . . . . . . . . . . . 13 |- (l = k -> ((l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l))) <-> (k e. (ZZ>=` 1) /\ y = ((f` k) / (3^k)))))
474	473	cbvopab1v 3407	. . . . . . . . . . . 12 |- {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))} = {<.k, y>. | (k e. (ZZ>=` 1) /\ y = ((f` k) / (3^k)))}
475	383, 474	isumclim3 8461	. . . . . . . . . . 11 |- ((1 e. ZZ /\ E.a(<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}) ~~> a) -> (<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}) ~~> sum_k e. (ZZ>=` 1)((f` k) / (3^k)))
476	475, 7, 428	sylancr 526	. . . . . . . . . 10 |- (f e. ({0, 2} ^m NN) -> (<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}) ~~> sum_k e. (ZZ>=` 1)((f` k) / (3^k)))
477		oprex 4907	. . . . . . . . . . . 12 |- (2 / (3^k)) e. _V
478	431	opreq2d 4898	. . . . . . . . . . . . . . 15 |- (l = k -> (2 / (3^l)) = (2 / (3^k)))
479	478	eqeq2d 1895	. . . . . . . . . . . . . 14 |- (l = k -> (y = (2 / (3^l)) <-> y = (2 / (3^k))))
480	471, 479	anbi12d 690	. . . . . . . . . . . . 13 |- (l = k -> ((l e. (ZZ>=` 1) /\ y = (2 / (3^l))) <-> (k e. (ZZ>=` 1) /\ y = (2 / (3^k)))))
481	480	cbvopab1v 3407	. . . . . . . . . . . 12 |- {<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))} = {<.k, y>. | (k e. (ZZ>=` 1) /\ y = (2 / (3^k)))}
482	477, 481	isumclim3 8461	. . . . . . . . . . 11 |- ((1 e. ZZ /\ E.a(<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}) ~~> a) -> (<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}) ~~> sum_k e. (ZZ>=` 1)(2 / (3^k)))
483	131	a1i 8	. . . . . . . . . . . . . . . . . . 19 |- (l e. (ZZ>=` 1) -> 1 e. CC)
484	162, 42, 68	sylancr 526	. . . . . . . . . . . . . . . . . . 19 |- (l e. (ZZ>=` 1) -> (3^l) e. CC)
485	42	a1i 8	. . . . . . . . . . . . . . . . . . . 20 |- (l e. (ZZ>=` 1) -> 3 e. CC)
486	44	a1i 8	. . . . . . . . . . . . . . . . . . . 20 |- (l e. (ZZ>=` 1) -> 3 =/= 0)
487		expne0i 7830	. . . . . . . . . . . . . . . . . . . 20 |- ((3 e. CC /\ 3 =/= 0 /\ l e. NN0) -> (3^l) =/= 0)
488	485, 486, 68, 487	syl111anc 1100	. . . . . . . . . . . . . . . . . . 19 |- (l e. (ZZ>=` 1) -> (3^l) =/= 0)
489		divcl 6901	. . . . . . . . . . . . . . . . . . 19 |- ((1 e. CC /\ (3^l) e. CC /\ (3^l) =/= 0) -> (1 / (3^l)) e. CC)
490	483, 484, 488, 489	syl111anc 1100	. . . . . . . . . . . . . . . . . 18 |- (l e. (ZZ>=` 1) -> (1 / (3^l)) e. CC)
491		fvopab2 4754	. . . . . . . . . . . . . . . . . . . 20 |- ((l e. (ZZ>=` 1) /\ (1 / (3^l)) e. CC) -> ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))}` l) = (1 / (3^l)))
492	491	eleq1d 1963	. . . . . . . . . . . . . . . . . . 19 |- ((l e. (ZZ>=` 1) /\ (1 / (3^l)) e. CC) -> (({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))}` l) e. CC <-> (1 / (3^l)) e. CC))
493	490, 492	mpdan 768	. . . . . . . . . . . . . . . . . 18 |- (l e. (ZZ>=` 1) -> (({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))}` l) e. CC <-> (1 / (3^l)) e. CC))
494	490, 493	mpbird 213	. . . . . . . . . . . . . . . . 17 |- (l e. (ZZ>=` 1) -> ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))}` l) e. CC)
495	132	a1i 8	. . . . . . . . . . . . . . . . . . 19 |- (l e. (ZZ>=` 1) -> 2 e. CC)
496		divcl 6901	. . . . . . . . . . . . . . . . . . 19 |- ((2 e. CC /\ (3^l) e. CC /\ (3^l) =/= 0) -> (2 / (3^l)) e. CC)
497	495, 484, 488, 496	syl111anc 1100	. . . . . . . . . . . . . . . . . 18 |- (l e. (ZZ>=` 1) -> (2 / (3^l)) e. CC)
498		fvopab2 4754	. . . . . . . . . . . . . . . . . . 19 |- ((l e. (ZZ>=` 1) /\ (2 / (3^l)) e. CC) -> ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}` l) = (2 / (3^l)))
499	495, 484, 488	3jca 1050	. . . . . . . . . . . . . . . . . . . . 21 |- (l e. (ZZ>=` 1) -> (2 e. CC /\ (3^l) e. CC /\ (3^l) =/= 0))
500	499	adantr 425	. . . . . . . . . . . . . . . . . . . 20 |- ((l e. (ZZ>=` 1) /\ (2 / (3^l)) e. CC) -> (2 e. CC /\ (3^l) e. CC /\ (3^l) =/= 0))
501		divrec 6922	. . . . . . . . . . . . . . . . . . . 20 |- ((2 e. CC /\ (3^l) e. CC /\ (3^l) =/= 0) -> (2 / (3^l)) = (2 x. (1 / (3^l))))
502	500, 501	syl 12	. . . . . . . . . . . . . . . . . . 19 |- ((l e. (ZZ>=` 1) /\ (2 / (3^l)) e. CC) -> (2 / (3^l)) = (2 x. (1 / (3^l))))
503	490, 491	mpdan 768	. . . . . . . . . . . . . . . . . . . . . 22 |- (l e. (ZZ>=` 1) -> ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))}` l) = (1 / (3^l)))
504	503	eqcomd 1889	. . . . . . . . . . . . . . . . . . . . 21 |- (l e. (ZZ>=` 1) -> (1 / (3^l)) = ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))}` l))
505	504	opreq2d 4898	. . . . . . . . . . . . . . . . . . . 20 |- (l e. (ZZ>=` 1) -> (2 x. (1 / (3^l))) = (2 x. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))}` l)))
506	505	adantr 425	. . . . . . . . . . . . . . . . . . 19 |- ((l e. (ZZ>=` 1) /\ (2 / (3^l)) e. CC) -> (2 x. (1 / (3^l))) = (2 x. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))}` l)))
507	498, 502, 506	3eqtrd 1929	. . . . . . . . . . . . . . . . . 18 |- ((l e. (ZZ>=` 1) /\ (2 / (3^l)) e. CC) -> ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}` l) = (2 x. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))}` l)))
508	497, 507	mpdan 768	. . . . . . . . . . . . . . . . 17 |- (l e. (ZZ>=` 1) -> ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}` l) = (2 x. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))}` l)))
509	494, 508	jca 310	. . . . . . . . . . . . . . . 16 |- (l e. (ZZ>=` 1) -> (({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))}` l) e. CC /\ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}` l) = (2 x. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))}` l))))
510	509	rgen 2159	. . . . . . . . . . . . . . 15 |- A.l e. (ZZ>=` 1)(({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))}` l) e. CC /\ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}` l) = (2 x. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))}` l)))
511	7, 132, 510	3pm3.2i 1048	. . . . . . . . . . . . . 14 |- (1 e. ZZ /\ 2 e. CC /\ A.l e. (ZZ>=` 1)(({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))}` l) e. CC /\ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}` l) = (2 x. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))}` l))))
512	11	opabex2 4539	. . . . . . . . . . . . . . . . 17 |- {<.l, y>. | (l e. NN /\ y = (1 / (3^l)))} e. _V
513	370, 512	seq1seqz 7784	. . . . . . . . . . . . . . . 16 |- ( + seq1 {<.l, y>. | (l e. NN /\ y = (1 / (3^l)))}) = (<.1, + >. seq {<.l, y>. | (l e. NN /\ y = (1 / (3^l)))})
514	42	a1i 8	. . . . . . . . . . . . . . . . . . . . . . 23 |- (l e. NN -> 3 e. CC)
515	44	a1i 8	. . . . . . . . . . . . . . . . . . . . . . 23 |- (l e. NN -> 3 =/= 0)
516		exprec 7837	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((3 e. CC /\ 3 =/= 0 /\ l e. NN0) -> ((1 / 3)^l) = (1 / (3^l)))
517	514, 515, 67, 516	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . 22 |- (l e. NN -> ((1 / 3)^l) = (1 / (3^l)))
518	517	eqcomd 1889	. . . . . . . . . . . . . . . . . . . . 21 |- (l e. NN -> (1 / (3^l)) = ((1 / 3)^l))
519	518	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . 20 |- (l e. NN -> (y = (1 / (3^l)) <-> y = ((1 / 3)^l)))
520	519	pm5.32i 707	. . . . . . . . . . . . . . . . . . 19 |- ((l e. NN /\ y = (1 / (3^l))) <-> (l e. NN /\ y = ((1 / 3)^l)))
521	520	opabbii 3402	. . . . . . . . . . . . . . . . . 18 |- {<.l, y>. | (l e. NN /\ y = (1 / (3^l)))} = {<.l, y>. | (l e. NN /\ y = ((1 / 3)^l))}
522	521	opreq2i 4893	. . . . . . . . . . . . . . . . 17 |- ( + seq1 {<.l, y>. | (l e. NN /\ y = (1 / (3^l)))}) = ( + seq1 {<.l, y>. | (l e. NN /\ y = ((1 / 3)^l))})
523		absdiv 8111	. . . . . . . . . . . . . . . . . . . 20 |- ((1 e. CC /\ 3 e. CC /\ 3 =/= 0) -> (abs` (1 / 3)) = ((abs` 1) / (abs` 3)))
524		absid 8113	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((1 e. RR /\ 0 <_ 1) -> (abs` 1) = 1)
525	70, 72, 524	mp2an 761	. . . . . . . . . . . . . . . . . . . . . . 23 |- (abs` 1) = 1
526	525	a1i 8	. . . . . . . . . . . . . . . . . . . . . 22 |- ((1 e. CC /\ 3 e. CC /\ 3 =/= 0) -> (abs` 1) = 1)
527	26, 36, 74	ltleii 6756	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 0 <_ 3
528		absid 8113	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((3 e. RR /\ 0 <_ 3) -> (abs` 3) = 3)
529	36, 527, 528	mp2an 761	. . . . . . . . . . . . . . . . . . . . . . 23 |- (abs` 3) = 3
530	529	a1i 8	. . . . . . . . . . . . . . . . . . . . . 22 |- ((1 e. CC /\ 3 e. CC /\ 3 =/= 0) -> (abs` 3) = 3)
531	526, 530	opreq12d 4900	. . . . . . . . . . . . . . . . . . . . 21 |- ((1 e. CC /\ 3 e. CC /\ 3 =/= 0) -> ((abs` 1) / (abs` 3)) = (1 / 3))
532	36, 118	pm3.2i 307	. . . . . . . . . . . . . . . . . . . . . . 23 |- (3 e. RR /\ 1 < 3)
533	532	a1i 8	. . . . . . . . . . . . . . . . . . . . . 22 |- ((1 e. CC /\ 3 e. CC /\ 3 =/= 0) -> (3 e. RR /\ 1 < 3))
534		recgt1i 7083	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((3 e. RR /\ 1 < 3) -> (0 < (1 / 3) /\ (1 / 3) < 1))
535	534	simprd 352	. . . . . . . . . . . . . . . . . . . . . 22 |- ((3 e. RR /\ 1 < 3) -> (1 / 3) < 1)
536	533, 535	syl 12	. . . . . . . . . . . . . . . . . . . . 21 |- ((1 e. CC /\ 3 e. CC /\ 3 =/= 0) -> (1 / 3) < 1)
537	531, 536	eqbrtrd 3357	. . . . . . . . . . . . . . . . . . . 20 |- ((1 e. CC /\ 3 e. CC /\ 3 =/= 0) -> ((abs` 1) / (abs` 3)) < 1)
538	523, 537	eqbrtrd 3357	. . . . . . . . . . . . . . . . . . 19 |- ((1 e. CC /\ 3 e. CC /\ 3 =/= 0) -> (abs` (1 / 3)) < 1)
539	131, 42, 44, 538	mp3an 1191	. . . . . . . . . . . . . . . . . 18 |- (abs` (1 / 3)) < 1
540	105, 106, 539	geolim1i 8500	. . . . . . . . . . . . . . . . 17 |- ( + seq1 {<.l, y>. | (l e. NN /\ y = ((1 / 3)^l))}) ~~> ((1 / 3) / (1 - (1 / 3)))
541	522, 540	eqbrtri 3356	. . . . . . . . . . . . . . . 16 |- ( + seq1 {<.l, y>. | (l e. NN /\ y = (1 / (3^l)))}) ~~> ((1 / 3) / (1 - (1 / 3)))
542	513, 541	eqbrtrri 3358	. . . . . . . . . . . . . . 15 |- (<.1, + >. seq {<.l, y>. | (l e. NN /\ y = (1 / (3^l)))}) ~~> ((1 / 3) / (1 - (1 / 3)))
543	408	anbi1i 539	. . . . . . . . . . . . . . . . 17 |- ((l e. (ZZ>=` 1) /\ y = (1 / (3^l))) <-> (l e. NN /\ y = (1 / (3^l))))
544	543	opabbii 3402	. . . . . . . . . . . . . . . 16 |- {<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))} = {<.l, y>. | (l e. NN /\ y = (1 / (3^l)))}
545	544	opreq2i 4893	. . . . . . . . . . . . . . 15 |- (<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))}) = (<.1, + >. seq {<.l, y>. | (l e. NN /\ y = (1 / (3^l)))})
546	542, 545, 150	3brtr4i 3365	. . . . . . . . . . . . . 14 |- (<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))}) ~~> (1 / 2)
547	371	opabex2 4539	. . . . . . . . . . . . . . . . 17 |- {<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))} e. _V
548	371	opabex2 4539	. . . . . . . . . . . . . . . . 17 |- {<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))} e. _V
549		hbopab1 3562	. . . . . . . . . . . . . . . . 17 |- (u e. {<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))} -> A.l u e. {<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))})
550		hbopab1 3562	. . . . . . . . . . . . . . . . 17 |- (u e. {<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))} -> A.l u e. {<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))})
551	60, 547, 548, 549, 550	iserzmulc1b 14528	. . . . . . . . . . . . . . . 16 |- ((1 e. ZZ /\ 2 e. CC /\ A.l e. (ZZ>=` 1)(({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))}` l) e. CC /\ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}` l) = (2 x. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))}` l)))) -> ((<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))}) ~~> (1 / 2) -> (<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}) ~~> (2 x. (1 / 2))))
552	551	imp 377	. . . . . . . . . . . . . . 15 |- (((1 e. ZZ /\ 2 e. CC /\ A.l e. (ZZ>=` 1)(({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))}` l) e. CC /\ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}` l) = (2 x. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))}` l)))) /\ (<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))}) ~~> (1 / 2)) -> (<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}) ~~> (2 x. (1 / 2)))
553	132, 133	recidi 6916	. . . . . . . . . . . . . . 15 |- (2 x. (1 / 2)) = 1
554	552, 553	syl6breq 3376	. . . . . . . . . . . . . 14 |- (((1 e. ZZ /\ 2 e. CC /\ A.l e. (ZZ>=` 1)(({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))}` l) e. CC /\ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}` l) = (2 x. ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))}` l)))) /\ (<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = (1 / (3^l)))}) ~~> (1 / 2)) -> (<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}) ~~> 1)
555	511, 546, 554	mp2an 761	. . . . . . . . . . . . 13 |- (<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}) ~~> 1
556	131	elisseti 2301	. . . . . . . . . . . . . 14 |- 1 e. _V
557		breq2 3342	. . . . . . . . . . . . . 14 |- (a = 1 -> ((<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}) ~~> a <-> (<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}) ~~> 1))
558	556, 557	cla4ev 2371	. . . . . . . . . . . . 13 |- ((<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}) ~~> 1 -> E.a(<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}) ~~> a)
559	555, 558	ax-mp 7	. . . . . . . . . . . 12 |- E.a(<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}) ~~> a
560	559	a1i 8	. . . . . . . . . . 11 |- (f e. ({0, 2} ^m NN) -> E.a(<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}) ~~> a)
561	482, 7, 560	sylancr 526	. . . . . . . . . 10 |- (f e. ({0, 2} ^m NN) -> (<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}) ~~> sum_k e. (ZZ>=` 1)(2 / (3^k)))
562		eqid 1884	. . . . . . . . . . . . . . . 16 |- {<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))} = {<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}
563	478, 562	fvopab4g 4742	. . . . . . . . . . . . . . 15 |- ((k e. (ZZ>=` 1) /\ (2 / (3^k)) e. _V) -> ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}` k) = (2 / (3^k)))
564	563, 9, 477	sylancl 525	. . . . . . . . . . . . . 14 |- ((f e. ({0, 2} ^m NN) /\ k e. (ZZ>=` 1)) -> ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}` k) = (2 / (3^k)))
565	29	a1i 8	. . . . . . . . . . . . . . . 16 |- (k e. (ZZ>=` 1) -> 2 e. RR)
566		redivcl 6978	. . . . . . . . . . . . . . . 16 |- ((2 e. RR /\ (3^k) e. RR /\ (3^k) =/= 0) -> (2 / (3^k)) e. RR)
567	565, 40, 47, 566	syl111anc 1100	. . . . . . . . . . . . . . 15 |- (k e. (ZZ>=` 1) -> (2 / (3^k)) e. RR)
568	567	adantl 424	. . . . . . . . . . . . . 14 |- ((f e. ({0, 2} ^m NN) /\ k e. (ZZ>=` 1)) -> (2 / (3^k)) e. RR)
569	564, 568	eqeltrd 1971	. . . . . . . . . . . . 13 |- ((f e. ({0, 2} ^m NN) /\ k e. (ZZ>=` 1)) -> ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}` k) e. RR)
570		opreq1 4889	. . . . . . . . . . . . . . . . . . 19 |- ((f` k) = 0 -> ((f` k) / (3^k)) = (0 / (3^k)))
571	570	breq1d 3348	. . . . . . . . . . . . . . . . . 18 |- ((f` k) = 0 -> (((f` k) / (3^k)) <_ (2 / (3^k)) <-> (0 / (3^k)) <_ (2 / (3^k))))
572		2pos 7173	. . . . . . . . . . . . . . . . . . . 20 |- 0 < 2
573	26, 29, 572	ltleii 6756	. . . . . . . . . . . . . . . . . . 19 |- 0 <_ 2
574	26	a1i 8	. . . . . . . . . . . . . . . . . . . 20 |- (k e. (ZZ>=` 1) -> 0 e. RR)
575		lediv1 7033	. . . . . . . . . . . . . . . . . . . 20 |- ((0 e. RR /\ 2 e. RR /\ ((3^k) e. RR /\ 0 < (3^k))) -> (0 <_ 2 <-> (0 / (3^k)) <_ (2 / (3^k))))
576	574, 565, 40, 445, 575	syl112anc 1104	. . . . . . . . . . . . . . . . . . 19 |- (k e. (ZZ>=` 1) -> (0 <_ 2 <-> (0 / (3^k)) <_ (2 / (3^k))))
577	573, 576	mpbii 210	. . . . . . . . . . . . . . . . . 18 |- (k e. (ZZ>=` 1) -> (0 / (3^k)) <_ (2 / (3^k)))
578	571, 577	syl5bir 227	. . . . . . . . . . . . . . . . 17 |- ((f` k) = 0 -> (k e. (ZZ>=` 1) -> ((f` k) / (3^k)) <_ (2 / (3^k))))
579		opreq1 4889	. . . . . . . . . . . . . . . . . . 19 |- ((f` k) = 2 -> ((f` k) / (3^k)) = (2 / (3^k)))
580	579	breq1d 3348	. . . . . . . . . . . . . . . . . 18 |- ((f` k) = 2 -> (((f` k) / (3^k)) <_ (2 / (3^k)) <-> (2 / (3^k)) <_ (2 / (3^k))))
581		leid 6701	. . . . . . . . . . . . . . . . . . 19 |- ((2 / (3^k)) e. RR -> (2 / (3^k)) <_ (2 / (3^k)))
582	567, 581	syl 12	. . . . . . . . . . . . . . . . . 18 |- (k e. (ZZ>=` 1) -> (2 / (3^k)) <_ (2 / (3^k)))
583	580, 582	syl5bir 227	. . . . . . . . . . . . . . . . 17 |- ((f` k) = 2 -> (k e. (ZZ>=` 1) -> ((f` k) / (3^k)) <_ (2 / (3^k))))
584	578, 583	jaoi 368	. . . . . . . . . . . . . . . 16 |- (((f` k) = 0 \/ (f` k) = 2) -> (k e. (ZZ>=` 1) -> ((f` k) / (3^k)) <_ (2 / (3^k))))
585	584	imp 377	. . . . . . . . . . . . . . 15 |- ((((f` k) = 0 \/ (f` k) = 2) /\ k e. (ZZ>=` 1)) -> ((f` k) / (3^k)) <_ (2 / (3^k)))
586	25, 585	syl 12	. . . . . . . . . . . . . 14 |- ((f e. ({0, 2} ^m NN) /\ k e. (ZZ>=` 1)) -> ((f` k) / (3^k)) <_ (2 / (3^k)))
587	586, 434, 564	3brtr4d 3367	. . . . . . . . . . . . 13 |- ((f e. ({0, 2} ^m NN) /\ k e. (ZZ>=` 1)) -> ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` k) <_ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}` k))
588	435, 569, 587	3jca 1050	. . . . . . . . . . . 12 |- ((f e. ({0, 2} ^m NN) /\ k e. (ZZ>=` 1)) -> (({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` k) e. RR /\ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}` k) e. RR /\ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` k) <_ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}` k)))
589	588	r19.21aiva 2176	. . . . . . . . . . 11 |- (f e. ({0, 2} ^m NN) -> A.k e. (ZZ>=` 1)(({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` k) e. RR /\ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}` k) e. RR /\ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` k) <_ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}` k)))
590	589, 7	jctil 316	. . . . . . . . . 10 |- (f e. ({0, 2} ^m NN) -> (1 e. ZZ /\ A.k e. (ZZ>=` 1)(({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` k) e. RR /\ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}` k) e. RR /\ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` k) <_ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}` k))))
591		sumex 8241	. . . . . . . . . . 11 |- sum_k e. (ZZ>=` 1)((f` k) / (3^k)) e. _V
592		sumex 8241	. . . . . . . . . . 11 |- sum_k e. (ZZ>=` 1)(2 / (3^k)) e. _V
593	591, 592, 422, 548	iserzcmp 8402	. . . . . . . . . 10 |- ((((<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}) ~~> sum_k e. (ZZ>=` 1)((f` k) / (3^k)) /\ (<.1, + >. seq {<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}) ~~> sum_k e. (ZZ>=` 1)(2 / (3^k))) /\ (1 e. ZZ /\ A.k e. (ZZ>=` 1)(({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` k) e. RR /\ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}` k) e. RR /\ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = ((f` l) / (3^l)))}` k) <_ ({<.l, y>. | (l e. (ZZ>=` 1) /\ y = (2 / (3^l)))}` k)))) -> sum_k e. (ZZ>=` 1)((f` k) / (3^k)) <_ sum_k e. (ZZ>=` 1)(2 / (3^k)))
594	476, 561, 590, 593	syl21anc 1099	. . . . . . . . 9 |- (f e. ({0, 2} ^m NN) -> sum_k e. (ZZ>=` 1)((f` k) / (3^k)) <_ sum_k e. (ZZ>=` 1)(2 / (3^k)))
595	13	sumeq1i 8247	. . . . . . . . 9 |- sum_k e. NN ((f` k) / (3^k)) = sum_k e. (ZZ>=` 1)((f` k) / (3^k))
596	13	sumeq1i 8247	. . . . . . . . 9 |- sum_k e. NN (2 / (3^k)) = sum_k e. (ZZ>=` 1)(2 / (3^k))
597	594, 595, 596	3brtr4g 3369	. . . . . . . 8 |- (f e. ({0, 2} ^m NN) -> sum_k e. NN ((f` k) / (3^k)) <_ sum_k e. NN (2 / (3^k)))
598	132	a1i 8	. . . . . . . . . . . . 13 |- (k e. NN -> 2 e. CC)
599		expcl 7824	. . . . . . . . . . . . . 14 |- ((3 e. CC /\ k e. NN0) -> (3^k) e. CC)
600	599, 42, 38	sylancr 526	. . . . . . . . . . . . 13 |- (k e. NN -> (3^k) e. CC)
601	42	a1i 8	. . . . . . . . . . . . . 14 |- (k e. NN -> 3 e. CC)
602	44	a1i 8	. . . . . . . . . . . . . 14 |- (k e. NN -> 3 =/= 0)
603	601, 602, 38, 46	syl111anc 1100	. . . . . . . . . . . . 13 |- (k e. NN -> (3^k) =/= 0)
604		divrec 6922	. . . . . . . . . . . . 13 |- ((2 e. CC /\ (3^k) e. CC /\ (3^k) =/= 0) -> (2 / (3^k)) = (2 x. (1 / (3^k))))
605	598, 600, 603, 604	syl111anc 1100	. . . . . . . . . . . 12 |- (k e. NN -> (2 / (3^k)) = (2 x. (1 / (3^k))))
606		exprec 7837	. . . . . . . . . . . . . . 15 |- ((3 e. CC /\ 3 =/= 0 /\ k e. NN0) -> ((1 / 3)^k) = (1 / (3^k)))
607	606	eqcomd 1889	. . . . . . . . . . . . . 14 |- ((3 e. CC /\ 3 =/= 0 /\ k e. NN0) -> (1 / (3^k)) = ((1 / 3)^k))
608	601, 602, 38, 607	syl111anc 1100	. . . . . . . . . . . . 13 |- (k e. NN -> (1 / (3^k)) = ((1 / 3)^k))
609	608	opreq2d 4898	. . . . . . . . . . . 12 |- (k e. NN -> (2 x. (1 / (3^k))) = (2 x. ((1 / 3)^k)))
610	605, 609	eqtrd 1925	. . . . . . . . . . 11 |- (k e. NN -> (2 / (3^k)) = (2 x. ((1 / 3)^k)))
611	610	sumeq2i 8248	. . . . . . . . . 10 |- sum_k e. NN (2 / (3^k)) = sum_k e. NN (2 x. ((1 / 3)^k))
612	611	a1i 8	. . . . . . . . 9 |- (f e. ({0, 2} ^m NN) -> sum_k e. NN (2 / (3^k)) = sum_k e. NN (2 x. ((1 / 3)^k)))
613	132, 106, 123	3pm3.2i 1048	. . . . . . . . . . 11 |- (2 e. CC /\ (1 / 3) e. CC /\ (abs` (1 / 3)) < 1)
614	613	a1i 8	. . . . . . . . . 10 |- (f e. ({0, 2} ^m NN) -> (2 e. CC /\ (1 / 3) e. CC /\ (abs` (1 / 3)) < 1))
615		geoisum1c 8507	. . . . . . . . . 10 |- ((2 e. CC /\ (1 / 3) e. CC /\ (abs` (1 / 3)) < 1) -> sum_k e. NN (2 x. ((1 / 3)^k)) = ((2 x. (1 / 3)) / (1 - (1 / 3))))
616	614, 615	syl 12	. . . . . . . . 9 |- (f e. ({0, 2} ^m NN) -> sum_k e. NN (2 x. ((1 / 3)^k)) = ((2 x. (1 / 3)) / (1 - (1 / 3))))
617	106, 106	addcli 6473	. . . . . . . . . . . . . 14 |- ((1 / 3) + (1 / 3)) e. CC
618	106	3timesi 14523	. . . . . . . . . . . . . . 15 |- (3 x. (1 / 3)) = ((1 / 3) + ((1 / 3) + (1 / 3)))
619	42, 44	recidi 6916	. . . . . . . . . . . . . . 15 |- (3 x. (1 / 3)) = 1
620	618, 619	eqtr3i 1910	. . . . . . . . . . . . . 14 |- ((1 / 3) + ((1 / 3) + (1 / 3))) = 1
621	131, 106, 617, 620	subaddrii 6529	. . . . . . . . . . . . 13 |- (1 - (1 / 3)) = ((1 / 3) + (1 / 3))
622	106	2timesi 7187	. . . . . . . . . . . . 13 |- (2 x. (1 / 3)) = ((1 / 3) + (1 / 3))
623	621, 622	eqtr4i 1911	. . . . . . . . . . . 12 |- (1 - (1 / 3)) = (2 x. (1 / 3))
624	623	opreq2i 4893	. . . . . . . . . . 11 |- ((2 x. (1 / 3)) / (1 - (1 / 3))) = ((2 x. (1 / 3)) / (2 x. (1 / 3)))
625	132, 106	mulcli 6474	. . . . . . . . . . . 12 |- (2 x. (1 / 3)) e. CC
626	42	recne0zi 6914	. . . . . . . . . . . . . 14 |- (3 =/= 0 -> (1 / 3) =/= 0)
627	44, 626	ax-mp 7	. . . . . . . . . . . . 13 |- (1 / 3) =/= 0
628	132, 106, 133, 627	mulne0i 6888	. . . . . . . . . . . 12 |- (2 x. (1 / 3)) =/= 0
629	625, 628	dividi 6946	. . . . . . . . . . 11 |- ((2 x. (1 / 3)) / (2 x. (1 / 3))) = 1
630	624, 629	eqtri 1908	. . . . . . . . . 10 |- ((2 x. (1 / 3)) / (1 - (1 / 3))) = 1
631	630	a1i 8	. . . . . . . . 9 |- (f e. ({0, 2} ^m NN) -> ((2 x. (1 / 3)) / (1 - (1 / 3))) = 1)
632	612, 616, 631	3eqtrd 1929	. . . . . . . 8 |- (f e. ({0, 2} ^m NN) -> sum_k e. NN (2 / (3^k)) = 1)
633	597, 632	breqtrd 3361	. . . . . . 7 |- (f e. ({0, 2} ^m NN) -> sum_k e. NN ((f` k) / (3^k)) <_ 1)
634	388, 470, 633	3jca 1050	. . . . . 6 |- (f e. ({0, 2} ^m NN) -> (sum_k e. NN ((f` k) / (3^k)) e. RR* /\ 0 <_ sum_k e. NN ((f` k) / (3^k)) /\ sum_k e. NN ((f` k) / (3^k)) <_ 1))
635	6, 634	syl5cbir 228	. . . . 5 |- (f e. ({0, 2} ^m NN) -> (x = sum_k e. NN ((f` k) / (3^k)) -> (x e. RR* /\ 0 <_ x /\ x <_ 1)))
636	635	r19.23aiv 2211	. . . 4 |- (E.f e. ({0, 2} ^m NN)x = sum_k e. NN ((f` k) / (3^k)) -> (x e. RR* /\ 0 <_ x /\ x <_ 1))
637	2, 636	sylbi 216	. . 3 |- (x e. {x | E.f e. ({0, 2} ^m NN)x = sum_k e. NN ((f` k) / (3^k))} -> (x e. RR* /\ 0 <_ x /\ x <_ 1))
638		cntrsetlem.1	. . . 4 |- C = {x | E.f e. ({0, 2} ^m NN)x = sum_k e. NN ((f` k) / (3^k))}
639	638	eleq2i 1961	. . 3 |- (x e. C <-> x e. {x | E.f e. ({0, 2} ^m NN)x = sum_k e. NN ((f` k) / (3^k))})
640		rexr 6668	. . . . 5 |- (0 e. RR -> 0 e. RR*)
641	26, 640	ax-mp 7	. . . 4 |- 0 e. RR*
642		rexr 6668	. . . . 5 |- (1 e. RR -> 1 e. RR*)
643	70, 642	ax-mp 7	. . . 4 |- 1 e. RR*
644		elicc1 7550	. . . 4 |- ((0 e. RR* /\ 1 e. RR*) -> (x e. (0[,]1) <-> (x e. RR* /\ 0 <_ x /\ x <_ 1)))
645	641, 643, 644	mp2an 761	. . 3 |- (x e. (0[,]1) <-> (x e. RR* /\ 0 <_ x /\ x <_ 1))
646	637, 639, 645	3imtr4i 236	. 2 |- (x e. C -> x e. (0[,]1))
647	1, 646	mpgbir 1334	1 |- C C_ (0[,]1)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326  {cab 1871   =/= wne 2017  A.wral 2105  E.wrex 2106  _Vcvv 2292   C_ wss 2593  {cpr 3045  <.cop 3046   class class class wbr 3338  {copab 3395  -->wf 3994  ` cfv 3998  (class class class)co 4884   ^m cmap 5381  CCcc 6384  RRcr 6385  0cc0 6386  1c1 6387   + caddc 6389   x. cmul 6391   - cmin 6445  -ucneg 6446   / cdiv 6447   <_ cle 6448  NNcn 6449  NN0cn0 6450  ZZcz 6451  RR+crp 6453  RR*cxr 6652   < clt 6653  2c2 7145  3c3 7146  [,]cicc 7527  ZZ>=cuz 7586   seq1 cseq1 7720   seq cseqz 7774  ^cexp 7811  abscabs 8000   ~~> cli 8234  sum_csu 8239

This theorem is referenced by:  cntrset 15000

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1302  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-inf2 5731

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-1st 5020  df-2nd 5021  df-iota 5089  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-map 5383  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-sup 5664  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-ltr 6322  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398  df-lt 6399  df-sub 6511  df-neg 6513  df-pnf 6654  df-mnf 6655  df-xr 6656  df-ltxr 6657  df-le 6658  df-div 6892  df-n 7108  df-2 7154  df-3 7155  df-rp 7232  df-n0 7309  df-z 7345  df-fl 7463  df-icc 7531  df-uz 7587  df-fz 7638  df-seq1 7721  df-shft 7754  df-seqz 7776  df-seq0 7777  df-exp 7812  df-sqr 7920  df-re 8001  df-im 8002  df-cj 8003  df-abs 8004  df-clim 8235  df-sum 8240

Copyright terms: Public domain