P. 363 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36201-36300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	frege105 36201	Proposition 105 of [Frege1879] p. 73. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)
|- Z e. V   =>    |- ( ( -. X ( t+ ` R ) Z -> Z = X ) -> X ( ( t+ ` R ) u. _I ) Z )
Theorem	frege106 36202	Whatever follows X in the R-sequence belongs to the R -sequence beginning with X. Proposition 106 of [Frege1879] p. 73. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)
|- Z e. V   =>    |- ( X ( t+ ` R ) Z -> X ( ( t+ ` R ) u. _I ) Z )
Theorem	frege107 36203	Proposition 107 of [Frege1879] p. 74. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)
|- V e. A   =>    |- ( ( Z ( ( t+ ` R ) u. _I ) Y -> ( Y R V -> Z ( t+ ` R ) V ) ) -> ( Z ( ( t+ ` R ) u. _I ) Y -> ( Y R V -> Z ( ( t+ ` R ) u. _I ) V ) ) )
Theorem	frege108 36204	If Y belongs to the R-sequence beginning with Z, then every result of an application of the procedure R to Y belongs to the R-sequence beginning with Z. Proposition 108 of [Frege1879] p. 74. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)
|- Z e. A   &    |- Y e. B   &    |- V e. C   &    |- R e. D   =>    |- ( Z ( ( t+ ` R ) u. _I ) Y -> ( Y R V -> Z ( ( t+ ` R ) u. _I ) V ) )
Theorem	frege109 36205	The property of belonging to the R-sequence beginning with X is hereditary in the R-sequence. Proposition 109 of [Frege1879] p. 74. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- R e. V   =>    |- R hereditary ( ( ( t+ ` R ) u. _I ) " { X } )
Theorem	frege110 36206*	Proposition 110 of [Frege1879] p. 75. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)
|- X e. A   &    |- Y e. B   &    |- M e. C   &    |- R e. D   =>    |- ( A. a ( Y R a -> X ( ( t+ ` R ) u. _I ) a ) -> ( Y ( t+ ` R ) M -> X ( ( t+ ` R ) u. _I ) M ) )
Theorem	frege111 36207	If Y belongs to the R-sequence beginning with Z, then every result of an application of the procedure R to Y belongs to the R-sequence beginning with Z or precedes Z in the R-sequence. Proposition 111 of [Frege1879] p. 75. (Contributed by RP, 7-Jul-2020.) (Revised by RP, 8-Jul-2020.) (Proof modification is discouraged.)
|- Z e. A   &    |- Y e. B   &    |- V e. C   &    |- R e. D   =>    |- ( Z ( ( t+ ` R ) u. _I ) Y -> ( Y R V -> ( -. V ( t+ ` R ) Z -> Z ( ( t+ ` R ) u. _I ) V ) ) )
Theorem	frege112 36208	Identity implies belonging to the R-sequence beginning with self. Proposition 112 of [Frege1879] p. 76. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)
|- Z e. V   =>    |- ( Z = X -> X ( ( t+ ` R ) u. _I ) Z )
Theorem	frege113 36209	Proposition 113 of [Frege1879] p. 76. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)
|- Z e. V   =>    |- ( ( Z ( ( t+ ` R ) u. _I ) X -> ( -. Z ( t+ ` R ) X -> Z = X ) ) -> ( Z ( ( t+ ` R ) u. _I ) X -> ( -. Z ( t+ ` R ) X -> X ( ( t+ ` R ) u. _I ) Z ) ) )
Theorem	frege114 36210	If X belongs to the R-sequence beginning with Z, then Z belongs to the R-sequence beginning with X or X follows Z in the R-sequence. Proposition 114 of [Frege1879] p. 76. (Contributed by RP, 7-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Z e. V   =>    |- ( Z ( ( t+ ` R ) u. _I ) X -> ( -. Z ( t+ ` R ) X -> X ( ( t+ ` R ) u. _I ) Z ) )
21.25.3.11  _Begriffsschrift_ Chapter III Single-valued procedures Fun `' `' R means the relationship content of procedure R is single-valued. The double converse allows us to simply apply this syntax in place of Frege's even though the original never explicitly limited discussion of propositional statments which vary on two variables to relations. dffrege115 36211 through frege133 36229 develop this and how functions relate to transitive and transitive-reflexive closures.
Theorem	dffrege115 36211*	If from the the circumstance that c is a result of an application of the procedure R to b, whatever b may be, it can be inferred that every result of an application of the procedure R to b is the same as c, then we say : "The procedure R is single-valued". Definition 115 of [Frege1879] p. 77. (Contributed by RP, 7-Jul-2020.)
|- ( A. c A. b ( b R c -> A. a ( b R a -> a = c ) ) <-> Fun `' `' R )
Theorem	frege116 36212*	One direction of dffrege115 36211. Proposition 116 of [Frege1879] p. 77. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   =>    |- ( Fun `' `' R -> A. b ( b R X -> A. a ( b R a -> a = X ) ) )
Theorem	frege117 36213*	Lemma for frege118 36214. Proposition 117 of [Frege1879] p. 78. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   =>    |- ( ( A. b ( b R X -> A. a ( b R a -> a = X ) ) -> ( Y R X -> A. a ( Y R a -> a = X ) ) ) -> ( Fun `' `' R -> ( Y R X -> A. a ( Y R a -> a = X ) ) ) )
Theorem	frege118 36214*	Simplified application of one direction of dffrege115 36211. Proposition 118 of [Frege1879] p. 78. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   =>    |- ( Fun `' `' R -> ( Y R X -> A. a ( Y R a -> a = X ) ) )
Theorem	frege119 36215*	Lemma for frege120 36216. Proposition 119 of [Frege1879] p. 78. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   =>    |- ( ( A. a ( Y R a -> a = X ) -> ( Y R A -> A = X ) ) -> ( Fun `' `' R -> ( Y R X -> ( Y R A -> A = X ) ) ) )
Theorem	frege120 36216	Simplified application of one direction of dffrege115 36211. Proposition 120 of [Frege1879] p. 78. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- A e. W   =>    |- ( Fun `' `' R -> ( Y R X -> ( Y R A -> A = X ) ) )
Theorem	frege121 36217	Lemma for frege122 36218. Proposition 121 of [Frege1879] p. 79. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- A e. W   =>    |- ( ( A = X -> X ( ( t+ ` R ) u. _I ) A ) -> ( Fun `' `' R -> ( Y R X -> ( Y R A -> X ( ( t+ ` R ) u. _I ) A ) ) ) )
Theorem	frege122 36218	If X is a result of an application of the single-valued procedure R to Y, then every result of an application of the procedure R to Y belongs to the R-sequence beginning with X. Proposition 122 of [Frege1879] p. 79. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- A e. W   =>    |- ( Fun `' `' R -> ( Y R X -> ( Y R A -> X ( ( t+ ` R ) u. _I ) A ) ) )
Theorem	frege123 36219*	Lemma for frege124 36220. Proposition 123 of [Frege1879] p. 79. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   =>    |- ( ( A. a ( Y R a -> X ( ( t+ ` R ) u. _I ) a ) -> ( Y ( t+ ` R ) M -> X ( ( t+ ` R ) u. _I ) M ) ) -> ( Fun `' `' R -> ( Y R X -> ( Y ( t+ ` R ) M -> X ( ( t+ ` R ) u. _I ) M ) ) ) )
Theorem	frege124 36220	If X is a result of an application of the single-valued procedure R to Y and if M follows Y in the R-sequence, then M belongs to the R-sequence beginning with X. Proposition 124 of [Frege1879] p. 80. (Contributed by RP, 8-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- M e. W   &    |- R e. S   =>    |- ( Fun `' `' R -> ( Y R X -> ( Y ( t+ ` R ) M -> X ( ( t+ ` R ) u. _I ) M ) ) )
Theorem	frege125 36221	Lemma for frege126 36222. Proposition 125 of [Frege1879] p. 81. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- M e. W   &    |- R e. S   =>    |- ( ( X ( ( t+ ` R ) u. _I ) M -> ( -. X ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) X ) ) -> ( Fun `' `' R -> ( Y R X -> ( Y ( t+ ` R ) M -> ( -. X ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) X ) ) ) ) )
Theorem	frege126 36222	If M follows Y in the R-sequence and if the procedure R is single-valued, then every result of an application of the procedure R to Y belongs to the R-sequence beginning with M or precedes M in the R-sequence. Proposition 126 of [Frege1879] p. 81. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- M e. W   &    |- R e. S   =>    |- ( Fun `' `' R -> ( Y R X -> ( Y ( t+ ` R ) M -> ( -. X ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) X ) ) ) )
Theorem	frege127 36223	Communte antecedents of frege126 36222. Proposition 127 of [Frege1879] p. 82. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- M e. W   &    |- R e. S   =>    |- ( Fun `' `' R -> ( Y ( t+ ` R ) M -> ( Y R X -> ( -. X ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) X ) ) ) )
Theorem	frege128 36224	Lemma for frege129 36225. Proposition 128 of [Frege1879] p. 83. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- M e. W   &    |- R e. S   =>    |- ( ( M ( ( t+ ` R ) u. _I ) Y -> ( Y R X -> ( -. X ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) X ) ) ) -> ( Fun `' `' R -> ( ( -. Y ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) Y ) -> ( Y R X -> ( -. X ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) X ) ) ) ) )
Theorem	frege129 36225	If the procedure R is single-valued and Y belongs to the R -sequence begining with M or precedes M in the R-sequence, then every result of an application of the procedure R to Y belongs to the R-sequence begining with M or precedes M in the R-sequence. Proposition 129 of [Frege1879] p. 83. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- M e. W   &    |- R e. S   =>    |- ( Fun `' `' R -> ( ( -. Y ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) Y ) -> ( Y R X -> ( -. X ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) X ) ) ) )
Theorem	frege130 36226*	Lemma for frege131 36227. Proposition 130 of [Frege1879] p. 84. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.)
|- M e. U   &    |- R e. V   =>    |- ( ( A. b ( ( -. b ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) b ) -> A. a ( b R a -> ( -. a ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) a ) ) ) -> R hereditary ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) ) -> ( Fun `' `' R -> R hereditary ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) ) )
Theorem	frege131 36227	If the procedure R is single-valued, then the property of belonging to the R-sequence begining with M or preceeding M in the R-sequence is hereditary in the R-sequence. Proposition 131 of [Frege1879] p. 85. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.)
|- M e. U   &    |- R e. V   =>    |- ( Fun `' `' R -> R hereditary ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) )
Theorem	frege132 36228	Lemma for frege133 36229. Proposition 132 of [Frege1879] p. 86. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.)
|- M e. U   &    |- R e. V   =>    |- ( ( R hereditary ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) -> ( X ( t+ ` R ) M -> ( X ( t+ ` R ) Y -> ( -. Y ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) Y ) ) ) ) -> ( Fun `' `' R -> ( X ( t+ ` R ) M -> ( X ( t+ ` R ) Y -> ( -. Y ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) Y ) ) ) ) )
Theorem	frege133 36229	If the procedure R is single-valued and if M and Y follow X in the R-sequence, then Y belongs to the R-sequence beginning with M or precedes M in the R-sequence. Proposition 133 of [Frege1879] p. 86. (Contributed by RP, 9-Jul-2020.) (Proof modification is discouraged.)
|- X e. U   &    |- Y e. V   &    |- M e. W   &    |- R e. S   =>    |- ( Fun `' `' R -> ( X ( t+ ` R ) M -> ( X ( t+ ` R ) Y -> ( -. Y ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) Y ) ) ) )
21.26  Mathbox for Stanislas Polu
Theorem	inductionexd 36230	Simple induction example. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( N e. NN -> 3 || ( ( 4 ^ N ) + 5 ) )
21.26.1  IMO Problems
21.26.1.1  IMO 1972 B2
Theorem	wwlemuld 36231	Natural deduction form of lemul2d 11382. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> ( C x. A ) <_ ( C x. B ) )   &    |- ( ph -> 0 < C )   =>    |- ( ph -> A <_ B )
Theorem	leeq1d 36232	Specialization of breq1d 4436 to reals and less than. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> A <_ C )   &    |- ( ph -> A = B )   &    |- ( ph -> A e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> B <_ C )
Theorem	leeq2d 36233	Specialization of breq2d 4438 to reals and less than. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> A <_ C )   &    |- ( ph -> C = D )   &    |- ( ph -> A e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> A <_ D )
Theorem	absmulrposd 36234	Specialization of absmuld with absidd 13463. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> 0 <_ A )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( abs ` ( A x. B ) ) = ( A x. ( abs ` B ) ) )
Theorem	imadisjld 36235	Natural dduction form of one side of imadisj 5207. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> ( dom A i^i B ) = (/) )   =>    |- ( ph -> ( A " B ) = (/) )
Theorem	imadisjlnd 36236	Natural deduction form of one negated side of imadisj 5207. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> ( dom A i^i B ) =/= (/) )   =>    |- ( ph -> ( A " B ) =/= (/) )
Theorem	wnefimgd 36237	The image of a mapping from A is non empty if A is non empty. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> A =/= (/) )   &    |- ( ph -> F : A --> B )   =>    |- ( ph -> ( F " A ) =/= (/) )
Theorem	fco2d 36238	Natural deduction form of fco2 5757. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> G : A --> B )   &    |- ( ph -> ( F |` B ) : B --> C )   =>    |- ( ph -> ( F o. G ) : A --> C )
Theorem	suprubd 36239*	Natural deduction form of suprubd 36239. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> A C_ RR )   &    |- ( ph -> A =/= (/) )   &    |- ( ph -> E. x e. RR A. y e. A y <_ x )   &    |- ( ph -> B e. A )   =>    |- ( ph -> B <_ sup ( A , RR , < ) )
Theorem	suprcld 36240*	Natural deduction form of suprcl 10569. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> A C_ RR )   &    |- ( ph -> A =/= (/) )   &    |- ( ph -> E. x e. RR A. y e. A y <_ x )   =>    |- ( ph -> sup ( A , RR , < ) e. RR )
Theorem	fvco3d 36241	Natural deduction form of fvco3 5958. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> G : A --> B )   &    |- ( ph -> C e. A )   =>    |- ( ph -> ( ( F o. G ) ` C ) = ( F ` ( G ` C ) ) )
Theorem	wfximgfd 36242	The value of a function on its domain is in the image of the function. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> C e. A )   &    |- ( ph -> F : A --> B )   =>    |- ( ph -> ( F ` C ) e. ( F " A ) )
Theorem	fvelimabd 36243*	Natural deduction form of fvelimab 5937. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> F Fn A )   &    |- ( ph -> B C_ A )   =>    |- ( ph -> ( C e. ( F " B ) <-> E. x e. B ( F ` x ) = C ) )
Theorem	extoimad 36244*	If |f(x)| <= C for all x then it applies to all x in the image of |f(x)| (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ C )   =>    |- ( ph -> A. x e. ( abs " ( F " RR ) ) x <_ C )
Theorem	imo72b2lem0 36245*	Lemma for imo72b2 36256. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> G : RR --> RR )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( ( F ` ( A + B ) ) + ( F ` ( A - B ) ) ) = ( 2 x. ( ( F ` A ) x. ( G ` B ) ) ) )   &    |- ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ 1 )   =>    |- ( ph -> ( ( abs ` ( F ` A ) ) x. ( abs ` ( G ` B ) ) ) <_ sup ( ( abs " ( F " RR ) ) , RR , < ) )
Theorem	suprleubrd 36246*	Natural deduction form of specialized suprleub 10573. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> A C_ RR )   &    |- ( ph -> A =/= (/) )   &    |- ( ph -> E. x e. RR A. y e. A y <_ x )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A. z e. A z <_ B )   =>    |- ( ph -> sup ( A , RR , < ) <_ B )
Theorem	imo72b2lem2 36247*	Lemma for imo72b2 36256. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A. z e. RR ( abs ` ( F ` z ) ) <_ C )   =>    |- ( ph -> sup ( ( abs " ( F " RR ) ) , RR , < ) <_ C )
Theorem	syldbl2 36248	Stacked hypotheseis implies goal. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ( ph /\ ps ) -> ( ps -> th ) )   =>    |- ( ( ph /\ ps ) -> th )
Theorem	funfvima2d 36249	A function's value in a preimage belongs to the image. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> F : A --> B )   =>    |- ( ( ph /\ x e. A ) -> ( F ` x ) e. ( F " A ) )
Theorem	suprlubrd 36250*	Natural deduction form of specialized suprlub 10571. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> A C_ RR )   &    |- ( ph -> A =/= (/) )   &    |- ( ph -> E. x e. RR A. y e. A y <_ x )   &    |- ( ph -> B e. RR )   &    |- ( ph -> E. z e. A B < z )   =>    |- ( ph -> B < sup ( A , RR , < ) )
Theorem	imo72b2lem1 36251*	Lemma for imo72b2 36256. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> E. x e. RR ( F ` x ) =/= 0 )   &    |- ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ 1 )   =>    |- ( ph -> 0 < sup ( ( abs " ( F " RR ) ) , RR , < ) )
Theorem	lemuldiv3d 36252	'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> ( B x. A ) <_ C )   &    |- ( ph -> 0 < A )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> B <_ ( C / A ) )
Theorem	lemuldiv4d 36253	'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> B <_ ( C / A ) )   &    |- ( ph -> 0 < A )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( B x. A ) <_ C )
Theorem	hypstkd 36254	Natural deductionm, stacks an hypothesis. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   &    |- ( ph -> ch )   =>    |- ( ( ph /\ ps ) -> th )
Theorem	rspcdvinvd 36255*	If something is true for all then it's true for some class. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ( ph /\ x = A ) -> ( ps <-> ch ) )   &    |- ( ph -> A e. B )   &    |- ( ph -> A. x e. B ps )   =>    |- ( ph -> ch )
Theorem	imo72b2 36256*	IMO 1972 B2. (14th International Mathemahics Olympiad in Poland, problem B2). (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> F : RR --> RR )   &    |- ( ph -> G : RR --> RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A. u e. RR A. v e. RR ( ( F ` ( u + v ) ) + ( F ` ( u - v ) ) ) = ( 2 x. ( ( F ` u ) x. ( G ` v ) ) ) )   &    |- ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ 1 )   &    |- ( ph -> E. x e. RR ( F ` x ) =/= 0 )   =>    |- ( ph -> ( abs ` ( G ` B ) ) <_ 1 )
21.26.2  INT Inequalities Proof Generator This section formalizes theorems necessary to reproduce the equality and inequality generator described in "Neural Theorem Proving on Inequality Problems" http://aitp-conference.org/2020/abstract/paper_18.pdf. Other theorems required: 0red 9643 1red 9657 readdcld 9669 remulcld 9670 eqcomd 2437.
Theorem	int-addcomd 36257	AdditionCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( B + C ) = ( C + A ) )
Theorem	int-addassocd 36258	AdditionAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( B + ( C + D ) ) = ( ( A + C ) + D ) )
Theorem	int-addsimpd 36259	AdditionSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> 0 = ( A - B ) )
Theorem	int-mulcomd 36260	MultiplicationCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( B x. C ) = ( C x. A ) )
Theorem	int-mulassocd 36261	MultiplicationAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( B x. ( C x. D ) ) = ( ( A x. C ) x. D ) )
Theorem	int-mulsimpd 36262	MultiplicationSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> B e. RR )   &    |- ( ph -> A = B )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> 1 = ( A / B ) )
Theorem	int-leftdistd 36263	AdditionMultiplicationLeftDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( ( C + D ) x. B ) = ( ( C x. A ) + ( D x. A ) ) )
Theorem	int-rightdistd 36264	AdditionMultiplicationRightDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( B x. ( C + D ) ) = ( ( A x. C ) + ( A x. D ) ) )
Theorem	int-sqdefd 36265	SquareDefinition generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> B e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( A x. B ) = ( A ^ 2 ) )
Theorem	int-mul11d 36266	First MultiplicationOne generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( A x. 1 ) = B )
Theorem	int-mul12d 36267	Second MultiplicationOne generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( 1 x. A ) = B )
Theorem	int-add01d 36268	First AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( A + 0 ) = B )
Theorem	int-add02d 36269	Second AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( 0 + A ) = B )
Theorem	int-sqgeq0d 36270	SquareGEQZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> 0 <_ ( A x. B ) )
Theorem	int-eqprincd 36271	PrincipleOfEquality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A + C ) = ( B + D ) )
Theorem	int-eqtransd 36272	EqualityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A = B )   &    |- ( ph -> B = C )   =>    |- ( ph -> A = C )
Theorem	int-eqmvtd 36273	EquMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A = B )   &    |- ( ph -> A = ( C + D ) )   =>    |- ( ph -> C = ( B - D ) )
Theorem	int-eqineqd 36274	EquivalenceImpliesDoubleInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> B e. RR )   &    |- ( ph -> A = B )   =>    |- ( ph -> B <_ A )
Theorem	int-ineqmvtd 36275	IneqMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> B <_ A )   &    |- ( ph -> A = ( C + D ) )   =>    |- ( ph -> ( B - D ) <_ C )
Theorem	int-ineq1stprincd 36276	FirstPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> B <_ A )   &    |- ( ph -> D <_ C )   =>    |- ( ph -> ( B + D ) <_ ( A + C ) )
Theorem	int-ineq2ndprincd 36277	SecondPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> B <_ A )   &    |- ( ph -> 0 <_ C )   =>    |- ( ph -> ( B x. C ) <_ ( A x. C ) )
Theorem	int-ineqtransd 36278	InequalityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> B <_ A )   &    |- ( ph -> C <_ B )   =>    |- ( ph -> C <_ A )
21.26.3  N-Digit Addition Proof Generator This section formalizes theorems used in an n-digit addition proof generator. Other theorems required: deccl 11065 addcomli 9824 00id 9807 addid1i 9819 addid2i 9820 eqid 2429 dec0h 11067 decadd 11092 decaddc 11093.
Theorem	unitadd 36279	Theorem used in conjunction with decaddc 11093 to absorb carry when generating n-digit addition synthetic proofs. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( A + B ) = F   &    |- ( C + 1 ) = B   &    |- A e. NN0   &    |- C e. NN0   =>    |- ( ( A + C ) + 1 ) = F
Theorem	5p5e10b 36280	5 + 5 = 10. Decimal form. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( 5 + 5 ) = ; 1 0
Theorem	6p4e10b 36281	6 + 4 = 10. Decimal form. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( 6 + 4 ) = ; 1 0
Theorem	7p3e10b 36282	7 + 3 = 10. Decimal form. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( 7 + 3 ) = ; 1 0
Theorem	8p2e10b 36283	8 + 2 = 10. Decimal form. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( 8 + 2 ) = ; 1 0
Theorem	9p1e10b 36284	9 + 1 = 10. Decimal form. (Contributed by Stanislas Polu, 7-Apr-2020.)
|- ( 9 + 1 ) = ; 1 0
21.26.4  AM-GM (for k = 2,3,4)
Theorem	gsumws3 36285	Valuation of a length 3 word in a monoid. (Contributed by Stanislas Polu, 9-Sep-2020.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Mnd /\ ( S e. B /\ ( T e. B /\ U e. B ) ) ) -> ( G gsumg <" S T U "> ) = ( S .+ ( T .+ U ) ) )
Theorem	gsumws4 36286	Valuation of a length 4 word in a monoid (Contributed by Stanislas Polu, 10-Sep-2020.)
|- B = ( Base ` G )   &    |- .+ = ( +g ` G )   =>    |- ( ( G e. Mnd /\ ( S e. B /\ ( T e. B /\ ( U e. B /\ V e. B ) ) ) ) -> ( G gsumg <" S T U V "> ) = ( S .+ ( T .+ ( U .+ V ) ) ) )
Theorem	amgm2d 36287	Arithmetic-geometric mean inequality for n = 2, derived from amgmlem 23780. (Contributed by Stanislas Polu, 8-Sep-2020.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( ( A x. B ) ^c ( 1 / 2 ) ) <_ ( ( A + B ) / 2 ) )
Theorem	amgm3d 36288	Arithmetic-geometric mean inequality for n = 3. (Contributed by Stanislas Polu, 11-Sep-2020.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> C e. RR+ )   =>    |- ( ph -> ( ( A x. ( B x. C ) ) ^c ( 1 / 3 ) ) <_ ( ( A + ( B + C ) ) / 3 ) )
Theorem	amgm4d 36289	Arithmetic-geometric mean inequality for n = 4. (Contributed by Stanislas Polu, 11-Sep-2020.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> C e. RR+ )   &    |- ( ph -> D e. RR+ )   =>    |- ( ph -> ( ( A x. ( B x. ( C x. D ) ) ) ^c ( 1 / 4 ) ) <_ ( ( A + ( B + ( C + D ) ) ) / 4 ) )
21.27  Mathbox for Steve Rodriguez
21.27.1  Miscellanea
Theorem	nanorxor 36290	'nand' is equivalent to the equivalence of inclusive and exclusive or. (Contributed by Steve Rodriguez, 28-Feb-2020.)
|- ( ( ph -/\ ps ) <-> ( ( ph \/ ps ) <-> ( ph \/_ ps ) ) )
Theorem	undisjrab 36291	Union of two disjoint restricted class abstractions; compare unrab 3750. (Contributed by Steve Rodriguez, 28-Feb-2020.)
|- ( ( { x e. A | ph } i^i { x e. A | ps } ) = (/) <-> ( { x e. A | ph } u. { x e. A | ps } ) = { x e. A | ( ph \/_ ps ) } )
Theorem	iso0 36292	The empty set is an R , S isomorphism from the empty set to the empty set. (Contributed by Steve Rodriguez, 24-Oct-2015.)
|- (/) Isom R , S ( (/) , (/) )
Theorem	ssrecnpr 36293	RR is a subset of both RR and CC. (Contributed by Steve Rodriguez, 22-Nov-2015.)
|- ( S e. { RR , CC } -> RR C_ S )
Theorem	seff 36294	Let set S be the real or complex numbers. Then the exponential function restricted to S is a mapping from S to S. (Contributed by Steve Rodriguez, 6-Nov-2015.)
|- ( ph -> S e. { RR , CC } )   =>    |- ( ph -> ( exp |` S ) : S --> S )
Theorem	sblpnf 36295	The infinity ball in the absolute value metric is just the whole space. S analog of blpnf 21343. (Contributed by Steve Rodriguez, 8-Nov-2015.)
|- ( ph -> S e. { RR , CC } )   &    |- D = ( ( abs o. - ) |` ( S X. S ) )   =>    |- ( ( ph /\ P e. S ) -> ( P ( ball ` D ) +oo ) = S )
Theorem	prmunb2 36296*	The primes are unbounded. This generalizes prmunb 14821 to real A with arch 10866 and lttrd 9795: every real is less than some positive integer, itself less than some prime. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( A e. RR -> E. p e. Prime A < p )
Theorem	isprm7 36297*	One need only check prime divisors of P up to sqr P in order to ensure primality. This version of isprm5 14622 combines the primality and bound on z into a finite interval of prime numbers. (Contributed by Steve Rodriguez, 20-Jan-2020.)
|- ( P e. Prime <-> ( P e. ( ZZ>= ` 2 ) /\ A. z e. ( ( 2 ... ( |_ ` ( sqr ` P ) ) ) i^i Prime ) -. z || P ) )
21.27.2  Ratio test for infinite series convergence and divergence
Theorem	dvgrat 36298*	Ratio test for divergence of a complex infinite series. See e.g. remark "if ( abs ` ( ( a ` ( n + 1 ) ) / ( a ` n ) ) ) >_ 1 for all large n..." in https://en.wikipedia.org/wiki/Ratio_test#The_test. (Contributed by Steve Rodriguez, 28-Feb-2020.)
|- Z = ( ZZ>= ` M )   &    |- W = ( ZZ>= ` N )   &    |- ( ph -> N e. Z )   &    |- ( ph -> F e. V )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. W ) -> ( F ` k ) =/= 0 )   &    |- ( ( ph /\ k e. W ) -> ( abs ` ( F ` k ) ) <_ ( abs ` ( F ` ( k + 1 ) ) ) )   =>    |- ( ph -> seq M ( + , F ) e/ dom ~~> )
Theorem	cvgdvgrat 36299*	Ratio test for convergence and divergence of a complex infinite series. If the ratio R of the absolute values of successive terms in an infinite sequence F converges to less than one, then the infinite sum of the terms of F converges to a complex number; and if R converges greater then the sum diverges. This combined form of cvgrat 13917 and dvgrat 36298 directly uses the limit of the ratio. (It also demonstrates how to use climi2 13553 and absltd 13470 to transform a limit to an inequality cf. https://math.stackexchange.com/q/2215191, and how to use r19.29a 2977 in a similar fashion to Mario Carneiro's proof sketch with rexlimdva 2924 at https://groups.google.com/forum/#!topic/metamath/2RPikOiXLMo.) (Contributed by Steve Rodriguez, 28-Feb-2020.)
|- Z = ( ZZ>= ` M )   &    |- W = ( ZZ>= ` N )   &    |- ( ph -> N e. Z )   &    |- ( ph -> F e. V )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. W ) -> ( F ` k ) =/= 0 )   &    |- R = ( k e. W |-> ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) )   &    |- ( ph -> R ~~> L )   &    |- ( ph -> L =/= 1 )   =>    |- ( ph -> ( L < 1 <-> seq M ( + , F ) e. dom ~~> ) )
Theorem	radcnvrat 36300*	Let L be the limit, if one exists, of the ratio ( abs ` ( ( A ` ( k + 1 ) ) / ( A ` k ) ) ) (as in the ratio test cvgdvgrat 36299) as k increases. Then the radius of convergence of power series sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) is ( 1 / L ) if L is nonzero. Proof "The limit involved in the ratio test..." in https://en.wikipedia.org/wiki/Radius_of_convergence —a few lines that evidently hide quite an involved process to confirm. (Contributed by Steve Rodriguez, 8-Mar-2020.)
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) )   &    |- ( ph -> A : NN0 --> CC )   &    |- R = sup ( { r e. RR | seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )   &    |- D = ( k e. NN0 |-> ( abs ` ( ( A ` ( k + 1 ) ) / ( A ` k ) ) ) )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. NN0 )   &    |- ( ( ph /\ k e. Z ) -> ( A ` k ) =/= 0 )   &    |- ( ph -> D ~~> L )   &    |- ( ph -> L =/= 0 )   =>    |- ( ph -> R = ( 1 / L ) )