Theorem nconstwlpolemgt0 13583

Description: Lemma for nconstwlpo 13585. If one of the terms of series is positive, so is the sum. (Contributed by Jim Kingdon, 26-Jul-2024.)

Hypotheses

Ref	Expression
nconstwlpolem0.g	|- ( ph -> G : NN --> { 0 , 1 } )
nconstwlpolem0.a	|- A = sum_ i e. NN ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) )
nconstwlpolemgt0.0	|- ( ph -> E. x e. NN ( G ` x ) = 1 )

Assertion

Ref	Expression
nconstwlpolemgt0	|- ( ph -> 0 < A )

Distinct variable groups:   x, A   i, G   ph, i, x

Allowed substitution hints:   A( i)   G( x)

Proof of Theorem nconstwlpolemgt0

Dummy variable n is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nconstwlpolemgt0.0	. 2 |- ( ph -> E. x e. NN ( G ` x ) = 1 )
2		1zzd 9173	. . . . . . 7 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> 1 e. ZZ )
3		simprl 521	. . . . . . . . . 10 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> x e. NN )
4	3	peano2nnd 8827	. . . . . . . . 9 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> ( x + 1 ) e. NN )
5	4	nnzd 9264	. . . . . . . 8 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> ( x + 1 ) e. ZZ )
6	5, 2	zsubcld 9270	. . . . . . 7 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> ( ( x + 1 ) - 1 ) e. ZZ )
7	2, 6	fzfigd 10308	. . . . . 6 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> ( 1 ... ( ( x + 1 ) - 1 ) ) e. Fin )
8		elfznn 9934	. . . . . . 7 |- ( i e. ( 1 ... ( ( x + 1 ) - 1 ) ) -> i e. NN )
9		2rp 9543	. . . . . . . . . . . 12 |- 2 e. RR+
10	9	a1i 9	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. NN ) -> 2 e. RR+ )
11		simpr 109	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. NN ) -> i e. NN )
12	11	nnzd 9264	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. NN ) -> i e. ZZ )
13	10, 12	rpexpcld 10552	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. NN ) -> ( 2 ^ i ) e. RR+ )
14	13	rpreccld 9592	. . . . . . . . 9 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. NN ) -> ( 1 / ( 2 ^ i ) ) e. RR+ )
15	14	rpred 9581	. . . . . . . 8 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. NN ) -> ( 1 / ( 2 ^ i ) ) e. RR )
16		0re 7857	. . . . . . . . . 10 |- 0 e. RR
17		1re 7856	. . . . . . . . . 10 |- 1 e. RR
18		prssi 3710	. . . . . . . . . 10 |- ( ( 0 e. RR /\ 1 e. RR ) -> { 0 , 1 } C_ RR )
19	16, 17, 18	mp2an 423	. . . . . . . . 9 |- { 0 , 1 } C_ RR
20		nconstwlpolem0.g	. . . . . . . . . . 11 |- ( ph -> G : NN --> { 0 , 1 } )
21	20	ad2antrr 480	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. NN ) -> G : NN --> { 0 , 1 } )
22	21, 11	ffvelrnd 5596	. . . . . . . . 9 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. NN ) -> ( G ` i ) e. { 0 , 1 } )
23	19, 22	sseldi 3122	. . . . . . . 8 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. NN ) -> ( G ` i ) e. RR )
24	15, 23	remulcld 7887	. . . . . . 7 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. NN ) -> ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) e. RR )
25	8, 24	sylan2 284	. . . . . 6 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. ( 1 ... ( ( x + 1 ) - 1 ) ) ) -> ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) e. RR )
26	7, 25	fsumrecl 11275	. . . . 5 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> sum_ i e. ( 1 ... ( ( x + 1 ) - 1 ) ) ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) e. RR )
27		eqid 2154	. . . . . 6 |- ( ZZ>= ` ( x + 1 ) ) = ( ZZ>= ` ( x + 1 ) )
28		eqid 2154	. . . . . . 7 |- ( n e. NN |-> ( ( 1 / ( 2 ^ n ) ) x. ( G ` n ) ) ) = ( n e. NN |-> ( ( 1 / ( 2 ^ n ) ) x. ( G ` n ) ) )
29		oveq2 5822	. . . . . . . . 9 |- ( n = i -> ( 2 ^ n ) = ( 2 ^ i ) )
30	29	oveq2d 5830	. . . . . . . 8 |- ( n = i -> ( 1 / ( 2 ^ n ) ) = ( 1 / ( 2 ^ i ) ) )
31		fveq2 5461	. . . . . . . 8 |- ( n = i -> ( G ` n ) = ( G ` i ) )
32	30, 31	oveq12d 5832	. . . . . . 7 |- ( n = i -> ( ( 1 / ( 2 ^ n ) ) x. ( G ` n ) ) = ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) )
33		eluznn 9489	. . . . . . . 8 |- ( ( ( x + 1 ) e. NN /\ i e. ( ZZ>= ` ( x + 1 ) ) ) -> i e. NN )
34	4, 33	sylan 281	. . . . . . 7 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. ( ZZ>= ` ( x + 1 ) ) ) -> i e. NN )
35	34, 24	syldan 280	. . . . . . 7 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. ( ZZ>= ` ( x + 1 ) ) ) -> ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) e. RR )
36	28, 32, 34, 35	fvmptd3 5554	. . . . . 6 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. ( ZZ>= ` ( x + 1 ) ) ) -> ( ( n e. NN |-> ( ( 1 / ( 2 ^ n ) ) x. ( G ` n ) ) ) ` i ) = ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) )
37	20, 28	trilpolemclim 13556	. . . . . . . 8 |- ( ph -> seq 1 ( + , ( n e. NN |-> ( ( 1 / ( 2 ^ n ) ) x. ( G ` n ) ) ) ) e. dom ~~> )
38	37	adantr 274	. . . . . . 7 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> seq 1 ( + , ( n e. NN |-> ( ( 1 / ( 2 ^ n ) ) x. ( G ` n ) ) ) ) e. dom ~~> )
39		nnuz 9453	. . . . . . . 8 |- NN = ( ZZ>= ` 1 )
40	28, 32, 11, 24	fvmptd3 5554	. . . . . . . . 9 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. NN ) -> ( ( n e. NN |-> ( ( 1 / ( 2 ^ n ) ) x. ( G ` n ) ) ) ` i ) = ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) )
41	24	recnd 7885	. . . . . . . . 9 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. NN ) -> ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) e. CC )
42	40, 41	eqeltrd 2231	. . . . . . . 8 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. NN ) -> ( ( n e. NN |-> ( ( 1 / ( 2 ^ n ) ) x. ( G ` n ) ) ) ` i ) e. CC )
43	39, 4, 42	iserex 11213	. . . . . . 7 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> ( seq 1 ( + , ( n e. NN |-> ( ( 1 / ( 2 ^ n ) ) x. ( G ` n ) ) ) ) e. dom ~~> <-> seq ( x + 1 ) ( + , ( n e. NN |-> ( ( 1 / ( 2 ^ n ) ) x. ( G ` n ) ) ) ) e. dom ~~> ) )
44	38, 43	mpbid 146	. . . . . 6 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> seq ( x + 1 ) ( + , ( n e. NN |-> ( ( 1 / ( 2 ^ n ) ) x. ( G ` n ) ) ) ) e. dom ~~> )
45	27, 5, 36, 35, 44	isumrecl 11303	. . . . 5 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> sum_ i e. ( ZZ>= ` ( x + 1 ) ) ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) e. RR )
46	3	nnzd 9264	. . . . . . . . . 10 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> x e. ZZ )
47		fzofig 10309	. . . . . . . . . 10 |- ( ( 1 e. ZZ /\ x e. ZZ ) -> ( 1..^ x ) e. Fin )
48	2, 46, 47	syl2anc 409	. . . . . . . . 9 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> ( 1..^ x ) e. Fin )
49		elfzo1 10067	. . . . . . . . . . 11 |- ( i e. ( 1..^ x ) <-> ( i e. NN /\ x e. NN /\ i < x ) )
50	49	simp1bi 997	. . . . . . . . . 10 |- ( i e. ( 1..^ x ) -> i e. NN )
51	50, 24	sylan2 284	. . . . . . . . 9 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. ( 1..^ x ) ) -> ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) e. RR )
52	48, 51	fsumrecl 11275	. . . . . . . 8 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> sum_ i e. ( 1..^ x ) ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) e. RR )
53	9	a1i 9	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> 2 e. RR+ )
54	53, 46	rpexpcld 10552	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> ( 2 ^ x ) e. RR+ )
55	54	rpreccld 9592	. . . . . . . . . 10 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> ( 1 / ( 2 ^ x ) ) e. RR+ )
56	55	rpred 9581	. . . . . . . . 9 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> ( 1 / ( 2 ^ x ) ) e. RR )
57	20	adantr 274	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> G : NN --> { 0 , 1 } )
58	57, 3	ffvelrnd 5596	. . . . . . . . . 10 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> ( G ` x ) e. { 0 , 1 } )
59	19, 58	sseldi 3122	. . . . . . . . 9 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> ( G ` x ) e. RR )
60	56, 59	remulcld 7887	. . . . . . . 8 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> ( ( 1 / ( 2 ^ x ) ) x. ( G ` x ) ) e. RR )
61	14	rpge0d 9585	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. NN ) -> 0 <_ ( 1 / ( 2 ^ i ) ) )
62		0le0 8901	. . . . . . . . . . . . 13 |- 0 <_ 0
63		simpr 109	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. NN ) /\ ( G ` i ) = 0 ) -> ( G ` i ) = 0 )
64	62, 63	breqtrrid 3998	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. NN ) /\ ( G ` i ) = 0 ) -> 0 <_ ( G ` i ) )
65		0le1 8335	. . . . . . . . . . . . 13 |- 0 <_ 1
66		simpr 109	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. NN ) /\ ( G ` i ) = 1 ) -> ( G ` i ) = 1 )
67	65, 66	breqtrrid 3998	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. NN ) /\ ( G ` i ) = 1 ) -> 0 <_ ( G ` i ) )
68		elpri 3579	. . . . . . . . . . . . 13 |- ( ( G ` i ) e. { 0 , 1 } -> ( ( G ` i ) = 0 \/ ( G ` i ) = 1 ) )
69	22, 68	syl 14	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. NN ) -> ( ( G ` i ) = 0 \/ ( G ` i ) = 1 ) )
70	64, 67, 69	mpjaodan 788	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. NN ) -> 0 <_ ( G ` i ) )
71	15, 23, 61, 70	mulge0d 8475	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. NN ) -> 0 <_ ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) )
72	50, 71	sylan2 284	. . . . . . . . 9 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. ( 1..^ x ) ) -> 0 <_ ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) )
73	48, 51, 72	fsumge0 11333	. . . . . . . 8 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> 0 <_ sum_ i e. ( 1..^ x ) ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) )
74	55	rpgt0d 9584	. . . . . . . . 9 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> 0 < ( 1 / ( 2 ^ x ) ) )
75		simprr 522	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> ( G ` x ) = 1 )
76	75	oveq2d 5830	. . . . . . . . . 10 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> ( ( 1 / ( 2 ^ x ) ) x. ( G ` x ) ) = ( ( 1 / ( 2 ^ x ) ) x. 1 ) )
77	56	recnd 7885	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> ( 1 / ( 2 ^ x ) ) e. CC )
78	77	mulid1d 7874	. . . . . . . . . 10 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> ( ( 1 / ( 2 ^ x ) ) x. 1 ) = ( 1 / ( 2 ^ x ) ) )
79	76, 78	eqtrd 2187	. . . . . . . . 9 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> ( ( 1 / ( 2 ^ x ) ) x. ( G ` x ) ) = ( 1 / ( 2 ^ x ) ) )
80	74, 79	breqtrrd 3988	. . . . . . . 8 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> 0 < ( ( 1 / ( 2 ^ x ) ) x. ( G ` x ) ) )
81	52, 60, 73, 80	addgegt0d 8373	. . . . . . 7 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> 0 < ( sum_ i e. ( 1..^ x ) ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) + ( ( 1 / ( 2 ^ x ) ) x. ( G ` x ) ) ) )
82		nfv 1505	. . . . . . . 8 |- F/ i ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) )
83		nfcv 2296	. . . . . . . 8 |- F/_ i ( ( 1 / ( 2 ^ x ) ) x. ( G ` x ) )
84		fzonel 10037	. . . . . . . . 9 |- -. x e. ( 1..^ x )
85	84	a1i 9	. . . . . . . 8 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> -. x e. ( 1..^ x ) )
86	50, 41	sylan2 284	. . . . . . . 8 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. ( 1..^ x ) ) -> ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) e. CC )
87		oveq2 5822	. . . . . . . . . 10 |- ( i = x -> ( 2 ^ i ) = ( 2 ^ x ) )
88	87	oveq2d 5830	. . . . . . . . 9 |- ( i = x -> ( 1 / ( 2 ^ i ) ) = ( 1 / ( 2 ^ x ) ) )
89		fveq2 5461	. . . . . . . . 9 |- ( i = x -> ( G ` i ) = ( G ` x ) )
90	88, 89	oveq12d 5832	. . . . . . . 8 |- ( i = x -> ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) = ( ( 1 / ( 2 ^ x ) ) x. ( G ` x ) ) )
91	60	recnd 7885	. . . . . . . 8 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> ( ( 1 / ( 2 ^ x ) ) x. ( G ` x ) ) e. CC )
92	82, 83, 48, 3, 85, 86, 90, 91	fsumsplitsn 11284	. . . . . . 7 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> sum_ i e. ( ( 1..^ x ) u. { x } ) ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) = ( sum_ i e. ( 1..^ x ) ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) + ( ( 1 / ( 2 ^ x ) ) x. ( G ` x ) ) ) )
93	81, 92	breqtrrd 3988	. . . . . 6 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> 0 < sum_ i e. ( ( 1..^ x ) u. { x } ) ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) )
94	3	nncnd 8826	. . . . . . . . . 10 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> x e. CC )
95		1cnd 7873	. . . . . . . . . 10 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> 1 e. CC )
96	94, 95	pncand 8166	. . . . . . . . 9 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> ( ( x + 1 ) - 1 ) = x )
97	96	oveq2d 5830	. . . . . . . 8 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> ( 1 ... ( ( x + 1 ) - 1 ) ) = ( 1 ... x ) )
98	3, 39	eleqtrdi 2247	. . . . . . . . 9 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> x e. ( ZZ>= ` 1 ) )
99		fzisfzounsn 10113	. . . . . . . . 9 |- ( x e. ( ZZ>= ` 1 ) -> ( 1 ... x ) = ( ( 1..^ x ) u. { x } ) )
100	98, 99	syl 14	. . . . . . . 8 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> ( 1 ... x ) = ( ( 1..^ x ) u. { x } ) )
101	97, 100	eqtrd 2187	. . . . . . 7 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> ( 1 ... ( ( x + 1 ) - 1 ) ) = ( ( 1..^ x ) u. { x } ) )
102	101	sumeq1d 11240	. . . . . 6 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> sum_ i e. ( 1 ... ( ( x + 1 ) - 1 ) ) ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) = sum_ i e. ( ( 1..^ x ) u. { x } ) ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) )
103	93, 102	breqtrrd 3988	. . . . 5 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> 0 < sum_ i e. ( 1 ... ( ( x + 1 ) - 1 ) ) ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) )
104	34, 15	syldan 280	. . . . . . 7 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. ( ZZ>= ` ( x + 1 ) ) ) -> ( 1 / ( 2 ^ i ) ) e. RR )
105	34, 23	syldan 280	. . . . . . 7 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. ( ZZ>= ` ( x + 1 ) ) ) -> ( G ` i ) e. RR )
106	34, 14	syldan 280	. . . . . . . 8 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. ( ZZ>= ` ( x + 1 ) ) ) -> ( 1 / ( 2 ^ i ) ) e. RR+ )
107	106	rpge0d 9585	. . . . . . 7 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. ( ZZ>= ` ( x + 1 ) ) ) -> 0 <_ ( 1 / ( 2 ^ i ) ) )
108	34, 70	syldan 280	. . . . . . 7 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. ( ZZ>= ` ( x + 1 ) ) ) -> 0 <_ ( G ` i ) )
109	104, 105, 107, 108	mulge0d 8475	. . . . . 6 |- ( ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) /\ i e. ( ZZ>= ` ( x + 1 ) ) ) -> 0 <_ ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) )
110	27, 5, 36, 35, 44, 109	isumge0 11304	. . . . 5 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> 0 <_ sum_ i e. ( ZZ>= ` ( x + 1 ) ) ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) )
111	26, 45, 103, 110	addgtge0d 8374	. . . 4 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> 0 < ( sum_ i e. ( 1 ... ( ( x + 1 ) - 1 ) ) ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) + sum_ i e. ( ZZ>= ` ( x + 1 ) ) ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) ) )
112	39, 27, 4, 40, 41, 38	isumsplit 11365	. . . 4 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> sum_ i e. NN ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) = ( sum_ i e. ( 1 ... ( ( x + 1 ) - 1 ) ) ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) + sum_ i e. ( ZZ>= ` ( x + 1 ) ) ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) ) )
113	111, 112	breqtrrd 3988	. . 3 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> 0 < sum_ i e. NN ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) ) )
114		nconstwlpolem0.a	. . 3 |- A = sum_ i e. NN ( ( 1 / ( 2 ^ i ) ) x. ( G ` i ) )
115	113, 114	breqtrrdi 4002	. 2 |- ( ( ph /\ ( x e. NN /\ ( G ` x ) = 1 ) ) -> 0 < A )
116	1, 115	rexlimddv 2576	1 |- ( ph -> 0 < A )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   \/ wo 698   = wceq 1332   e. wcel 2125   E.wrex 2433   u. cun 3096   C_ wss 3098   {csn 3556   {cpr 3557   class class class wbr 3961   |-> cmpt 4021   dom cdm 4579   -->wf 5159   ` cfv 5163  (class class class)co 5814   Fincfn 6674   CCcc 7709   RRcr 7710   0cc0 7711   1c1 7712   + caddc 7714   x. cmul 7716   < clt 7891   <_ cle 7892   - cmin 8025   / cdiv 8524   NNcn 8812   2c2 8863   ZZcz 9146   ZZ>=cuz 9418   RR+crp 9538   ...cfz 9890  ..^cfzo 10019   seqcseq 10322   ^cexp 10396   ~~> cli 11152   sum_csu 11227

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-13 2127  ax-14 2128  ax-ext 2136  ax-coll 4075  ax-sep 4078  ax-nul 4086  ax-pow 4130  ax-pr 4164  ax-un 4388  ax-setind 4490  ax-iinf 4541  ax-cnex 7802  ax-resscn 7803  ax-1cn 7804  ax-1re 7805  ax-icn 7806  ax-addcl 7807  ax-addrcl 7808  ax-mulcl 7809  ax-mulrcl 7810  ax-addcom 7811  ax-mulcom 7812  ax-addass 7813  ax-mulass 7814  ax-distr 7815  ax-i2m1 7816  ax-0lt1 7817  ax-1rid 7818  ax-0id 7819  ax-rnegex 7820  ax-precex 7821  ax-cnre 7822  ax-pre-ltirr 7823  ax-pre-ltwlin 7824  ax-pre-lttrn 7825  ax-pre-apti 7826  ax-pre-ltadd 7827  ax-pre-mulgt0 7828  ax-pre-mulext 7829  ax-arch 7830  ax-caucvg 7831

This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1740  df-eu 2006  df-mo 2007  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-ne 2325  df-nel 2420  df-ral 2437  df-rex 2438  df-reu 2439  df-rmo 2440  df-rab 2441  df-v 2711  df-sbc 2934  df-csb 3028  df-dif 3100  df-un 3102  df-in 3104  df-ss 3111  df-nul 3391  df-if 3502  df-pw 3541  df-sn 3562  df-pr 3563  df-op 3565  df-uni 3769  df-int 3804  df-iun 3847  df-br 3962  df-opab 4022  df-mpt 4023  df-tr 4059  df-id 4248  df-po 4251  df-iso 4252  df-iord 4321  df-on 4323  df-ilim 4324  df-suc 4326  df-iom 4544  df-xp 4585  df-rel 4586  df-cnv 4587  df-co 4588  df-dm 4589  df-rn 4590  df-res 4591  df-ima 4592  df-iota 5128  df-fun 5165  df-fn 5166  df-f 5167  df-f1 5168  df-fo 5169  df-f1o 5170  df-fv 5171  df-isom 5172  df-riota 5770  df-ov 5817  df-oprab 5818  df-mpo 5819  df-1st 6078  df-2nd 6079  df-recs 6242  df-irdg 6307  df-frec 6328  df-1o 6353  df-oadd 6357  df-er 6469  df-en 6675  df-dom 6676  df-fin 6677  df-pnf 7893  df-mnf 7894  df-xr 7895  df-ltxr 7896  df-le 7897  df-sub 8027  df-neg 8028  df-reap 8429  df-ap 8436  df-div 8525  df-inn 8813  df-2 8871  df-3 8872  df-4 8873  df-n0 9070  df-z 9147  df-uz 9419  df-q 9507  df-rp 9539  df-ico 9776  df-fz 9891  df-fzo 10020  df-seqfrec 10323  df-exp 10397  df-ihash 10627  df-cj 10719  df-re 10720  df-im 10721  df-rsqrt 10875  df-abs 10876  df-clim 11153  df-sumdc 11228

This theorem is referenced by:  nconstwlpolem  13584