Theorem indstr 9388

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 3933	. . . . 5 ⊢ (𝑧 = 1 → (𝑦 < 𝑧 ↔ 𝑦 < 1))
2	1	imbi1d 230	. . . 4 ⊢ (𝑧 = 1 → ((𝑦 < 𝑧 → 𝜓) ↔ (𝑦 < 1 → 𝜓)))
3	2	ralbidv 2437	. . 3 ⊢ (𝑧 = 1 → (∀𝑦 ∈ ℕ (𝑦 < 𝑧 → 𝜓) ↔ ∀𝑦 ∈ ℕ (𝑦 < 1 → 𝜓)))
4		breq2 3933	. . . . 5 ⊢ (𝑧 = 𝑤 → (𝑦 < 𝑧 ↔ 𝑦 < 𝑤))
5	4	imbi1d 230	. . . 4 ⊢ (𝑧 = 𝑤 → ((𝑦 < 𝑧 → 𝜓) ↔ (𝑦 < 𝑤 → 𝜓)))
6	5	ralbidv 2437	. . 3 ⊢ (𝑧 = 𝑤 → (∀𝑦 ∈ ℕ (𝑦 < 𝑧 → 𝜓) ↔ ∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓)))
7		breq2 3933	. . . . 5 ⊢ (𝑧 = (𝑤 + 1) → (𝑦 < 𝑧 ↔ 𝑦 < (𝑤 + 1)))
8	7	imbi1d 230	. . . 4 ⊢ (𝑧 = (𝑤 + 1) → ((𝑦 < 𝑧 → 𝜓) ↔ (𝑦 < (𝑤 + 1) → 𝜓)))
9	8	ralbidv 2437	. . 3 ⊢ (𝑧 = (𝑤 + 1) → (∀𝑦 ∈ ℕ (𝑦 < 𝑧 → 𝜓) ↔ ∀𝑦 ∈ ℕ (𝑦 < (𝑤 + 1) → 𝜓)))
10		breq2 3933	. . . . 5 ⊢ (𝑧 = 𝑥 → (𝑦 < 𝑧 ↔ 𝑦 < 𝑥))
11	10	imbi1d 230	. . . 4 ⊢ (𝑧 = 𝑥 → ((𝑦 < 𝑧 → 𝜓) ↔ (𝑦 < 𝑥 → 𝜓)))
12	11	ralbidv 2437	. . 3 ⊢ (𝑧 = 𝑥 → (∀𝑦 ∈ ℕ (𝑦 < 𝑧 → 𝜓) ↔ ∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓)))
13		nnnlt1 8746	. . . . 5 ⊢ (𝑦 ∈ ℕ → ¬ 𝑦 < 1)
14	13	pm2.21d 608	. . . 4 ⊢ (𝑦 ∈ ℕ → (𝑦 < 1 → 𝜓))
15	14	rgen 2485	. . 3 ⊢ ∀𝑦 ∈ ℕ (𝑦 < 1 → 𝜓)
16		1nn 8731	. . . . 5 ⊢ 1 ∈ ℕ
17		elex2 2702	. . . . 5 ⊢ (1 ∈ ℕ → ∃𝑢 𝑢 ∈ ℕ)
18		nfra1 2466	. . . . . 6 ⊢ Ⅎ𝑦∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓)
19	18	r19.3rm 3451	. . . . 5 ⊢ (∃𝑢 𝑢 ∈ ℕ → (∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) ↔ ∀𝑦 ∈ ℕ ∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓)))
20	16, 17, 19	mp2b 8	. . . 4 ⊢ (∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) ↔ ∀𝑦 ∈ ℕ ∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓))
21		rsp 2480	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) → (𝑦 ∈ ℕ → (𝑦 < 𝑤 → 𝜓)))
22	21	com12 30	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) → (𝑦 < 𝑤 → 𝜓)))
23	22	adantl 275	. . . . . . . 8 ⊢ ((𝑤 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) → (𝑦 < 𝑤 → 𝜓)))
24		indstr.2	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℕ → (∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) → 𝜑))
25	24	rgen 2485	. . . . . . . . . . . 12 ⊢ ∀𝑥 ∈ ℕ (∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) → 𝜑)
26		nfv 1508	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑤(∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) → 𝜑)
27		nfv 1508	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓)
28		nfsbc1v 2927	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥[𝑤 / 𝑥]𝜑
29	27, 28	nfim 1551	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) → [𝑤 / 𝑥]𝜑)
30		breq2 3933	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → (𝑦 < 𝑥 ↔ 𝑦 < 𝑤))
31	30	imbi1d 230	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → ((𝑦 < 𝑥 → 𝜓) ↔ (𝑦 < 𝑤 → 𝜓)))
32	31	ralbidv 2437	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) ↔ ∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓)))
33		sbceq1a 2918	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (𝜑 ↔ [𝑤 / 𝑥]𝜑))
34	32, 33	imbi12d 233	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → ((∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) → 𝜑) ↔ (∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) → [𝑤 / 𝑥]𝜑)))
35	26, 29, 34	cbvral 2650	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ ℕ (∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) → 𝜑) ↔ ∀𝑤 ∈ ℕ (∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) → [𝑤 / 𝑥]𝜑))
36	25, 35	mpbi 144	. . . . . . . . . . 11 ⊢ ∀𝑤 ∈ ℕ (∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) → [𝑤 / 𝑥]𝜑)
37	36	rspec 2484	. . . . . . . . . 10 ⊢ (𝑤 ∈ ℕ → (∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) → [𝑤 / 𝑥]𝜑))
38		vex 2689	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
39		indstr.1	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
40	38, 39	sbcie 2943	. . . . . . . . . . . 12 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)
41		dfsbcq 2911	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑤 → ([𝑦 / 𝑥]𝜑 ↔ [𝑤 / 𝑥]𝜑))
42	40, 41	syl5bbr 193	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑤 → (𝜓 ↔ [𝑤 / 𝑥]𝜑))
43	42	biimprcd 159	. . . . . . . . . 10 ⊢ ([𝑤 / 𝑥]𝜑 → (𝑦 = 𝑤 → 𝜓))
44	37, 43	syl6 33	. . . . . . . . 9 ⊢ (𝑤 ∈ ℕ → (∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) → (𝑦 = 𝑤 → 𝜓)))
45	44	adantr 274	. . . . . . . 8 ⊢ ((𝑤 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) → (𝑦 = 𝑤 → 𝜓)))
46	23, 45	jcad 305	. . . . . . 7 ⊢ ((𝑤 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) → ((𝑦 < 𝑤 → 𝜓) ∧ (𝑦 = 𝑤 → 𝜓))))
47		jaob 699	. . . . . . 7 ⊢ (((𝑦 < 𝑤 ∨ 𝑦 = 𝑤) → 𝜓) ↔ ((𝑦 < 𝑤 → 𝜓) ∧ (𝑦 = 𝑤 → 𝜓)))
48	46, 47	syl6ibr 161	. . . . . 6 ⊢ ((𝑤 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) → ((𝑦 < 𝑤 ∨ 𝑦 = 𝑤) → 𝜓)))
49		nnleltp1 9113	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) → (𝑦 ≤ 𝑤 ↔ 𝑦 < (𝑤 + 1)))
50		nnz 9073	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
51		nnz 9073	. . . . . . . . . 10 ⊢ (𝑤 ∈ ℕ → 𝑤 ∈ ℤ)
52		zleloe 9101	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℤ ∧ 𝑤 ∈ ℤ) → (𝑦 ≤ 𝑤 ↔ (𝑦 < 𝑤 ∨ 𝑦 = 𝑤)))
53	50, 51, 52	syl2an 287	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) → (𝑦 ≤ 𝑤 ↔ (𝑦 < 𝑤 ∨ 𝑦 = 𝑤)))
54	49, 53	bitr3d 189	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) → (𝑦 < (𝑤 + 1) ↔ (𝑦 < 𝑤 ∨ 𝑦 = 𝑤)))
55	54	ancoms 266	. . . . . . 7 ⊢ ((𝑤 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑦 < (𝑤 + 1) ↔ (𝑦 < 𝑤 ∨ 𝑦 = 𝑤)))
56	55	imbi1d 230	. . . . . 6 ⊢ ((𝑤 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝑦 < (𝑤 + 1) → 𝜓) ↔ ((𝑦 < 𝑤 ∨ 𝑦 = 𝑤) → 𝜓)))
57	48, 56	sylibrd 168	. . . . 5 ⊢ ((𝑤 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) → (𝑦 < (𝑤 + 1) → 𝜓)))
58	57	ralimdva 2499	. . . 4 ⊢ (𝑤 ∈ ℕ → (∀𝑦 ∈ ℕ ∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) → ∀𝑦 ∈ ℕ (𝑦 < (𝑤 + 1) → 𝜓)))
59	20, 58	syl5bi 151	. . 3 ⊢ (𝑤 ∈ ℕ → (∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) → ∀𝑦 ∈ ℕ (𝑦 < (𝑤 + 1) → 𝜓)))
60	3, 6, 9, 12, 15, 59	nnind 8736	. 2 ⊢ (𝑥 ∈ ℕ → ∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓))
61	60, 24	mpd 13	1 ⊢ (𝑥 ∈ ℕ → 𝜑)

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 697   = wceq 1331  ∃wex 1468   ∈ wcel 1480  ∀wral 2416  [wsbc 2909   class class class wbr 3929  (class class class)co 5774  1c1 7621   + caddc 7623   < clt 7800   ≤ cle 7801  ℕcn 8720  ℤcz 9054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-cnex 7711  ax-resscn 7712  ax-1cn 7713  ax-1re 7714  ax-icn 7715  ax-addcl 7716  ax-addrcl 7717  ax-mulcl 7718  ax-addcom 7720  ax-addass 7722  ax-distr 7724  ax-i2m1 7725  ax-0lt1 7726  ax-0id 7728  ax-rnegex 7729  ax-cnre 7731  ax-pre-ltirr 7732  ax-pre-ltwlin 7733  ax-pre-lttrn 7734  ax-pre-ltadd 7736

This theorem depends on definitions:  df-bi 116  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-br 3930  df-opab 3990  df-id 4215  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-iota 5088  df-fun 5125  df-fv 5131  df-riota 5730  df-ov 5777  df-oprab 5778  df-mpo 5779  df-pnf 7802  df-mnf 7803  df-xr 7804  df-ltxr 7805  df-le 7806  df-sub 7935  df-neg 7936  df-inn 8721  df-n0 8978  df-z 9055

This theorem is referenced by:  indstr2  9403