plyeq0lem - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > plyeq0lem		Structured version Unicode version

Theorem plyeq0lem 22711

Description: Lemma for plyeq0 22712. If

is the coefficient function for a nonzero polynomial such that

for every

and

is the nonzero leading coefficient, then the function

is a sum of powers of

, and so the limit of this function as

is the constant term,

. But

everywhere, so this limit is also equal to zero so that

, a contradiction. (Contributed by Mario Carneiro, 22-Jul-2014.)

**Hypotheses**
Ref	Expression
plyeq0.1
plyeq0.2
plyeq0.3
plyeq0.4
plyeq0.5
plyeq0.6	$\$
plyeq0.7	$\$

**Assertion**
Ref	Expression
plyeq0lem

Distinct variable groups:

Allowed substitution hint:

(

)

Proof of Theorem plyeq0lem Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnuz 11054	. . . . . 6
2		1zzd 10830	. . . . . 6
3		fzfid 12005	. . . . . 6
4		1zzd 10830	. . . . . . . . . 10 $/\$ $/\$
5		plyeq0.3	. . . . . . . . . . . . . . . . 17
6		plyeq0.1	. . . . . . . . . . . . . . . . . . . 20
7		0cn 9517	. . . . . . . . . . . . . . . . . . . . . 22
8	7	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
9	8	snssd 4102	. . . . . . . . . . . . . . . . . . . 20
10	6, 9	unssd 3607	. . . . . . . . . . . . . . . . . . 19
11		cnex 9502	. . . . . . . . . . . . . . . . . . 19
12		ssexg 4524	. . . . . . . . . . . . . . . . . . 19 $/\$
13	10, 11, 12	sylancl 660	. . . . . . . . . . . . . . . . . 18
14		nn0ex 10736	. . . . . . . . . . . . . . . . . 18
15		elmapg 7369	. . . . . . . . . . . . . . . . . 18 $/\$
16	13, 14, 15	sylancl 660	. . . . . . . . . . . . . . . . 17
17	5, 16	mpbid 210	. . . . . . . . . . . . . . . 16
18	17, 10	fssd 5661	. . . . . . . . . . . . . . 15
19		elfznn0 11711	. . . . . . . . . . . . . . 15
20		ffvelrn 5944	. . . . . . . . . . . . . . 15 $/\$
21	18, 19, 20	syl2an 475	. . . . . . . . . . . . . 14 $/\$
22	21	adantr 463	. . . . . . . . . . . . 13 $/\$ $/\$
23	22	abscld 13288	. . . . . . . . . . . 12 $/\$ $/\$
24	23	recnd 9551	. . . . . . . . . . 11 $/\$ $/\$
25		divcnv 13686	. . . . . . . . . . 11
26	24, 25	syl 16	. . . . . . . . . 10 $/\$ $/\$
27		nnex 10476	. . . . . . . . . . . 12
28	27	mptex 6060	. . . . . . . . . . 11
29	28	a1i 11	. . . . . . . . . 10 $/\$ $/\$
30		oveq2 6222	. . . . . . . . . . . . 13
31		eqid 2392	. . . . . . . . . . . . 13
32		ovex 6242	. . . . . . . . . . . . 13
33	30, 31, 32	fvmpt 5870	. . . . . . . . . . . 12
34	33	adantl 464	. . . . . . . . . . 11 $/\$ $/\$ $/\$
35		nndivre 10506	. . . . . . . . . . . 12 $/\$
36	23, 35	sylan 469	. . . . . . . . . . 11 $/\$ $/\$ $/\$
37	34, 36	eqeltrd 2480	. . . . . . . . . 10 $/\$ $/\$ $/\$
38		oveq1 6221	. . . . . . . . . . . . . 14
39	38	oveq2d 6230	. . . . . . . . . . . . 13
40		eqid 2392	. . . . . . . . . . . . 13
41		ovex 6242	. . . . . . . . . . . . 13
42	39, 40, 41	fvmpt 5870	. . . . . . . . . . . 12
43	42	adantl 464	. . . . . . . . . . 11 $/\$ $/\$ $/\$
44	21	ad2antrr 723	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
45	44	abscld 13288	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
46		nnrp 11166	. . . . . . . . . . . . . . 15
47	46	adantl 464	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
48		elfzelz 11627	. . . . . . . . . . . . . . . 16
49		cnvimass 5282	. . . . . . . . . . . . . . . . . . 19 $\$
50		fdm 5656	. . . . . . . . . . . . . . . . . . . 20
51	17, 50	syl 16	. . . . . . . . . . . . . . . . . . 19
52	49, 51	syl5sseq 3478	. . . . . . . . . . . . . . . . . 18 $\$
53		plyeq0.6	. . . . . . . . . . . . . . . . . . 19 $\$
54		nn0ssz 10820	. . . . . . . . . . . . . . . . . . . . 21
55	52, 54	syl6ss 3442	. . . . . . . . . . . . . . . . . . . 20 $\$
56		plyeq0.7	. . . . . . . . . . . . . . . . . . . 20 $\$
57		plyeq0.2	. . . . . . . . . . . . . . . . . . . . . 22
58	57	nn0red 10788	. . . . . . . . . . . . . . . . . . . . 21
59	52	sselda 3430	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$
60		plyeq0.4	. . . . . . . . . . . . . . . . . . . . . . . . 25
61		plyco0 22693	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
62	57, 18, 61	syl2anc 659	. . . . . . . . . . . . . . . . . . . . . . . . 25
63	60, 62	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . 24
64	63	adantr 463	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$
65		ffn 5652	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
66	17, 65	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . 26
67		elpreima 5922	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $\$
68	66, 67	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$ $\$
69	68	simplbda 622	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$ $\$
70		eldifsni 4083	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
71	69, 70	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$
72		fveq2 5787	. . . . . . . . . . . . . . . . . . . . . . . . . 26
73	72	neeq1d 2669	. . . . . . . . . . . . . . . . . . . . . . . . 25
74		breq1 4383	. . . . . . . . . . . . . . . . . . . . . . . . 25
75	73, 74	imbi12d 318	. . . . . . . . . . . . . . . . . . . . . . . 24
76	75	rspcv 3144	. . . . . . . . . . . . . . . . . . . . . . 23
77	59, 64, 71, 76	syl3c 61	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$
78	77	ralrimiva 2806	. . . . . . . . . . . . . . . . . . . . 21 $\$
79		breq2 4384	. . . . . . . . . . . . . . . . . . . . . . 23
80	79	ralbidv 2831	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
81	80	rspcev 3148	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $\$
82	58, 78, 81	syl2anc 659	. . . . . . . . . . . . . . . . . . . 20 $\$
83		suprzcl 10877	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$ $\$ $/\$ $\$ $\$ $\$
84	55, 56, 82, 83	syl3anc 1226	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
85	53, 84	syl5eqel 2484	. . . . . . . . . . . . . . . . . 18 $\$
86	52, 85	sseldd 3431	. . . . . . . . . . . . . . . . 17
87	86	nn0zd 10900	. . . . . . . . . . . . . . . 16
88		zsubcl 10841	. . . . . . . . . . . . . . . 16 $/\$
89	48, 87, 88	syl2anr 476	. . . . . . . . . . . . . . 15 $/\$
90	89	ad2antrr 723	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
91	47, 90	rpexpcld 12254	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
92	91	rpred 11195	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
93	45, 92	remulcld 9553	. . . . . . . . . . 11 $/\$ $/\$ $/\$
94	43, 93	eqeltrd 2480	. . . . . . . . . 10 $/\$ $/\$ $/\$
95		nnrecre 10507	. . . . . . . . . . . . 13
96	95	adantl 464	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
97	22	absge0d 13296	. . . . . . . . . . . . 13 $/\$ $/\$
98	97	adantr 463	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
99		nnre 10477	. . . . . . . . . . . . . . 15
100	99	adantl 464	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
101		nnge1 10496	. . . . . . . . . . . . . . 15
102	101	adantl 464	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
103		1red 9540	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
104	90	zred 10902	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
105		simplr 753	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
106	48	adantl 464	. . . . . . . . . . . . . . . . . . . . 21 $/\$
107	106	ad2antrr 723	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
108	87	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
109		zltp1le 10848	. . . . . . . . . . . . . . . . . . . 20 $/\$
110	107, 108, 109	syl2anc 659	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
111	105, 110	mpbid 210	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
112	19	adantl 464	. . . . . . . . . . . . . . . . . . . . 21 $/\$
113	112	nn0red 10788	. . . . . . . . . . . . . . . . . . . 20 $/\$
114	113	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
115	86	adantr 463	. . . . . . . . . . . . . . . . . . . . 21 $/\$
116	115	nn0red 10788	. . . . . . . . . . . . . . . . . . . 20 $/\$
117	116	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
118	114, 103, 117	leaddsub2d 10089	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
119	111, 118	mpbid 210	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
120	113	recnd 9551	. . . . . . . . . . . . . . . . . . 19 $/\$
121	120	ad2antrr 723	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
122	116	recnd 9551	. . . . . . . . . . . . . . . . . . 19 $/\$
123	122	ad2antrr 723	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
124	121, 123	negsubdi2d 9878	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
125	119, 124	breqtrrd 4406	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
126	103, 104, 125	lenegcon2d 10070	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
127		neg1z 10835	. . . . . . . . . . . . . . . 16
128		eluz 11032	. . . . . . . . . . . . . . . 16 $/\$
129	90, 127, 128	sylancl 660	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
130	126, 129	mpbird 232	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
131	100, 102, 130	leexp2ad 12263	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
132		nncn 10478	. . . . . . . . . . . . . . 15
133	132	adantl 464	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
134		expn1 12098	. . . . . . . . . . . . . 14
135	133, 134	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
136	131, 135	breqtrd 4404	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
137	92, 96, 45, 98, 136	lemul2ad 10420	. . . . . . . . . . 11 $/\$ $/\$ $/\$
138	24	adantr 463	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
139		nnne0 10503	. . . . . . . . . . . . . 14
140	139	adantl 464	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
141	138, 133, 140	divrecd 10258	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
142	34, 141	eqtrd 2433	. . . . . . . . . . 11 $/\$ $/\$ $/\$
143	137, 43, 142	3brtr4d 4410	. . . . . . . . . 10 $/\$ $/\$ $/\$
144	91	rpge0d 11199	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
145	45, 92, 98, 144	mulge0d 10064	. . . . . . . . . . 11 $/\$ $/\$ $/\$
146	145, 43	breqtrrd 4406	. . . . . . . . . 10 $/\$ $/\$ $/\$
147	1, 4, 26, 29, 37, 94, 143, 146	climsqz2 13485	. . . . . . . . 9 $/\$ $/\$
148	27	mptex 6060	. . . . . . . . . . 11
149	148	a1i 11	. . . . . . . . . 10 $/\$ $/\$
150	38	oveq2d 6230	. . . . . . . . . . . . . . 15
151		eqid 2392	. . . . . . . . . . . . . . 15
152		ovex 6242	. . . . . . . . . . . . . . 15
153	150, 151, 152	fvmpt 5870	. . . . . . . . . . . . . 14
154	153	ad2antlr 724	. . . . . . . . . . . . 13 $/\$ $/\$
155	18	adantr 463	. . . . . . . . . . . . . . 15 $/\$
156	155, 19, 20	syl2an 475	. . . . . . . . . . . . . 14 $/\$ $/\$
157	132	ad2antlr 724	. . . . . . . . . . . . . . 15 $/\$ $/\$
158	139	ad2antlr 724	. . . . . . . . . . . . . . 15 $/\$ $/\$
159	87	adantr 463	. . . . . . . . . . . . . . . 16 $/\$
160	48, 159, 88	syl2anr 476	. . . . . . . . . . . . . . 15 $/\$ $/\$
161	157, 158, 160	expclzd 12236	. . . . . . . . . . . . . 14 $/\$ $/\$
162	156, 161	mulcld 9545	. . . . . . . . . . . . 13 $/\$ $/\$
163	154, 162	eqeltrd 2480	. . . . . . . . . . . 12 $/\$ $/\$
164	163	an32s 802	. . . . . . . . . . 11 $/\$ $/\$
165	164	adantlr 712	. . . . . . . . . 10 $/\$ $/\$ $/\$
166	92	recnd 9551	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
167	44, 166	absmuld 13306	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
168	92, 144	absidd 13275	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
169	168	oveq2d 6230	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
170	167, 169	eqtrd 2433	. . . . . . . . . . 11 $/\$ $/\$ $/\$
171	153	adantl 464	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
172	171	fveq2d 5791	. . . . . . . . . . 11 $/\$ $/\$ $/\$
173	170, 172, 43	3eqtr4rd 2444	. . . . . . . . . 10 $/\$ $/\$ $/\$
174	1, 4, 149, 29, 165, 173	climabs0 13429	. . . . . . . . 9 $/\$ $/\$
175	147, 174	mpbird 232	. . . . . . . 8 $/\$ $/\$
176	113	adantr 463	. . . . . . . . . . 11 $/\$ $/\$
177		simpr 459	. . . . . . . . . . 11 $/\$ $/\$
178	176, 177	ltned 9650	. . . . . . . . . 10 $/\$ $/\$
179		elsn 3971	. . . . . . . . . . 11
180	179	necon3bbii 2653	. . . . . . . . . 10
181	178, 180	sylibr 212	. . . . . . . . 9 $/\$ $/\$
182	181	iffalsed 3881	. . . . . . . 8 $/\$ $/\$
183	175, 182	breqtrrd 4406	. . . . . . 7 $/\$ $/\$
184		nncn 10478	. . . . . . . . . . . . . . 15
185	184	ad2antlr 724	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
186		nnne0 10503	. . . . . . . . . . . . . . 15
187	186	ad2antlr 724	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
188	89	ad3antrrr 727	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
189	185, 187, 188	expclzd 12236	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
190	189	mul02d 9707	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
191		simpr 459	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
192	191	oveq1d 6229	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
193	191	ifeq1d 3888	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
194		ifid 3907	. . . . . . . . . . . . 13
195	193, 194	syl6eq 2449	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
196	190, 192, 195	3eqtr4d 2443	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
197	21	adantr 463	. . . . . . . . . . . . . 14 $/\$ $/\$
198	197	ad2antrr 723	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
199	198	mulid1d 9542	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
200		nn0ssre 10734	. . . . . . . . . . . . . . . . . . . . . . . 24
201	52, 200	syl6ss 3442	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
202	201	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$
203	56	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$
204	82	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$
205	19	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
206		ffvelrn 5944	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
207	17, 19, 206	syl2an 475	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
208	207	anim1i 566	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
209		eldifsn 4082	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$
210	208, 209	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$
211		difun2 3836	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
212	210, 211	syl6eleq 2490	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$
213		elpreima 5922	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$ $\$
214	66, 213	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$ $\$
215	214	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$ $/\$ $\$
216	205, 212, 215	mpbir2and 920	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$
217		suprub 10438	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$
218	202, 203, 204, 216, 217	syl31anc 1229	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
219	218, 53	syl6breqr 4420	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
220	219	adantlr 712	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
221	220	adantlr 712	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
222		simpllr 758	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
223	113	ad3antrrr 727	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
224	116	ad3antrrr 727	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
225	223, 224	letri3d 9656	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
226	221, 222, 225	mpbir2and 920	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
227	226	oveq1d 6229	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
228	122	ad3antrrr 727	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
229	228	subidd 9850	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
230	227, 229	eqtrd 2433	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
231	230	oveq2d 6230	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
232	184	ad2antlr 724	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
233	232	exp0d 12225	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
234	231, 233	eqtrd 2433	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
235	234	oveq2d 6230	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
236	226, 179	sylibr 212	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
237	236	iftrued 3878	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
238	199, 235, 237	3eqtr4d 2443	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
239	196, 238	pm2.61dane 2710	. . . . . . . . . 10 $/\$ $/\$ $/\$
240	239	mpteq2dva 4466	. . . . . . . . 9 $/\$ $/\$
241		fconstmpt 4970	. . . . . . . . 9
242	240, 241	syl6eqr 2451	. . . . . . . 8 $/\$ $/\$
243		ifcl 3912	. . . . . . . . . 10 $/\$
244	197, 7, 243	sylancl 660	. . . . . . . . 9 $/\$ $/\$
245		1z 10829	. . . . . . . . 9
246	1	eqimss2i 3485	. . . . . . . . . 10
247	246, 27	climconst2 13392	. . . . . . . . 9 $/\$
248	244, 245, 247	sylancl 660	. . . . . . . 8 $/\$ $/\$
249	242, 248	eqbrtrd 4400	. . . . . . 7 $/\$ $/\$
250	183, 249, 113, 116	ltlecasei 9621	. . . . . 6 $/\$
251		snex 4616	. . . . . . . 8
252	27, 251	xpex 6521	. . . . . . 7
253	252	a1i 11	. . . . . 6
254	164	anasss 645	. . . . . 6 $/\$ $/\$
255		plyeq0.5	. . . . . . . . . . . 12
256	255	fveq1d 5789	. . . . . . . . . . 11
257	256	adantr 463	. . . . . . . . . 10 $/\$
258	132	adantl 464	. . . . . . . . . . 11 $/\$
259		0pval 22182	. . . . . . . . . . 11
260	258, 259	syl 16	. . . . . . . . . 10 $/\$
261		oveq1 6221	. . . . . . . . . . . . . 14
262	261	oveq2d 6230	. . . . . . . . . . . . 13
263	262	sumeq2sdv 13547	. . . . . . . . . . . 12
264		eqid 2392	. . . . . . . . . . . 12
265		sumex 13531	. . . . . . . . . . . 12
266	263, 264, 265	fvmpt 5870	. . . . . . . . . . 11
267	258, 266	syl 16	. . . . . . . . . 10 $/\$
268	257, 260, 267	3eqtr3d 2441	. . . . . . . . 9 $/\$
269	268	oveq1d 6229	. . . . . . . 8 $/\$
270		expcl 12106	. . . . . . . . . 10 $/\$
271	132, 86, 270	syl2anr 476	. . . . . . . . 9 $/\$
272	139	adantl 464	. . . . . . . . . 10 $/\$
273	258, 272, 159	expne0d 12237	. . . . . . . . 9 $/\$
274	271, 273	div0d 10254	. . . . . . . 8 $/\$
275		fzfid 12005	. . . . . . . . 9 $/\$
276		expcl 12106	. . . . . . . . . . 11 $/\$
277	258, 19, 276	syl2an 475	. . . . . . . . . 10 $/\$ $/\$
278	156, 277	mulcld 9545	. . . . . . . . 9 $/\$ $/\$
279	275, 271, 278, 273	fsumdivc 13622	. . . . . . . 8 $/\$
280	269, 274, 279	3eqtr3d 2441	. . . . . . 7 $/\$
281		fvconst2g 6041	. . . . . . . 8 $/\$
282	8, 281	sylan 469	. . . . . . 7 $/\$
283	159	adantr 463	. . . . . . . . . . 11 $/\$ $/\$
284	48	adantl 464	. . . . . . . . . . 11 $/\$ $/\$
285	157, 158, 283, 284	expsubd 12242	. . . . . . . . . 10 $/\$ $/\$
286	285	oveq2d 6230	. . . . . . . . 9 $/\$ $/\$
287	271	adantr 463	. . . . . . . . . 10 $/\$ $/\$
288	273	adantr 463	. . . . . . . . . 10 $/\$ $/\$
289	156, 277, 287, 288	divassd 10290	. . . . . . . . 9 $/\$ $/\$
290	286, 154, 289	3eqtr4d 2443	. . . . . . . 8 $/\$ $/\$
291	290	sumeq2dv 13546	. . . . . . 7 $/\$
292	280, 282, 291	3eqtr4d 2443	. . . . . 6 $/\$
293	1, 2, 3, 250, 253, 254, 292	climfsum 13655	. . . . 5
294		suprleub 10441	. . . . . . . . . . . 12 $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $\$
295	201, 56, 82, 58, 294	syl31anc 1229	. . . . . . . . . . 11 $\$ $\$
296	78, 295	mpbird 232	. . . . . . . . . 10 $\$
297	53, 296	syl5eqbr 4413	. . . . . . . . 9
298		nn0uz 11053	. . . . . . . . . . 11
299	86, 298	syl6eleq 2490	. . . . . . . . . 10
300	57	nn0zd 10900	. . . . . . . . . 10
301		elfz5 11619	. . . . . . . . . 10 $/\$
302	299, 300, 301	syl2anc 659	. . . . . . . . 9
303	297, 302	mpbird 232	. . . . . . . 8
304	303	snssd 4102	. . . . . . 7
305	18, 86	ffvelrnd 5947	. . . . . . . . 9
306		elsni 3982	. . . . . . . . . . 11
307	306	fveq2d 5791	. . . . . . . . . 10
308	307	eleq1d 2461	. . . . . . . . 9
309	305, 308	syl5ibrcom 222	. . . . . . . 8
310	309	ralrimiv 2804	. . . . . . 7
311	3	olcd 391	. . . . . . 7 $\/$
312		sumss2 13569	. . . . . . 7 $/\$ $/\$ $\/$
313	304, 310, 311, 312	syl21anc 1225	. . . . . 6
314		ltso 9594	. . . . . . . . 9
315	314	supex 7855	. . . . . . . 8 $\$
316	53, 315	eqeltri 2476	. . . . . . 7
317		fveq2 5787	. . . . . . . 8
318	317	sumsn 13584	. . . . . . 7 $/\$
319	316, 305, 318	sylancr 661	. . . . . 6
320	313, 319	eqtr3d 2435	. . . . 5
321	293, 320	breqtrd 4404	. . . 4
322	246, 27	climconst2 13392	. . . . 5 $/\$
323	7, 245, 322	mp2an 670	. . . 4
324		climuni 13396	. . . 4 $/\$
325	321, 323, 324	sylancl 660	. . 3
326		fvex 5797	. . . 4
327	326	elsnc 3981	. . 3
328	325, 327	sylibr 212	. 2
329		elpreima 5922	. . . . . 6 $\$ $/\$ $\$
330	66, 329	syl 16	. . . . 5 $\$ $/\$ $\$
331	85, 330	mpbid 210	. . . 4 $/\$ $\$
332	331	simprd 461	. . 3 $\$
333	332	eldifbd 3415	. 2
334	328, 333	pm2.65i 173	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 366 $/\$ wa 367

