Theorem indstr 8681

Description: Strong Mathematical Induction for positive integers (inference schema). (Contributed by NM, 17-Aug-2001.)

Hypotheses

Ref	Expression
indstr.1	|- ( x = y -> ( ph <-> ps ) )
indstr.2	|- ( x e. NN -> ( A. y e. NN ( y < x -> ps ) -> ph ) )

Assertion

Ref	Expression
indstr	|- ( x e. NN -> ph )

Distinct variable groups:   x, y   ph, y   ps, x

Allowed substitution hints:   ph( x)   ps( y)

Proof of Theorem indstr

Dummy variables z w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq2 3789	. . . . 5 |- ( z = 1 -> ( y < z <-> y < 1 ) )
2	1	imbi1d 229	. . . 4 |- ( z = 1 -> ( ( y < z -> ps ) <-> ( y < 1 -> ps ) ) )
3	2	ralbidv 2368	. . 3 |- ( z = 1 -> ( A. y e. NN ( y < z -> ps ) <-> A. y e. NN ( y < 1 -> ps ) ) )
4		breq2 3789	. . . . 5 |- ( z = w -> ( y < z <-> y < w ) )
5	4	imbi1d 229	. . . 4 |- ( z = w -> ( ( y < z -> ps ) <-> ( y < w -> ps ) ) )
6	5	ralbidv 2368	. . 3 |- ( z = w -> ( A. y e. NN ( y < z -> ps ) <-> A. y e. NN ( y < w -> ps ) ) )
7		breq2 3789	. . . . 5 |- ( z = ( w + 1 ) -> ( y < z <-> y < ( w + 1 ) ) )
8	7	imbi1d 229	. . . 4 |- ( z = ( w + 1 ) -> ( ( y < z -> ps ) <-> ( y < ( w + 1 ) -> ps ) ) )
9	8	ralbidv 2368	. . 3 |- ( z = ( w + 1 ) -> ( A. y e. NN ( y < z -> ps ) <-> A. y e. NN ( y < ( w + 1 ) -> ps ) ) )
10		breq2 3789	. . . . 5 |- ( z = x -> ( y < z <-> y < x ) )
11	10	imbi1d 229	. . . 4 |- ( z = x -> ( ( y < z -> ps ) <-> ( y < x -> ps ) ) )
12	11	ralbidv 2368	. . 3 |- ( z = x -> ( A. y e. NN ( y < z -> ps ) <-> A. y e. NN ( y < x -> ps ) ) )
13		nnnlt1 8065	. . . . 5 |- ( y e. NN -> -. y < 1 )
14	13	pm2.21d 581	. . . 4 |- ( y e. NN -> ( y < 1 -> ps ) )
15	14	rgen 2416	. . 3 |- A. y e. NN ( y < 1 -> ps )
16		1nn 8050	. . . . 5 |- 1 e. NN
17		elex2 2615	. . . . 5 |- ( 1 e. NN -> E. u u e. NN )
18		nfra1 2397	. . . . . 6 |- F/ y A. y e. NN ( y < w -> ps )
19	18	r19.3rm 3330	. . . . 5 |- ( E. u u e. NN -> ( A. y e. NN ( y < w -> ps ) <-> A. y e. NN A. y e. NN ( y < w -> ps ) ) )
20	16, 17, 19	mp2b 8	. . . 4 |- ( A. y e. NN ( y < w -> ps ) <-> A. y e. NN A. y e. NN ( y < w -> ps ) )
21		rsp 2411	. . . . . . . . . 10 |- ( A. y e. NN ( y < w -> ps ) -> ( y e. NN -> ( y < w -> ps ) ) )
22	21	com12 30	. . . . . . . . 9 |- ( y e. NN -> ( A. y e. NN ( y < w -> ps ) -> ( y < w -> ps ) ) )
23	22	adantl 271	. . . . . . . 8 |- ( ( w e. NN /\ y e. NN ) -> ( A. y e. NN ( y < w -> ps ) -> ( y < w -> ps ) ) )
24		indstr.2	. . . . . . . . . . . . 13 |- ( x e. NN -> ( A. y e. NN ( y < x -> ps ) -> ph ) )
25	24	rgen 2416	. . . . . . . . . . . 12 |- A. x e. NN ( A. y e. NN ( y < x -> ps ) -> ph )
26		nfv 1461	. . . . . . . . . . . . 13 |- F/ w ( A. y e. NN ( y < x -> ps ) -> ph )
27		nfv 1461	. . . . . . . . . . . . . 14 |- F/ x A. y e. NN ( y < w -> ps )
28		nfsbc1v 2833	. . . . . . . . . . . . . 14 |- F/ x [. w / x ]. ph
29	27, 28	nfim 1504	. . . . . . . . . . . . 13 |- F/ x ( A. y e. NN ( y < w -> ps ) -> [. w / x ]. ph )
30		breq2 3789	. . . . . . . . . . . . . . . 16 |- ( x = w -> ( y < x <-> y < w ) )
31	30	imbi1d 229	. . . . . . . . . . . . . . 15 |- ( x = w -> ( ( y < x -> ps ) <-> ( y < w -> ps ) ) )
32	31	ralbidv 2368	. . . . . . . . . . . . . 14 |- ( x = w -> ( A. y e. NN ( y < x -> ps ) <-> A. y e. NN ( y < w -> ps ) ) )
33		sbceq1a 2824	. . . . . . . . . . . . . 14 |- ( x = w -> ( ph <-> [. w / x ]. ph ) )
34	32, 33	imbi12d 232	. . . . . . . . . . . . 13 |- ( x = w -> ( ( A. y e. NN ( y < x -> ps ) -> ph ) <-> ( A. y e. NN ( y < w -> ps ) -> [. w / x ]. ph ) ) )
35	26, 29, 34	cbvral 2573	. . . . . . . . . . . 12 |- ( A. x e. NN ( A. y e. NN ( y < x -> ps ) -> ph ) <-> A. w e. NN ( A. y e. NN ( y < w -> ps ) -> [. w / x ]. ph ) )
36	25, 35	mpbi 143	. . . . . . . . . . 11 |- A. w e. NN ( A. y e. NN ( y < w -> ps ) -> [. w / x ]. ph )
37	36	rspec 2415	. . . . . . . . . 10 |- ( w e. NN -> ( A. y e. NN ( y < w -> ps ) -> [. w / x ]. ph ) )
38		vex 2604	. . . . . . . . . . . . 13 |- y e. _V
39		indstr.1	. . . . . . . . . . . . 13 |- ( x = y -> ( ph <-> ps ) )
40	38, 39	sbcie 2848	. . . . . . . . . . . 12 |- ( [. y / x ]. ph <-> ps )
41		dfsbcq 2817	. . . . . . . . . . . 12 |- ( y = w -> ( [. y / x ]. ph <-> [. w / x ]. ph ) )
42	40, 41	syl5bbr 192	. . . . . . . . . . 11 |- ( y = w -> ( ps <-> [. w / x ]. ph ) )
43	42	biimprcd 158	. . . . . . . . . 10 |- ( [. w / x ]. ph -> ( y = w -> ps ) )
44	37, 43	syl6 33	. . . . . . . . 9 |- ( w e. NN -> ( A. y e. NN ( y < w -> ps ) -> ( y = w -> ps ) ) )
45	44	adantr 270	. . . . . . . 8 |- ( ( w e. NN /\ y e. NN ) -> ( A. y e. NN ( y < w -> ps ) -> ( y = w -> ps ) ) )
46	23, 45	jcad 301	. . . . . . 7 |- ( ( w e. NN /\ y e. NN ) -> ( A. y e. NN ( y < w -> ps ) -> ( ( y < w -> ps ) /\ ( y = w -> ps ) ) ) )
47		jaob 663	. . . . . . 7 |- ( ( ( y < w \/ y = w ) -> ps ) <-> ( ( y < w -> ps ) /\ ( y = w -> ps ) ) )
48	46, 47	syl6ibr 160	. . . . . 6 |- ( ( w e. NN /\ y e. NN ) -> ( A. y e. NN ( y < w -> ps ) -> ( ( y < w \/ y = w ) -> ps ) ) )
49		nnleltp1 8410	. . . . . . . . 9 |- ( ( y e. NN /\ w e. NN ) -> ( y <_ w <-> y < ( w + 1 ) ) )
50		nnz 8370	. . . . . . . . . 10 |- ( y e. NN -> y e. ZZ )
51		nnz 8370	. . . . . . . . . 10 |- ( w e. NN -> w e. ZZ )
52		zleloe 8398	. . . . . . . . . 10 |- ( ( y e. ZZ /\ w e. ZZ ) -> ( y <_ w <-> ( y < w \/ y = w ) ) )
53	50, 51, 52	syl2an 283	. . . . . . . . 9 |- ( ( y e. NN /\ w e. NN ) -> ( y <_ w <-> ( y < w \/ y = w ) ) )
54	49, 53	bitr3d 188	. . . . . . . 8 |- ( ( y e. NN /\ w e. NN ) -> ( y < ( w + 1 ) <-> ( y < w \/ y = w ) ) )
55	54	ancoms 264	. . . . . . 7 |- ( ( w e. NN /\ y e. NN ) -> ( y < ( w + 1 ) <-> ( y < w \/ y = w ) ) )
56	55	imbi1d 229	. . . . . 6 |- ( ( w e. NN /\ y e. NN ) -> ( ( y < ( w + 1 ) -> ps ) <-> ( ( y < w \/ y = w ) -> ps ) ) )
57	48, 56	sylibrd 167	. . . . 5 |- ( ( w e. NN /\ y e. NN ) -> ( A. y e. NN ( y < w -> ps ) -> ( y < ( w + 1 ) -> ps ) ) )
58	57	ralimdva 2429	. . . 4 |- ( w e. NN -> ( A. y e. NN A. y e. NN ( y < w -> ps ) -> A. y e. NN ( y < ( w + 1 ) -> ps ) ) )
59	20, 58	syl5bi 150	. . 3 |- ( w e. NN -> ( A. y e. NN ( y < w -> ps ) -> A. y e. NN ( y < ( w + 1 ) -> ps ) ) )
60	3, 6, 9, 12, 15, 59	nnind 8055	. 2 |- ( x e. NN -> A. y e. NN ( y < x -> ps ) )
61	60, 24	mpd 13	1 |- ( x e. NN -> ph )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103   \/ wo 661   = wceq 1284   E.wex 1421   e. wcel 1433   A.wral 2348   [.wsbc 2815   class class class wbr 3785  (class class class)co 5532   1c1 6982   + caddc 6984   < clt 7153   <_ cle 7154   NNcn 8039   ZZcz 8351

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 576  ax-in2 577  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-13 1444  ax-14 1445  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-sep 3896  ax-pow 3948  ax-pr 3964  ax-un 4188  ax-setind 4280  ax-cnex 7067  ax-resscn 7068  ax-1cn 7069  ax-1re 7070  ax-icn 7071  ax-addcl 7072  ax-addrcl 7073  ax-mulcl 7074  ax-addcom 7076  ax-addass 7078  ax-distr 7080  ax-i2m1 7081  ax-0lt1 7082  ax-0id 7084  ax-rnegex 7085  ax-cnre 7087  ax-pre-ltirr 7088  ax-pre-ltwlin 7089  ax-pre-lttrn 7090  ax-pre-ltadd 7092

This theorem depends on definitions:  df-bi 115  df-3or 920  df-3an 921  df-tru 1287  df-fal 1290  df-nf 1390  df-sb 1686  df-eu 1944  df-mo 1945  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ne 2246  df-nel 2340  df-ral 2353  df-rex 2354  df-reu 2355  df-rab 2357  df-v 2603  df-sbc 2816  df-dif 2975  df-un 2977  df-in 2979  df-ss 2986  df-pw 3384  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-int 3637  df-br 3786  df-opab 3840  df-id 4048  df-xp 4369  df-rel 4370  df-cnv 4371  df-co 4372  df-dm 4373  df-iota 4887  df-fun 4924  df-fv 4930  df-riota 5488  df-ov 5535  df-oprab 5536  df-mpt2 5537  df-pnf 7155  df-mnf 7156  df-xr 7157  df-ltxr 7158  df-le 7159  df-sub 7281  df-neg 7282  df-inn 8040  df-n0 8289  df-z 8352

This theorem is referenced by:  indstr2  8696