Theorem indpi 5034

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 groups:   x,y   x,A   ps,x   ch,x   th,x   ta,x   ph,y

Proof of Theorem indpi

Step	Hyp	Ref	Expression
1		nlt1pi 5033	. . . 4 |- -. A <N 1o
2		1pi 5011	. . . . 5 |- 1o e. N.
3		ltsopi 5016	. . . . . 6 |- <N Or N.
4		sotric 2860	. . . . . 6 |- (( <N Or N. /\ (A e. N. /\ 1o e. N.)) -> (A <N 1o <-> -. (A = 1o \/ 1o <N A)))
5	3, 4	mpan 695	. . . . 5 |- ((A e. N. /\ 1o e. N.) -> (A <N 1o <-> -. (A = 1o \/ 1o <N A)))
6	2, 5	mpan2 696	. . . 4 |- (A e. N. -> (A <N 1o <-> -. (A = 1o \/ 1o <N A)))
7	1, 6	mtbii 716	. . 3 |- (A e. N. -> -. -. (A = 1o \/ 1o <N A))
8		nega 84	. . 3 |- (-. -. (A = 1o \/ 1o <N A) -> (A = 1o \/ 1o <N A))
9	7, 8	syl 10	. 2 |- (A e. N. -> (A = 1o \/ 1o <N A))
10	2	elisseti 1818	. . . . . . 7 |- 1o e. V
11	10	eqvinc 1883	. . . . . 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 194	. . . . . 6 |- (x = 1o -> ph)
16	11, 12, 15	gencl 1828	. . . . 5 |- (1o = A -> ta)
17	16	eqcoms 1478	. . . 4 |- (A = 1o -> ta)
18	17	a1i 8	. . 3 |- (A e. N. -> (A = 1o -> ta))
19		1onn 4253	. . . . . . 7 |- 1o e. om
20		eleq1 1534	. . . . . . . . . 10 |- (x = 1o -> (x e. N. <-> 1o e. N.))
21		breq2 2623	. . . . . . . . . 10 |- (x = 1o -> (1o <N x <-> 1o <N 1o))
22	20, 21	anbi12d 628	. . . . . . . . 9 |- (x = 1o -> ((x e. N. /\ 1o <N x) <-> (1o e. N. /\ 1o <N 1o)))
23	22, 14	imbi12d 626	. . . . . . . 8 |- (x = 1o -> (((x e. N. /\ 1o <N x) -> ph) <-> ((1o e. N. /\ 1o <N 1o) -> ps)))
24		eleq1 1534	. . . . . . . . . 10 |- (x = y -> (x e. N. <-> y e. N.))
25		breq2 2623	. . . . . . . . . 10 |- (x = y -> (1o <N x <-> 1o <N y))
26	24, 25	anbi12d 628	. . . . . . . . 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 626	. . . . . . . 8 |- (x = y -> (((x e. N. /\ 1o <N x) -> ph) <-> ((y e. N. /\ 1o <N y) -> ch)))
29		eleq1 1534	. . . . . . . . . . . . . . . . 17 |- (x = suc y -> (x e. om <-> suc y e. om))
30		peano2b 3147	. . . . . . . . . . . . . . . . 17 |- (y e. om <-> suc y e. om)
31	29, 30	syl6bbr 538	. . . . . . . . . . . . . . . 16 |- (x = suc y -> (x e. om <-> y e. om))
32		pinn 5006	. . . . . . . . . . . . . . . 16 |- (x e. N. -> x e. om)
33	31, 32	syl5bi 208	. . . . . . . . . . . . . . 15 |- (x = suc y -> (x e. N. -> y e. om))
34	33	adantrd 391	. . . . . . . . . . . . . 14 |- (x = suc y -> ((x e. N. /\ 1o <N x) -> y e. om))
35		eleq2 1535	. . . . . . . . . . . . . . . 16 |- (x = suc y -> (1o e. x <-> 1o e. suc y))
36		elsuci 3035	. . . . . . . . . . . . . . . . 17 |- (1o e. suc y -> (1o e. y \/ 1o = y))
37		ne0i 2286	. . . . . . . . . . . . . . . . . 18 |- (1o e. y -> y =/= (/))
38		0lt1o 4147	. . . . . . . . . . . . . . . . . . . 20 |- (/) e. 1o
39		eleq2 1535	. . . . . . . . . . . . . . . . . . . 20 |- (1o = y -> ((/) e. 1o <-> (/) e. y))
40	38, 39	mpbii 193	. . . . . . . . . . . . . . . . . . 19 |- (1o = y -> (/) e. y)
41		ne0i 2286	. . . . . . . . . . . . . . . . . . 19 |- ((/) e. y -> y =/= (/))
42	40, 41	syl 10	. . . . . . . . . . . . . . . . . 18 |- (1o = y -> y =/= (/))
43	37, 42	jaoi 341	. . . . . . . . . . . . . . . . 17 |- ((1o e. y \/ 1o = y) -> y =/= (/))
44	36, 43	syl 10	. . . . . . . . . . . . . . . 16 |- (1o e. suc y -> y =/= (/))
45	35, 44	syl6bi 214	. . . . . . . . . . . . . . 15 |- (x = suc y -> (1o e. x -> y =/= (/)))
46		ltpiord 5015	. . . . . . . . . . . . . . . . 17 |- ((1o e. N. /\ x e. N.) -> (1o <N x <-> 1o e. x))
47	2, 46	mpan 695	. . . . . . . . . . . . . . . 16 |- (x e. N. -> (1o <N x <-> 1o e. x))
48	47	biimpa 416	. . . . . . . . . . . . . . 15 |- ((x e. N. /\ 1o <N x) -> 1o e. x)
49	45, 48	syl5 21	. . . . . . . . . . . . . 14 |- (x = suc y -> ((x e. N. /\ 1o <N x) -> y =/= (/)))
50	34, 49	jcad 600	. . . . . . . . . . . . 13 |- (x = suc y -> ((x e. N. /\ 1o <N x) -> (y e. om /\ y =/= (/))))
51		elni 5004	. . . . . . . . . . . . 13 |- (y e. N. <-> (y e. om /\ y =/= (/)))
52	50, 51	syl6ibr 213	. . . . . . . . . . . 12 |- (x = suc y -> ((x e. N. /\ 1o <N x) -> y e. N.))
53		breq2 2623	. . . . . . . . . . . . 13 |- (x = suc y -> (1o <N x <-> 1o <N suc y))
54		pm3.27 323	. . . . . . . . . . . . 13 |- ((x e. N. /\ 1o <N x) -> 1o <N x)
55	53, 54	syl5bi 208	. . . . . . . . . . . 12 |- (x = suc y -> ((x e. N. /\ 1o <N x) -> 1o <N suc y))
56	52, 55	jcad 600	. . . . . . . . . . 11 |- (x = suc y -> ((x e. N. /\ 1o <N x) -> (y e. N. /\ 1o <N suc y)))
57		addpiord 5012	. . . . . . . . . . . . . . . . . . . 20 |- ((y e. N. /\ 1o e. N.) -> (y +N 1o) = (y +o 1o))
58	2, 57	mpan2 696	. . . . . . . . . . . . . . . . . . 19 |- (y e. N. -> (y +N 1o) = (y +o 1o))
59		pion 5007	. . . . . . . . . . . . . . . . . . . 20 |- (y e. N. -> y e. On)
60		oa1suc 4164	. . . . . . . . . . . . . . . . . . . 20 |- (y e. On -> (y +o 1o) = suc y)
61	59, 60	syl 10	. . . . . . . . . . . . . . . . . . 19 |- (y e. N. -> (y +o 1o) = suc y)
62	58, 61	eqtrd 1507	. . . . . . . . . . . . . . . . . 18 |- (y e. N. -> (y +N 1o) = suc y)
63	62	eqeq2d 1486	. . . . . . . . . . . . . . . . 17 |- (y e. N. -> (x = (y +N 1o) <-> x = suc y))
64	63	biimparc 419	. . . . . . . . . . . . . . . 16 |- ((x = suc y /\ y e. N.) -> x = (y +N 1o))
65	64	eleq1d 1540	. . . . . . . . . . . . . . 15 |- ((x = suc y /\ y e. N.) -> (x e. N. <-> (y +N 1o) e. N.))
66		addclpi 5020	. . . . . . . . . . . . . . . 16 |- ((y e. N. /\ 1o e. N.) -> (y +N 1o) e. N.)
67	2, 66	mpan2 696	. . . . . . . . . . . . . . 15 |- (y e. N. -> (y +N 1o) e. N.)
68	65, 67	syl5bir 210	. . . . . . . . . . . . . 14 |- ((x = suc y /\ y e. N.) -> (y e. N. -> x e. N.))
69	68	ex 373	. . . . . . . . . . . . 13 |- (x = suc y -> (y e. N. -> (y e. N. -> x e. N.)))
70	69	pm2.43d 65	. . . . . . . . . . . 12 |- (x = suc y -> (y e. N. -> x e. N.))
71	53	biimprd 154	. . . . . . . . . . . 12 |- (x = suc y -> (1o <N suc y -> 1o <N x))
72	70, 71	anim12d 558	. . . . . . . . . . 11 |- (x = suc y -> ((y e. N. /\ 1o <N suc y) -> (x e. N. /\ 1o <N x)))
73	56, 72	impbid 516	. . . . . . . . . 10 |- (x = suc y -> ((x e. N. /\ 1o <N x) <-> (y e. N. /\ 1o <N suc y)))
74	73	imbi1d 613	. . . . . . . . 9 |- (x = suc y -> (((x e. N. /\ 1o <N x) -> ph) <-> ((y e. N. /\ 1o <N suc y) -> ph)))
75		indpi.3	. . . . . . . . . . . . 13 |- (x = (y +N 1o) -> (ph <-> th))
76	63, 75	syl6bir 215	. . . . . . . . . . . 12 |- (y e. N. -> (x = suc y -> (ph <-> th)))
77	76	adantr 389	. . . . . . . . . . 11 |- ((y e. N. /\ 1o <N suc y) -> (x = suc y -> (ph <-> th)))
78	77	com12 11	. . . . . . . . . 10 |- (x = suc y -> ((y e. N. /\ 1o <N suc y) -> (ph <-> th)))
79	78	pm5.74d 585	. . . . . . . . 9 |- (x = suc y -> (((y e. N. /\ 1o <N suc y) -> ph) <-> ((y e. N. /\ 1o <N suc y) -> th)))
80	74, 79	bitrd 528	. . . . . . . 8 |- (x = suc y -> (((x e. N. /\ 1o <N x) -> ph) <-> ((y e. N. /\ 1o <N suc y) -> th)))
81		eleq1 1534	. . . . . . . . . 10 |- (x = A -> (x e. N. <-> A e. N.))
82		breq2 2623	. . . . . . . . . 10 |- (x = A -> (1o <N x <-> 1o <N A))
83	81, 82	anbi12d 628	. . . . . . . . 9 |- (x = A -> ((x e. N. /\ 1o <N x) <-> (A e. N. /\ 1o <N A)))
84	83, 12	imbi12d 626	. . . . . . . 8 |- (x = A -> (((x e. N. /\ 1o <N x) -> ph) <-> ((A e. N. /\ 1o <N A) -> ta)))
85	13	a1i 8	. . . . . . . . 9 |- ((1o e. N. /\ 1o <N 1o) -> ps)
86	85	a1i 8	. . . . . . . 8 |- (1o e. om -> ((1o e. N. /\ 1o <N 1o) -> ps))
87		pm3.2 283	. . . . . . . . . . . . . 14 |- (y e. N. -> (1o e. y -> (y e. N. /\ 1o e. y)))
88		ltpiord 5015	. . . . . . . . . . . . . . . 16 |- ((1o e. N. /\ y e. N.) -> (1o <N y <-> 1o e. y))
89	2, 88	mpan 695	. . . . . . . . . . . . . . 15 |- (y e. N. -> (1o <N y <-> 1o e. y))
90	89	pm5.32i 645	. . . . . . . . . . . . . 14 |- ((y e. N. /\ 1o <N y) <-> (y e. N. /\ 1o e. y))
91	87, 90	syl6ibr 213	. . . . . . . . . . . . 13 |- (y e. N. -> (1o e. y -> (y e. N. /\ 1o <N y)))
92	91	imim1d 28	. . . . . . . . . . . 12 |- (y e. N. -> (((y e. N. /\ 1o <N y) -> ch) -> (1o e. y -> ch)))
93	10	eqvinc 1883	. . . . . . . . . . . . . . . 16 |- (1o = y <-> E.x