wceq 1399

wcel 1836

wne 2587

wral 2742

wrex 2743

cvv 3047 $\$ cdif 3399

cun 3400

wss 3402

c0 3724

cif 3870

csn 3957 class class class wbr 4380

cmpt 4438

cxp 4924

ccnv 4925

cdm 4926

cima 4929

wfn 5504

wf 5505

cfv 5509 (class class class)co 6214

cmap 7356

cfn 7453

csup 7833

cc 9419

cr 9420

cc0 9421

c1 9422

caddc 9424

cmul 9426

clt 9557

cle 9558

cmin 9736

cneg 9737

cdiv 10141

cn 10470

cn0 10730

cz 10799

cuz 11019

crp 11157

cfz 11611

cexp 12088

cabs 13088

cli 13328

csu 13529

c0p 22180

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1633 ax-4 1646 ax-5 1719 ax-6 1765 ax-7 1808 ax-8 1838 ax-9 1840 ax-10 1855 ax-11 1860 ax-12 1872 ax-13 2016 ax-ext 2370 ax-rep 4491 ax-sep 4501 ax-nul 4509 ax-pow 4556 ax-pr 4614 ax-un 6509 ax-inf2 7990 ax-cnex 9477 ax-resscn 9478 ax-1cn 9479 ax-icn 9480 ax-addcl 9481 ax-addrcl 9482 ax-mulcl 9483 ax-mulrcl 9484 ax-mulcom 9485 ax-addass 9486 ax-mulass 9487 ax-distr 9488 ax-i2m1 9489 ax-1ne0 9490 ax-1rid 9491 ax-rnegex 9492 ax-rrecex 9493 ax-cnre 9494 ax-pre-lttri 9495 ax-pre-lttrn 9496 ax-pre-ltadd 9497 ax-pre-mulgt0 9498 ax-pre-sup 9499 ax-addf 9500

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1402 df-fal 1405 df-ex 1628 df-nf 1632 df-sb 1758 df-eu 2232 df-mo 2233 df-clab 2378 df-cleq 2384 df-clel 2387 df-nfc 2542 df-ne 2589 df-nel 2590 df-ral 2747 df-rex 2748 df-reu 2749 df-rmo 2750 df-rab 2751 df-v 3049 df-sbc 3266 df-csb 3362 df-dif 3405 df-un 3407 df-in 3409 df-ss 3416 df-pss 3418 df-nul 3725 df-if 3871 df-pw 3942 df-sn 3958 df-pr 3960 df-tp 3962 df-op 3964 df-uni 4177 df-int 4213 df-iun 4258 df-br 4381 df-opab 4439 df-mpt 4440 df-tr 4474 df-eprel 4718 df-id 4722 df-po 4727 df-so 4728 df-fr 4765 df-se 4766 df-we 4767 df-ord 4808 df-on 4809 df-lim 4810 df-suc 4811 df-xp 4932 df-rel 4933 df-cnv 4934 df-co 4935 df-dm 4936 df-rn 4937 df-res 4938 df-ima 4939 df-iota 5473 df-fun 5511 df-fn 5512 df-f 5513 df-f1 5514 df-fo 5515 df-f1o 5516 df-fv 5517 df-isom 5518 df-riota 6176 df-ov 6217 df-oprab 6218 df-mpt2 6219 df-om 6618 df-1st 6717 df-2nd 6718 df-recs 6978 df-rdg 7012 df-1o 7066 df-oadd 7070 df-er 7247 df-map 7358 df-pm 7359 df-en 7454 df-dom 7455 df-sdom 7456 df-fin 7457 df-sup 7834 df-oi 7868 df-card 8251 df-pnf 9559 df-mnf 9560 df-xr 9561 df-ltxr 9562 df-le 9563 df-sub 9738 df-neg 9739 df-div 10142 df-nn 10471 df-2 10529 df-3 10530 df-n0 10731 df-z 10800 df-uz 11020 df-rp 11158 df-fz 11612 df-fzo 11736 df-fl 11847 df-seq 12030 df-exp 12089 df-hash 12327 df-cj 12953 df-re 12954 df-im 12955 df-sqrt 13089 df-abs 13090 df-clim 13332 df-rlim 13333 df-sum 13530 df-0p 22181

This theorem is referenced by: plyeq0 22712

W3C validator