Most Recent Proofs - Metamath Proof Explorer

Metamath Proof Explorer
Most Recent Proofs

A theorem a day prevents mental decay. —mathematician Eric Charles Milner (1928-1997)

Most Recent Proofs These are the 10 (GIF, Unicode) or 100 (GIF, Unicode) most recent proofs in the Metamath Proof Explorer and the Hilbert Space Explorer. The official, cleaned up set.mm database file in the Metamath program download is sometimes several days behind the preproduction set.mm (7MB) that corresponds to this page. Email: Norm Megill. Wikis: AsteroidMeta (Recent Changes); Ghestalt (Recent Changes). Mailing list: Google Groups. Syndication: RSS feed (web version) courtesy of Dan Getz.

As a speed-up experiment, all mpegif/mpeuni HTML pages except mmrecent.html have been gzipped (on us2 only). If your browser has a problem with this, please let me know or discuss here. Thanks. — Norm 21 Nov 2007

Color key:

Metamath Proof Explorer

Hilbert Space Explorer

Last updated on 6-May-2008 at 2:08 PM ET.

**Recent Additions to the Metamath Proof Explorer** Notes (last updated 6-May-08 ) News (last updated 14-Apr-08 )
Date	Label	Description
Theorem

6-May-2008	pnfnemnf 5460	Plus and minus infinity are distinguished elements of ℝ^*.
⊢ +∞ ≠ -∞

6-May-2008	mnfnre 5420	Minus infinity is not a real number.
⊢ -∞ ∉ ℝ

6-May-2008	pnfnre 5419	Plus infinity is not a real number.
⊢ +∞ ∉ ℝ

6-May-2008	mnfxr 5417	Minus infinity belongs to the set of extended reals.
⊢ -∞ ∈ ℝ^*

6-May-2008	pnfxr 5416	Plus infinity belongs to the set of extended reals.
⊢ +∞ ∈ ℝ^*

6-May-2008	axinf2 4548	A standard version of Axiom of Infinity, expanded to primitives, derived from our version of Infinity ax-inf 4546 and Regularity ax-reg 4517. This theorem should not be referenced in any proof. Instead, use ax-inf2 4549 below so that the uses of Regularity and standard Infinity can be more easily identified.
⊢ ∃x(∃y(y ∈ x ⋀ ∀z ¬ z ∈ y) ⋀ ∀y(y ∈ x → ∃z(z ∈ x ⋀ ∀w(w ∈ z ↔ (w ∈ y ⋁ w = y)))))

6-May-2008	sdomn2lp 4409	Strict dominance has no 2-cycle loops.
⊢ ¬ (A ≺ B ⋀ B ≺ A)

5-May-2008	sspid 8253	A normed complex vector space is a subspace of itself.
⊢ H = (SubSp ‘U) ⇒ ⊢ (U ∈ NrmCVec → U ∈ H)

5-May-2008	curry1val 4038	The value of a curried function with a constant first argument.
⊢ G = (F ∘ ^◡(2^nd ↾ ({C} × V))) ⇒ ⊢ ((F Fn (A × B) ⋀ C ∈ A ⋀ D ∈ U) → (G ‘D) = (CFD))

5-May-2008	curry1f 4037	Functionality of a curried function with a constant first argument.
⊢ G = (F ∘ ^◡(2^nd ↾ ({C} × V))) ⇒ ⊢ ((F:(A × B)–→D ⋀ C ∈ A) → G:B–→D)

4-May-2008	minvecex2 8454	Existence version of minvecle 8452.
⊢ X = (Base ‘U) & ⊢ M = ( −_v ‘U) & ⊢ N = (norm ‘U) & ⊢ Y = (Base ‘W) & ⊢ U ∈ CPreHil & ⊢ W ∈ ((SubSp ‘U) ∩ CBan) & ⊢ A ∈ X ⇒ ⊢ ∃x ∈ Y ∀y ∈ Y (N ‘(AMx)) ≤ (N ‘(AMy))

4-May-2008	minveclem39 8453	Lemma for minvecex2 8454.
⊢ X = (Base ‘U) & ⊢ M = ( −_v ‘U) & ⊢ N = (norm ‘U) & ⊢ Y = (Base ‘W) & ⊢ R = {x∣∃y ∈ Y x = -(N ‘(AMy))} & ⊢ P = -sup(R, ℝ, < ) & ⊢ U ∈ CPreHil & ⊢ W ∈ ((SubSp ‘U) ∩ CBan) & ⊢ A ∈ X & ⊢ Q = ∪{b ∈ Y∣(N ‘(AMb)) = P} ⇒ ⊢ ∃a ∈ Y ∀f ∈ Y (N ‘(AMa)) ≤ (N ‘(AMf))

