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 25099

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 1137	. . . . 5 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → 𝑁 ∈ ℕ₀)
2		nn0uz 12630	. . . . 5 ⊢ ℕ₀ = (ℤ_≥‘0)
3	1, 2	eleqtrdi 2849	. . . 4 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → 𝑁 ∈ (ℤ_≥‘0))
4		seqp1 13746	. . . 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 6779	. . . 4 ⊢ (seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘𝑁) ∈ V
7		fvex 6779	. . . 4 ⊢ ((ℕ₀ × {𝐹})‘(𝑁 + 1)) ∈ V
8	6, 7	opco1i 7953	. . 3 ⊢ ((seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘𝑁)((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st )((ℕ₀ × {𝐹})‘(𝑁 + 1))) = ((𝑥 ∈ V ↦ (𝑆 D 𝑥))‘(seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘𝑁))
9	5, 8	eqtrdi 2794	. 2 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → (seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘(𝑁 + 1)) = ((𝑥 ∈ V ↦ (𝑆 D 𝑥))‘(seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘𝑁)))
10		eqid 2738	. . . . 5 ⊢ (𝑥 ∈ V ↦ (𝑆 D 𝑥)) = (𝑥 ∈ V ↦ (𝑆 D 𝑥))
11	10	dvnfval 25096	. . . 4 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆)) → (𝑆 D^𝑛 𝐹) = seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹})))
12	11	3adant3 1131	. . 3 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → (𝑆 D^𝑛 𝐹) = seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹})))
13	12	fveq1d 6768	. 2 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → ((𝑆 D^𝑛 𝐹)‘(𝑁 + 1)) = (seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘(𝑁 + 1)))
14		fvex 6779	. . . 4 ⊢ ((𝑆 D^𝑛 𝐹)‘𝑁) ∈ V
15		oveq2 7275	. . . . 5 ⊢ (𝑥 = ((𝑆 D^𝑛 𝐹)‘𝑁) → (𝑆 D 𝑥) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘𝑁)))
16		ovex 7300	. . . . 5 ⊢ (𝑆 D ((𝑆 D^𝑛 𝐹)‘𝑁)) ∈ V
17	15, 10, 16	fvmpt 6867	. . . 4 ⊢ (((𝑆 D^𝑛 𝐹)‘𝑁) ∈ V → ((𝑥 ∈ V ↦ (𝑆 D 𝑥))‘((𝑆 D^𝑛 𝐹)‘𝑁)) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘𝑁)))
18	14, 17	ax-mp 5	. . 3 ⊢ ((𝑥 ∈ V ↦ (𝑆 D 𝑥))‘((𝑆 D^𝑛 𝐹)‘𝑁)) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘𝑁))
19	12	fveq1d 6768	. . . 4 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → ((𝑆 D^𝑛 𝐹)‘𝑁) = (seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘𝑁))
20	19	fveq2d 6770	. . 3 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → ((𝑥 ∈ V ↦ (𝑆 D 𝑥))‘((𝑆 D^𝑛 𝐹)‘𝑁)) = ((𝑥 ∈ V ↦ (𝑆 D 𝑥))‘(seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘𝑁)))
21	18, 20	eqtr3id 2792	. 2 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → (𝑆 D ((𝑆 D^𝑛 𝐹)‘𝑁)) = ((𝑥 ∈ V ↦ (𝑆 D 𝑥))‘(seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘𝑁)))
22	9, 13, 21	3eqtr4d 2788	1 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → ((𝑆 D^𝑛 𝐹)‘(𝑁 + 1)) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘𝑁)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 Vcvv 3429 ⊆ wss 3886 {csn 4561 ↦ cmpt 5156 × cxp 5582 ∘ ccom 5588 ‘cfv 6426 (class class class)co 7267 1^st c1st 7818 ↑_pm cpm 8603 ℂcc 10879 0cc0 10881 1c1 10882 + caddc 10884 ℕ₀cn0 12243 ℤ_≥cuz 12592 seqcseq 13731 D cdv 25037 D^𝑛 cdvn 25038

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5208 ax-sep 5221 ax-nul 5228 ax-pow 5286 ax-pr 5350 ax-un 7578 ax-inf2 9386 ax-cnex 10937 ax-resscn 10938 ax-1cn 10939 ax-icn 10940 ax-addcl 10941 ax-addrcl 10942 ax-mulcl 10943 ax-mulrcl 10944 ax-mulcom 10945 ax-addass 10946 ax-mulass 10947 ax-distr 10948 ax-i2m1 10949 ax-1ne0 10950 ax-1rid 10951 ax-rnegex 10952 ax-rrecex 10953 ax-cnre 10954 ax-pre-lttri 10955 ax-pre-lttrn 10956 ax-pre-ltadd 10957 ax-pre-mulgt0 10958

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-reu 3071 df-rab 3073 df-v 3431 df-sbc 3716 df-csb 3832 df-dif 3889 df-un 3891 df-in 3893 df-ss 3903 df-pss 3905 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-iun 4926 df-br 5074 df-opab 5136 df-mpt 5157 df-tr 5191 df-id 5484 df-eprel 5490 df-po 5498 df-so 5499 df-fr 5539 df-we 5541 df-xp 5590 df-rel 5591 df-cnv 5592 df-co 5593 df-dm 5594 df-rn 5595 df-res 5596 df-ima 5597 df-pred 6195 df-ord 6262 df-on 6263 df-lim 6264 df-suc 6265 df-iota 6384 df-fun 6428 df-fn 6429 df-f 6430 df-f1 6431 df-fo 6432 df-f1o 6433 df-fv 6434 df-riota 7224 df-ov 7270 df-oprab 7271 df-mpo 7272 df-om 7703 df-1st 7820 df-2nd 7821 df-frecs 8084 df-wrecs 8115 df-recs 8189 df-rdg 8228 df-er 8485 df-en 8721 df-dom 8722 df-sdom 8723 df-pnf 11021 df-mnf 11022 df-xr 11023 df-ltxr 11024 df-le 11025 df-sub 11217 df-neg 11218 df-nn 11984 df-n0 12244 df-z 12330 df-uz 12593 df-seq 13732 df-dvn 25042

This theorem is referenced by: dvn1 25100 dvnadd 25103 dvnres 25105 cpnord 25109 dvnfre 25126 c1lip2 25172 dvnply2 25457 dvntaylp 25540 taylthlem1 25542 taylthlem2 25543 dvnmptdivc 43460 dvnmptconst 43463 dvnxpaek 43464 dvnmul 43465 etransclem2 43758

W3C validator