Theorem indpi 3828

Description: Principle of Finite Induction on positive integers.

Hypotheses

Ref	Expression
indpi.1	|- (x = 1o -> (ph <-> ps))
indpi.2	|- (x = y -> (ph <-> ch))
indpi.3	|- (x = (y +N 1o) -> (ph <-> th))
indpi.4	|- (x = A -> (ph <-> ta ))
indpi.5	|- ps
indpi.6	|- (y e. N. -> (ch -> th))

Assertion

Ref	Expression
indpi	|- (A e. N. -> ta )

Distinct variable group(s):   x,y   x,A   ps,x   ch,x   th,x   ta ,x   ph,y

Proof of Theorem indpi

Step	Hyp	Ref	Expression
1		nlt1pi 3827	. . . 4 |- -. A <N 1o
2		1pi 3805	. . . . 5 |- 1o e. N.
3		ltsopi 3810	. . . . . 6 |- <N Or N.
4		sotric 2148	. . . . . 6 |- (( <N Or N. /\ (A e. N. /\ 1o e. N.)) -> (A <N 1o <-> -. (A = 1o \/ 1o <N A)))
5	3, 4	mpan 518	. . . . 5 |- ((A e. N. /\ 1o e. N.) -> (A <N 1o <-> -. (A = 1o \/ 1o <N A)))
6	2, 5	mpan2 519	. . . 4 |- (A e. N. -> (A <N 1o <-> -. (A = 1o \/ 1o <N A)))
7	1, 6	mtbii 538	. . 3 |- (A e. N. -> -. -. (A = 1o \/ 1o <N A))
8		nega 78	. . 3 |- (-. -. (A = 1o \/ 1o <N A) -> (A = 1o \/ 1o <N A))
9	7, 8	syl 12	. 2 |- (A e. N. -> (A = 1o \/ 1o <N A))
10	2	elisseti 1355	. . . . . . 7 |- 1o e. V
11	10	eqvinc 1407	. . . . . 6 |- (1o = A <-> E.x(x = 1o /\ x = A))
12		indpi.4	. . . . . 6 |- (x = A -> (ph <-> ta ))
13		indpi.5	. . . . . . 7 |- ps
14		indpi.1	. . . . . . 7 |- (x = 1o -> (ph <-> ps))
15	13, 14	mpbiri 169	. . . . . 6 |- (x = 1o -> ph)
16	11, 12, 15	gencl 1365	. . . . 5 |- (1o = A -> ta )
17	16	cleqcoms 1104	. . . 4 |- (A = 1o -> ta )
18	17	a1i 7	. . 3 |- (A e. N. -> (A = 1o -> ta ))
19		1onn 3193	. . . . . . 7 |- 1o e. om
20		eleq1 1149	. . . . . . . . . 10 |- (x = 1o -> (x e. N. <-> 1o e. N.))
21		breq2 2066	. . . . . . . . . 10 |- (x = 1o -> (1o <N x <-> 1o <N 1o))
22	20, 21	anbi12d 476	. . . . . . . . 9 |- (x = 1o -> ((x e. N. /\ 1o <N x) <-> (1o e. N. /\ 1o <N 1o)))
23	22, 14	imbi12d 474	. . . . . . . 8 |- (x = 1o -> (((x e. N. /\ 1o <N x) -> ph) <-> ((1o e. N. /\ 1o <N 1o) -> ps)))
24		eleq1 1149	. . . . . . . . . 10 |- (x = y -> (x e. N. <-> y e. N.))
25		breq2 2066	. . . . . . . . . 10 |- (x = y -> (1o <N x <-> 1o <N y))
26	24, 25	anbi12d 476	. . . . . . . . 9 |- (x = y -> ((x e. N. /\ 1o <N x) <-> (y e. N. /\ 1o <N y)))
27		indpi.2	. . . . . . . . 9 |- (x = y -> (ph <-> ch))
28	26, 27	imbi12d 474	. . . . . . . 8 |- (x = y -> (((x e. N. /\ 1o <N x) -> ph) <-> ((y e. N. /\ 1o <N y) -> ch)))
29		eleq1 1149	. . . . . . . . . . . . . . . . 17 |- (x = suc y -> (x e. om <-> suc y e. om))
30		peano2b 2388	. . . . . . . . . . . . . . . . 17 |- (y e. om <-> suc y e. om)
31	29, 30	syl6bbr 416	. . . . . . . . . . . . . . . 16 |- (x = suc y -> (x e. om <-> y e. om))
32		pinn 3800	. . . . . . . . . . . . . . . 16 |- (x e. N. -> x e. om)
33	31, 32	syl5bi 183	. . . . . . . . . . . . . . 15 |- (x = suc y -> (x e. N. -> y e. om))
34	33	adantrd 308	. . . . . . . . . . . . . 14 |- (x = suc y -> ((x e. N. /\ 1o <N x) -> y e. om))
35		eleq2 1150	. . . . . . . . . . . . . . . 16 |- (x = suc y -> (1o e. x <-> 1o e. suc y))
36		elsuci 2289	. . . . . . . . . . . . . . . . 17 |- (1o e. suc y -> (1o e. y \/ 1o = y))
37		n0i 1712	. . . . . . . . . . . . . . . . . 18 |- (1o e. y -> -. y = (/))
38		0ex 1745	. . . . . . . . . . . . . . . . . . . . . 22 |- (/) e. V
39	38	sucid 2304	. . . . . . . . . . . . . . . . . . . . 21 |- (/) e. suc (/)
40		df-1o 3104	. . . . . . . . . . . . . . . . . . . . 21 |- 1o = suc (/)
41	39, 40	eleqtrr 1162	. . . . . . . . . . . . . . . . . . . 20 |- (/) e. 1o
42		eleq2 1150	. . . . . . . . . . . . . . . . . . . 20 |- (1o = y -> ((/) e. 1o <-> (/) e. y))
43	41, 42	mpbii 168	. . . . . . . . . . . . . . . . . . 19 |- (1o = y -> (/) e. y)
44		n0i 1712	. . . . . . . . . . . . . . . . . . 19 |- ((/) e. y -> -. y = (/))
45	43, 44	syl 12	. . . . . . . . . . . . . . . . . 18 |- (1o = y -> -. y = (/))
46	37, 45	jaoi 275	. . . . . . . . . . . . . . . . 17 |- ((1o e. y \/ 1o = y) -> -. y = (/))
47	36, 46	syl 12	. . . . . . . . . . . . . . . 16 |- (1o e. suc y -> -. y = (/))
48	35, 47	syl6bi 187	. . . . . . . . . . . . . . 15 |- (x = suc y -> (1o e. x -> -. y = (/)))
49		ltpiord 3809	. . . . . . . . . . . . . . . . 17 |- ((1o e. N. /\ x e. N.) -> (1o <N x <-> 1o e. x))
50	2, 49	mpan 518	. . . . . . . . . . . . . . . 16 |- (x e. N. -> (1o <N x <-> 1o e. x))
51	50	biimpa 324	. . . . . . . . . . . . . . 15 |- ((x e. N. /\ 1o <N x) -> 1o e. x)
52	48, 51	syl5 22	. . . . . . . . . . . . . 14 |- (x = suc y -> ((x e. N. /\ 1o <N x) -> -. y = (/)))
53	34, 52	jcad 455	. . . . . . . . . . . . 13 |- (x = suc y -> ((x e. N. /\ 1o <N x) -> (y e. om /\ -. y = (/))))
54		elni 3798	. . . . . . . . . . . . 13 |- (y e. N. <-> (y e. om /\ -. y = (/)))
55	53, 54	syl6ibr 186	. . . . . . . . . . . 12 |- (x = suc y -> ((x e. N. /\ 1o <N x) -> y e. N.))
56		breq2 2066	. . . . . . . . . . . . 13 |- (x = suc y -> (1o <N x <-> 1o <N suc y))
57		pm3.27 260	. . . . . . . . . . . . 13 |- ((x e. N. /\ 1o <N x) -> 1o <N x)
58	56, 57	syl5bi 183	. . . . . . . . . . . 12 |- (x = suc y -> ((x e. N. /\ 1o <N x) -> 1o <N suc y))
59	55, 58	jcad 455	. . . . . . . . . . 11 |- (x = suc y -> ((x e. N. /\ 1o <N x) -> (y e. N. /\ 1o <N suc y)))
60		addpiord 3806	. . . . . . . . . . . . . . . . . . . 20 |- ((y e. N. /\ 1o e. N.) -> (y +N 1o) = (y +o 1o))
61	2, 60	mpan2 519	. . . . . . . . . . . . . . . . . . 19 |- (y e. N. -> (y +N 1o) = (y +o 1o))
62		pion 3801	. . . . . . . . . . . . . . . . . . . 20 |- (y e. N. -> y e. On)
63		oa1suc 3132	. . . . . . . . . . . . . . . . . . . 20 |- (y e. On -> (y +o 1o) = suc y)
64	62, 63	syl 12	. . . . . . . . . . . . . . . . . . 19 |- (y e. N. -> (y +o 1o) = suc y)
65	61, 64	eqtrd 1128	. . . . . . . . . . . . . . . . . 18 |- (y e. N. -> (y +N 1o) = suc y)
66	65	cleq2d 1112	. . . . . . . . . . . . . . . . 17 |- (y e. N. -> (x = (y +N 1o) <-> x = suc y))
67	66	biimparc 327	. . . . . . . . . . . . . . . 16 |- ((x = suc y /\ y e. N.) -> x = (y +N 1o))
68	67	eleq1d 1155	. . . . . . . . . . . . . . 15 |- ((x = suc y /\ y e. N.) -> (x e. N. <-> (y +N 1o) e. N.))
69		addclpi 3814	. . . . . . . . . . . . . . . 16 |- ((y e. N. /\ 1o e. N.) -> (y +N 1o) e. N.)
70	2, 69	mpan2 519	. . . . . . . . . . . . . . 15 |- (y e. N. -> (y +N 1o) e. N.)
71	68, 70	syl5bir 184	. . . . . . . . . . . . . 14 |- ((x = suc y /\ y e. N.) -> (y e. N. -> x e. N.))
72	71	exp 291	. . . . . . . . . . . . 13 |- (x = suc y -> (y e. N. -> (y e. N. -> x e. N.)))
73	72	pm2.43d 59	. . . . . . . . . . . 12 |- (x = suc y -> (y e. N. -> x e. N.))
74	56	biimprd 136	. . . . . . . . . . . 12 |- (x = suc y -> (1o <N suc y -> 1o <N x))
75	73, 74	anim12d 431	. . . . . . . . . . 11 |- (x = suc y -> ((y e. N. /\ 1o <N suc y) -> (x e. N. /\ 1o <N x)))
76	59, 75	impbid 397	. . . . . . . . . 10 |- (x = suc y -> ((x e. N. /\ 1o <N x) <-> (y e. N. /\ 1o <N suc y)))
77	76	imbi1d 465	. . . . . . . . 9 |- (x = suc y -> (((x e. N. /\ 1o <N x) -> ph) <-> ((y e. N. /\ 1o <N suc y) -> ph)))
78		indpi.3	. . . . . . . . . . . . 13 |- (x = (y +N 1o) -> (ph <-> th))
79	66, 78	syl6bir 188	. . . . . . . . . . . 12 |- (y e. N. -> (x = suc y -> (ph <-> th)))
80	79	adantr 306	. . . . . . . . . . 11 |- ((y e. N. /\ 1o <N suc y) -> (x = suc y -> (ph <-> th)))
81	80	com12 13	. . . . . . . . . 10 |- (x = suc y -> ((y e. N. /\ 1o <N suc y) -> (ph <-> th)))
82	81	pm5.74d 444	. . . . . . . . 9 |- (x = suc y -> (((y e. N. /\ 1o <N suc y) -> ph) <-> ((y e. N. /\ 1o <N suc y) -> th)))
83	77, 82	bitrd 406	. . . . . . . 8 |- (x = suc y -> (((x e. N. /\ 1o <N x) -> ph) <-> ((y e. N. /\ 1o <N suc y) -> th)))
84		eleq1 1149	. . . . . . . . . 10 |- (x = A -> (x e. N. <-> A e. N.))
85		breq2 2066	. . . . . . . . . 10 |- (x = A -> (1o <N x <-> 1o <N A))
86	84, 85	anbi12d 476	. . . . . . . . 9 |- (x = A -> ((x e. N. /\ 1o <N x) <-> (A e. N. /\ 1o <N A)))
87	86, 12	imbi12d 474	. . . . . . . 8 |- (x = A -> (((x e. N. /\ 1o <N x) -> ph) <-> ((A e. N. /\ 1o <N A) -> ta )))
88	13	a1i 7	. . . . . . . . 9 |- ((1o e. N. /\ 1o <N 1o) -> ps)
89	88	a1i 7	. . . . . . . 8 |- (1o e. om -> ((1o e. N. /\ 1o <N 1o) -> ps))
90		pm3.2 232	. . . . . . . . . . . . . . 15 |- (y e. N. -> (1o e. y -> (y e. N. /\ 1o e. y)))
91		ltpiord 3809	. . . . . . . . . . . . . . . . 17 |- ((1o e. N. /\ y e. N.) -> (1o <N y <-> 1o e. y))
92	2, 91	mpan 518	. . . . . . . . . . . . . . . 16 |- (y e. N. -> (1o <N y <-> 1o e. y))
93	92	pm5.32i 489	. . . . . . . . . . . . . . 15 |- ((y e. N. /\ 1o <N y) <-> (y e. N. /\ 1o e. y))
94	90, 93	syl6ibr 186	. . . . . . . . . . . . . 14 |- (y e. N. -> (1o e. y -> (y e. N. /\ 1o <N y)))
95	94	syl4d 28	. . . . . . . . . . . . 13 |- (y e. N. -> (((y e. N. /\ 1o <N y) -> ch) -> (1o e. y -> ch)))
96	10	eqvinc 1407	. . . . . . . . . . . . . . . . 17 |- (1o = y <-> E.x(x = 1o /\ x = y))
97	96, 27, 15	gencl 1365	. . . . . . . . . . . . . . . 16 |- (1o = y -> ch)
98		jao 274	. . . . . . . . . . . . . . . 16 |- ((1o e. y -> ch) -> ((1o = y -> ch) -> ((1o e. y \/ 1o = y) -> ch)))
99	97, 98	mpi 44	. . . . . . . . . . . . . . 15 |- (