4-May-2008	ntridm 7592	The interior operation is idempotent.
⊢ X = ∪J ⇒ ⊢ ((J ∈ Top ⋀ S ⊆ X) → ((int ‘J) ‘((int ‘J) ‘S)) = ((int ‘J) ‘S))

3-May-2008	minvecle 8452	The minimizing vector from minveceu 8449 has the smallest distance.
⊢ X = (Base ‘U) & ⊢ M = ( −_v ‘U) & ⊢ N = (norm ‘U) & ⊢ Y = (Base ‘W) & ⊢ R = {x∣∃y ∈ Y x = -(N ‘(AMy))} & ⊢ P = -sup(R, ℝ, < ) & ⊢ U ∈ CPreHil & ⊢ W ∈ ((SubSp ‘U) ∩ CBan) & ⊢ A ∈ X & ⊢ Q = ∪{b ∈ Y∣(N ‘(AMb)) = P} ⇒ ⊢ (B ∈ Y → (N ‘(AMQ)) ≤ (N ‘(AMB)))

3-May-2008	minvecdist 8451	Distance of the minimizing vector of minveceu 8449.
⊢ X = (Base ‘U) & ⊢ M = ( −_v ‘U) & ⊢ N = (norm ‘U) & ⊢ Y = (Base ‘W) & ⊢ R = {x∣∃y ∈ Y x = -(N ‘(AMy))} & ⊢ P = -sup(R, ℝ, < ) & ⊢ U ∈ CPreHil & ⊢ W ∈ ((SubSp ‘U) ∩ CBan) & ⊢ A ∈ X & ⊢ Q = ∪{b ∈ Y∣(N ‘(AMb)) = P} ⇒ ⊢ (N ‘(AMQ)) = P

3-May-2008	minveccl 8450	The minimizing vector of minveceu 8449 belongs to the subspace Y.
⊢ X = (Base ‘U) & ⊢ M = ( −_v ‘U) & ⊢ N = (norm ‘U) & ⊢ Y = (Base ‘W) & ⊢ R = {x∣∃y ∈ Y x = -(N ‘(AMy))} & ⊢ P = -sup(R, ℝ, < ) & ⊢ U ∈ CPreHil & ⊢ W ∈ ((SubSp ‘U) ∩ CBan) & ⊢ A ∈ X & ⊢ Q = ∪{b ∈ Y∣(N ‘(AMb)) = P} ⇒ ⊢ Q ∈ Y

2-May-2008	minveceu 8449	Minimizing vector theorem. There is exactly one vector in a complete subspace W that minimizes the distance to an arbitrary vector A in a parent inner product space. Theorem 3.3-1 of [Kreyszig] p. 144, specialized to subspaces instead of convex subsets. Note that we work with the negative of the supremum of negatives instead of infimum in order to use theorems we already have available.
⊢ X = (Base ‘U) & ⊢ M = ( −_v ‘U) & ⊢ N = (norm ‘U) & ⊢ Y = (Base ‘W) & ⊢ R = {x∣∃y ∈ Y x = -(N ‘(AMy))} & ⊢ P = -sup(R, ℝ, < ) & ⊢ U ∈ CPreHil & ⊢ W ∈ ((SubSp ‘U) ∩ CBan) & ⊢ A ∈ X ⇒ ⊢ ∃!a ∈ Y (N ‘(AMa)) = P

2-May-2008	minveclem38 8448	Lemma for minveceu 8449.
⊢ X = (Base ‘U) & ⊢ G = ( +_v ‘U) & ⊢ M = ( −_v ‘U) & ⊢ S = ( ·_s ‘U) & ⊢ N = (norm ‘U) & ⊢ Y = (Base ‘W) & ⊢ U ∈ CPreHil & ⊢ A ∈ X & ⊢ W ∈ (SubSp ‘U) & ⊢ P = -sup(R, ℝ, < ) & ⊢ R = {x∣∃y ∈ Y x = -(N ‘(AMy))} ⇒ ⊢ (((a ∈ Y ⋀ b ∈ Y) ⋀ ((N ‘(AMa)) = P ⋀ (N ‘(AMb)) = P)) → (N ‘(aMb)) ≤ 0)

