dvef - Metamath Proof Explorer

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

Theorem dvef 24295

Description: Derivative of the exponential function. (Contributed by Mario Carneiro, 9-Aug-2014.) (Proof shortened by Mario Carneiro, 10-Feb-2015.)

**Assertion**
Ref	Expression
dvef	⊢ (ℂ D exp) = exp

Proof of Theorem dvef Dummy variables 𝑥 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dvfcn 24224	. . . . . . 7 ⊢ (ℂ D exp):dom (ℂ D exp)⟶ℂ
2		dvbsss 24218	. . . . . . . . 9 ⊢ dom (ℂ D exp) ⊆ ℂ
3		subcl 10691	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑧 − 𝑥) ∈ ℂ)
4	3	ancoms 451	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑧 − 𝑥) ∈ ℂ)
5		efadd 15313	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ (𝑧 − 𝑥) ∈ ℂ) → (exp‘(𝑥 + (𝑧 − 𝑥))) = ((exp‘𝑥) · (exp‘(𝑧 − 𝑥))))
6	4, 5	syldan 583	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (exp‘(𝑥 + (𝑧 − 𝑥))) = ((exp‘𝑥) · (exp‘(𝑧 − 𝑥))))
7		pncan3 10700	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑥 + (𝑧 − 𝑥)) = 𝑧)
8	7	fveq2d 6508	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (exp‘(𝑥 + (𝑧 − 𝑥))) = (exp‘𝑧))
9	6, 8	eqtr3d 2818	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((exp‘𝑥) · (exp‘(𝑧 − 𝑥))) = (exp‘𝑧))
10	9	mpteq2dva 5027	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → (𝑧 ∈ ℂ ↦ ((exp‘𝑥) · (exp‘(𝑧 − 𝑥)))) = (𝑧 ∈ ℂ ↦ (exp‘𝑧)))
11		cnex 10422	. . . . . . . . . . . . . . . 16 ⊢ ℂ ∈ V
12	11	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ → ℂ ∈ V)
13		fvexd 6519	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (exp‘𝑥) ∈ V)
14		fvexd 6519	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (exp‘(𝑧 − 𝑥)) ∈ V)
15		fconstmpt 5468	. . . . . . . . . . . . . . . 16 ⊢ (ℂ × {(exp‘𝑥)}) = (𝑧 ∈ ℂ ↦ (exp‘𝑥))
16	15	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ → (ℂ × {(exp‘𝑥)}) = (𝑧 ∈ ℂ ↦ (exp‘𝑥)))
17		eqidd 2781	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ → (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥))) = (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥))))
18	12, 13, 14, 16, 17	offval2 7250	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → ((ℂ × {(exp‘𝑥)}) ∘_𝑓 · (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))) = (𝑧 ∈ ℂ ↦ ((exp‘𝑥) · (exp‘(𝑧 − 𝑥)))))
19		eff 15301	. . . . . . . . . . . . . . . 16 ⊢ exp:ℂ⟶ℂ
20	19	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ → exp:ℂ⟶ℂ)
21	20	feqmptd 6568	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → exp = (𝑧 ∈ ℂ ↦ (exp‘𝑧)))
22	10, 18, 21	3eqtr4d 2826	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → ((ℂ × {(exp‘𝑥)}) ∘_𝑓 · (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))) = exp)
23	22	oveq2d 6998	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → (ℂ D ((ℂ × {(exp‘𝑥)}) ∘_𝑓 · (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥))))) = (ℂ D exp))
24		efcl 15302	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℂ → (exp‘𝑥) ∈ ℂ)
25		fconstg 6400	. . . . . . . . . . . . . . . 16 ⊢ ((exp‘𝑥) ∈ ℂ → (ℂ × {(exp‘𝑥)}):ℂ⟶{(exp‘𝑥)})
26	24, 25	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ → (ℂ × {(exp‘𝑥)}):ℂ⟶{(exp‘𝑥)})
27	24	snssd 4621	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ → {(exp‘𝑥)} ⊆ ℂ)
28	26, 27	fssd 6363	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → (ℂ × {(exp‘𝑥)}):ℂ⟶ℂ)
29		ssidd 3882	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → ℂ ⊆ ℂ)
30		efcl 15302	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 − 𝑥) ∈ ℂ → (exp‘(𝑧 − 𝑥)) ∈ ℂ)
31	4, 30	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (exp‘(𝑧 − 𝑥)) ∈ ℂ)
32	31	fmpttd 6708	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥))):ℂ⟶ℂ)
33		0cnd 10438	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → 0 ∈ ℂ)
34		1cnd 10440	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → 1 ∈ ℂ)
35		c0ex 10439	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ V
36	35	snid 4478	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ {0}
37		opelxpi 5448	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ 0 ∈ {0}) → ⟨𝑥, 0⟩ ∈ (ℂ × {0}))
38	36, 37	mpan2 679	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℂ → ⟨𝑥, 0⟩ ∈ (ℂ × {0}))
39		dvconst 24232	. . . . . . . . . . . . . . . . 17 ⊢ ((exp‘𝑥) ∈ ℂ → (ℂ D (ℂ × {(exp‘𝑥)})) = (ℂ × {0}))
40	24, 39	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℂ → (ℂ D (ℂ × {(exp‘𝑥)})) = (ℂ × {0}))
41	38, 40	eleqtrrd 2871	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ → ⟨𝑥, 0⟩ ∈ (ℂ D (ℂ × {(exp‘𝑥)})))
42		df-br 4935	. . . . . . . . . . . . . . 15 ⊢ (𝑥(ℂ D (ℂ × {(exp‘𝑥)}))0 ↔ ⟨𝑥, 0⟩ ∈ (ℂ D (ℂ × {(exp‘𝑥)})))
43	41, 42	sylibr 226	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D (ℂ × {(exp‘𝑥)}))0)
44	20, 4	cofmpt 6723	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℂ → (exp ∘ (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))) = (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥))))
45	44	oveq2d 6998	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ → (ℂ D (exp ∘ (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)))) = (ℂ D (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))))
46	4	fmpttd 6708	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℂ → (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)):ℂ⟶ℂ)
47		oveq1 6989	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑥 → (𝑧 − 𝑥) = (𝑥 − 𝑥))
48		eqid 2780	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)) = (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))
49		ovex 7014	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 − 𝑥) ∈ V
50	47, 48, 49	fvmpt 6601	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℂ → ((𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))‘𝑥) = (𝑥 − 𝑥))
51		subid 10712	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℂ → (𝑥 − 𝑥) = 0)
52	50, 51	eqtrd 2816	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℂ → ((𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))‘𝑥) = 0)
53		dveflem 24294	. . . . . . . . . . . . . . . . . 18 ⊢ 0(ℂ D exp)1
54	52, 53	syl6eqbr 4973	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℂ → ((𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))‘𝑥)(ℂ D exp)1)
55		1ex 10441	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ V
56	55	snid 4478	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ∈ {1}
57		opelxpi 5448	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℂ ∧ 1 ∈ {1}) → ⟨𝑥, 1⟩ ∈ (ℂ × {1}))
58	56, 57	mpan2 679	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℂ → ⟨𝑥, 1⟩ ∈ (ℂ × {1}))
59		cnelprrecn 10434	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℂ ∈ {ℝ, ℂ}
60	59	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℂ → ℂ ∈ {ℝ, ℂ})
61		simpr 477	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → 𝑧 ∈ ℂ)
62		1cnd 10440	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → 1 ∈ ℂ)
63	60	dvmptid 24272	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℂ → (ℂ D (𝑧 ∈ ℂ ↦ 𝑧)) = (𝑧 ∈ ℂ ↦ 1))
64		simpl 475	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → 𝑥 ∈ ℂ)
65		0cnd 10438	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → 0 ∈ ℂ)
66		id 22	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℂ → 𝑥 ∈ ℂ)
67	60, 66	dvmptc 24273	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℂ → (ℂ D (𝑧 ∈ ℂ ↦ 𝑥)) = (𝑧 ∈ ℂ ↦ 0))
68	60, 61, 62, 63, 64, 65, 67	dvmptsub 24282	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℂ → (ℂ D (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))) = (𝑧 ∈ ℂ ↦ (1 − 0)))
69		1m0e1 11574	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 − 0) = 1
70	69	mpteq2i 5024	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ ℂ ↦ (1 − 0)) = (𝑧 ∈ ℂ ↦ 1)
71		fconstmpt 5468	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℂ × {1}) = (𝑧 ∈ ℂ ↦ 1)
72	70, 71	eqtr4i 2807	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ℂ ↦ (1 − 0)) = (ℂ × {1})
73	68, 72	syl6eq 2832	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℂ → (ℂ D (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))) = (ℂ × {1}))
74	58, 73	eleqtrrd 2871	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℂ → ⟨𝑥, 1⟩ ∈ (ℂ D (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))))
75		df-br 4935	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥(ℂ D (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)))1 ↔ ⟨𝑥, 1⟩ ∈ (ℂ D (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))))
76	74, 75	sylibr 226	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)))1)
77		eqid 2780	. . . . . . . . . . . . . . . . 17 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
78	20, 29, 46, 29, 29, 29, 34, 34, 54, 76, 77	dvcobr 24261	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D (exp ∘ (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))))(1 · 1))
79		1t1e1 11615	. . . . . . . . . . . . . . . 16 ⊢ (1 · 1) = 1
80	78, 79	syl6breq 4975	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D (exp ∘ (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))))1)
81	45, 80	breqdi 4949	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥))))1)
82	28, 29, 32, 29, 29, 33, 34, 43, 81, 77	dvmulbr 24254	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D ((ℂ × {(exp‘𝑥)}) ∘_𝑓 · (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))))((0 · ((𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))‘𝑥)) + (1 · ((ℂ × {(exp‘𝑥)})‘𝑥))))
83	32, 66	ffvelrnd 6683	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℂ → ((𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))‘𝑥) ∈ ℂ)
84	83	mul02d 10644	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ → (0 · ((𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))‘𝑥)) = 0)
85		fvex 6517	. . . . . . . . . . . . . . . . . 18 ⊢ (exp‘𝑥) ∈ V
86	85	fvconst2 6799	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℂ → ((ℂ × {(exp‘𝑥)})‘𝑥) = (exp‘𝑥))
87	86	oveq2d 6998	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℂ → (1 · ((ℂ × {(exp‘𝑥)})‘𝑥)) = (1 · (exp‘𝑥)))
88	24	mulid2d 10464	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℂ → (1 · (exp‘𝑥)) = (exp‘𝑥))
89	87, 88	eqtrd 2816	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ → (1 · ((ℂ × {(exp‘𝑥)})‘𝑥)) = (exp‘𝑥))
90	84, 89	oveq12d 7000	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → ((0 · ((𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))‘𝑥)) + (1 · ((ℂ × {(exp‘𝑥)})‘𝑥))) = (0 + (exp‘𝑥)))
91	24	addid2d 10647	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → (0 + (exp‘𝑥)) = (exp‘𝑥))
92	90, 91	eqtrd 2816	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → ((0 · ((𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))‘𝑥)) + (1 · ((ℂ × {(exp‘𝑥)})‘𝑥))) = (exp‘𝑥))
93	82, 92	breqtrd 4960	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D ((ℂ × {(exp‘𝑥)}) ∘_𝑓 · (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))))(exp‘𝑥))
94	23, 93	breqdi 4949	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D exp)(exp‘𝑥))
95		vex 3420	. . . . . . . . . . . 12 ⊢ 𝑥 ∈ V
96	95, 85	breldm 5631	. . . . . . . . . . 11 ⊢ (𝑥(ℂ D exp)(exp‘𝑥) → 𝑥 ∈ dom (ℂ D exp))
97	94, 96	syl 17	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℂ → 𝑥 ∈ dom (ℂ D exp))
98	97	ssriv 3864	. . . . . . . . 9 ⊢ ℂ ⊆ dom (ℂ D exp)
99	2, 98	eqssi 3876	. . . . . . . 8 ⊢ dom (ℂ D exp) = ℂ
100	99	feq2i 6341	. . . . . . 7 ⊢ ((ℂ D exp):dom (ℂ D exp)⟶ℂ ↔ (ℂ D exp):ℂ⟶ℂ)
101	1, 100	mpbi 222	. . . . . 6 ⊢ (ℂ D exp):ℂ⟶ℂ
102	101	a1i 11	. . . . 5 ⊢ (⊤ → (ℂ D exp):ℂ⟶ℂ)
103	102	feqmptd 6568	. . . 4 ⊢ (⊤ → (ℂ D exp) = (𝑥 ∈ ℂ ↦ ((ℂ D exp)‘𝑥)))
104		ffun 6352	. . . . . . 7 ⊢ ((ℂ D exp):dom (ℂ D exp)⟶ℂ → Fun (ℂ D exp))
105	1, 104	ax-mp 5	. . . . . 6 ⊢ Fun (ℂ D exp)
106		funbrfv 6551	. . . . . 6 ⊢ (Fun (ℂ D exp) → (𝑥(ℂ D exp)(exp‘𝑥) → ((ℂ D exp)‘𝑥) = (exp‘𝑥)))
107	105, 94, 106	mpsyl 68	. . . . 5 ⊢ (𝑥 ∈ ℂ → ((ℂ D exp)‘𝑥) = (exp‘𝑥))
108	107	mpteq2ia 5023	. . . 4 ⊢ (𝑥 ∈ ℂ ↦ ((ℂ D exp)‘𝑥)) = (𝑥 ∈ ℂ ↦ (exp‘𝑥))
109	103, 108	syl6eq 2832	. . 3 ⊢ (⊤ → (ℂ D exp) = (𝑥 ∈ ℂ ↦ (exp‘𝑥)))
110	19	a1i 11	. . . 4 ⊢ (⊤ → exp:ℂ⟶ℂ)
111	110	feqmptd 6568	. . 3 ⊢ (⊤ → exp = (𝑥 ∈ ℂ ↦ (exp‘𝑥)))
112	109, 111	eqtr4d 2819	. 2 ⊢ (⊤ → (ℂ D exp) = exp)
113	112	mptru 1515	1 ⊢ (ℂ D exp) = exp

