seq1lem1 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem seq1lem1 6310

Description: We prove by induction that the first member of the ordered pair value of the internal sequence of

equals its index.

**Hypothesis**
Ref	Expression
seq1lem1.1

**Assertion**
Ref	Expression
seq1lem1

**Proof of Theorem seq1lem1**
Step	Hyp	Ref	Expression
1		fveq2 3730	. . . 4
2	1	fveq2d 3734	. . 3
3		id 59	. . 3
4	2, 3	eqeq12d 1492	. 2
5		fveq2 3730	. . . 4
6	5	fveq2d 3734	. . 3
7		id 59	. . 3
8	6, 7	eqeq12d 1492	. 2
9		fveq2 3730	. . . 4
10	9	fveq2d 3734	. . 3
11		id 59	. . 3
12	10, 11	eqeq12d 1492	. 2
13		fveq2 3730	. . . 4
14	13	fveq2d 3734	. . 3
15		id 59	. . 3
16	14, 15	eqeq12d 1492	. 2
17		opex 2788	. . . . 5
18		1z 6161	. . . . . 6
19		seq1lem1.1	. . . . . 6
20	18, 19	uzrdgini 6304	. . . . 5
21	17, 20	ax-mp 7	. . . 4
22	21	fveq2i 3733	. . 3
23	18	elisseti 1821	. . . 4
24	23	op1st 4091	. . 3
25	22, 24	eqtr 1498	. 2
26		nnzrab 6159	. . . . . . . . 9
27	26	eleq2i 1541	. . . . . . . 8
28	18, 19	uzrdgsuc 6305	. . . . . . . 8
29	27, 28	sylbi 199	. . . . . . 7
30		ax-17 973	. . . . . . . . . 10
31		ax-17 973	. . . . . . . . . . . 12
32		hbs1 1334	. . . . . . . . . . . . 13
33	32	hbab 1470	. . . . . . . . . . . 12
34	31, 33	hbop 2500	. . . . . . . . . . 11
35	34	hbeleq 1570	. . . . . . . . . 10