1-May-2008	minveclem37 8447	Lemma for minveceu 8449.
⊢ X = (Base ‘U) & ⊢ G = ( +_v ‘U) & ⊢ M = ( −_v ‘U) & ⊢ S = ( ·_s ‘U) & ⊢ N = (norm ‘U) & ⊢ Y = (Base ‘W) & ⊢ U ∈ CPreHil & ⊢ A ∈ X & ⊢ W ∈ (SubSp ‘U) & ⊢ P = -sup(R, ℝ, < ) & ⊢ R = {x∣∃y ∈ Y x = -(N ‘(AMy))} ⇒ ⊢ ((a ∈ Y ⋀ b ∈ Y) → P ≤ (N ‘(AM((1 / 2)S(aGb)))))

1-May-2008	minveclem36 8446	Lemma for minveceu 8449.
⊢ X = (Base ‘U) & ⊢ G = ( +_v ‘U) & ⊢ M = ( −_v ‘U) & ⊢ S = ( ·_s ‘U) & ⊢ N = (norm ‘U) & ⊢ Y = (Base ‘W) & ⊢ U ∈ CPreHil & ⊢ A ∈ X & ⊢ W ∈ (SubSp ‘U) & ⊢ P = -sup(R, ℝ, < ) & ⊢ R = {x∣∃y ∈ Y x = -(N ‘(AMy))} ⇒ ⊢ (((a ∈ X ⋀ b ∈ X) ⋀ ((N ‘(AMa)) = P ⋀ (N ‘(AMb)) = P)) → ((N ‘(aMb))↑2) = ((2 · ((P↑2) + (P↑2))) − ((N ‘((AMa)G(AMb)))↑2)))

1-May-2008	grprndm 7936	A group's range in terms of its domain.
⊢ (G ∈ Grp → ran G = dom dom G)

30-Apr-2008	ho02 9886	A condition implying that a Hilbert space operator is identically zero. Lemma 3.2(S10) of [Beran] p. 95.
⊢ T: ℋ –→ ℋ ⇒ ⊢ (∀x ∈ ℋ ∀y ∈ ℋ (x ·_ih (T ‘y)) = 0 ↔ T = 0_hop )

30-Apr-2008	hhssnm 9282	The norm operation on a subspace.
⊢ W = ⟨⟨( +_h ↾ (H × H)), ( ·_h ↾ (ℂ × H))⟩, (norm_h ↾ H)⟩ ⇒ ⊢ (norm_h ↾ H) = (norm ‘W)

30-Apr-2008	sb6f 1185	Equivalence for substitution when y is not free in φ.
⊢ (φ → ∀yφ) ⇒ ⊢ ([y / x]φ ↔ ∀x(x = y → φ))

29-Apr-2008	hhsssm 9281	The scalar multiplication operation on a subspace.
⊢ W = ⟨⟨( +_h ↾ (H × H)), ( ·_h ↾ (ℂ × H))⟩, (norm_h ↾ H)⟩ ⇒ ⊢ ( ·_h ↾ (ℂ × H)) = ( ·_s ‘W)

28-Apr-2008	clsidm 7591	The closure operation is idempotent.
⊢ X = ∪J ⇒ ⊢ ((J ∈ Top ⋀ S ⊆ X) → ((cls ‘J) ‘((cls ‘J) ‘S)) = ((cls ‘J) ‘S))