Colors of variables: wff setvar class

Syntax hints: ∧ wa 387 = wceq 1508 ⊤wtru 1509 ∈ wcel 2051 Vcvv 3417 {csn 4444 {cpr 4446 ⟨cop 4450 class class class wbr 4934 ↦ cmpt 5013 × cxp 5409 dom cdm 5411 ∘ ccom 5415 Fun wfun 6187 ⟶wf 6189 ‘cfv 6193 (class class class)co 6982 ∘_𝑓 cof 7231 ℂcc 10339 ℝcr 10340 0cc0 10341 1c1 10342 + caddc 10344 · cmul 10346 − cmin 10676 expce 15281 TopOpenctopn 16557 ℂ_fldccnfld 20262 D cdv 24179

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2752 ax-rep 5053 ax-sep 5064 ax-nul 5071 ax-pow 5123 ax-pr 5190 ax-un 7285 ax-inf2 8904 ax-cnex 10397 ax-resscn 10398 ax-1cn 10399 ax-icn 10400 ax-addcl 10401 ax-addrcl 10402 ax-mulcl 10403 ax-mulrcl 10404 ax-mulcom 10405 ax-addass 10406 ax-mulass 10407 ax-distr 10408 ax-i2m1 10409 ax-1ne0 10410 ax-1rid 10411 ax-rnegex 10412 ax-rrecex 10413 ax-cnre 10414 ax-pre-lttri 10415 ax-pre-lttrn 10416 ax-pre-ltadd 10417 ax-pre-mulgt0 10418 ax-pre-sup 10419 ax-addf 10420 ax-mulf 10421

This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3or 1070 df-3an 1071 df-tru 1511 df-fal 1521 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2551 df-eu 2589 df-clab 2761 df-cleq 2773 df-clel 2848 df-nfc 2920 df-ne 2970 df-nel 3076 df-ral 3095 df-rex 3096 df-reu 3097 df-rmo 3098 df-rab 3099 df-v 3419 df-sbc 3684 df-csb 3789 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-pss 3847 df-nul 4182 df-if 4354 df-pw 4427 df-sn 4445 df-pr 4447 df-tp 4449 df-op 4451 df-uni 4718 df-int 4755 df-iun 4799 df-iin 4800 df-br 4935 df-opab 4997 df-mpt 5014 df-tr 5036 df-id 5316 df-eprel 5321 df-po 5330 df-so 5331 df-fr 5370 df-se 5371 df-we 5372 df-xp 5417 df-rel 5418 df-cnv 5419 df-co 5420 df-dm 5421 df-rn 5422 df-res 5423 df-ima 5424 df-pred 5991 df-ord 6037 df-on 6038 df-lim 6039 df-suc 6040 df-iota 6157 df-fun 6195 df-fn 6196 df-f 6197 df-f1 6198 df-fo 6199 df-f1o 6200 df-fv 6201 df-isom 6202 df-riota 6943 df-ov 6985 df-oprab 6986 df-mpo 6987 df-of 7233 df-om 7403 df-1st 7507 df-2nd 7508 df-supp 7640 df-wrecs 7756 df-recs 7818 df-rdg 7856 df-1o 7911 df-2o 7912 df-oadd 7915 df-er 8095 df-map 8214 df-pm 8215 df-ixp 8266 df-en 8313 df-dom 8314 df-sdom 8315 df-fin 8316 df-fsupp 8635 df-fi 8676 df-sup 8707 df-inf 8708 df-oi 8775 df-card 9168 df-cda 9394 df-pnf 10482 df-mnf 10483 df-xr 10484 df-ltxr 10485 df-le 10486 df-sub 10678 df-neg 10679 df-div 11105 df-nn 11446 df-2 11509 df-3 11510 df-4 11511 df-5 11512 df-6 11513 df-7 11514 df-8 11515 df-9 11516 df-n0 11714 df-z 11800 df-dec 11918 df-uz 12065 df-q 12169 df-rp 12211 df-xneg 12330 df-xadd 12331 df-xmul 12332 df-ico 12566 df-icc 12567 df-fz 12715 df-fzo 12856 df-fl 12983 df-seq 13191 df-exp 13251 df-fac 13455 df-bc 13484 df-hash 13512 df-shft 14293 df-cj 14325 df-re 14326 df-im 14327 df-sqrt 14461 df-abs 14462 df-limsup 14695 df-clim 14712 df-rlim 14713 df-sum 14910 df-ef 15287 df-struct 16347 df-ndx 16348 df-slot 16349 df-base 16351 df-sets 16352 df-ress 16353 df-plusg 16440 df-mulr 16441 df-starv 16442 df-sca 16443 df-vsca 16444 df-ip 16445 df-tset 16446 df-ple 16447 df-ds 16449 df-unif 16450 df-hom 16451 df-cco 16452 df-rest 16558 df-topn 16559 df-0g 16577 df-gsum 16578 df-topgen 16579 df-pt 16580 df-prds 16583 df-xrs 16637 df-qtop 16642 df-imas 16643 df-xps 16645 df-mre 16727 df-mrc 16728 df-acs 16730 df-mgm 17722 df-sgrp 17764 df-mnd 17775 df-submnd 17816 df-mulg 18024 df-cntz 18230 df-cmn 18680 df-psmet 20254 df-xmet 20255 df-met 20256 df-bl 20257 df-mopn 20258 df-fbas 20259 df-fg 20260 df-cnfld 20263 df-top 21221 df-topon 21238 df-topsp 21260 df-bases 21273 df-cld 21346 df-ntr 21347 df-cls 21348 df-nei 21425 df-lp 21463 df-perf 21464 df-cn 21554 df-cnp 21555 df-haus 21642 df-tx 21889 df-hmeo 22082 df-fil 22173 df-fm 22265 df-flim 22266 df-flf 22267 df-xms 22648 df-ms 22649 df-tms 22650 df-cncf 23204 df-limc 24182 df-dv 24183

This theorem is referenced by: dvsincos 24296 efcn 24749 efcvx 24755 pige3ALT 24823 dvrelog 24936 dvlog 24950 dvcxp1 25037 dvcxp2 25038 dvcncxp1 25040 itgexpif 31557 dvsef 40121 expgrowthi 40122 expgrowth 40124

W3C validator