Theorem indstr 9483

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 3965	. . . . 5 ⊢ (𝑧 = 1 → (𝑦 < 𝑧 ↔ 𝑦 < 1))
2	1	imbi1d 230	. . . 4 ⊢ (𝑧 = 1 → ((𝑦 < 𝑧 → 𝜓) ↔ (𝑦 < 1 → 𝜓)))
3	2	ralbidv 2454	. . 3 ⊢ (𝑧 = 1 → (∀𝑦 ∈ ℕ (𝑦 < 𝑧 → 𝜓) ↔ ∀𝑦 ∈ ℕ (𝑦 < 1 → 𝜓)))
4		breq2 3965	. . . . 5 ⊢ (𝑧 = 𝑤 → (𝑦 < 𝑧 ↔ 𝑦 < 𝑤))
5	4	imbi1d 230	. . . 4 ⊢ (𝑧 = 𝑤 → ((𝑦 < 𝑧 → 𝜓) ↔ (𝑦 < 𝑤 → 𝜓)))
6	5	ralbidv 2454	. . 3 ⊢ (𝑧 = 𝑤 → (∀𝑦 ∈ ℕ (𝑦 < 𝑧 → 𝜓) ↔ ∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓)))
7		breq2 3965	. . . . 5 ⊢ (𝑧 = (𝑤 + 1) → (𝑦 < 𝑧 ↔ 𝑦 < (𝑤 + 1)))
8	7	imbi1d 230	. . . 4 ⊢ (𝑧 = (𝑤 + 1) → ((𝑦 < 𝑧 → 𝜓) ↔ (𝑦 < (𝑤 + 1) → 𝜓)))
9	8	ralbidv 2454	. . 3 ⊢ (𝑧 = (𝑤 + 1) → (∀𝑦 ∈ ℕ (𝑦 < 𝑧 → 𝜓) ↔ ∀𝑦 ∈ ℕ (𝑦 < (𝑤 + 1) → 𝜓)))
10		breq2 3965	. . . . 5 ⊢ (𝑧 = 𝑥 → (𝑦 < 𝑧 ↔ 𝑦 < 𝑥))
11	10	imbi1d 230	. . . 4 ⊢ (𝑧 = 𝑥 → ((𝑦 < 𝑧 → 𝜓) ↔ (𝑦 < 𝑥 → 𝜓)))
12	11	ralbidv 2454	. . 3 ⊢ (𝑧 = 𝑥 → (∀𝑦 ∈ ℕ (𝑦 < 𝑧 → 𝜓) ↔ ∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓)))
13		nnnlt1 8838	. . . . 5 ⊢ (𝑦 ∈ ℕ → ¬ 𝑦 < 1)
14	13	pm2.21d 609	. . . 4 ⊢ (𝑦 ∈ ℕ → (𝑦 < 1 → 𝜓))
15	14	rgen 2507	. . 3 ⊢ ∀𝑦 ∈ ℕ (𝑦 < 1 → 𝜓)
16		1nn 8823	. . . . 5 ⊢ 1 ∈ ℕ
17		elex2 2725	. . . . 5 ⊢ (1 ∈ ℕ → ∃𝑢 𝑢 ∈ ℕ)
18		nfra1 2485	. . . . . 6 ⊢ Ⅎ𝑦∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓)
19	18	r19.3rm 3478	. . . . 5 ⊢ (∃𝑢 𝑢 ∈ ℕ → (∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) ↔ ∀𝑦 ∈ ℕ ∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓)))
20	16, 17, 19	mp2b 8	. . . 4 ⊢ (∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) ↔ ∀𝑦 ∈ ℕ ∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓))
21		rsp 2501	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) → (𝑦 ∈ ℕ → (𝑦 < 𝑤 → 𝜓)))
22	21	com12 30	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) → (𝑦 < 𝑤 → 𝜓)))
23	22	adantl 275	. . . . . . . 8 ⊢ ((𝑤 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) → (𝑦 < 𝑤 → 𝜓)))
24		indstr.2	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℕ → (∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) → 𝜑))
25	24	rgen 2507	. . . . . . . . . . . 12 ⊢ ∀𝑥 ∈ ℕ (∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) → 𝜑)
26		nfv 1505	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑤(∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) → 𝜑)
27		nfv 1505	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓)
28		nfsbc1v 2951	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥[𝑤 / 𝑥]𝜑
29	27, 28	nfim 1549	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) → [𝑤 / 𝑥]𝜑)
30		breq2 3965	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → (𝑦 < 𝑥 ↔ 𝑦 < 𝑤))
31	30	imbi1d 230	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → ((𝑦 < 𝑥 → 𝜓) ↔ (𝑦 < 𝑤 → 𝜓)))
32	31	ralbidv 2454	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) ↔ ∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓)))
33		sbceq1a 2942	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (𝜑 ↔ [𝑤 / 𝑥]𝜑))
34	32, 33	imbi12d 233	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → ((∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) → 𝜑) ↔ (∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) → [𝑤 / 𝑥]𝜑)))
35	26, 29, 34	cbvral 2673	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ ℕ (∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓) → 𝜑) ↔ ∀𝑤 ∈ ℕ (∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) → [𝑤 / 𝑥]𝜑))
36	25, 35	mpbi 144	. . . . . . . . . . 11 ⊢ ∀𝑤 ∈ ℕ (∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) → [𝑤 / 𝑥]𝜑)
37	36	rspec 2506	. . . . . . . . . 10 ⊢ (𝑤 ∈ ℕ → (∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) → [𝑤 / 𝑥]𝜑))
38		vex 2712	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
39		indstr.1	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
40	38, 39	sbcie 2967	. . . . . . . . . . . 12 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)
41		dfsbcq 2935	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑤 → ([𝑦 / 𝑥]𝜑 ↔ [𝑤 / 𝑥]𝜑))
42	40, 41	bitr3id 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 700	. . . . . . 7 ⊢ (((𝑦 < 𝑤 ∨ 𝑦 = 𝑤) → 𝜓) ↔ ((𝑦 < 𝑤 → 𝜓) ∧ (𝑦 = 𝑤 → 𝜓)))
48	46, 47	syl6ibr 161	. . . . . 6 ⊢ ((𝑤 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) → ((𝑦 < 𝑤 ∨ 𝑦 = 𝑤) → 𝜓)))
49		nnleltp1 9205	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) → (𝑦 ≤ 𝑤 ↔ 𝑦 < (𝑤 + 1)))
50		nnz 9165	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
51		nnz 9165	. . . . . . . . . 10 ⊢ (𝑤 ∈ ℕ → 𝑤 ∈ ℤ)
52		zleloe 9193	. . . . . . . . . 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 2521	. . . 4 ⊢ (𝑤 ∈ ℕ → (∀𝑦 ∈ ℕ ∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) → ∀𝑦 ∈ ℕ (𝑦 < (𝑤 + 1) → 𝜓)))
59	20, 58	syl5bi 151	. . 3 ⊢ (𝑤 ∈ ℕ → (∀𝑦 ∈ ℕ (𝑦 < 𝑤 → 𝜓) → ∀𝑦 ∈ ℕ (𝑦 < (𝑤 + 1) → 𝜓)))
60	3, 6, 9, 12, 15, 59	nnind 8828	. 2 ⊢ (𝑥 ∈ ℕ → ∀𝑦 ∈ ℕ (𝑦 < 𝑥 → 𝜓))
61	60, 24	mpd 13	1 ⊢ (𝑥 ∈ ℕ → 𝜑)

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698   = wceq 1332  ∃wex 1469   ∈ wcel 2125  ∀wral 2432  [wsbc 2933   class class class wbr 3961  (class class class)co 5814  1c1 7712   + caddc 7714   < clt 7891   ≤ cle 7892  ℕcn 8812  ℤcz 9146

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 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-13 2127  ax-14 2128  ax-ext 2136  ax-sep 4078  ax-pow 4130  ax-pr 4164  ax-un 4388  ax-setind 4490  ax-cnex 7802  ax-resscn 7803  ax-1cn 7804  ax-1re 7805  ax-icn 7806  ax-addcl 7807  ax-addrcl 7808  ax-mulcl 7809  ax-addcom 7811  ax-addass 7813  ax-distr 7815  ax-i2m1 7816  ax-0lt1 7817  ax-0id 7819  ax-rnegex 7820  ax-cnre 7822  ax-pre-ltirr 7823  ax-pre-ltwlin 7824  ax-pre-lttrn 7825  ax-pre-ltadd 7827

This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1740  df-eu 2006  df-mo 2007  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-ne 2325  df-nel 2420  df-ral 2437  df-rex 2438  df-reu 2439  df-rab 2441  df-v 2711  df-sbc 2934  df-dif 3100  df-un 3102  df-in 3104  df-ss 3111  df-pw 3541  df-sn 3562  df-pr 3563  df-op 3565  df-uni 3769  df-int 3804  df-br 3962  df-opab 4022  df-id 4248  df-xp 4585  df-rel 4586  df-cnv 4587  df-co 4588  df-dm 4589  df-iota 5128  df-fun 5165  df-fv 5171  df-riota 5770  df-ov 5817  df-oprab 5818  df-mpo 5819  df-pnf 7893  df-mnf 7894  df-xr 7895  df-ltxr 7896  df-le 7897  df-sub 8027  df-neg 8028  df-inn 8813  df-n0 9070  df-z 9147

This theorem is referenced by:  indstr2  9498