Metamath Proof Explorer - mmtheorems46

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 - 4501-4600 - Page 46 of 58

Type	Label	Description
Statement
Theorem	6p3e9 4501	6 + 3 = 9.
|- (6 + 3) = 9
Theorem	7p2e9 4502	7 + 2 = 9.
|- (7 + 2) = 9
Theorem	2t2e4 4503	2 times 2 equals 4.
|- (2 x. 2) = 4
Theorem	3t2e6 4504	3 times 2 equals 6.
|- (3 x. 2) = 6
Theorem	3t3e9 4505	3 times 3 equals 9.
|- (3 x. 3) = 9
Theorem	4t2e8 4506	4 times 2 equals 8.
|- (4 x. 2) = 8
Theorem	4d2e2 4507	One half of four is two.
|- (4 / 2) = 2
Theorem	halfpost 4508	A positive number is greater than its half.
|- (A e. RR -> (0 < A <-> (A / 2) < A))
Theorem	nominpos 4509	There exists no smallest positive real number.
|- -. E.x e. RR (0 < x /\ -. E.y e. RR (0 < y /\ y < x))
Theorem	sup2 4510	A non-empty, bounded-above set of reals has a supremum. Stronger version of completeness axiom (it has a slightly weaker antecedent).
|- ((A (_ RR /\ A =/= (/) /\ E.x e. RR A.y e. A (y < x \/ y = x)) -> E.x e. RR (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z)))
Theorem	sup3 4511	A version of the completeness axiom for reals.
|- ((A (_ RR /\ -. A = (/) /\ E.x e. RR A.y e. A y <_ x) -> E.x e. RR (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z)))
Theorem	suprcl 4512	Closure of supremum of a non-empty bounded set of reals.
|- ((A (_ RR /\ -. A = (/) /\ E.x e. RR A.y e. A y <_ x) -> sup(A, RR, < ) e. RR)
Theorem	suprub 4513	A member of a non-empty bounded set of reals is less than or equal to the set's upper bound.
|- (((A (_ RR /\ -. A = (/) /\ E.x e. RR A.y e. A y <_ x) /\ B e. A) -> B <_ sup(A, RR, < ))
Theorem	suprlub 4514	The supremum of a non-empty bounded set of reals is the least upper bound.
|- (((A (_ RR /\ -. A = (/) /\ E.x e. RR A.y e. A y <_ x) /\ (B e. RR /\ B < sup(A, RR, < ))) -> E.z e. A B < z)
Theorem	sup3i 4515	A version of the completeness axiom for reals.
|- (A (_ RR /\ -. A = (/) /\ E.x e. RR A.y e. A y <_ x)   =>   |- E.x e. RR (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z))
Theorem	suprcli 4516	Closure of supremum of a non-empty bounded set of reals.
|- (A (_ RR /\ -. A = (/) /\ E.x e. RR A.y e. A y <_ x)   =>   |- sup(A, RR, < ) e. RR
Theorem	suprubi 4517	A member of a non-empty bounded set of reals is less than or equal to the set's upper bound.
|- (A (_ RR /\ -. A = (/) /\ E.x e. RR A.y e. A y <_ x)   =>   |- (B e. A -> B <_ sup(A, RR, < ))
Theorem	suprlubi 4518	The supremum of a non-empty bounded set of reals is the least upper bound.
|- (A (_ RR /\ -. A = (/) /\ E.x e. RR A.y e. A y <_ x)   =>   |- ((B e. RR /\ B < sup(A, RR, < )) -> E.z e. A B < z)
Theorem	suprnubi 4519	An upper bound is not less than the supremum of a non-empty bounded set of reals.
|- (A (_ RR /\ -. A = (/) /\ E.x e. RR A.y e. A y <_ x)   =>   |- ((B e. RR /\ A.z e. A -. B < z) -> -. B < sup(A, RR, < ))
Theorem	nnunb 4520	The set of natural numbers is unbounded above. Theorem I.28 of [Apostol] p. 26.
|- -. E.x e. RR A.y e. NN (y < x \/ y = x)
Theorem	arch 4521	Archimedean property of real numbers. For any real number, there is an integer greater than it. Theorem I.29 of [Apostol] p. 26.
|- (A e. RR -> E.x e. NN A < x)
Theorem	nnreclt 4522	There exists a natural number whose reciprocal is less than a given positive real. Exercise 3 of [Apostol] p. 28.
|- ((A e. RR /\ 0 < A) -> E.x e. NN (1 / x) < A)
Theorem	avril1 4523	Poisson d'Avril's Theorem. This theorem is noted for its Selbstdokumentieren property, which means, literally, "self-documenting." (Contributed by Loof Lirpa 1-Apr-04.)
|- -. (AP~R(i` 1) /\ F(/)(0 x. 1))
Theorem	ine0 4524	The imaginary unit i is not zero.
|- -. i = 0
Theorem	isqm1 4525	i -squared is minus 1.
|- (i x. i) = -u1
Theorem	irec 4526	The reciprocal of i.
|- (1 / i) = -ui
Theorem	inelr 4527	The imaginary unit i is not a real number.
|- -. i e. RR
Theorem	crulem 4528	The real representation of complex numbers is unique. Lemma for Proposition 10-1.3 of [Gleason] p. 130.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   &   |- D e. RR   =>   |- ((A + (B x. i)) = (C + (D x. i)) -> B = D)
Theorem	cru 4529	The real representation of complex numbers is unique. Proposition 10-1.3 of [Gleason] p. 130.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   &   |- D e. RR   =>   |- ((A + (B x. i)) = (C + (D x. i)) -> (A = C /\ B = D))
Theorem	crmult 4530	Multiplication rule for complex number representation. Remark of [Apostol] p. 361.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   &   |- D e. RR   =>   |- ((A + (B x. i)) x. (C + (D x. i))) = (((A x. C) - (B x. D)) + (((A x. D) + (B x. C)) x. i))
Theorem	crut 4531	The real representation of complex numbers is unique. Proposition 10-1.3 of [Gleason] p. 130.
|- (((A e. RR /\ B e. RR) /\ (C e. RR /\ D e. RR)) -> ((A + (B x. i)) = (C + (D x. i)) -> (A = C /\ B = D)))
Theorem	creur 4532	The real part of a complex number is unique. Proposition 10-1.3 of [Gleason] p. 130.
|- (A e. CC -> E!x e. RR E.y e. RR A = (x + (y x. i)))
Theorem	creui 4533	The imaginary part of a complex number is unique. Proposition 10-1.3 of [Gleason] p. 130.
|- (A e. CC -> E!y e. RR E.x e. RR A = (x + (y x. i)))
Theorem	rimul 4534	A real number times the imaginary unit is real only if the number is 0.
|- ((A e. RR /\ (A x. i) e. RR) -> A = 0)
Definition	df-n0 4535	Define the set of nonnegative integers.
|- NN0 = (NN u. {0})
Theorem	elnn0 4536	Nonnegative integers expressed in terms of naturals and zero. (Contributed by Raph Levien, 10-Dec-02.)
|- (A e. NN0 <-> (A e. NN \/ A = 0))
Theorem	nnssnn0 4537	Positive naturals are a subset of nonnegative integers. (Contributed by Raph Levien, 10-Dec-02.)
|- NN (_ NN0
Theorem	nn0ssre 4538	Nonnegative integers are a subset of the reals. (Contributed by Raph Levien, 10-Dec-02.)
|- NN0 (_ RR
Theorem	nn0sscn 4539	Nonnegative integers are a subset of the complex numbers.)
|- NN0 (_ CC
Theorem	nn0ex 4540	The set of nonnegative integers exists.
|- NN0 e. V
Theorem	nnnn0t 4541	A natural number is a nonnegative integer.
|- (A e. NN -> A e. NN0)
Theorem	nn0ret 4542	A nonnegative integer is a real number.
|- (A e. NN0 -> A e. RR)
Theorem	nn0cnt 4543	A nonnegative integer is a complex number.
|- (A e. NN0 -> A e. CC)
Theorem	nn0re 4544	A nonnegative integer is a real number.
|- A e. NN0   =>   |- A e. RR
Theorem	nn0cn 4545	A nonnegative integer is a complex number.
|- A e. NN0   =>   |- A e. CC
Theorem	0nn0 4546	0 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-02.)
|- 0 e. NN0
Theorem	1nn0 4547	1 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-02.)
|- 1 e. NN0
Theorem	2nn0 4548	2 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-02.)
|- 2 e. NN0
Theorem	lt0nnn0 4549	No number less than zero is a nonnegative integer.
|- ((A e. RR /\ A < 0) -> -. A e. NN0)
Theorem	nn0ge0t 4550	A nonnegative integer is greater than or equal to zero.
|- (A e. NN0 -> 0 <_ A)
Theorem	nn0addclt 4551	Closure of addition of nonnegative integers. (Contributed by Raph Levien, 10-Dec-02.)
|- ((A e. NN0 /\ B e. NN0) -> (A + B) e. NN0)
Theorem	nn0addcl 4552	Closure of addition of nonnegative integers, inference form. (Contributed by Raph Levien, 10-Dec-02.)
|- A e. NN0   &   |- B e. NN0   =>   |- (A + B) e. NN0
Theorem	nn0mulcl 4553	Closure of multiplication of nonnegative integers, inference form. (Contributed by Raph Levien, 10-Dec-02.)
|- A e. NN0   &   |- B e. NN0   =>   |- (A x. B) e. NN0
Theorem	nn0mulclt 4554	Closure of multiplication of nonnegative integers.
|- ((A e. NN0 /\ B e. NN0) -> (A x. B) e. NN0)
Theorem	peano2nn0 4555	Second Peano postulate for nonnegative integers.
|- (A e. NN0 -> (A + 1) e. NN0)
Theorem	nn0ltp1let 4556	Nonnegative integer ordering relation. (Contributed by Raph Levien, 10-Dec-02.)
|- ((A e. NN0 /\ B e. NN0) -> (A < B <-> (A + 1) <_ B))
Theorem	nn0leltp1t 4557	Nonnegative integer ordering relation. (Contributed by Raph Levien, 10-Apr-04.)
|- ((A e. NN0 /\ B e. NN0) -> (A <_ B <-> A < (B + 1)))
Theorem	nn0ltlem1 4558	Nonnegative integer ordering relation.
|- ((A e. NN0 /\ B e. NN0) -> (A < B <-> A <_ (B - 1)))
Theorem	nn0ge0i 4559	Nonnegative integers are nonnegative. (Contributed by Raph Levien, 10-Dec-02.)
|- A e. NN0   =>   |- 0 <_ A
Theorem	nn0addge1 4560	A nonnegative integer is less than or equal to itself plus another. (Contributed by Raph Levien, 10-Dec-02.)
|- A e. NN0   &   |- B e. NN0   =>   |- A <_ (A + B)
Theorem	nn0addge2 4561	A nonnegative integer is less than or equal to itself plus another. (Contributed by Raph Levien, 10-Dec-02.)
|- A e. NN0   &   |- B e. NN0   =>   |- B <_ (A + B)
Theorem	nn0le2x 4562	A nonnegative integer is less than or equal to twice itself. (Contributed by Raph Levien, 10-Dec-02.)
|- A e. NN0   =>   |- A <_ (2 x. A)
Theorem	nn0lele2x 4563	'Less than or equal to' implies 'less than or equal to twice' for nonnegative integers. (Contributed by Raph Levien, 10-Dec-02.)
|- A e. NN0   &   |- B e. NN0   =>   |- (B <_ A -> B <_ (2 x. A))
Definition	df-z 4564	Define the set of integers. Definition of integers in [Apostol] p. 22.
|- ZZ = {x e. RR | (x = 0 \/ x e. NN \/ -ux e. NN)}
Theorem	elz 4565	Membership in the set of integers.
|- (A e. ZZ <-> (A e. RR /\ (A = 0 \/ A e. NN \/ -uA e. NN)))
Theorem	nnnegz 4566	The negative of a natural number is an integer.
|- (A e. NN -> -uA e. ZZ)
Theorem	zret 4567	An integer is a real.
|- (A e. ZZ -> A e. RR)
Theorem	zcnt 4568	An integer is a complex number.
|- (A e. ZZ -> A e. CC)
Theorem	zssre 4569	The integers are a subset of the reals.
|- ZZ (_ RR
Theorem	zsscn 4570	The integers are a subset of the complex numbers.
|- ZZ (_ CC
Theorem	zex 4571	The set of integers exists.
|- ZZ e. V
Theorem	elnnz 4572	Natural number property expressed in terms of integers.
|- (A e. NN <-> (A e. ZZ /\ 0 < A))
Theorem	0z 4573	Zero is an integer.
|- 0 e. ZZ
Theorem	elnn0z 4574	Nonnegative integer property expressed in terms of integers.
|- (A e. NN0 <-> (A e. ZZ /\ 0 <_ A))
Theorem	elznn0nn 4575	Integer property expressed in terms nonnegative integers and natural numbers.
|- (A e. ZZ <-> (A e. NN0 \/ (A e. RR /\ -uA e. NN)))
Theorem	elznn0 4576	Integer property expressed in terms of nonnegative integers.
|- (A e. ZZ <-> (A e. RR /\ (A e. NN0 \/ -uA e. NN0)))
Theorem	nnssz 4577	Natural numbers are a subset of integers.
|- NN (_ ZZ
Theorem	nn0ssz 4578	Nonnegative integers are a subset of the integers.
|- NN0 (_ <