Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem infcvglem3 7158

Description: Lemma for infcvg 7159. Using climsqueeze 7076, show that sequence , constructed from , converges to the supremum.

Hypotheses

Ref	Expression
infcvg.1
infcvg.2
infcvg.3
infcvg.4
infcvg.5c
infcvg.9
infcvg.10
infcvg.11
infcvg.12
infcvg.6a
infcvg.7a
infcvg.8a

Assertion

Ref	Expression
infcvglem3

Distinct variable groups:   ,,   ,,   ,   ,   ,   ,,   ,,,   ,   ,,,   ,,   ,

---

Proof of Theorem infcvglem3

Step	Hyp	Ref	Expression
1		infcvg.1	. . 3
2		infcvg.2	. . 3
3		infcvg.3	. . 3
4		infcvg.4	. . 3
5		infcvg.5c	. . 3
6		infcvg.7a	. . 3
7	1, 2, 3, 4, 5, 6	infcvglem1 7156	. 2
8		pm3.26 319	. . . 4
9		infcvg.8a	. . . . . . . . . . . 12
10		infcvg.10	. . . . . . . . . . . 12
11	9, 10	breq12d 2621	. . . . . . . . . . 11
12	11	adantl 388	. . . . . . . . . 10
13		ltlet 5493	. . . . . . . . . . 11
14	9	adantl 388	. . . . . . . . . . . 12
15		ffvelrn 3799	. . . . . . . . . . . . 13
16	6	eleq1d 1532	. . . . . . . . . . . . . 14
17	16, 2	vtoclga 1843	. . . . . . . . . . . . 13
18	15, 17	syl 10	. . . . . . . . . . . 12
19	14, 18	eqeltrd 1540	. . . . . . . . . . 11
20		nnrecret 6215	. . . . . . . . . . . . . 14
21	1, 2, 3, 4	infcvgaux1 7154	. . . . . . . . . . . . . . . . . 18
22	21	suprcli 6008	. . . . . . . . . . . . . . . . 17
23	22	renegcl 5388	. . . . . . . . . . . . . . . 16
24	5, 23	eqeltr 1536	. . . . . . . . . . . . . . 15
25		axaddrcl 5244	. . . . . . . . . . . . . . 15
26	24, 25	mpan 693	. . . . . . . . . . . . . 14
27	20, 26	syl 10	. . . . . . . . . . . . 13
28	10, 27	eqeltrd 1540	. . . . . . . . . . . 12
29	28	adantl 388	. . . . . . . . . . 11
30	13, 19, 29	sylanc 471	. . . . . . . . . 10
31	12, 30	sylbird 205	. . . . . . . . 9
32	1, 2, 3, 4, 5, 6	infcvgaux2 7155	. . . . . . . . . . . . . 14
33	15, 32	syl 10	. . . . . . . . . . . . 13
34	33, 14	breqtrrd 2631	. . . . . . . . . . . 12
35	34	a1d 12	. . . . . . . . . . 11
36	35	ancrd 299	. . . . . . . . . 10
37	29, 19	jca 288	. . . . . . . . . 10
38	36, 37	jctild 599	. . . . . . . . 9
39	31, 38	syld 27	. . . . . . . 8
40	39	r19.20dva 1701	. . . . . . 7
41	40	imp 350	. . . . . 6
42		nnuz 6371	. . . . . . 7
43		raleq1 1778	. . . . . . 7
44	42, 43	ax-mp 7	. . . . . 6
45	41, 44	sylib 198	. . . . 5
46		infcvg.9	. . . . . . 7
47		infcvg.11	. . . . . . 7
48		infcvg.12	. . . . . . 7
49	1, 2, 3, 4, 5, 46, 10, 47, 48	infcvglem2 7157	. . . . . 6
50		1z 6106	. . . . . 6
51		infcvg.6a	. . . . . . 7
52	24	elisseti 1809	. . . . . . 7
53	46, 51, 52	climsqueeze2 7077	. . . . . 6
54	49, 50, 53	mp3an12 903	. . . . 5
55	45, 54	syl 10	. . . 4
56	8, 55	jca 288	. . 3
57	56	19.22i 1036	. 2
58	7, 57	ax-mp 7	1

Colors of variables: wff set class

Syntax hints:   wi 3   wb 146   wa 223   wceq 953   wcel 955  wex 977  cab 1456  wral 1637  wrex 1638  cvv 1802   class class class wbr 2609  wf 3168  cfv 3172  (class class class)co 3948  csup 4547  cr 5205  c1 5207   caddc 5209  cneg 5265   cdiv 5266   cle 5267  cn 5268  cz 5270   clt 5458  cuz 6349   cli 6912

This theorem is referenced by:  infcvg 7159

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-rep 2683  ax-sep 2693  ax-nul 2700  ax-pow 2732  ax-pr 2769  ax-un 2857  ax-reg 4565  ax-inf2 4597  ax-ac 4716

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 774  df-3an 775  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-nel 1580  df-ral