P. 150 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 14901-15000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	subsin 14901	Difference of sines. (Contributed by Paul Chapman, 12-Oct-2007.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( sin ` A ) - ( sin ` B ) ) = ( 2 x. ( ( cos ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) ) )
Theorem	sinmul 14902	Product of sines can be rewritten as half the difference of certain cosines. This follows from cosadd 14895 and cossub 14899. (Contributed by David A. Wheeler, 26-May-2015.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( sin ` A ) x. ( sin ` B ) ) = ( ( ( cos ` ( A - B ) ) - ( cos ` ( A + B ) ) ) / 2 ) )
Theorem	cosmul 14903	Product of cosines can be rewritten as half the sum of certain cosines. This follows from cosadd 14895 and cossub 14899. (Contributed by David A. Wheeler, 26-May-2015.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( cos ` A ) x. ( cos ` B ) ) = ( ( ( cos ` ( A - B ) ) + ( cos ` ( A + B ) ) ) / 2 ) )
Theorem	addcos 14904	Sum of cosines. (Contributed by Paul Chapman, 12-Oct-2007.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( cos ` A ) + ( cos ` B ) ) = ( 2 x. ( ( cos ` ( ( A + B ) / 2 ) ) x. ( cos ` ( ( A - B ) / 2 ) ) ) ) )
Theorem	subcos 14905	Difference of cosines. (Contributed by Paul Chapman, 12-Oct-2007.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( cos ` B ) - ( cos ` A ) ) = ( 2 x. ( ( sin ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) ) )
Theorem	sincossq 14906	Sine squared plus cosine squared is 1. Equation 17 of [Gleason] p. 311. Note that this holds for non-real arguments, even though individually each term is unbounded. (Contributed by NM, 15-Jan-2006.)
|- ( A e. CC -> ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) = 1 )
Theorem	sin2t 14907	Double-angle formula for sine. (Contributed by Paul Chapman, 17-Jan-2008.)
|- ( A e. CC -> ( sin ` ( 2 x. A ) ) = ( 2 x. ( ( sin ` A ) x. ( cos ` A ) ) ) )
Theorem	cos2t 14908	Double-angle formula for cosine. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( A e. CC -> ( cos ` ( 2 x. A ) ) = ( ( 2 x. ( ( cos ` A ) ^ 2 ) ) - 1 ) )
Theorem	cos2tsin 14909	Double-angle formula for cosine in terms of sine. (Contributed by NM, 12-Sep-2008.)
|- ( A e. CC -> ( cos ` ( 2 x. A ) ) = ( 1 - ( 2 x. ( ( sin ` A ) ^ 2 ) ) ) )
Theorem	sinbnd 14910	The sine of a real number lies between -1 and 1. Equation 18 of [Gleason] p. 311. (Contributed by NM, 16-Jan-2006.)
|- ( A e. RR -> ( -u 1 <_ ( sin ` A ) /\ ( sin ` A ) <_ 1 ) )
Theorem	cosbnd 14911	The cosine of a real number lies between -1 and 1. Equation 18 of [Gleason] p. 311. (Contributed by NM, 16-Jan-2006.)
|- ( A e. RR -> ( -u 1 <_ ( cos ` A ) /\ ( cos ` A ) <_ 1 ) )
Theorem	sinbnd2 14912	The sine of a real number is in the closed interval from -1 to 1. (Contributed by Mario Carneiro, 12-May-2014.)
|- ( A e. RR -> ( sin ` A ) e. ( -u 1 [,] 1 ) )
Theorem	cosbnd2 14913	The cosine of a real number is in the closed interval from -1 to 1. (Contributed by Mario Carneiro, 12-May-2014.)
|- ( A e. RR -> ( cos ` A ) e. ( -u 1 [,] 1 ) )
Theorem	ef01bndlem 14914*	Lemma for sin01bnd 14915 and cos01bnd 14916. (Contributed by Paul Chapman, 19-Jan-2008.)
|- F = ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) )   =>    |- ( A e. ( 0 (,] 1 ) -> ( abs ` sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) < ( ( A ^ 4 ) / 6 ) )
Theorem	sin01bnd 14915	Bounds on the sine of a positive real number less than or equal to 1. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.)
|- ( A e. ( 0 (,] 1 ) -> ( ( A - ( ( A ^ 3 ) / 3 ) ) < ( sin ` A ) /\ ( sin ` A ) < A ) )
Theorem	cos01bnd 14916	Bounds on the cosine of a positive real number less than or equal to 1. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.)
|- ( A e. ( 0 (,] 1 ) -> ( ( 1 - ( 2 x. ( ( A ^ 2 ) / 3 ) ) ) < ( cos ` A ) /\ ( cos ` A ) < ( 1 - ( ( A ^ 2 ) / 3 ) ) ) )
Theorem	cos1bnd 14917	Bounds on the cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.)
|- ( ( 1 / 3 ) < ( cos ` 1 ) /\ ( cos ` 1 ) < ( 2 / 3 ) )
Theorem	cos2bnd 14918	Bounds on the cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008.)
|- ( -u ( 7 / 9 ) < ( cos ` 2 ) /\ ( cos ` 2 ) < -u ( 1 / 9 ) )
Theorem	sinltx 14919	The sine of a positive real number is less than its argument. (Contributed by Mario Carneiro, 29-Jul-2014.)
|- ( A e. RR+ -> ( sin ` A ) < A )
Theorem	sin01gt0 14920	The sine of a positive real number less than or equal to 1 is positive. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Wolf Lammen, 25-Sep-2020.)
|- ( A e. ( 0 (,] 1 ) -> 0 < ( sin ` A ) )
Theorem	cos01gt0 14921	The cosine of a positive real number less than or equal to 1 is positive. (Contributed by Paul Chapman, 19-Jan-2008.)
|- ( A e. ( 0 (,] 1 ) -> 0 < ( cos ` A ) )
Theorem	sin02gt0 14922	The sine of a positive real number less than or equal to 2 is positive. (Contributed by Paul Chapman, 19-Jan-2008.)
|- ( A e. ( 0 (,] 2 ) -> 0 < ( sin ` A ) )
Theorem	sincos1sgn 14923	The signs of the sine and cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.)
|- ( 0 < ( sin ` 1 ) /\ 0 < ( cos ` 1 ) )
Theorem	sincos2sgn 14924	The signs of the sine and cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008.)
|- ( 0 < ( sin ` 2 ) /\ ( cos ` 2 ) < 0 )
Theorem	sin4lt0 14925	The sine of 4 is negative. (Contributed by Paul Chapman, 19-Jan-2008.)
|- ( sin ` 4 ) < 0
Theorem	absefi 14926	The absolute value of the exponential function of an imaginary number is one. Equation 48 of [Rudin] p. 167. (Contributed by Jason Orendorff, 9-Feb-2007.)
|- ( A e. RR -> ( abs ` ( exp ` ( _i x. A ) ) ) = 1 )
Theorem	absef 14927	The absolute value of the exponential function is the exponential function of the real part. (Contributed by Paul Chapman, 13-Sep-2007.)
|- ( A e. CC -> ( abs ` ( exp ` A ) ) = ( exp ` ( Re ` A ) ) )
Theorem	absefib 14928	A number is real iff its imaginary exponential has absolute value one. (Contributed by NM, 21-Aug-2008.)
|- ( A e. CC -> ( A e. RR <-> ( abs ` ( exp ` ( _i x. A ) ) ) = 1 ) )
Theorem	efieq1re 14929	A number whose imaginary exponential is one is real. (Contributed by NM, 21-Aug-2008.)
|- ( ( A e. CC /\ ( exp ` ( _i x. A ) ) = 1 ) -> A e. RR )
Theorem	demoivre 14930	De Moivre's Formula. Proof by induction given at http://en.wikipedia.org/wiki/De_Moivre's_formula, but restricted to nonnegative integer powers. See also demoivreALT 14931 for an alternate longer proof not using the exponential function. (Contributed by NM, 24-Jul-2007.)
|- ( ( A e. CC /\ N e. ZZ ) -> ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) ^ N ) = ( ( cos ` ( N x. A ) ) + ( _i x. ( sin ` ( N x. A ) ) ) ) )
Theorem	demoivreALT 14931	Alternate proof of demoivre 14930. It is longer but does not use the exponential function. This is Metamath 100 proof #17. (Contributed by Steve Rodriguez, 10-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( A e. CC /\ N e. NN0 ) -> ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) ^ N ) = ( ( cos ` ( N x. A ) ) + ( _i x. ( sin ` ( N x. A ) ) ) ) )
5.11.2  _e is irrational
Theorem	eirrlem 14932*	Lemma for eirr 14933. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 29-Apr-2014.)
|- F = ( n e. NN0 |-> ( 1 / ( ! ` n ) ) )   &    |- ( ph -> P e. ZZ )   &    |- ( ph -> Q e. NN )   &    |- ( ph -> _e = ( P / Q ) )   =>    |- -. ph
Theorem	eirr 14933	_e is irrational. (Contributed by Paul Chapman, 9-Feb-2008.) (Proof shortened by Mario Carneiro, 29-Apr-2014.)
|- _e e/ QQ
Theorem	egt2lt3 14934	Euler's constant _e = 2.71828... is bounded by 2 and 3. (Contributed by NM, 28-Nov-2008.) (Revised by Mario Carneiro, 29-Apr-2014.)
|- ( 2 < _e /\ _e < 3 )
Theorem	epos 14935	Euler's constant _e is greater than 0. (Contributed by Jeff Hankins, 22-Nov-2008.)
|- 0 < _e
Theorem	epr 14936	Euler's constant _e is a positive real. (Contributed by Jeff Hankins, 22-Nov-2008.)
|- _e e. RR+
Theorem	ene0 14937	_e is not 0. (Contributed by David A. Wheeler, 17-Oct-2017.)
|- _e =/= 0
Theorem	ene1 14938	_e is not 1. (Contributed by David A. Wheeler, 17-Oct-2017.)
|- _e =/= 1
5.12  Cardinality of real and complex number subsets
5.12.1  Countability of integers and rationals
Theorem	xpnnen 14939	The Cartesian product of the set of positive integers with itself is equinumerous to the set of positive integers. (Contributed by NM, 1-Aug-2004.) (Revised by Mario Carneiro, 9-Mar-2013.)
|- ( NN X. NN ) ~~ NN
Theorem	znnenlem 14940	Lemma for znnen 14941. (Contributed by NM, 31-Jul-2004.)
|- ( ( ( 0 <_ x /\ -. 0 <_ y ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( x = y <-> ( 2 x. x ) = ( ( -u 2 x. y ) + 1 ) ) )
Theorem	znnen 14941	The set of integers and the set of positive integers are equinumerous. Exercise 1 of [Gleason] p. 140. (Contributed by NM, 31-Jul-2004.) (Proof shortened by Mario Carneiro, 13-Jun-2014.)
|- ZZ ~~ NN
Theorem	qnnen 14942	The rational numbers are countable. This proof does not use the Axiom of Choice, even though it uses an onto function, because the base set ( ZZ X. NN ) is numerable. Exercise 2 of [Enderton] p. 133. For purposes of the Metamath 100 list, we are considering Mario Carneiro's revision as the date this proof was completed. This is Metamath 100 proof #3. (Contributed by NM, 31-Jul-2004.) (Revised by Mario Carneiro, 3-Mar-2013.)
|- QQ ~~ NN
5.12.2  The reals are uncountable
Theorem	rpnnen2lem1 14943*	Lemma for rpnnen2 14955. (Contributed by Mario Carneiro, 13-May-2013.)
|- F = ( x e. ~P NN |-> ( n e. NN |-> if ( n e. x , ( ( 1 / 3 ) ^ n ) , 0 ) ) )   =>    |- ( ( A C_ NN /\ N e. NN ) -> ( ( F ` A ) ` N ) = if ( N e. A , ( ( 1 / 3 ) ^ N ) , 0 ) )
Theorem	rpnnen2lem2 14944*	Lemma for rpnnen2 14955. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- F = ( x e. ~P NN |-> ( n e. NN |-> if ( n e. x , ( ( 1 / 3 ) ^ n ) , 0 ) ) )   =>    |- ( A C_ NN -> ( F ` A ) : NN --> RR )
Theorem	rpnnen2lem3 14945*	Lemma for rpnnen2 14955. (Contributed by Mario Carneiro, 13-May-2013.)
|- F = ( x e. ~P NN |-> ( n e. NN |-> if ( n e. x , ( ( 1 / 3 ) ^ n ) , 0 ) ) )   =>    |- seq 1 ( + , ( F ` NN ) ) ~~> ( 1 / 2 )
Theorem	rpnnen2lem4 14946*	Lemma for rpnnen2 14955. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 31-Aug-2014.)
|- F = ( x e. ~P NN |-> ( n e. NN |-> if ( n e. x , ( ( 1 / 3 ) ^ n ) , 0 ) ) )   =>    |- ( ( A C_ B /\ B C_ NN /\ k e. NN ) -> ( 0 <_ ( ( F ` A ) ` k ) /\ ( ( F ` A ) ` k ) <_ ( ( F ` B ) ` k ) ) )
Theorem	rpnnen2lem5 14947*	Lemma for rpnnen2 14955. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.)
|- F = ( x e. ~P NN |-> ( n e. NN |-> if ( n e. x , ( ( 1 / 3 ) ^ n ) , 0 ) ) )   =>    |- ( ( A C_ NN /\ M e. NN ) -> seq M ( + , ( F ` A ) ) e. dom ~~> )
Theorem	rpnnen2lem6 14948*	Lemma for rpnnen2 14955. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.)
|- F = ( x e. ~P NN |-> ( n e. NN |-> if ( n e. x , ( ( 1 / 3 ) ^ n ) , 0 ) ) )   =>    |- ( ( A C_ NN /\ M e. NN ) -> sum_ k e. ( ZZ>= ` M ) ( ( F ` A ) ` k ) e. RR )
Theorem	rpnnen2lem7 14949*	Lemma for rpnnen2 14955. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.)
|- F = ( x e. ~P NN |-> ( n e. NN |-> if ( n e. x , ( ( 1 / 3 ) ^ n ) , 0 ) ) )   =>    |- ( ( A C_ B /\ B C_ NN /\ M e. NN ) -> sum_ k e. ( ZZ>= ` M ) ( ( F ` A ) ` k ) <_ sum_ k e. ( ZZ>= ` M ) ( ( F ` B ) ` k ) )
Theorem	rpnnen2lem8 14950*	Lemma for rpnnen2 14955. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.)
|- F = ( x e. ~P NN |-> ( n e. NN |-> if ( n e. x , ( ( 1 / 3 ) ^ n ) , 0 ) ) )   =>    |- ( ( A C_ NN /\ M e. NN ) -> sum_ k e. NN ( ( F ` A ) ` k ) = ( sum_ k e. ( 1 ... ( M - 1 ) ) ( ( F ` A ) ` k ) + sum_ k e. ( ZZ>= ` M ) ( ( F ` A ) ` k ) ) )
Theorem	rpnnen2lem9 14951*	Lemma for rpnnen2 14955. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.)
|- F = ( x e. ~P NN |-> ( n e. NN |-> if ( n e. x , ( ( 1 / 3 ) ^ n ) , 0 ) ) )   =>    |- ( M e. NN -> sum_ k e. ( ZZ>= ` M ) ( ( F ` ( NN \ { M } ) ) ` k ) = ( 0 + ( ( ( 1 / 3 ) ^ ( M + 1 ) ) / ( 1 - ( 1 / 3 ) ) ) ) )
Theorem	rpnnen2lem10 14952*	Lemma for rpnnen2 14955. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.)
|- F = ( x e. ~P NN |-> ( n e. NN |-> if ( n e. x , ( ( 1 / 3 ) ^ n ) , 0 ) ) )   &    |- ( ph -> A C_ NN )   &    |- ( ph -> B C_ NN )   &    |- ( ph -> m e. ( A \ B ) )   &    |- ( ph -> A. n e. NN ( n < m -> ( n e. A <-> n e. B ) ) )   &    |- ( ps <-> sum_ k e. NN ( ( F ` A ) ` k ) = sum_ k e. NN ( ( F ` B ) ` k ) )   =>    |- ( ( ph /\ ps ) -> sum_ k e. ( ZZ>= ` m ) ( ( F ` A ) ` k ) = sum_ k e. ( ZZ>= ` m ) ( ( F ` B ) ` k ) )
Theorem	rpnnen2lem11 14953*	Lemma for rpnnen2 14955. (Contributed by Mario Carneiro, 13-May-2013.)
|- F = ( x e. ~P NN |-> ( n e. NN |-> if ( n e. x , ( ( 1 / 3 ) ^ n ) , 0 ) ) )   &    |- ( ph -> A C_ NN )   &    |- ( ph -> B C_ NN )   &    |- ( ph -> m e. ( A \ B ) )   &    |- ( ph -> A. n e. NN ( n < m -> ( n e. A <-> n e. B ) ) )   &    |- ( ps <-> sum_ k e. NN ( ( F ` A ) ` k ) = sum_ k e. NN ( ( F ` B ) ` k ) )   =>    |- ( ph -> -. ps )
Theorem	rpnnen2lem12 14954*	Lemma for rpnnen2 14955. (Contributed by Mario Carneiro, 13-May-2013.)
|- F = ( x e. ~P NN |-> ( n e. NN |-> if ( n e. x , ( ( 1 / 3 ) ^ n ) , 0 ) ) )   =>    |- ~P NN ~<_ ( 0 [,] 1 )
Theorem	rpnnen2 14955	The other half of rpnnen 14956, where we show an injection from sets of positive integers to real numbers. The obvious choice for this is binary expansion, but it has the unfortunate property that it does not produce an injection on numbers which end with all 0's or all 1's (the more well-known decimal version of this is 0.999... 14612). Instead, we opt for a ternary expansion, which produces (a scaled version of) the Cantor set. Since the Cantor set is riddled with gaps, we can show that any two sequences that are not equal must differ somewhere, and when they do, they are placed a finite distance apart, thus ensuring that the map is injective. Our map assigns to each subset A of the positive integers the number sum_ k e. A ( 3 ^ -u k ) = sum_ k e. NN ( ( F ` A ) ` k ), where ( ( F ` A ) ` k ) = if ( k e. A , ( 3 ^ -u k ) , 0 ) ) (rpnnen2lem1 14943). This is an infinite sum of real numbers (rpnnen2lem2 14944), and since A C_ B implies ( F ` A ) <_ ( F ` B ) (rpnnen2lem4 14946) and ( F ` NN ) converges to 1 / 2 (rpnnen2lem3 14945) by geoisum1 14610, the sum is convergent to some real (rpnnen2lem5 14947 and rpnnen2lem6 14948) by the comparison test for convergence cvgcmp 14548. The comparison test also tells us that A C_ B implies sum_ ( F ` A ) <_ sum_ ( F ` B ) (rpnnen2lem7 14949). Putting it all together, if we have two sets x =/= y, there must differ somewhere, and so there must be an m such that A. n < m ( n e. x <-> n e. y ) but m e. ( x \ y ) or vice versa. In this case, we split off the first m - 1 terms (rpnnen2lem8 14950) and cancel them (rpnnen2lem10 14952), since these are the same for both sets. For the remaining terms, we use the subset property to establish that sum_ ( F ` y ) <_ sum_ ( F ` ( NN \ { m } ) ) and sum_ ( F ` { m } ) <_ sum_ ( F ` x ) (where these sums are only over ( ZZ>= ` m )), and since sum_ ( F ` ( NN \ { m } ) ) = ( 3 ^ -u m ) / 2 (rpnnen2lem9 14951) and sum_ ( F ` { m } ) = ( 3 ^ -u m ), we establish that sum_ ( F ` y ) < sum_ ( F ` x ) (rpnnen2lem11 14953) so that they must be different. By contraposition (rpnnen2lem12 14954), we find that this map is an injection. (Contributed by Mario Carneiro, 13-May-2013.) (Proof shortened by Mario Carneiro, 30-Apr-2014.) (Revised by NM, 17-Aug-2021.)
|- ~P NN ~<_ ( 0 [,] 1 )
Theorem	rpnnen 14956	The cardinality of the continuum is the same as the powerset of om. This is a stronger statement than ruc 14972, which only asserts that RR is uncountable, i.e. has a cardinality larger than om. The main proof is in two parts, rpnnen1 11820 and rpnnen2 14955, each showing an injection in one direction, and this last part uses sbth 8080 to prove that the sets are equinumerous. By constructing explicit injections, we avoid the use of AC. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- RR ~~ ~P NN
Theorem	rexpen 14957	The real numbers are equinumerous to their own Cartesian product, even though it is not necessarily true that RR is well-orderable (so we cannot use infxpidm2 8840 directly). (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 16-Jun-2013.)
|- ( RR X. RR ) ~~ RR
Theorem	cpnnen 14958	The complex numbers are equinumerous to the powerset of the positive integers. (Contributed by Mario Carneiro, 16-Jun-2013.)
|- CC ~~ ~P NN
Theorem	rucALT 14959	Alternate proof of ruc 14972. This proof is a simple corollary of rpnnen 14956, which determines the exact cardinality of the reals. For an alternate proof discussed at mmcomplex.html#uncountable, see ruc 14972. (Contributed by NM, 13-Oct-2004.) (Revised by Mario Carneiro, 13-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
|- NN ~< RR
Theorem	ruclem1 14960*	Lemma for ruc 14972 (the reals are uncountable). Substitutions for the function D. (Contributed by Mario Carneiro, 28-May-2014.) (Revised by Fan Zheng, 6-Jun-2016.)
|- ( ph -> F : NN --> RR )   &    |- ( ph -> D = ( x e. ( RR X. RR ) , y e. RR |-> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> M e. RR )   &    |- X = ( 1st ` ( <. A , B >. D M ) )   &    |- Y = ( 2nd ` ( <. A , B >. D M ) )   =>    |- ( ph -> ( ( <. A , B >. D M ) e. ( RR X. RR ) /\ X = if ( ( ( A + B ) / 2 ) < M , A , ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) /\ Y = if ( ( ( A + B ) / 2 ) < M , ( ( A + B ) / 2 ) , B ) ) )
Theorem	ruclem2 14961*	Lemma for ruc 14972. Ordering property for the input to D. (Contributed by Mario Carneiro, 28-May-2014.)
|- ( ph -> F : NN --> RR )   &    |- ( ph -> D = ( x e. ( RR X. RR ) , y e. RR |-> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> M e. RR )   &    |- X = ( 1st ` ( <. A , B >. D M ) )   &    |- Y = ( 2nd ` ( <. A , B >. D M ) )   &    |- ( ph -> A < B )   =>    |- ( ph -> ( A <_ X /\ X < Y /\ Y <_ B ) )
Theorem	ruclem3 14962*	Lemma for ruc 14972. The constructed interval [ X , Y ] always excludes M. (Contributed by Mario Carneiro, 28-May-2014.)
|- ( ph -> F : NN --> RR )   &    |- ( ph -> D = ( x e. ( RR X. RR ) , y e. RR |-> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> M e. RR )   &    |- X = ( 1st ` ( <. A , B >. D M ) )   &    |- Y = ( 2nd ` ( <. A , B >. D M ) )   &    |- ( ph -> A < B )   =>    |- ( ph -> ( M < X \/ Y < M ) )
Theorem	ruclem4 14963*	Lemma for ruc 14972. Initial value of the interval sequence. (Contributed by Mario Carneiro, 28-May-2014.)
|- ( ph -> F : NN --> RR )   &    |- ( ph -> D = ( x e. ( RR X. RR ) , y e. RR |-> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) ) )   &    |- C = ( { <. 0 , <. 0 , 1 >. >. } u. F )   &    |- G = seq 0 ( D , C )   =>    |- ( ph -> ( G ` 0 ) = <. 0 , 1 >. )
Theorem	ruclem6 14964*	Lemma for ruc 14972. Domain and range of the interval sequence. (Contributed by Mario Carneiro, 28-May-2014.)
|- ( ph -> F : NN --> RR )   &    |- ( ph -> D = ( x e. ( RR X. RR ) , y e. RR |-> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) ) )   &    |- C = ( { <. 0 , <. 0 , 1 >. >. } u. F )   &    |- G = seq 0 ( D , C )   =>    |- ( ph -> G : NN0 --> ( RR X. RR ) )
Theorem	ruclem7 14965*	Lemma for ruc 14972. Successor value for the interval sequence. (Contributed by Mario Carneiro, 28-May-2014.)
|- ( ph -> F : NN --> RR )   &    |- ( ph -> D = ( x e. ( RR X. RR ) , y e. RR |-> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) ) )   &    |- C = ( { <. 0 , <. 0 , 1 >. >. } u. F )   &    |- G = seq 0 ( D , C )   =>    |- ( ( ph /\ N e. NN0 ) -> ( G ` ( N + 1 ) ) = ( ( G ` N ) D ( F ` ( N + 1 ) ) ) )
Theorem	ruclem8 14966*	Lemma for ruc 14972. The intervals of the G sequence are all nonempty. (Contributed by Mario Carneiro, 28-May-2014.)
|- ( ph -> F : NN --> RR )   &    |- ( ph -> D = ( x e. ( RR X. RR ) , y e. RR |-> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) ) )   &    |- C = ( { <. 0 , <. 0 , 1 >. >. } u. F )   &    |- G = seq 0 ( D , C )   =>    |- ( ( ph /\ N e. NN0 ) -> ( 1st ` ( G ` N ) ) < ( 2nd ` ( G ` N ) ) )
Theorem	ruclem9 14967*	Lemma for ruc 14972. The first components of the G sequence are increasing, and the second components are decreasing. (Contributed by Mario Carneiro, 28-May-2014.)
|- ( ph -> F : NN --> RR )   &    |- ( ph -> D = ( x e. ( RR X. RR ) , y e. RR |-> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) ) )   &    |- C = ( { <. 0 , <. 0 , 1 >. >. } u. F )   &    |- G = seq 0 ( D , C )   &    |- ( ph -> M e. NN0 )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   =>    |- ( ph -> ( ( 1st ` ( G ` M ) ) <_ ( 1st ` ( G ` N ) ) /\ ( 2nd ` ( G ` N ) ) <_ ( 2nd ` ( G ` M ) ) ) )
Theorem	ruclem10 14968*	Lemma for ruc 14972. Every first component of the G sequence is less than every second component. That is, the sequences form a chain a1 < a2 <... < b2 < b1, where ai are the first components and bi are the second components. (Contributed by Mario Carneiro, 28-May-2014.)
|- ( ph -> F : NN --> RR )   &    |- ( ph -> D = ( x e. ( RR X. RR ) , y e. RR |-> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) ) )   &    |- C = ( { <. 0 , <. 0 , 1 >. >. } u. F )   &    |- G = seq 0 ( D , C )   &    |- ( ph -> M e. NN0 )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( 1st ` ( G ` M ) ) < ( 2nd ` ( G ` N ) ) )
Theorem	ruclem11 14969*	Lemma for ruc 14972. Closure lemmas for supremum. (Contributed by Mario Carneiro, 28-May-2014.)
|- ( ph -> F : NN --> RR )   &    |- ( ph -> D = ( x e. ( RR X. RR ) , y e. RR |-> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) ) )   &    |- C = ( { <. 0 , <. 0 , 1 >. >. } u. F )   &    |- G = seq 0 ( D , C )   =>    |- ( ph -> ( ran ( 1st o. G ) C_ RR /\ ran ( 1st o. G ) =/= (/) /\ A. z e. ran ( 1st o. G ) z <_ 1 ) )
Theorem	ruclem12 14970*	Lemma for ruc 14972. The supremum of the increasing sequence 1st o. G is a real number that is not in the range of F. (Contributed by Mario Carneiro, 28-May-2014.)
|- ( ph -> F : NN --> RR )   &    |- ( ph -> D = ( x e. ( RR X. RR ) , y e. RR |-> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) ) )   &    |- C = ( { <. 0 , <. 0 , 1 >. >. } u. F )   &    |- G = seq 0 ( D , C )   &    |- S = sup ( ran ( 1st o. G ) , RR , < )   =>    |- ( ph -> S e. ( RR \ ran F ) )
Theorem	ruclem13 14971	Lemma for ruc 14972. There is no function that maps NN onto RR. (Use nex 1731 if you want this in the form -. E. f f : NN -onto-> RR.) (Contributed by NM, 14-Oct-2004.) (Proof shortened by Fan Zheng, 6-Jun-2016.)
|- -. F : NN -onto-> RR
Theorem	ruc 14972	The set of positive integers is strictly dominated by the set of real numbers, i.e. the real numbers are uncountable. The proof consists of lemmas ruclem1 14960 through ruclem13 14971 and this final piece. Our proof is based on the proof of Theorem 5.18 of [Truss] p. 114. See ruclem13 14971 for the function existence version of this theorem. For an informal discussion of this proof, see mmcomplex.html#uncountable. For an alternate proof see rucALT 14959. This is Metamath 100 proof #22. (Contributed by NM, 13-Oct-2004.)
|- NN ~< RR
Theorem	resdomq 14973	The set of rationals is strictly less equinumerous than the set of reals ( RR strictly dominates QQ). (Contributed by NM, 18-Dec-2004.)
|- QQ ~< RR
Theorem	aleph1re 14974	There are at least aleph-one real numbers. (Contributed by NM, 2-Feb-2005.)
|- ( aleph ` 1o ) ~<_ RR
Theorem	aleph1irr 14975	There are at least aleph-one irrationals. (Contributed by NM, 2-Feb-2005.)
|- ( aleph ` 1o ) ~<_ ( RR \ QQ )
Theorem	cnso 14976	The complex numbers can be linearly ordered. (Contributed by Stefan O'Rear, 16-Nov-2014.)
|- E. x x Or CC
PART 6  ELEMENTARY NUMBER THEORY Here we introduce elementary number theory, in particular the elementary properties of divisibility and elementary prime number theory.
6.1  Elementary properties of divisibility
6.1.1  Irrationality of square root of 2
Theorem	sqrt2irrlem 14977	Lemma for sqrt2irr 14979. This is the core of the proof: if A / B = sqr ( 2 ), then A and B are even, so A / 2 and B / 2 are smaller representatives, which is absurd by the method of infinite descent (here implemented by strong induction). This is Metamath 100 proof #1. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 12-Sep-2015.) (Proof shortened by JV, 4-Jan-2022.)
|- ( ph -> A e. ZZ )   &    |- ( ph -> B e. NN )   &    |- ( ph -> ( sqr ` 2 ) = ( A / B ) )   =>    |- ( ph -> ( ( A / 2 ) e. ZZ /\ ( B / 2 ) e. NN ) )
Theorem	sqrt2irrlemOLD 14978	Obsolete proof of sqrt2irrlem 14977 as of 4-Jan-2022. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 12-Sep-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> A e. ZZ )   &    |- ( ph -> B e. NN )   &    |- ( ph -> ( sqr ` 2 ) = ( A / B ) )   =>    |- ( ph -> ( ( A / 2 ) e. ZZ /\ ( B / 2 ) e. NN ) )
Theorem	sqrt2irr 14979	The square root of 2 is irrational. See zsqrtelqelz 15466 for a generalization to all non-square integers. The proof's core is proven in sqrt2irrlem 14977, which shows that if A / B = sqr ( 2 ), then A and B are even, so A / 2 and B / 2 are smaller representatives, which is absurd. An older version of this proof was included in The Seventeen Provers of the World compiled by Freek Wiedijk. It is also the first of the "top 100" mathematical theorems whose formalization is tracked by Freek Wiedijk on his Formalizing 100 Theorems page at http://www.cs.ru.nl/~freek/100/. (Contributed by NM, 8-Jan-2002.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
|- ( sqr ` 2 ) e/ QQ
Theorem	sqrt2re 14980	The square root of 2 exists and is a real number. (Contributed by NM, 3-Dec-2004.)
|- ( sqr ` 2 ) e. RR
6.1.2  Some Number sets are chains of proper subsets
Theorem	nthruc 14981	The sequence NN, ZZ, QQ, RR, and CC forms a chain of proper subsets. In each case the proper subset relationship is shown by demonstrating a number that belongs to one set but not the other. We show that zero belongs to ZZ but not NN, one-half belongs to QQ but not ZZ, the square root of 2 belongs to RR but not QQ, and finally that the imaginary number _i belongs to CC but not RR. See nthruz 14982 for a further refinement. (Contributed by NM, 12-Jan-2002.)
|- ( ( NN C. ZZ /\ ZZ C. QQ ) /\ ( QQ C. RR /\ RR C. CC ) )
Theorem	nthruz 14982	The sequence NN, NN0, and ZZ forms a chain of proper subsets. In each case the proper subset relationship is shown by demonstrating a number that belongs to one set but not the other. We show that zero belongs to NN0 but not NN and minus one belongs to ZZ but not NN0. This theorem refines the chain of proper subsets nthruc 14981. (Contributed by NM, 9-May-2004.)
|- ( NN C. NN0 /\ NN0 C. ZZ )
6.1.3  The divides relation
Syntax	cdvds 14983	Extend the definition of a class to include the divides relation. See df-dvds 14984.
class ||
Definition	df-dvds 14984*	Define the divides relation, see definition in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.)
|- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
Theorem	divides 14985*	Define the divides relation. M || N means M divides into N with no remainder. For example, 3 || 6 (ex-dvds 27313). As proven in dvdsval3 14987, M || N <-> ( N mod M ) = 0. See divides 14985 and dvdsval2 14986 for other equivalent expressions. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> E. n e. ZZ ( n x. M ) = N ) )
Theorem	dvdsval2 14986	One nonzero integer divides another integer if and only if their quotient is an integer. (Contributed by Jeff Hankins, 29-Sep-2013.)
|- ( ( M e. ZZ /\ M =/= 0 /\ N e. ZZ ) -> ( M || N <-> ( N / M ) e. ZZ ) )
Theorem	dvdsval3 14987	One nonzero integer divides another integer if and only if the remainder upon division is zero, see remark in [ApostolNT] p. 106. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 15-Jul-2014.)
|- ( ( M e. NN /\ N e. ZZ ) -> ( M || N <-> ( N mod M ) = 0 ) )
Theorem	dvdszrcl 14988	Reverse closure for the divisibility relation. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- ( X || Y -> ( X e. ZZ /\ Y e. ZZ ) )
Theorem	nndivdvds 14989	Strong form of dvdsval2 14986 for positive integers. (Contributed by Stefan O'Rear, 13-Sep-2014.)
|- ( ( A e. NN /\ B e. NN ) -> ( B || A <-> ( A / B ) e. NN ) )
Theorem	nndivides 14990*	Definition of the divides relation for positive integers. (Contributed by AV, 26-Jul-2021.)
|- ( ( M e. NN /\ N e. NN ) -> ( M || N <-> E. n e. NN ( n x. M ) = N ) )
Theorem	moddvds 14991	Two ways to say A == B (mod N), see also definition in [ApostolNT] p. 106. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- ( ( N e. NN /\ A e. ZZ /\ B e. ZZ ) -> ( ( A mod N ) = ( B mod N ) <-> N || ( A - B ) ) )
Theorem	dvds0lem 14992	A lemma to assist theorems of || with no antecedents. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K x. M ) = N ) -> M || N )
Theorem	dvds1lem 14993*	A lemma to assist theorems of || with one antecedent. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ph -> ( J e. ZZ /\ K e. ZZ ) )   &    |- ( ph -> ( M e. ZZ /\ N e. ZZ ) )   &    |- ( ( ph /\ x e. ZZ ) -> Z e. ZZ )   &    |- ( ( ph /\ x e. ZZ ) -> ( ( x x. J ) = K -> ( Z x. M ) = N ) )   =>    |- ( ph -> ( J || K -> M || N ) )
Theorem	dvds2lem 14994*	A lemma to assist theorems of || with two antecedents. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ph -> ( I e. ZZ /\ J e. ZZ ) )   &    |- ( ph -> ( K e. ZZ /\ L e. ZZ ) )   &    |- ( ph -> ( M e. ZZ /\ N e. ZZ ) )   &    |- ( ( ph /\ ( x e. ZZ /\ y e. ZZ ) ) -> Z e. ZZ )   &    |- ( ( ph /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( ( x x. I ) = J /\ ( y x. K ) = L ) -> ( Z x. M ) = N ) )   =>    |- ( ph -> ( ( I || J /\ K || L ) -> M || N ) )
Theorem	iddvds 14995	An integer divides itself. Theorem 1.1(a) in [ApostolNT] p. 14 (reflexive property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( N e. ZZ -> N || N )
Theorem	1dvds 14996	1 divides any integer. Theorem 1.1(f) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( N e. ZZ -> 1 || N )
Theorem	dvds0 14997	Any integer divides 0. Theorem 1.1(g) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( N e. ZZ -> N || 0 )
Theorem	negdvdsb 14998	An integer divides another iff its negation does. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> -u M || N ) )
Theorem	dvdsnegb 14999	An integer divides another iff it divides its negation. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> M || -u N ) )
Theorem	absdvdsb 15000	An integer divides another iff its absolute value does. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> ( abs ` M ) || N ) )