Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem seqlem1 4662

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
seqlem1.1

**Assertion**
Ref	Expression
seqlem1

Distinct variable group(s):

**Proof of Theorem seqlem1**
Step	Hyp	Ref	Expression
1		fveq2 2832	. . . 4
2	1	fveq2d 2836	. . 3
3		id 9	. . 3
4	2, 3	cleq12d 1115	. 2
5		fveq2 2832	. . . 4
6	5	fveq2d 2836	. . 3
7		id 9	. . 3
8	6, 7	cleq12d 1115	. 2
9		fveq2 2832	. . . 4
10	9	fveq2d 2836	. . 3
11		id 9	. . 3
12	10, 11	cleq12d 1115	. 2
13		fveq2 2832	. . . 4
14	13	fveq2d 2836	. . 3
15		id 9	. . 3
16	14, 15	cleq12d 1115	. 2
17		opex 1893	. . . . 5
18		1z 4584	. . . . . 6
19		seqlem1.1	. . . . . 6
20	18, 19	uzrdgini 4658	. . . . 5
21	17, 20	ax-mp 6	. . . 4
22	21	fveq2i 2835	. . 3
23	18	elisseti 1355	. . . 4
24	23	op1st 3091	. . 3
25	22, 24	eqtr 1119	. 2
26		nnz 4582	. . . . . . . . 9
27	26	eleq2i 1153	. . . . . . . 8
28	18, 19	uzrdgsuc 4659	. . . . . . . 8
29	27, 28	sylbi 174	. . . . . . 7
30		ax-17 925	. . . . . . . . . 10
31		ax-17 925	. . . . . . . . . . . 12
32		hbs1 986	. . . . . . . . . . . . 13
33	32	hbab 1096	. . . . . . . . . . . 12
34	31, 33	hbop 1879	. . . . . . . . . . 11
35	34	hbeleq 1173	. . . . . . . . . 10
36		opeq12 1878	. . . . . . . . . . . 12 $/\$ <