27-Apr-2008	icmpmon 8937	If (GRF) is monic then F is monic. JFM CAT₁ th. 62 (Part of FL's sandbox.)
⊢ O = dom (id ‘T) & ⊢ H = (hom ‘T) & ⊢ R = (o ‘T) ⇒ ⊢ ((T ∈ Cat ⋀ ((A ∈ O ⋀ B ∈ O ⋀ C ∈ O) ⋀ (F ∈ (H ‘⟨A, B⟩) ⋀ G ∈ (H ‘⟨B, C⟩)) ⋀ (GRF) ∈ (Monic ‘T))) → F ∈ (Monic ‘T))

27-Apr-2008	cnfilca 8801	Condition to have a filter finer than a given filter and containing a set A. (Part of FL's sandbox.) Bourbaki T.G. I.37 cor. 1
⊢ ((F ∈ Fil ⋀ A ⊆ ∪F ⋀ A ≠ ∅) → (∃g ∈ Fil (A ∈ g ⋀ F ⊆ g) ↔ ∀x ∈ F (x ∩ A) ≠ ∅))

27-Apr-2008	efilcp2 8800	A filter containing a set A exists iff A has the finite intersection property (i.e. no finite intersection of elements of A is empty). Bourbaki TG I.37 prop. 1. (Part of FL's sandbox.)
⊢ ((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) → (¬ ∅ ∈ (fi ‘A) ↔ ∃x ∈ Fil A ⊆ x))

27-Apr-2008	fgsb2 8799	Filter generated by a subbasis A. Bourbaki TG I.37 paragraph above prop. 1. (The theorem has been slightly modified because the definitions of the empty set are different in Bourbaki and Metamath.) (Part of FL's sandbox.)
⊢ ((A ⊆ ℘X ⋀ X ∈ V ⋀ A ≠ ∅) → (¬ ∅ ∈ (fi ‘A) → {x ∈ ℘X∣∃y ∈ (fi ‘A)y ⊆ x} ∈ Fil))

27-Apr-2008	infi 8798	The intersection of two finite intersections is a finite intersection. (Part of FL's sandbox.)
⊢ (C ∈ D → ((A ∈ (fi ‘C) ⋀ B ∈ (fi ‘C)) → (A ∩ B) ∈ (fi ‘C)))

27-Apr-2008	fisub 8797	If a set has the finite intersection property, its subsets have also this property. (Part of FL's sandbox.)
⊢ B = {z∣∃y(y ⊆ A ⋀ ∃u ∈ ω y ≈ u ⋀ z = ∩y)} & ⊢ D = {z∣∃y(y ⊆ C ⋀ ∃u ∈ ω y ≈ u ⋀ z = ∩y)} ⇒ ⊢ (C ⊆ A → (¬ ∅ ∈ B → ¬ ∅ ∈ D))

27-Apr-2008	filint2 8796	A filter is closed under taking finite intersections. (Part of FL's sandbox.)
⊢ (F ∈ Fil → ((A ⊆ F ⋀ A ≠ ∅ ⋀ ∃x ∈ ω A ≈ x) → ∩A ∈ F))

27-Apr-2008	abfi2 8735	Any element of a set A is the intersection of a finite subset of A. (Part of FL's sandbox.)
⊢ (A ∈ B → A ⊆ (fi ‘A))

27-Apr-2008	fiiu2 8734	If A is the intersection of a finite set of elements of B then A ⊆ ∪B. (Part of FL's sandbox.)
⊢ (B ∈ C → (A ∈ (fi ‘B) → A ⊆ ∪B))

27-Apr-2008	sppfi 8733	Specific properties of an element of (fi ‘C). (Part of FL's sandbox.)
⊢ ((A ∈ B ⋀ C ∈ D) → (A ∈ (fi ‘C) ↔ ∃z(z ⊆ C ⋀ ∃a ∈ ω z ≈ a ⋀ A = ∩z)))

27-Apr-2008	fine2 8732	If A is not empty, the class of all the finite intersections of A is not empty either. (Part of FL's sandbox.)
⊢ (A ∈ B → (A ≠ ∅ → (fi ‘A) ≠ ∅))

27-Apr-2008	fiv 8731	The set of all the finite intersections of the elements of A. (Part of FL's sandbox.)
⊢ (A ∈ B → (fi ‘A) = {u∣∃z(z ⊆ A ⋀ ∃a ∈ ω z ≈ a ⋀ u = ∩z)})

27-Apr-2008	neiopne 8728	If an intersection is not empty its operands are not empty. (Part of FL's sandbox.)
⊢ ((A ∩ B) ≠ ∅ → (A ≠ ∅ ⋀ B ≠ ∅))

27-Apr-2008	ficli 8727	The class of finite intersections of a class L are closed under intersection. (Part of FL's sandbox.)
⊢ F = {x∣∃y(y ⊆ L ⋀ ∃z ∈ ω y ≈ z ⋀ x = ∩y)} ⇒ ⊢ ((A ∈ F ⋀ B ∈ F) → (A ∩ B) ∈ F)

27-Apr-2008	intprd 8726	The intersection of a pair is the intersection of its members. Closed for of intpr 2531.Theorem 71 of [Suppes] p. 42. (Part of FL's sandbox.)
⊢ ((A ∈ V ⋀ B ∈ V) → ∩{A, B} = (A ∩ B))

27-Apr-2008	cbvrexf 8698	Rule used to change bound variables with implicit substitution. More general than cbvrex 1774. (Part of FL's sandbox.)
⊢ (z ∈ A → ∀x z ∈ A) & ⊢ (z ∈ A → ∀y z ∈ A) & ⊢ (φ → ∀yφ) & ⊢ (ψ → ∀xψ) & ⊢ (x = y → (φ ↔ ψ)) ⇒ ⊢ (∃x ∈ A φ ↔ ∃y ∈ A ψ)

27-Apr-2008	minveclem35 8445	Lemma for minveceu 8449.
⊢ X = (Base ‘U) & ⊢ G = ( +_v ‘U) & ⊢ M = ( −_v ‘U) & ⊢ S = ( ·_s ‘U) & ⊢ N = (norm ‘U) & ⊢ Y = (Base ‘W) & ⊢ U ∈ CPreHil & ⊢ A ∈ X ⇒ ⊢ ((a ∈ X ⋀ b ∈ X) → (N ‘((AMa)G(AMb))) = (2 · (N ‘(AM((1 / 2)S(aGb))))))

26-Apr-2008	effoi 8579	The exponential function maps the set S, of complex numbers with imaginary part in a closed-below, open-above real interval of length 2 · π starting at A, onto the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008.)
⊢ A ∈ ℝ & ⊢ D = (A[,)(A + (2 · π))) & ⊢ S = {v ∈ ℂ∣(ℑ ‘v) ∈ D} & ⊢ F = {⟨z, w⟩∣(z ∈ D ⋀ w = (exp ‘(i · z)))} & ⊢ C = {v ∈ ℂ∣(abs ‘v) = 1} ⇒ ⊢ (exp ↾ S):S–onto→(ℂ ∖ {0})

26-Apr-2008	shftefif1olem 8574	Lemma for shftefif1o 8576.
⊢ D = (A[,)(A + (2 · π))) & ⊢ G = {⟨x, y⟩∣(x ∈ D ⋀ y = (exp ‘(i · x)))} & ⊢ C = {w ∈ ℂ∣(abs ‘w) = 1} & ⊢ F = {⟨x, y⟩∣(x ∈ (0[,)(2 · π)) ⋀ y = (exp ‘(i · x)))} & ⊢ S = {⟨x, y⟩∣(x ∈ (A[,)(A + (2 · π))) ⋀ y = (x + -A))} & ⊢ T = ( · ↾ (C × C)) & ⊢ L = {⟨u, v⟩∣(u ∈ C ⋀ v = {⟨x, y⟩∣(x ∈ C ⋀ y = (uTx))})} & ⊢ H = ((L ‘(exp ‘(i · A))) ∘ (F ∘ S)) ⇒ ⊢ (A ∈ ℝ → G:D–1-1-onto→C)

26-Apr-2008	circgrp 8573	The circle group T is an Abelian group. (Contributed by Paul Chapman, 25-Mar-2008.)
⊢ C = {w ∈ ℂ∣(abs ‘w) = 1} & ⊢ T = ( · ↾ (C × C)) ⇒ ⊢ T ∈ Abel

26-Apr-2008	efielcirc 8572	Membership of the exponential function of i times a real number in the unit circle. (Contributed by Paul Chapman, 25-Mar-2008.)
⊢ C = {w ∈ ℂ∣(abs ‘w) = 1} ⇒ ⊢ (A ∈ ℝ → (exp ‘(i · A)) ∈ C)

26-Apr-2008	ghsubgi 8023	The image of a subgroup S of group G under a group homomorphism F on G is a group, and furthermore is Abelian if S is Abelian. (Contributed by Paul Chapman, 25-Apr-2008.)
⊢ S ∈ (SubGrp ‘G) & ⊢ X = ran G & ⊢ F:X–→Y & ⊢ Y ⊆ A & ⊢ O Fn (A × A) & ⊢ ((x ∈ X ⋀ y ∈ X) → (F ‘(xGy)) = ((F ‘x)O(F ‘y))) & ⊢ Z = ran S & ⊢ W = (F “ Z) & ⊢ H = (O ↾ (W × W)) ⇒ ⊢ (H ∈ Grp ⋀ (S ∈ Abel → H ∈ Abel))

26-Apr-2008	ghgrpi 8022	The image of a group G under a group homomorphism F is a group, and furthermore is Abelian if G is Abelian. This is a stronger result than that usually found in the literature, since the target of the homomorphism (operator O in our model) need not have any of the properties of a group as a prerequisite. (Contributed by Paul Chapman, 25-Apr-2008.)
⊢ G ∈ Grp & ⊢ X = ran G & ⊢ F:X–onto→Y & ⊢ Y ⊆ A & ⊢ O Fn (A × A) & ⊢ ((x ∈ X ⋀ y ∈ X) → (F ‘(xGy)) = ((F ‘x)O(F ‘y))) & ⊢ H = (O ↾ (Y × Y)) ⇒ ⊢ (H ∈ Grp ⋀ (G ∈ Abel → H ∈ Abel))

26-Apr-2008	ghgrpilem4 8021	Lemma for ghgrpi 8022.
⊢ G ∈ Grp & ⊢ X = ran G & ⊢ F:X–onto→Y & ⊢ Y ⊆ A & ⊢ O Fn (A × A) & ⊢ ((x ∈ X ⋀ y ∈ X) → (F ‘(xGy)) = ((F ‘x)O(F ‘y))) & ⊢ H = (O ↾ (Y × Y)) & ⊢ U = (Id ‘G) & ⊢ N = (inv ‘G) & ⊢ D = ( /_g ‘G) ⇒ ⊢ H ∈ Grp

26-Apr-2008	ghgrpilem3 8020	Lemma for ghgrpi 8022.
⊢ G ∈ Grp & ⊢ X = ran G & ⊢ F:X–onto→Y & ⊢ Y ⊆ A & ⊢ O Fn (A × A) & ⊢ ((x ∈ X ⋀ y ∈ X) → (F ‘(xGy)) = ((F ‘x)O(F ‘y))) & ⊢ H = (O ↾ (Y × Y)) & ⊢ U = (Id ‘G) & ⊢ N = (inv ‘G) & ⊢ D = ( /_g ‘G) ⇒ ⊢ ((a ∈ Y ⋀ b ∈ Y) → (∃c ∈ Y (cHa) = b ⋀ ∃c ∈ Y (aHc) = b))

26-Apr-2008	ghgrpilem2 8019	Lemma for ghgrpi 8022.
⊢ G ∈ Grp & ⊢ X = ran G & ⊢ F:X–onto→Y & ⊢ Y ⊆ A & ⊢ O Fn (A × A) & ⊢ ((x ∈ X ⋀ y ∈ X) → (F ‘(xGy)) = ((F ‘x)O(F ‘y))) & ⊢ H = (O ↾ (Y × Y)) & ⊢ ((w ∈ X ⋀ φ) → ψ) & ⊢ ((F ‘w) = C → (ψ ↔ χ)) ⇒ ⊢ ((φ ⋀ C ∈ Y) → χ)

26-Apr-2008	ghgrpilem1 8018	Lemma for ghgrpi 8022.
⊢ G ∈ Grp & ⊢ X = ran G & ⊢ F:X–onto→Y & ⊢ Y ⊆ A & ⊢ O Fn (A × A) & ⊢ ((x ∈ X ⋀ y ∈ X) → (F ‘(xGy)) = ((F ‘x)O(F ‘y))) & ⊢ H = (O ↾ (Y × Y)) ⇒ ⊢ ((C ∈ X ⋀ D ∈ X) → (F ‘(CGD)) = ((F ‘C)H(F ‘D)))

26-Apr-2008	zaddsubg 8015	The integers under addition comprise a subgroup of the complex numbers under addition. (Contributed by Paul Chapman, 25-Apr-2008.)
⊢ ( + ↾ (ℤ × ℤ)) ∈ (SubGrp ‘ + )

26-Apr-2008	readdsubg 8014	The real numbers under addition comprise a subgroup of the complex numbers under addition. (Contributed by Paul Chapman, 25-Apr-2008.)
⊢ ( + ↾ (ℝ × ℝ)) ∈ (SubGrp ‘ + )

26-Apr-2008	subgabl 8008	A subgroup of an Abelian group is Abelian. (Contributed by Paul Chapman, 25-Apr-2008.)
⊢ ((G ∈ Abel ⋀ H ∈ (SubGrp ‘G)) → H ∈ Abel)

26-Apr-2008	sin0ALT 7338	Value of the sine function at 0.
⊢ (sin ‘0) = 0

25-Apr-2008	efghgrpi 8548	The image of a subgroup of the group +, under the exponential function of a scaled complex number, is an Abelian group. (Contributed by Paul Chapman, 25-Apr-2008.)
⊢ S = {y∣∃x ∈ X y = (exp ‘(A · x))} & ⊢ G = ( · ↾ (S × S)) & ⊢ A ∈ ℂ & ⊢ X ⊆ ℂ & ⊢ ( + ↾ (X × X)) ∈ (SubGrp ‘ + ) ⇒ ⊢ G ∈ Abel

25-Apr-2008	efghgrpilem 8547	Lemma for efghgrpi 8548,
⊢ S = {y∣∃x ∈ X y = (exp ‘(A · x))} & ⊢ G = ( · ↾ (S × S)) & ⊢ A ∈ ℂ & ⊢ X ⊆ ℂ & ⊢ ( + ↾ (X × X)) ∈ (SubGrp ‘ + ) & ⊢ F = {⟨x, y⟩∣(x ∈ ℂ ⋀ y = (exp ‘(A · x)))} ⇒ ⊢ G ∈ Abel

25-Apr-2008	efgh 8546	The exponential function of a scaled complex number is a group homomorphism from the group of complex numbers under addition to the set of complex numbers under multiplication. (Contributed by Paul Chapman, 25-Apr-2008.)
⊢ F = {⟨x, y⟩∣(x ∈ ℂ ⋀ y = (exp ‘(A · x)))} ⇒ ⊢ ((A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ ℂ) → (F ‘(B + C)) = ((F ‘B) · (F ‘C)))

25-Apr-2008	resgrprn 7978	The underlying set of a group operation which is a restriction of a mapping. (Contributed by Paul Chapman, 25-Mar-2008.)
⊢ H = (G ↾ (Y × Y)) ⇒ ⊢ ((dom G = (X × X) ⋀ H ∈ Grp ⋀ Y ⊆ X) → Y = ran H)

25-Apr-2008	equs45f 1184	Two ways of expressing substitution when y is not free in φ.
⊢ (φ → ∀yφ) ⇒ ⊢ (∃x(x = y ⋀ φ) ↔ ∀x(x = y → φ))

24-Apr-2008	geoisumr 7129	The infinite sum of reciprocals 1 + (1 / A)↑1 + (1 / A)↑2 ... is A / (A − 1). (Contributed by rpenner, 3-Nov-2007.)
⊢ ((A ∈ ℂ ⋀ 1 < (abs ‘A)) → Σk ∈ ℕ₀ ((1 / A)↑k) = (A / (A − 1)))

24-Apr-2008	subsq 6528	Factor the difference of two squares.
⊢ A ∈ ℂ & ⊢ B ∈ ℂ ⇒ ⊢ ((A↑2) − (B↑2)) = ((A + B) · (A − B))

24-Apr-2008	f1orescnv 3643	The converse of a one-to-one-onto restricted function. (Contributed by Paul Chapman, 21-Apr-2008.)
⊢ ((Fun ^◡F ⋀ (F ↾ R):R–1-1-onto→P) → (^◡F ↾ P):P–1-1-onto→R)

23-Apr-2008	leoptrit 10195	The positive operator ordering relation satisfies trichotomy. Exercise 1(iii) of [Retherford] p. 49.
⊢ ((T ∈ HrmOp ⋀ U ∈ HrmOp) → ((T ≤_op U ⋀ U ≤_op T) ↔ T = U))

23-Apr-2008	lnocoi 8287	The composition of two linear operators is linear.
⊢ L = (U LnOp W) & ⊢ M = (W LnOp X) & ⊢ N = (U LnOp X) & ⊢ U ∈ NrmCVec & ⊢ W ∈ NrmCVec & ⊢ X ∈ NrmCVec & ⊢ S ∈ L & ⊢ T ∈ M ⇒ ⊢ (T ∘ S) ∈ N

22-Apr-2008	hhssva 9280	The vector addition operation on a subspace.
⊢ W = ⟨⟨( +_h ↾ (H × H)), ( ·_h ↾ (ℂ × H))⟩, (norm_h ↾ H)⟩ ⇒ ⊢ ( +_h ↾ (H × H)) = ( +_v ‘W)

22-Apr-2008	cmntrcld 7587	The complement of an interior is closed.
⊢ X = ∪J ⇒ ⊢ ((J ∈ Top ⋀ S ⊆ X) → (X ∖ ((int ‘J) ‘S)) ∈ (Clsd ‘J))

21-Apr-2008	logltbt 8611	The natural logarithm function on positive reals is strictly monotonic. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ ((A ∈ ℝ⁺ ⋀ B ∈ ℝ⁺) → (A < B ↔ (log ‘A) < (log ‘B)))

21-Apr-2008	relogiso 8610	The natural logarithm function on positive reals determines an isomorphism from the positive reals onto the reals. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ (log ↾ ℝ⁺) Isom < , < (ℝ⁺, ℝ)

21-Apr-2008	relogexpt 8609	The natural logarithm of positive A raised to an nonnegative integer power. Property 4 of [Cohen] p. 301-302, restricted to natural logarithms and nonnegative-integer powers N. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ ((A ∈ ℝ⁺ ⋀ N ∈ ℕ₀) → (log ‘(A↑N)) = (N · (log ‘A)))

21-Apr-2008	reexplogt 8608	Exponentiation of a positive real number to a nonnegative integer power. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ ((A ∈ ℝ⁺ ⋀ N ∈ ℕ₀) → (A↑N) = (exp ‘(N · (log ‘A))))

21-Apr-2008	explogt 8607	Exponentiation of a nonzero complex number to a nonnegative integer power. (Contributed by Paul Chapman, 21-Apr-2008.)
⊢ ((A ∈ ℂ ⋀ A ≠ 0 ⋀ N ∈ ℕ₀) → (A↑N) = (exp ‘(N · (log ‘A))))

21-Apr-2008	relogdivt 8606	The natural logarithm of the quotient of two positive real numbers is the difference of natural logarithms. Exercise 72(a) and Property 3 of [Cohen] p. 301, restricted to natural logarithms. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ ((A ∈ ℝ⁺ ⋀ B ∈ ℝ⁺) → (log ‘(A / B)) = ((log ‘A) − (log ‘B)))

21-Apr-2008	relogmult 8605	The natural logarithm of the product of two positive real numbers is the sum of natural logarithms. Property 2 of [Cohen] p. 301, restricted to natural logarithms. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ ((A ∈ ℝ⁺ ⋀ B ∈ ℝ⁺) → (log ‘(A · B)) = ((log ‘A) + (log ‘B)))

21-Apr-2008	relogoprlem 8604	Lemma for relogmult 8605 and relogdivt 8606. Remark of [Cohen] p. 301 ("The proof of Property 3 is quite similar to the proof given for Property 2").
⊢ (((log ‘A) ∈ ℂ ⋀ (log ‘B) ∈ ℂ) → (exp ‘((log ‘A)F(log ‘B))) = ((exp ‘(log ‘A))G(exp ‘(log ‘B)))) & ⊢ (((log ‘A) ∈ ℝ ⋀ (log ‘B) ∈ ℝ) → ((log ‘A)F(log ‘B)) ∈ ℝ) ⇒ ⊢ ((A ∈ ℝ⁺ ⋀ B ∈ ℝ⁺) → (log ‘(AGB)) = ((log ‘A)F(log ‘B)))

21-Apr-2008	pilog 8603	Relationship between π and the natural logarithm function. (Contributed by Paul Chapman, 21-Apr-2008.)
⊢ π = (i · (log ‘-1))

21-Apr-2008	loge 8602	The natural logarithm of e. One case of Property 1b of [Cohen] p. 301. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ (log ‘e) = 1

21-Apr-2008	log1 8601	The natural logarithm of 1. One case of Property 1a of [Cohen] p. 301. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ (log ‘1) = 0

21-Apr-2008	relogeftb 8600	Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ ((A ∈ ℝ⁺ ⋀ B ∈ ℝ) → ((log ‘A) = B ↔ (exp ‘B) = A))

21-Apr-2008	logeftb 8599	Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008.)
⊢ ((A ∈ ℂ ⋀ A ≠ 0 ⋀ B ∈ ran log) → ((log ‘A) = B ↔ (exp ‘B) = A))

21-Apr-2008	relogeft 8598	Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
⊢ (A ∈ ℝ &