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

Theorem dvef 23461
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.
StepHypRef Expression
1 dvfcn 23392 . . . . . . 7 (ℂ D exp):dom (ℂ D exp)⟶ℂ
2 dvbsss 23386 . . . . . . . . 9 dom (ℂ D exp) ⊆ ℂ
3 efcl 14595 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℂ → (exp‘𝑥) ∈ ℂ)
4 fconstg 5987 . . . . . . . . . . . . . . . 16 ((exp‘𝑥) ∈ ℂ → (ℂ × {(exp‘𝑥)}):ℂ⟶{(exp‘𝑥)})
53, 4syl 17 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℂ → (ℂ × {(exp‘𝑥)}):ℂ⟶{(exp‘𝑥)})
63snssd 4277 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℂ → {(exp‘𝑥)} ⊆ ℂ)
75, 6fssd 5953 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → (ℂ × {(exp‘𝑥)}):ℂ⟶ℂ)
8 ssid 3583 . . . . . . . . . . . . . . 15 ℂ ⊆ ℂ
98a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → ℂ ⊆ ℂ)
10 subcl 10128 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑧𝑥) ∈ ℂ)
1110ancoms 467 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑧𝑥) ∈ ℂ)
12 efcl 14595 . . . . . . . . . . . . . . . 16 ((𝑧𝑥) ∈ ℂ → (exp‘(𝑧𝑥)) ∈ ℂ)
1311, 12syl 17 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (exp‘(𝑧𝑥)) ∈ ℂ)
14 eqid 2606 . . . . . . . . . . . . . . 15 (𝑧 ∈ ℂ ↦ (exp‘(𝑧𝑥))) = (𝑧 ∈ ℂ ↦ (exp‘(𝑧𝑥)))
1513, 14fmptd 6274 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → (𝑧 ∈ ℂ ↦ (exp‘(𝑧𝑥))):ℂ⟶ℂ)
16 0cn 9885 . . . . . . . . . . . . . . 15 0 ∈ ℂ
1716a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → 0 ∈ ℂ)
18 ax-1cn 9847 . . . . . . . . . . . . . . 15 1 ∈ ℂ
1918a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → 1 ∈ ℂ)
2016elexi 3182 . . . . . . . . . . . . . . . . . 18 0 ∈ V
2120snid 4151 . . . . . . . . . . . . . . . . 17 0 ∈ {0}
22 opelxpi 5059 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℂ ∧ 0 ∈ {0}) → ⟨𝑥, 0⟩ ∈ (ℂ × {0}))
2321, 22mpan2 702 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℂ → ⟨𝑥, 0⟩ ∈ (ℂ × {0}))
24 dvconst 23400 . . . . . . . . . . . . . . . . 17 ((exp‘𝑥) ∈ ℂ → (ℂ D (ℂ × {(exp‘𝑥)})) = (ℂ × {0}))
253, 24syl 17 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℂ → (ℂ D (ℂ × {(exp‘𝑥)})) = (ℂ × {0}))
2623, 25eleqtrrd 2687 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℂ → ⟨𝑥, 0⟩ ∈ (ℂ D (ℂ × {(exp‘𝑥)})))
27 df-br 4575 . . . . . . . . . . . . . . 15 (𝑥(ℂ D (ℂ × {(exp‘𝑥)}))0 ↔ ⟨𝑥, 0⟩ ∈ (ℂ D (ℂ × {(exp‘𝑥)})))
2826, 27sylibr 222 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → 𝑥(ℂ D (ℂ × {(exp‘𝑥)}))0)
29 eff 14594 . . . . . . . . . . . . . . . . . 18 exp:ℂ⟶ℂ
3029a1i 11 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → exp:ℂ⟶ℂ)
31 eqid 2606 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ℂ ↦ (𝑧𝑥)) = (𝑧 ∈ ℂ ↦ (𝑧𝑥))
3211, 31fmptd 6274 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → (𝑧 ∈ ℂ ↦ (𝑧𝑥)):ℂ⟶ℂ)
33 oveq1 6531 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑥 → (𝑧𝑥) = (𝑥𝑥))
34 ovex 6552 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝑥) ∈ V
3533, 31, 34fvmpt 6173 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℂ → ((𝑧 ∈ ℂ ↦ (𝑧𝑥))‘𝑥) = (𝑥𝑥))
36 subid 10148 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℂ → (𝑥𝑥) = 0)
3735, 36eqtrd 2640 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → ((𝑧 ∈ ℂ ↦ (𝑧𝑥))‘𝑥) = 0)
38 dveflem 23460 . . . . . . . . . . . . . . . . . 18 0(ℂ D exp)1
3937, 38syl6eqbr 4613 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → ((𝑧 ∈ ℂ ↦ (𝑧𝑥))‘𝑥)(ℂ D exp)1)
4018elexi 3182 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ V
4140snid 4151 . . . . . . . . . . . . . . . . . . . 20 1 ∈ {1}
42 opelxpi 5059 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ℂ ∧ 1 ∈ {1}) → ⟨𝑥, 1⟩ ∈ (ℂ × {1}))
4341, 42mpan2 702 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℂ → ⟨𝑥, 1⟩ ∈ (ℂ × {1}))
44 cnelprrecn 9882 . . . . . . . . . . . . . . . . . . . . . 22 ℂ ∈ {ℝ, ℂ}
4544a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℂ → ℂ ∈ {ℝ, ℂ})
46 simpr 475 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → 𝑧 ∈ ℂ)
4718a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → 1 ∈ ℂ)
4845dvmptid 23440 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℂ → (ℂ D (𝑧 ∈ ℂ ↦ 𝑧)) = (𝑧 ∈ ℂ ↦ 1))
49 simpl 471 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → 𝑥 ∈ ℂ)
5016a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → 0 ∈ ℂ)
51 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℂ → 𝑥 ∈ ℂ)
5245, 51dvmptc 23441 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℂ → (ℂ D (𝑧 ∈ ℂ ↦ 𝑥)) = (𝑧 ∈ ℂ ↦ 0))
5345, 46, 47, 48, 49, 50, 52dvmptsub 23450 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℂ → (ℂ D (𝑧 ∈ ℂ ↦ (𝑧𝑥))) = (𝑧 ∈ ℂ ↦ (1 − 0)))
54 1m0e1 10975 . . . . . . . . . . . . . . . . . . . . . 22 (1 − 0) = 1
5554mpteq2i 4660 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ ℂ ↦ (1 − 0)) = (𝑧 ∈ ℂ ↦ 1)
56 fconstmpt 5072 . . . . . . . . . . . . . . . . . . . . 21 (ℂ × {1}) = (𝑧 ∈ ℂ ↦ 1)
5755, 56eqtr4i 2631 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ ℂ ↦ (1 − 0)) = (ℂ × {1})
5853, 57syl6eq 2656 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℂ → (ℂ D (𝑧 ∈ ℂ ↦ (𝑧𝑥))) = (ℂ × {1}))
5943, 58eleqtrrd 2687 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → ⟨𝑥, 1⟩ ∈ (ℂ D (𝑧 ∈ ℂ ↦ (𝑧𝑥))))
60 df-br 4575 . . . . . . . . . . . . . . . . . 18 (𝑥(ℂ D (𝑧 ∈ ℂ ↦ (𝑧𝑥)))1 ↔ ⟨𝑥, 1⟩ ∈ (ℂ D (𝑧 ∈ ℂ ↦ (𝑧𝑥))))
6159, 60sylibr 222 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → 𝑥(ℂ D (𝑧 ∈ ℂ ↦ (𝑧𝑥)))1)
62 eqid 2606 . . . . . . . . . . . . . . . . 17 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
6330, 9, 32, 9, 9, 9, 19, 19, 39, 61, 62dvcobr 23429 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℂ → 𝑥(ℂ D (exp ∘ (𝑧 ∈ ℂ ↦ (𝑧𝑥))))(1 · 1))
64 1t1e1 11019 . . . . . . . . . . . . . . . 16 (1 · 1) = 1
6563, 64syl6breq 4615 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℂ → 𝑥(ℂ D (exp ∘ (𝑧 ∈ ℂ ↦ (𝑧𝑥))))1)
66 eqidd 2607 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → (𝑧 ∈ ℂ ↦ (𝑧𝑥)) = (𝑧 ∈ ℂ ↦ (𝑧𝑥)))
6730feqmptd 6141 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → exp = (𝑦 ∈ ℂ ↦ (exp‘𝑦)))
68 fveq2 6085 . . . . . . . . . . . . . . . . . 18 (𝑦 = (𝑧𝑥) → (exp‘𝑦) = (exp‘(𝑧𝑥)))
6911, 66, 67, 68fmptco 6285 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → (exp ∘ (𝑧 ∈ ℂ ↦ (𝑧𝑥))) = (𝑧 ∈ ℂ ↦ (exp‘(𝑧𝑥))))
7069oveq2d 6540 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℂ → (ℂ D (exp ∘ (𝑧 ∈ ℂ ↦ (𝑧𝑥)))) = (ℂ D (𝑧 ∈ ℂ ↦ (exp‘(𝑧𝑥)))))
7170breqd 4585 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℂ → (𝑥(ℂ D (exp ∘ (𝑧 ∈ ℂ ↦ (𝑧𝑥))))1 ↔ 𝑥(ℂ D (𝑧 ∈ ℂ ↦ (exp‘(𝑧𝑥))))1))
7265, 71mpbid 220 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → 𝑥(ℂ D (𝑧 ∈ ℂ ↦ (exp‘(𝑧𝑥))))1)
737, 9, 15, 9, 9, 17, 19, 28, 72, 62dvmulbr 23422 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ → 𝑥(ℂ D ((ℂ × {(exp‘𝑥)}) ∘𝑓 · (𝑧 ∈ ℂ ↦ (exp‘(𝑧𝑥)))))((0 · ((𝑧 ∈ ℂ ↦ (exp‘(𝑧𝑥)))‘𝑥)) + (1 · ((ℂ × {(exp‘𝑥)})‘𝑥))))
7415, 51ffvelrnd 6250 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℂ → ((𝑧 ∈ ℂ ↦ (exp‘(𝑧𝑥)))‘𝑥) ∈ ℂ)
7574mul02d 10082 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℂ → (0 · ((𝑧 ∈ ℂ ↦ (exp‘(𝑧𝑥)))‘𝑥)) = 0)
76 fvex 6095 . . . . . . . . . . . . . . . . . 18 (exp‘𝑥) ∈ V
7776fvconst2 6349 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → ((ℂ × {(exp‘𝑥)})‘𝑥) = (exp‘𝑥))
7877oveq2d 6540 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℂ → (1 · ((ℂ × {(exp‘𝑥)})‘𝑥)) = (1 · (exp‘𝑥)))
793mulid2d 9911 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℂ → (1 · (exp‘𝑥)) = (exp‘𝑥))
8078, 79eqtrd 2640 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℂ → (1 · ((ℂ × {(exp‘𝑥)})‘𝑥)) = (exp‘𝑥))
8175, 80oveq12d 6542 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → ((0 · ((𝑧 ∈ ℂ ↦ (exp‘(𝑧𝑥)))‘𝑥)) + (1 · ((ℂ × {(exp‘𝑥)})‘𝑥))) = (0 + (exp‘𝑥)))
823addid2d 10085 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → (0 + (exp‘𝑥)) = (exp‘𝑥))
8381, 82eqtrd 2640 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ → ((0 · ((𝑧 ∈ ℂ ↦ (exp‘(𝑧𝑥)))‘𝑥)) + (1 · ((ℂ × {(exp‘𝑥)})‘𝑥))) = (exp‘𝑥))
8473, 83breqtrd 4600 . . . . . . . . . . . 12 (𝑥 ∈ ℂ → 𝑥(ℂ D ((ℂ × {(exp‘𝑥)}) ∘𝑓 · (𝑧 ∈ ℂ ↦ (exp‘(𝑧𝑥)))))(exp‘𝑥))
85 cnex 9870 . . . . . . . . . . . . . . . . 17 ℂ ∈ V
8685a1i 11 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℂ → ℂ ∈ V)
8776a1i 11 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (exp‘𝑥) ∈ V)
88 fvex 6095 . . . . . . . . . . . . . . . . 17 (exp‘(𝑧𝑥)) ∈ V
8988a1i 11 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (exp‘(𝑧𝑥)) ∈ V)
90 fconstmpt 5072 . . . . . . . . . . . . . . . . 17 (ℂ × {(exp‘𝑥)}) = (𝑧 ∈ ℂ ↦ (exp‘𝑥))
9190a1i 11 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℂ → (ℂ × {(exp‘𝑥)}) = (𝑧 ∈ ℂ ↦ (exp‘𝑥)))
92 eqidd 2607 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℂ → (𝑧 ∈ ℂ ↦ (exp‘(𝑧𝑥))) = (𝑧 ∈ ℂ ↦ (exp‘(𝑧𝑥))))
9386, 87, 89, 91, 92offval2 6786 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℂ → ((ℂ × {(exp‘𝑥)}) ∘𝑓 · (𝑧 ∈ ℂ ↦ (exp‘(𝑧𝑥)))) = (𝑧 ∈ ℂ ↦ ((exp‘𝑥) · (exp‘(𝑧𝑥)))))
9430feqmptd 6141 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℂ → exp = (𝑧 ∈ ℂ ↦ (exp‘𝑧)))
95 efadd 14606 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℂ ∧ (𝑧𝑥) ∈ ℂ) → (exp‘(𝑥 + (𝑧𝑥))) = ((exp‘𝑥) · (exp‘(𝑧𝑥))))
9611, 95syldan 485 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (exp‘(𝑥 + (𝑧𝑥))) = ((exp‘𝑥) · (exp‘(𝑧𝑥))))
97 pncan3 10137 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑥 + (𝑧𝑥)) = 𝑧)
9897fveq2d 6089 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (exp‘(𝑥 + (𝑧𝑥))) = (exp‘𝑧))
9996, 98eqtr3d 2642 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((exp‘𝑥) · (exp‘(𝑧𝑥))) = (exp‘𝑧))
10099mpteq2dva 4663 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℂ → (𝑧 ∈ ℂ ↦ ((exp‘𝑥) · (exp‘(𝑧𝑥)))) = (𝑧 ∈ ℂ ↦ (exp‘𝑧)))
10194, 100eqtr4d 2643 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℂ → exp = (𝑧 ∈ ℂ ↦ ((exp‘𝑥) · (exp‘(𝑧𝑥)))))
10293, 101eqtr4d 2643 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ → ((ℂ × {(exp‘𝑥)}) ∘𝑓 · (𝑧 ∈ ℂ ↦ (exp‘(𝑧𝑥)))) = exp)
103102oveq2d 6540 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ → (ℂ D ((ℂ × {(exp‘𝑥)}) ∘𝑓 · (𝑧 ∈ ℂ ↦ (exp‘(𝑧𝑥))))) = (ℂ D exp))
104103breqd 4585 . . . . . . . . . . . 12 (𝑥 ∈ ℂ → (𝑥(ℂ D ((ℂ × {(exp‘𝑥)}) ∘𝑓 · (𝑧 ∈ ℂ ↦ (exp‘(𝑧𝑥)))))(exp‘𝑥) ↔ 𝑥(ℂ D exp)(exp‘𝑥)))
10584, 104mpbid 220 . . . . . . . . . . 11 (𝑥 ∈ ℂ → 𝑥(ℂ D exp)(exp‘𝑥))
106 vex 3172 . . . . . . . . . . . 12 𝑥 ∈ V
107106, 76breldm 5235 . . . . . . . . . . 11 (𝑥(ℂ D exp)(exp‘𝑥) → 𝑥 ∈ dom (ℂ D exp))
108105, 107syl 17 . . . . . . . . . 10 (𝑥 ∈ ℂ → 𝑥 ∈ dom (ℂ D exp))
109108ssriv 3568 . . . . . . . . 9 ℂ ⊆ dom (ℂ D exp)
1102, 109eqssi 3580 . . . . . . . 8 dom (ℂ D exp) = ℂ
111110feq2i 5933 . . . . . . 7 ((ℂ D exp):dom (ℂ D exp)⟶ℂ ↔ (ℂ D exp):ℂ⟶ℂ)
1121, 111mpbi 218 . . . . . 6 (ℂ D exp):ℂ⟶ℂ
113112a1i 11 . . . . 5 (⊤ → (ℂ D exp):ℂ⟶ℂ)
114113feqmptd 6141 . . . 4 (⊤ → (ℂ D exp) = (𝑥 ∈ ℂ ↦ ((ℂ D exp)‘𝑥)))
115 ffun 5944 . . . . . . 7 ((ℂ D exp):dom (ℂ D exp)⟶ℂ → Fun (ℂ D exp))
1161, 115ax-mp 5 . . . . . 6 Fun (ℂ D exp)
117 funbrfv 6126 . . . . . 6 (Fun (ℂ D exp) → (𝑥(ℂ D exp)(exp‘𝑥) → ((ℂ D exp)‘𝑥) = (exp‘𝑥)))
118116, 105, 117mpsyl 65 . . . . 5 (𝑥 ∈ ℂ → ((ℂ D exp)‘𝑥) = (exp‘𝑥))
119118mpteq2ia 4659 . . . 4 (𝑥 ∈ ℂ ↦ ((ℂ D exp)‘𝑥)) = (𝑥 ∈ ℂ ↦ (exp‘𝑥))
120114, 119syl6eq 2656 . . 3 (⊤ → (ℂ D exp) = (𝑥 ∈ ℂ ↦ (exp‘𝑥)))
12129a1i 11 . . . 4 (⊤ → exp:ℂ⟶ℂ)
122121feqmptd 6141 . . 3 (⊤ → exp = (𝑥 ∈ ℂ ↦ (exp‘𝑥)))
123120, 122eqtr4d 2643 . 2 (⊤ → (ℂ D exp) = exp)
124123trud 1483 1 (ℂ D exp) = exp
Colors of variables: wff setvar class
Syntax hints:  wa 382   = wceq 1474  wtru 1475  wcel 1976  Vcvv 3169  wss 3536  {csn 4121  {cpr 4123  cop 4127   class class class wbr 4574  cmpt 4634   × cxp 5023  dom cdm 5025  ccom 5029  Fun wfun 5781  wf 5783  cfv 5787  (class class class)co 6524  𝑓 cof 6767  cc 9787  cr 9788  0cc0 9789  1c1 9790   + caddc 9792   · cmul 9794  cmin 10114  expce 14574  TopOpenctopn 15848  fldccnfld 19510   D cdv 23347
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-rep 4690  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-inf2 8395  ax-cnex 9845  ax-resscn 9846  ax-1cn 9847  ax-icn 9848  ax-addcl 9849  ax-addrcl 9850  ax-mulcl 9851  ax-mulrcl 9852  ax-mulcom 9853  ax-addass 9854  ax-mulass 9855  ax-distr 9856  ax-i2m1 9857  ax-1ne0 9858  ax-1rid 9859  ax-rnegex 9860  ax-rrecex 9861  ax-cnre 9862  ax-pre-lttri 9863  ax-pre-lttrn 9864  ax-pre-ltadd 9865  ax-pre-mulgt0 9866  ax-pre-sup 9867  ax-addf 9868  ax-mulf 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-nel 2779  df-ral 2897  df-rex 2898  df-reu 2899  df-rmo 2900  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-pss 3552  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-tp 4126  df-op 4128  df-uni 4364  df-int 4402  df-iun 4448  df-iin 4449  df-br 4575  df-opab 4635  df-mpt 4636  df-tr 4672  df-eprel 4936  df-id 4940  df-po 4946  df-so 4947  df-fr 4984  df-se 4985  df-we 4986  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-pred 5580  df-ord 5626  df-on 5627  df-lim 5628  df-suc 5629  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-isom 5796  df-riota 6486  df-ov 6527  df-oprab 6528  df-mpt2 6529  df-of 6769  df-om 6932  df-1st 7033  df-2nd 7034  df-supp 7157  df-wrecs 7268  df-recs 7329  df-rdg 7367  df-1o 7421  df-2o 7422  df-oadd 7425  df-er 7603  df-map 7720  df-pm 7721  df-ixp 7769  df-en 7816  df-dom 7817  df-sdom 7818  df-fin 7819  df-fsupp 8133  df-fi 8174  df-sup 8205  df-inf 8206  df-oi 8272  df-card 8622  df-cda 8847  df-pnf 9929  df-mnf 9930  df-xr 9931  df-ltxr 9932  df-le 9933  df-sub 10116  df-neg 10117  df-div 10531  df-nn 10865  df-2 10923  df-3 10924  df-4 10925  df-5 10926  df-6 10927  df-7 10928  df-8 10929  df-9 10930  df-n0 11137  df-z 11208  df-dec 11323  df-uz 11517  df-q 11618  df-rp 11662  df-xneg 11775  df-xadd 11776  df-xmul 11777  df-ico 12005  df-icc 12006  df-fz 12150  df-fzo 12287  df-fl 12407  df-seq 12616  df-exp 12675  df-fac 12875  df-bc 12904  df-hash 12932  df-shft 13598  df-cj 13630  df-re 13631  df-im 13632  df-sqrt 13766  df-abs 13767  df-limsup 13993  df-clim 14010  df-rlim 14011  df-sum 14208  df-ef 14580  df-struct 15640  df-ndx 15641  df-slot 15642  df-base 15643  df-sets 15644  df-ress 15645  df-plusg 15724  df-mulr 15725  df-starv 15726  df-sca 15727  df-vsca 15728  df-ip 15729  df-tset 15730  df-ple 15731  df-ds 15734  df-unif 15735  df-hom 15736  df-cco 15737  df-rest 15849  df-topn 15850  df-0g 15868  df-gsum 15869  df-topgen 15870  df-pt 15871  df-prds 15874  df-xrs 15928  df-qtop 15933  df-imas 15934  df-xps 15936  df-mre 16012  df-mrc 16013  df-acs 16015  df-mgm 17008  df-sgrp 17050  df-mnd 17061  df-submnd 17102  df-mulg 17307  df-cntz 17516  df-cmn 17961  df-psmet 19502  df-xmet 19503  df-met 19504  df-bl 19505  df-mopn 19506  df-fbas 19507  df-fg 19508  df-cnfld 19511  df-top 20460  df-bases 20461  df-topon 20462  df-topsp 20463  df-cld 20572  df-ntr 20573  df-cls 20574  df-nei 20651  df-lp 20689  df-perf 20690  df-cn 20780  df-cnp 20781  df-haus 20868  df-tx 21114  df-hmeo 21307  df-fil 21399  df-fm 21491  df-flim 21492  df-flf 21493  df-xms 21873  df-ms 21874  df-tms 21875  df-cncf 22417  df-limc 23350  df-dv 23351
This theorem is referenced by:  dvsincos  23462  efcn  23915  efcvx  23921  pige3  23987  dvrelog  24097  dvlog  24111  dvcxp1  24195  dvcxp2  24196  dvcncxp1  24198  dvsef  37353  expgrowthi  37354  expgrowth  37356
  Copyright terms: Public domain W3C validator