Theorem indpi 6186

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 6185	. . . 4 |- -. A <N 1o
2		1pi 6163	. . . . 5 |- 1o e. N.
3		ltsopi 6168	. . . . . 6 |- <N Or N.
4		sotric 3615	. . . . . 6 |- (( <N Or N. /\ (A e. N. /\ 1o e. N.)) -> (A <N 1o <-> -. (A = 1o \/ 1o <N A)))
5	3, 4	mpan 759	. . . . 5 |- ((A e. N. /\ 1o e. N.) -> (A <N 1o <-> -. (A = 1o \/ 1o <N A)))
6	2, 5	mpan2 760	. . . 4 |- (A e. N. -> (A <N 1o <-> -. (A = 1o \/ 1o <N A)))
7	1, 6	mtbii 784	. . 3 |- (A e. N. -> -. -. (A = 1o \/ 1o <N A))
8		notnot2 100	. . 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 2301	. . . . . . 7 |- 1o e. _V
11	10	eqvinc 2387	. . . . . 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 211	. . . . . 6 |- (x = 1o -> ph)
16	11, 12, 15	gencl 2318	. . . . 5 |- (1o = A -> ta)
17	16	eqcoms 1887	. . . 4 |- (A = 1o -> ta)
18	17	a1i 8	. . 3 |- (A e. N. -> (A = 1o -> ta))
19		pinn 6158	. . . . . 6 |- (A e. N. -> A e. om)
20		elni2 6157	. . . . . . 7 |- (A e. N. <-> (A e. om /\ (/) e. A))
21		nnord 3959	. . . . . . . . . 10 |- (A e. om -> Ord A)
22		ordsucss 3899	. . . . . . . . . 10 |- (Ord A -> ((/) e. A -> suc (/) C_ A))
23	21, 22	syl 12	. . . . . . . . 9 |- (A e. om -> ((/) e. A -> suc (/) C_ A))
24		df-1o 5177	. . . . . . . . . 10 |- 1o = suc (/)
25	24	sseq1i 2641	. . . . . . . . 9 |- (1o C_ A <-> suc (/) C_ A)
26	23, 25	syl6ibr 230	. . . . . . . 8 |- (A e. om -> ((/) e. A -> 1o C_ A))
27	26	imp 377	. . . . . . 7 |- ((A e. om /\ (/) e. A) -> 1o C_ A)
28	20, 27	sylbi 216	. . . . . 6 |- (A e. N. -> 1o C_ A)
29		1onn 5310	. . . . . . 7 |- 1o e. om
30		eleq1 1957	. . . . . . . . . 10 |- (x = 1o -> (x e. N. <-> 1o e. N.))
31		breq2 3342	. . . . . . . . . 10 |- (x = 1o -> (1o <N x <-> 1o <N 1o))
32	30, 31	anbi12d 690	. . . . . . . . 9 |- (x = 1o -> ((x e. N. /\ 1o <N x) <-> (1o e. N. /\ 1o <N 1o)))
33	32, 14	imbi12d 688	. . . . . . . 8 |- (x = 1o -> (((x e. N. /\ 1o <N x) -> ph) <-> ((1o e. N. /\ 1o <N 1o) -> ps)))
34		eleq1 1957	. . . . . . . . . 10 |- (x = y -> (x e. N. <-> y e. N.))
35		breq2 3342	. . . . . . . . . 10 |- (x = y -> (1o <N x <-> 1o <N y))
36	34, 35	anbi12d 690	. . . . . . . . 9 |- (x = y -> ((x e. N. /\ 1o <N x) <-> (y e. N. /\ 1o <N y)))
37		indpi.2	. . . . . . . . 9 |- (x = y -> (ph <-> ch))
38	36, 37	imbi12d 688	. . . . . . . 8 |- (x = y -> (((x e. N. /\ 1o <N x) -> ph) <-> ((y e. N. /\ 1o <N y) -> ch)))
39		eleq1 1957	. . . . . . . . . . . . . . . . 17 |- (x = suc y -> (x e. om <-> suc y e. om))
40		peano2b 3968	. . . . . . . . . . . . . . . . 17 |- (y e. om <-> suc y e. om)
41	39, 40	syl6bbr 597	. . . . . . . . . . . . . . . 16 |- (x = suc y -> (x e. om <-> y e. om))
42		pinn 6158	. . . . . . . . . . . . . . . 16 |- (x e. N. -> x e. om)
43	41, 42	syl5bi 225	. . . . . . . . . . . . . . 15 |- (x = suc y -> (x e. N. -> y e. om))
44	43	adantrd 427	. . . . . . . . . . . . . 14 |- (x = suc y -> ((x e. N. /\ 1o <N x) -> y e. om))
45		eleq2 1958	. . . . . . . . . . . . . . . 16 |- (x = suc y -> (1o e. x <-> 1o e. suc y))
46		elsuci 3731	. . . . . . . . . . . . . . . . 17 |- (1o e. suc y -> (1o e. y \/ 1o = y))
47		ne0i 2881	. . . . . . . . . . . . . . . . . 18 |- (1o e. y -> y =/= (/))
48		0lt1o 5192	. . . . . . . . . . . . . . . . . . . 20 |- (/) e. 1o
49		eleq2 1958	. . . . . . . . . . . . . . . . . . . 20 |- (1o = y -> ((/) e. 1o <-> (/) e. y))
50	48, 49	mpbii 210	. . . . . . . . . . . . . . . . . . 19 |- (1o = y -> (/) e. y)
51		ne0i 2881	. . . . . . . . . . . . . . . . . . 19 |- ((/) e. y -> y =/= (/))
52	50, 51	syl 12	. . . . . . . . . . . . . . . . . 18 |- (1o = y -> y =/= (/))
53	47, 52	jaoi 368	. . . . . . . . . . . . . . . . 17 |- ((1o e. y \/ 1o = y) -> y =/= (/))
54	46, 53	syl 12	. . . . . . . . . . . . . . . 16 |- (1o e. suc y -> y =/= (/))
55	45, 54	syl6bi 231	. . . . . . . . . . . . . . 15 |- (x = suc y -> (1o e. x -> y =/= (/)))
56		ltpiord 6167	. . . . . . . . . . . . . . . . 17 |- ((1o e. N. /\ x e. N.) -> (1o <N x <-> 1o e. x))
57	2, 56	mpan 759	. . . . . . . . . . . . . . . 16 |- (x e. N. -> (1o <N x <-> 1o e. x))
58	57	biimpa 460	. . . . . . . . . . . . . . 15 |- ((x e. N. /\ 1o <N x) -> 1o e. x)
59	55, 58	syl5 20	. . . . . . . . . . . . . 14 |- (x = suc y -> ((x e. N. /\ 1o <N x) -> y =/= (/)))
60	44, 59	jcad 661	. . . . . . . . . . . . 13 |- (x = suc y -> ((x e. N. /\ 1o <N x) -> (y e. om /\ y =/= (/))))
61		elni 6156	. . . . . . . . . . . . 13 |- (y e. N. <-> (y e. om /\ y =/= (/)))
62	60, 61	syl6ibr 230	. . . . . . . . . . . 12 |- (x = suc y -> ((x e. N. /\ 1o <N x) -> y e. N.))
63		breq2 3342	. . . . . . . . . . . . 13 |- (x = suc y -> (1o <N x <-> 1o <N suc y))
64		simpr 350	. . . . . . . . . . . . 13 |- ((x e. N. /\ 1o <N x) -> 1o <N x)
65	63, 64	syl5bi 225	. . . . . . . . . . . 12 |- (x = suc y -> ((x e. N. /\ 1o <N x) -> 1o <N suc y))
66	62, 65	jcad 661	. . . . . . . . . . 11 |- (x = suc y -> ((x e. N. /\ 1o <N x) -> (y e. N. /\ 1o <N suc y)))
67		addpiord 6164	. . . . . . . . . . . . . . . . . . . 20 |- ((y e. N. /\ 1o e. N.) -> (y +N 1o) = (y +o 1o))
68	2, 67	mpan2 760	. . . . . . . . . . . . . . . . . . 19 |- (y e. N. -> (y +N 1o) = (y +o 1o))
69		pion 6159	. . . . . . . . . . . . . . . . . . . 20 |- (y e. N. -> y e. On)
70		oa1suc 5209	. . . . . . . . . . . . . . . . . . . 20 |- (y e. On -> (y +o 1o) = suc y)
71	69, 70	syl 12	. . . . . . . . . . . . . . . . . . 19 |- (y e. N. -> (y +o 1o) = suc y)
72	68, 71	eqtrd 1925	. . . . . . . . . . . . . . . . . 18 |- (y e. N. -> (y +N 1o) = suc y)
73	72	eqeq2d 1895	. . . . . . . . . . . . . . . . 17 |- (y e. N. -> (x = (y +N 1o) <-> x = suc y))
74	73	biimparc 463	. . . . . . . . . . . . . . . 16 |- ((x = suc y /\ y e. N.) -> x = (y +N 1o))
75	74	eleq1d 1963	. . . . . . . . . . . . . . 15 |- ((x = suc y /\ y e. N.) -> (x e. N. <-> (y +N 1o) e. N.))
76		addclpi 6172	. . . . . . . . . . . . . . . 16 |- ((y e. N. /\ 1o e. N.) -> (y +N 1o) e. N.)
77	2, 76	mpan2 760	. . . . . . . . . . . . . . 15 |- (y e. N. -> (y +N 1o) e. N.)
78	75, 77	syl5bir 227	. . . . . . . . . . . . . 14 |- ((x = suc y /\ y e. N.) -> (y e. N. -> x e. N.))
79	78	ex 402	. . . . . . . . . . . . 13 |- (x = suc y -> (y e. N. -> (y e. N. -> x e. N.)))
80	79	pm2.43d 79	. . . . . . . . . . . 12 |- (x = suc y -> (y e. N. -> x e. N.))
81	63	biimprd 171	. . . . . . . . . . . 12 |- (x = suc y -> (1o <N suc y -> 1o <N x))
82	80, 81	anim12d 617	. . . . . . . . . . 11 |- (x = suc y -> ((y e. N. /\ 1o <N suc y) -> (x e. N. /\ 1o <N x)))
83	66, 82	impbid 574	. . . . . . . . . 10 |- (x = suc y -> ((x e. N. /\ 1o <N x) <-> (y e. N. /\ 1o <N suc y)))
84	83	imbi1d 675	. . . . . . . . 9 |- (x = suc y -> (((x e. N. /\ 1o <N x) -> ph) <-> ((y e. N. /\ 1o <N suc y) -> ph)))
85		indpi.3	. . . . . . . . . . . . 13 |- (x = (y +N 1o) -> (ph <-> th))
86	73, 85	syl6bir 232	. . . . . . . . . . . 12 |- (y e. N. -> (x = suc y -> (ph <-> th)))
87	86	adantr 425	. . . . . . . . . . 11 |- ((y e. N. /\ 1o <N suc y) -> (x = suc y -> (ph <-> th)))
88	87	com12 14	. . . . . . . . . 10 |- (x = suc y -> ((y e. N. /\ 1o <N suc y) -> (ph <-> th)))
89	88	pm5.74d 645	. . . . . . . . 9 |- (x = suc y -> (((y e. N. /\ 1o <N suc y) -> ph) <-> ((y e. N. /\ 1o <N suc y) -> th)))
90	84, 89	bitrd 587	. . . . . . . 8 |- (x = suc y -> (((x e. N. /\ 1o <N x) -> ph) <-> ((y e. N. /\ 1o <N suc y) -> th)))
91		eleq1 1957	. . . . . . . . . 10 |- (x = A -> (x e. N. <-> A e. N.))
92		breq2 3342	. . . . . . . . . 10 |- (x = A -> (1o <N x <-> 1o <N A))
93	91, 92	anbi12d 690	. . . . . . . . 9 |- (x = A -> ((x e. N. /\ 1o <N x) <-> (A e. N. /\ 1o <N A)))
94	93, 12	imbi12d 688	. . . . . . . 8 |- (x = A -> (((x e. N. /\ 1o <N x) -> ph) <-> ((A e. N. /\ 1o <N A) -> ta)))
95	13	a1i12 9	. . . . . . . 8 |- (1o e. om -> ((1o e. N. /\ 1o <N 1o) -> ps))
96		ltpiord 6167	. . . . . . . . . . . . . . . 16 |- ((1o e. N. /\ y e. N.) -> (1o <N y <-> 1o e. y))
97	2, 96	mpan 759	. . . . . . . . . . . . . . 15 |- (y e. N. -> (1o <N y <-> 1o e. y))
98	97	pm5.32i 707	. . . . . . . . . . . . . 14 |- ((y e. N. /\ 1o <N y) <-> (y e. N. /\ 1o e. y))
99	98	simplbi2 466	. . . . . . . . . . . . 13 |- (y e. N. -> (1o e. y -> (y e. N. /\ 1o <N y)))
100	99	imim1d 33	. . . . . . . . . . . 12 |- (y e. N. -> (((y e. N. /\ 1o <N y) -> ch) -> (1o e. y -> ch)))
101	10	eqvinc 2387	. . . . . . . . . . . . . . . 16 |- (1o = y <-> E.x(x = 1o /\ x = y))
102	101, 37, 15	gencl 2318	. . . . . . . . . . . . . . 15 |- (1o = y -> ch)
103		jao 367	. . . . . . . . . . . . . . 15 |- ((1o e. y -> ch) -> ((1o = y -> ch) -> ((1o e. y \/ 1o = y) -> ch)))
104	102, 103	mpi 55	. . . . . . . . . . . . . 14 |- ((1o e. y -> ch) -> ((1o e. y \/ 1o = y) -> ch))
105	104, 46	syl5 20	. . . . . . . . . . . . 13 |- ((1o e. y -> ch) -> (1o e. suc y -> ch))
106		visset 2295	. . . . . . . . . . . . . . . . 17 |- y e. _V
107	106	sucex 3892	. . . . . . . . . . . . . . . 16 |- suc y e. _V
108		ltrelpi 6169	. . . . . . . . . . . . . . . 16 |- <N C_ (N. X. N.)
109	107, 108	brel 4048	. . . . . . . . . . . . . . 15 |- (1o <N suc y -> (1o e. N. /\ suc y e. N.))
110		ltpiord 6167	. . . . . . . . . . . . . . 15 |- ((1o e. N. /\ suc y e. N.) -> (1o <N suc y <-> 1o e. suc y))
111	109, 110	syl 12	. . . . . . . . . . . . . 14 |- (1o <N suc y -> (1o <N suc y <-> 1o e. suc y))
112	111	ibi 652	. . . . . . . . . . . . 13 |- (1o <N suc y -> 1o e. suc y)
113	105, 112	syl5 20	. . . . . . . . . . . 12 |- ((1o e. y -> ch) -> (1o <N suc y -> ch))
114	100, 113	syl6com 64	. . . . . . . . . . 11 |- (((y e. N. /\ 1o <N y) -> ch) -> (y e. N. -> (1o <N suc y -> ch)))
115	114	imp3a 388	. . . . . . . . . 10 |- (((y e. N. /\ 1o <N y) -> ch) -> ((y e. N. /\ 1o <N suc y) -> ch))
116		elni2 6157	. . . . . . . . . . . 12 |- (y e. N. <-> (y e. om /\ (/) e. y))
117		indpi.6	. . . . . . . . . . . 12 |- (y e. N. -> (ch -> th))
118	116, 117	sylbir 218	. . . . . . . . . . 11 |- ((y e. om /\ (/) e. y) -> (ch -> th))
119	24	sseq1i 2641	. . . . . . . . . . . 12 |- (1o C_ y <-> suc (/) C_ y)
120		0ex 3446	. . . . . . . . . . . . 13 |- (/) e. _V
121		sucssel 3763	. . . . . . . . . . . . 13 |- ((/) e. _V -> (suc (/) C_ y -> (/) e. y))
122	120, 121	ax-mp 7	. . . . . . . . . . . 12 |- (suc (/) C_ y -> (/) e. y)
123	119, 122	sylbi 216	. . . . . . . . . . 11 |- (1o C_ y -> (/) e. y)
124	118, 123	sylan2 500	. . . . . . . . . 10 |- ((y e. om /\ 1o C_ y) -> (ch -> th))
125	115, 124	syl9r 72	. . . . . . . . 9 |- ((y e. om /\ 1o C_ y) -> (((y e. N. /\ 1o <N y) -> ch) -> ((y e. N. /\ 1o <N suc y) -> th)))
126	125	adantlr 429	. . . . . . . 8 |- (((y e. om /\ 1o e. om) /\ 1o C_ y) -> (((y e. N. /\ 1o <N y) -> ch) -> ((y e. N. /\ 1o <N suc y) -> th)))
127	33, 38, 90, 94, 95, 126	findsg 3980	. . . . . . 7 |- (((A e. om /\ 1o e. om) /\ 1o C_ A) -> ((A e. N. /\ 1o <N A) -> ta))
128	29, 127	mpanl2 771	. . . . . 6 |- ((A e. om /\ 1o C_ A) -> ((A e. N. /\ 1o <N A) -> ta))
129	19, 28, 128	syl11anc 524	. . . . 5 |- (A e. N. -> ((A e. N. /\ 1o <N A) -> ta))
130	129	exp3a 405	. . . 4 |- (A e. N. -> (A e. N. -> (1o <N A -> ta)))
131	130	pm2.43i 78	. . 3 |- (A e. N. -> (1o <N A -> ta))
132	18, 131	jaod 469	. 2 |- (A e. N. -> ((A = 1o \/ 1o <N A) -> ta))
133	9, 132	mpd 29	1 |- (A e. N. -> ta)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   = wceq 1298   e. wcel 1300   =/= wne 2017  _Vcvv 2292   C_ wss 2593  (/)c0 2875   class class class wbr 3338   Or wor 3590  Ord word 3656  Oncon0 3657  suc csuc 3659  omcom 3949  (class class class)co 4884  1oc1o 5172   +o coa 5174  N.cnpi 6124   +N cpli 6125   <N clti 6127

This theorem is referenced by:  prlem934a 6289

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-fv 4014  df-opr 4886  df-oprab 4887  df-rdg 5140  df-1o 5177  df-oadd 5179  df-ni 6152  df-pli 6153  df-lti 6155

Copyright terms: Public domain