seq1lem1 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem seq1lem1 6246

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 3709	. . . 4
2	1	fveq2d 3713	. . 3
3		id 59	. . 3
4	2, 3	eqeq12d 1481	. 2
5		fveq2 3709	. . . 4
6	5	fveq2d 3713	. . 3
7		id 59	. . 3
8	6, 7	eqeq12d 1481	. 2
9		fveq2 3709	. . . 4
10	9	fveq2d 3713	. . 3
11		id 59	. . 3
12	10, 11	eqeq12d 1481	. 2
13		fveq2 3709	. . . 4
14	13	fveq2d 3713	. . 3
15		id 59	. . 3
16	14, 15	eqeq12d 1481	. 2
17		opex 2772	. . . . 5
18		1z 6106	. . . . . 6
19		seq1lem1.1	. . . . . 6
20	18, 19	uzrdgini 6240	. . . . 5
21	17, 20	ax-mp 7	. . . 4
22	21	fveq2i 3712	. . 3
23	18	elisseti 1809	. . . 4
24	23	op1st 4069	. . 3
25	22, 24	eqtr 1487	. 2
26		nnzrab 6104	. . . . . . . . 9
27	26	eleq2i 1530	. . . . . . . 8
28	18, 19	uzrdgsuc 6241	. . . . . . . 8
29	27, 28	sylbi 199	. . . . . . 7
30		ax-17 968	. . . . . . . . . 10
31		ax-17 968	. . . . . . . . . . . 12
32		hbs1 1327	. . . . . . . . . . . . 13
33	32	hbab 1460	. . . . . . . . . . . 12
34	31, 33	hbop 2487	. . . . . . . . . . 11
35	34	hbeleq 1559	. . . . . . . . . 10