Metamath Proof Explorer - mmtheorems40

Jump to page: 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5787

Statement List for Metamath Proof Explorer - 3901-4000 - Page 40 of 58

Type	Label	Description
Statement
Theorem	genpss 3901	The result of an operation on positive reals is a subset of the positive fractions.
|- F = {<.<.w, v>., u>. | ((w e. P. /\ v e. P.) /\ u = {x | E.y e. w E.z e. v x = (yGz)})}   &   |- ((g e. Q. /\ h e. Q.) -> (gGh) e. Q.)   =>   |- ((A e. P. /\ B e. P.) -> (AFB) (_ Q.)
Theorem	genpnnp 3902	The result of an operation on positive reals is different from the set of positive fractions.
|- F = {<.<.w, v>., u>. | ((w e. P. /\ v e. P.) /\ u = {x | E.y e. w E.z e. v x = (yGz)})}   &   |- ((w e. Q. /\ v e. Q.) -> (wGv) e. Q.)   &   |- (z e. Q. -> (x <Q y <-> (zGx) <Q (zGy)))   &   |- (xGy) = (yGx)   =>   |- ((A e. P. /\ B e. P.) -> -. (AFB) = Q.)
Theorem	genpcd 3903	Downward closure of an operation on positive reals.
|- F = {<.<.w, v>., u>. | ((w e. P. /\ v e. P.) /\ u = {x | E.y e. w E.z e. v x = (yGz)})}   &   |- ((((A e. P. /\ g e. A) /\ (B e. P. /\ h e. B)) /\ x e. Q.) -> (x <Q (gGh) -> x e. (AFB)))   =>   |- ((A e. P. /\ B e. P.) -> (f e. (AFB) -> (x <Q f -> x e. (AFB))))
Theorem	genpnmax 3904	An operation on positive reals has no largest member.
|- F = {<.<.w, v>., u>. | ((w e. P. /\ v e. P.) /\ u = {x | E.y e. w E.z e. v x = (yGz)})}   &   |- (v e. Q. -> (z <Q w <-> (vGz) <Q (vGw)))   &   |- (zGw) = (wGz)   =>   |- ((A e. P. /\ B e. P.) -> (f e. (AFB) -> E.x(x e. (AFB) /\ f <Q x)))
Theorem	genpcl 3905	Closure of an operation on reals.
|- F = {<.<.w, v>., u>. | ((w e. P. /\ v e. P.) /\ u = {x | E.y e. w E.z e. v x = (yGz)})}   &   |- ((x e. Q. /\ y e. Q.) -> (xGy) e. Q.)   &   |- (h e. Q. -> (f <Q g <-> (hGf) <Q (hGg)))   &   |- (xGy) = (yGx)   &   |- ((((A e. P. /\ g e. A) /\ (B e. P. /\ h e. B)) /\ x e. Q.) -> (x <Q (gGh) -> x e. (AFB)))   =>   |- ((A e. P. /\ B e. P.) -> (AFB) e. P.)
Theorem	genpass 3906	Associativity of an operation on reals.
|- F = {<.<.w, v>., u>. | ((w e. P. /\ v e. P.) /\ u = {x | E.y e. w E.z e. v x = (yGz)})}   &   |- B e. V   &   |- C e. V   &   |- dom F = (P. X. P.)   &   |- ((f e. P. /\ g e. P.) -> (fFg) e. P.)   &   |- ((fGg)Gh) = (fG(gGh))   =>   |- ((AFB)FC) = (AF(BFC))
Theorem	plpv 3907	Value of addition on positive reals.
|- ((A e. P. /\ B e. P.) -> (A +P. B) = {x | E.yE.z((y e. A /\ z e. B) /\ x = (y +Q z))})
Theorem	mpv 3908	Value of multiplication on positive reals.
|- ((A e. P. /\ B e. P.) -> (A .P B) = {x | E.yE.z((y e. A /\ z e. B) /\ x = (y .Q z))})
Theorem	dmplp 3909	Domain of addition on positive reals.
|- dom +P. = (P. X. P.)
Theorem	dmmp 3910	Domain of multiplication on positive reals.
|- dom .P = (P. X. P.)
Theorem	1pr 3911	The positive real number 'one'.
|- 1P e. P.
Theorem	addclprlem1 3912	Lemma to prove downward closure in positive real addition. Part of proof of Proposition 9-3.5 of [Gleason] p. 123.
|- (((A e. P. /\ g e. A) /\ x e. Q.) -> (x <Q (g +Q h) -> ((x .Q (*Q` (g +Q h))) .Q g) e. A))
Theorem	addclprlem2 3913	Lemma to prove downward closure in positive real addition. Part of proof of Proposition 9-3.5 of [Gleason] p. 123.
|- ((((A e. P. /\ g e. A) /\ (B e. P. /\ h e. B)) /\ x e. Q.) -> (x <Q (g +Q h) -> x e. (A +P. B)))
Theorem	addclpr 3914	Closure of addition on positive reals. First statement of Proposition 9-3.5 of [Gleason] p. 123.
|- ((A e. P. /\ B e. P.) -> (A +P. B) e. P.)
Theorem	mulclprlem 3915	Lemma to prove downward closure in positive real multiplication. Part of proof of Proposition 9-3.7 of [Gleason] p. 124.
|- ((((A e. P. /\ g e. A) /\ (B e. P. /\ h e. B)) /\ x e. Q.) -> (x <Q (g .Q h) -> x e. (A .P B)))
Theorem	mulclpr 3916	Closure of multiplication on positive reals. First statement of Proposition 9-3.7 of [Gleason] p. 124.
|- ((A e. P. /\ B e. P.) -> (A .P B) e. P.)
Theorem	addcompr 3917	Addition of positive reals is commutative. Proposition 9-3.5(ii) of [Gleason] p. 123.
|- A e. V   &   |- B e. V   =>   |- (A +P. B) = (B +P. A)
Theorem	addasspr 3918	Addition of positive reals is associative. Proposition 9-3.5(i) of [Gleason] p. 123.
|- B e. V   &   |- C e. V   =>   |- ((A +P. B) +P. C) = (A +P. (B +P. C))
Theorem	mulcompr 3919	Multiplication of positive reals is commutative. Proposition 9-3.7(ii) of [Gleason] p. 124.
|- A e. V   &   |- B e. V   =>   |- (A .P B) = (B .P A)
Theorem	mulasspr 3920	Multiplication of positive reals is associative. Proposition 9-3.7(i) of [Gleason] p. 124.
|- B e. V   &   |- C e. V   =>   |- ((A .P B) .P C) = (A .P (B .P C))
Theorem	distrlem1pr 3921	Lemma for distributive law for positive reals.
|- ((A e. P. /\ (B e. P. /\ C e. P.)) -> (A .P (B +P. C)) (_ ((A .P B) +P. (A .P C)))
Theorem	distrlem2pr 3922	Lemma for distributive law for positive reals.
|- ((A e. P. /\ (B e. P. /\ C e. P.)) -> ((x e. A /\ (y e. B /\ z e. C)) -> ((x .Q y) +Q (x .Q z)) e. (A .P (B +P. C))))
Theorem	distrlem3pr 3923	Lemma for distributive law for positive reals.
|- (((A e. P. /\ (B e. P. /\ C e. P.)) /\ (x e. A /\ (y e. B /\ z e. C))) -> (x e. Q. /\ (y e. Q. /\ z e. Q.)))
Theorem	distrlem4pr 3924	Lemma for distributive law for positive reals.
|- (((A e. P. /\ (B e. P. /\ C e. P.)) /\ ((x e. A /\ f e. A) /\ (y e. B /\ z e. C))) -> ((x .Q y) +Q (f .Q z)) e. (A .P (B +P. C)))
Theorem	distrlem5pr 3925	Lemma for distributive law for positive reals.
|- ((A e. P. /\ (B e. P. /\ C e. P.)) -> ((A .P B) +P. (A .P C)) (_ (A .P (B +P. C)))
Theorem	distrpr 3926	Multiplication of positive reals is distributive. Proposition 9-3.7(iii) of [Gleason] p. 124.
|- B e. V   &   |- C e. V   =>   |- (A .P (B +P. C)) = ((A .P B) +P. (A .P C))
Theorem	1idpr 3927	1 is an identity element for positive real multiplication. Theorem 9-3.7(iv) of [Gleason] p. 124.
|- (A e. P. -> (A .P 1P) = A)
Theorem	ltprord 3928	Positive real 'less than' in terms of proper subset.
|- ((A e. P. /\ B e. P.) -> (A <P B <-> A (. B))
Theorem	psslinpr 3929	Proper subset is a linear ordering on positive reals. Part of Proposition 9-3.3 of [Gleason] p. 122.
|- ((A e. P. /\ B e. P.) -> (A (. B \/ A = B \/ B (. A))
Theorem	ltsopr 3930	Positive real 'less than' is a strict ordering. Part of Proposition 9-3.3 of [Gleason] p. 122.
|- <P Or P.
Theorem	prlem934a 3931	Sublemma for Lemma 9-3.4 of [Gleason] p. 122.
|- B e. V   =>   |- (C e. N. -> (((B e. Q. /\ A.x(x e. A -> (x +Q B) e. A)) /\ y e. A) -> (y +Q ([<.C, 1o>.] ~Q .Q B)) e. A))
Theorem	prlem934b 3932	Sublemma for Lemma 9-3.4 of [Gleason] p. 122.
|- (((u e. N. /\ w e. N.) /\ (v e. N. /\ z e. N.)) -> (([<.(w .N v), 1o>.] ~Q .Q [<.z, w>.] ~Q ) = [<.v, u>.] ~Q \/ [<.v, u>.] ~Q <Q ([<.(w .N v), 1o>.] ~Q .Q [<.z, w>.] ~Q )))
Theorem	prlem934 3933	Lemma 9-3.4 of [Gleason] p. 122.
|- ((A e. P. /\ B e. Q.) -> E.x(x e. A /\ -. (x +Q B) e. A))
Theorem	ltaddpr 3934	The sum of two positive reals is greater than one of them. Proposition 9-3.5(iii) of [Gleason] p. 123.
|- ((A e. P. /\ B e. P.) -> A <P (A +P. B))
Theorem	ltaddpr2 3935	The sum of two positive reals is greater than one of them.
|- B e. V   =>   |- (C e. P. -> ((A +P. B) = C -> A <P C))
Theorem	ltexprlem1 3936	Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123.
|- C = {x | E.y(-. y e. A /\ (y +Q x) e. B)}   =>   |- (B e. P. -> (A (. B -> -. C = (/)))
Theorem	ltexprlem2 3937	Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123.
|- C = {