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 25892

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 1139	. . . . 5 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → 𝑁 ∈ ℕ₀)
2		nn0uz 12826	. . . . 5 ⊢ ℕ₀ = (ℤ_≥‘0)
3	1, 2	eleqtrdi 2846	. . . 4 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → 𝑁 ∈ (ℤ_≥‘0))
4		seqp1 13978	. . . 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 6853	. . . 4 ⊢ (seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘𝑁) ∈ V
7		fvex 6853	. . . 4 ⊢ ((ℕ₀ × {𝐹})‘(𝑁 + 1)) ∈ V
8	6, 7	opco1i 8075	. . 3 ⊢ ((seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘𝑁)((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st )((ℕ₀ × {𝐹})‘(𝑁 + 1))) = ((𝑥 ∈ V ↦ (𝑆 D 𝑥))‘(seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘𝑁))
9	5, 8	eqtrdi 2787	. 2 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → (seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘(𝑁 + 1)) = ((𝑥 ∈ V ↦ (𝑆 D 𝑥))‘(seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘𝑁)))
10		eqid 2736	. . . . 5 ⊢ (𝑥 ∈ V ↦ (𝑆 D 𝑥)) = (𝑥 ∈ V ↦ (𝑆 D 𝑥))
11	10	dvnfval 25889	. . . 4 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆)) → (𝑆 D^𝑛 𝐹) = seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹})))
12	11	3adant3 1133	. . 3 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → (𝑆 D^𝑛 𝐹) = seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹})))
13	12	fveq1d 6842	. 2 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → ((𝑆 D^𝑛 𝐹)‘(𝑁 + 1)) = (seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘(𝑁 + 1)))
14		fvex 6853	. . . 4 ⊢ ((𝑆 D^𝑛 𝐹)‘𝑁) ∈ V
15		oveq2 7375	. . . . 5 ⊢ (𝑥 = ((𝑆 D^𝑛 𝐹)‘𝑁) → (𝑆 D 𝑥) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘𝑁)))
16		ovex 7400	. . . . 5 ⊢ (𝑆 D ((𝑆 D^𝑛 𝐹)‘𝑁)) ∈ V
17	15, 10, 16	fvmpt 6947	. . . 4 ⊢ (((𝑆 D^𝑛 𝐹)‘𝑁) ∈ V → ((𝑥 ∈ V ↦ (𝑆 D 𝑥))‘((𝑆 D^𝑛 𝐹)‘𝑁)) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘𝑁)))
18	14, 17	ax-mp 5	. . 3 ⊢ ((𝑥 ∈ V ↦ (𝑆 D 𝑥))‘((𝑆 D^𝑛 𝐹)‘𝑁)) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘𝑁))
19	12	fveq1d 6842	. . . 4 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → ((𝑆 D^𝑛 𝐹)‘𝑁) = (seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘𝑁))
20	19	fveq2d 6844	. . 3 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → ((𝑥 ∈ V ↦ (𝑆 D 𝑥))‘((𝑆 D^𝑛 𝐹)‘𝑁)) = ((𝑥 ∈ V ↦ (𝑆 D 𝑥))‘(seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘𝑁)))
21	18, 20	eqtr3id 2785	. 2 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → (𝑆 D ((𝑆 D^𝑛 𝐹)‘𝑁)) = ((𝑥 ∈ V ↦ (𝑆 D 𝑥))‘(seq0(((𝑥 ∈ V ↦ (𝑆 D 𝑥)) ∘ 1^st ), (ℕ₀ × {𝐹}))‘𝑁)))
22	9, 13, 21	3eqtr4d 2781	1 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm 𝑆) ∧ 𝑁 ∈ ℕ₀) → ((𝑆 D^𝑛 𝐹)‘(𝑁 + 1)) = (𝑆 D ((𝑆 D^𝑛 𝐹)‘𝑁)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 Vcvv 3429 ⊆ wss 3889 {csn 4567 ↦ cmpt 5166 × cxp 5629 ∘ ccom 5635 ‘cfv 6498 (class class class)co 7367 1^st c1st 7940 ↑_pm cpm 8774 ℂcc 11036 0cc0 11038 1c1 11039 + caddc 11041 ℕ₀cn0 12437 ℤ_≥cuz 12788 seqcseq 13963 D cdv 25830 D^𝑛 cdvn 25831

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-inf2 9562 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3062 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4851 df-iun 4935 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-om 7818 df-1st 7942 df-2nd 7943 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-er 8643 df-en 8894 df-dom 8895 df-sdom 8896 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-nn 12175 df-n0 12438 df-z 12525 df-uz 12789 df-seq 13964 df-dvn 25835

This theorem is referenced by: dvn1 25893 dvnadd 25896 dvnres 25898 cpnord 25902 dvnfre 25919 c1lip2 25965 dvnply2 26253 dvntaylp 26336 taylthlem1 26338 taylthlem2 26339 dvnmptdivc 46366 dvnmptconst 46369 dvnxpaek 46370 dvnmul 46371 etransclem2 46664

W3C validator