dvnp1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dvnp1		Structured version Visualization version GIF version

Theorem dvnp1 25825

Description: Successor iterated derivative. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)

**Assertion**
Ref	Expression
dvnp1	⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → ((𝑆 D^𝑛 𝐹)‘(𝑁 + 1)) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘𝑁)))

Proof of Theorem dvnp1 Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp3 1138	. . . . 5 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → 𝑁 ∈ ℕ₀)
2		nn0uz 12777	. . . . 5 ⊢ ℕ₀ = (ℤ_≥‘0)
3	1, 2	eleqtrdi 2838	. . . 4 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → 𝑁 ∈ (ℤ_≥‘0))
4		seqp1 13923	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘0) → (seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘(𝑁 + 1)) = ((seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘𝑁)((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st )((ℕ₀ × {𝐹})‘(𝑁 + 1))))
5	3, 4	syl 17	. . 3 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → (seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘(𝑁 + 1)) = ((seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘𝑁)((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st )((ℕ₀ × {𝐹})‘(𝑁 + 1))))
6		fvex 6835	. . . 4 ⊢ (seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘𝑁) ∈ V
7		fvex 6835	. . . 4 ⊢ ((ℕ₀ × {𝐹})‘(𝑁 + 1)) ∈ V
8	6, 7	opco1i 8058	. . 3 ⊢ ((seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘𝑁)((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st )((ℕ₀ × {𝐹})‘(𝑁 + 1))) = ((𝑥 ∈ V ↦ (𝑆 D 𝑥))‘(seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘𝑁))
9	5, 8	eqtrdi 2780	. 2 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → (seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘(𝑁 + 1)) = ((𝑥 ∈ V ↦ (𝑆 D 𝑥))‘(seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘𝑁)))
10		eqid 2729	. . . . 5 ⊢ (𝑥 ∈ V ↦ (𝑆 D 𝑥)) = (𝑥 ∈ V ↦ (𝑆 D 𝑥))
11	10	dvnfval 25822	. . . 4 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆)) → (𝑆 D^𝑛 𝐹) = seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹})))
12	11	3adant3 1132	. . 3 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → (𝑆 D^𝑛 𝐹) = seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹})))
13	12	fveq1d 6824	. 2 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → ((𝑆 D^𝑛 𝐹)‘(𝑁 + 1)) = (seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘(𝑁 + 1)))
14		fvex 6835	. . . 4 ⊢ ((𝑆 D^𝑛 𝐹)‘𝑁) ∈ V
15		oveq2 7357	. . . . 5 ⊢ (𝑥 = ((𝑆 D^𝑛 𝐹)‘𝑁) → (𝑆 D 𝑥) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘𝑁)))
16		ovex 7382	. . . . 5 ⊢ (𝑆 D ((𝑆 D^𝑛 𝐹)‘𝑁)) ∈ V
17	15, 10, 16	fvmpt 6930	. . . 4 ⊢ (((𝑆 D^𝑛 𝐹)‘𝑁) ∈ V → ((𝑥 ∈ V ↦ (𝑆 D 𝑥))‘((𝑆 D^𝑛 𝐹)‘𝑁)) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘𝑁)))
18	14, 17	ax-mp 5	. . 3 ⊢ ((𝑥 ∈ V ↦ (𝑆 D 𝑥))‘((𝑆 D^𝑛 𝐹)‘𝑁)) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘𝑁))
19	12	fveq1d 6824	. . . 4 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → ((𝑆 D^𝑛 𝐹)‘𝑁) = (seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘𝑁))
20	19	fveq2d 6826	. . 3 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → ((𝑥 ∈ V ↦ (𝑆 D 𝑥))‘((𝑆 D^𝑛 𝐹)‘𝑁)) = ((𝑥 ∈ V ↦ (𝑆 D 𝑥))‘(seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘𝑁)))
21	18, 20	eqtr3id 2778	. 2 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → (𝑆 D ((𝑆 D^𝑛 𝐹)‘𝑁)) = ((𝑥 ∈ V ↦ (𝑆 D 𝑥))‘(seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘𝑁)))
22	9, 13, 21	3eqtr4d 2774	1 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → ((𝑆 D^𝑛 𝐹)‘(𝑁 + 1)) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘𝑁)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 Vcvv 3436 ⊆ wss 3903 {csn 4577 ↦ cmpt 5173 × cxp 5617 ∘ ccom 5623 ‘cfv 6482 (class class class)co 7349 1^st c1st 7922 ↑_pm cpm 8754 ℂcc 11007 0cc0 11009 1c1 11010 + caddc 11012 ℕ₀cn0 12384 ℤ_≥cuz 12735 seqcseq 13908 D cdv 25762 D^𝑛 cdvn 25763

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-inf2 9537 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4859 df-iun 4943 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-om 7800 df-1st 7924 df-2nd 7925 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-er 8625 df-en 8873 df-dom 8874 df-sdom 8875 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-nn 12129 df-n0 12385 df-z 12472 df-uz 12736 df-seq 13909 df-dvn 25767

This theorem is referenced by: dvn1 25826 dvnadd 25829 dvnres 25831 cpnord 25835 dvnfre 25854 c1lip2 25901 dvnply2 26193 dvntaylp 26277 taylthlem1 26279 taylthlem2 26280 taylthlem2OLD 26281 dvnmptdivc 45919 dvnmptconst 45922 dvnxpaek 45923 dvnmul 45924 etransclem2 46217

W3C validator