Theorem indstr 8681

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

Hypotheses

Ref	Expression
indstr.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
indstr.2	⊢ (𝑥 ∈ ℕ → (∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) → 𝜑))

Assertion

Ref	Expression
indstr	⊢ (𝑥 ∈ ℕ → 𝜑)

Distinct variable groups:   𝑥,𝑦   𝜑,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem indstr

Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.

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

Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103   ∨ wo 661   = wceq 1284  ∃wex 1421   ∈ wcel 1433  ∀wral 2348  [wsbc 2815   class class class wbr 3785  (class class class)co 5532  1c1 6982   + caddc 6984   < clt 7153   ≤ cle 7154  ℕcn 8039  ℤcz 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