P. 308 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 30701-30800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	reprfi2 30701	Corollary of reprinfz1 30700. (Contributed by Thierry Arnoux, 15-Dec-2021.)
|- ( ph -> N e. NN0 )   &    |- ( ph -> S e. NN0 )   &    |- ( ph -> A C_ NN )   =>    |- ( ph -> ( A (repr ` S ) N ) e. Fin )
Theorem	reprfz1 30702	Corollary of reprinfz1 30700. (Contributed by Thierry Arnoux, 14-Dec-2021.)
|- ( ph -> N e. NN0 )   &    |- ( ph -> S e. NN0 )   =>    |- ( ph -> ( NN (repr ` S ) N ) = ( ( 1 ... N ) (repr ` S ) N ) )
Theorem	hashrepr 30703*	Develop the number of representations of an integer M as a sum of nonnegative integers in set A. (Contributed by Thierry Arnoux, 14-Dec-2021.)
|- ( ph -> A C_ NN )   &    |- ( ph -> M e. NN0 )   &    |- ( ph -> S e. NN0 )   =>    |- ( ph -> ( # ` ( A (repr ` S ) M ) ) = sum_ c e. ( NN (repr ` S ) M ) prod_ a e. ( 0..^ S ) ( ( (𝟭 ` NN ) ` A ) ` ( c ` a ) ) )
Theorem	reprpmtf1o 30704*	Transposing 0 and X maps representations with a condition on the first index to transpositions with the same condition on the index X. (Contributed by Thierry Arnoux, 27-Dec-2021.)
|- ( ph -> S e. NN )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> A C_ NN )   &    |- ( ph -> X e. ( 0..^ S ) )   &    |- O = { c e. ( A (repr ` S ) M ) | -. ( c ` 0 ) e. B }   &    |- P = { c e. ( A (repr ` S ) M ) | -. ( c ` X ) e. B }   &    |- T = if ( X = 0 , ( _I |` ( 0..^ S ) ) , ( (pmTrsp ` ( 0..^ S ) ) ` { X , 0 } ) )   &    |- F = ( c e. P |-> ( c o. T ) )   =>    |- ( ph -> F : P -1-1-onto-> O )
Theorem	reprdifc 30705*	Express the representations as a sum of integers in a difference of sets using conditions on each of the indices. (Contributed by Thierry Arnoux, 27-Dec-2021.)
|- C = { c e. ( A (repr ` S ) M ) | -. ( c ` x ) e. B }   &    |- ( ph -> A C_ NN )   &    |- ( ph -> B C_ NN )   &    |- ( ph -> M e. NN0 )   &    |- ( ph -> S e. NN0 )   =>    |- ( ph -> ( ( A (repr ` S ) M ) \ ( B (repr ` S ) M ) ) = U_ x e. ( 0..^ S ) C )
Theorem	chpvalz 30706*	Value of the second Chebyshev function, or summatory of the von Mangoldt function. (Contributed by Thierry Arnoux, 28-Dec-2021.)
|- ( N e. ZZ -> (ψ ` N ) = sum_ n e. ( 1 ... N ) (Λ ` n ) )
Theorem	chtvalz 30707*	Value of the Chebyshev function for integers. (Contributed by Thierry Arnoux, 28-Dec-2021.)
|- ( N e. ZZ -> ( theta ` N ) = sum_ n e. ( ( 1 ... N ) i^i Prime ) ( log ` n ) )
Theorem	breprexplema 30708*	Lemma for breprexp 30711 (induction step for weighted sums over representations) (Contributed by Thierry Arnoux, 7-Dec-2021.)
|- ( ph -> N e. NN0 )   &    |- ( ph -> S e. NN0 )   &    |- ( ph -> M e. NN0 )   &    |- ( ph -> M <_ ( ( S + 1 ) x. N ) )   &    |- ( ( ( ph /\ x e. ( 0..^ ( S + 1 ) ) ) /\ y e. NN ) -> ( ( L ` x ) ` y ) e. CC )   =>    |- ( ph -> sum_ d e. ( ( 1 ... N ) (repr ` ( S + 1 ) ) M ) prod_ a e. ( 0..^ ( S + 1 ) ) ( ( L ` a ) ` ( d ` a ) ) = sum_ b e. ( 1 ... N ) sum_ d e. ( ( 1 ... N ) (repr ` S ) ( M - b ) ) ( prod_ a e. ( 0..^ S ) ( ( L ` a ) ` ( d ` a ) ) x. ( ( L ` S ) ` b ) ) )
Theorem	breprexplemb 30709	Lemma for breprexp 30711 (closure) (Contributed by Thierry Arnoux, 7-Dec-2021.)
|- ( ph -> N e. NN0 )   &    |- ( ph -> S e. NN0 )   &    |- ( ph -> Z e. CC )   &    |- ( ph -> L : ( 0..^ S ) --> ( CC ^m NN ) )   &    |- ( ph -> X e. ( 0..^ S ) )   &    |- ( ph -> Y e. NN )   =>    |- ( ph -> ( ( L ` X ) ` Y ) e. CC )
Theorem	breprexplemc 30710*	Lemma for breprexp 30711 (induction step) (Contributed by Thierry Arnoux, 6-Dec-2021.)
|- ( ph -> N e. NN0 )   &    |- ( ph -> S e. NN0 )   &    |- ( ph -> Z e. CC )   &    |- ( ph -> L : ( 0..^ S ) --> ( CC ^m NN ) )   &    |- ( ph -> T e. NN0 )   &    |- ( ph -> ( T + 1 ) <_ S )   &    |- ( ph -> prod_ a e. ( 0..^ T ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( T x. N ) ) sum_ d e. ( ( 1 ... N ) (repr ` T ) m ) ( prod_ a e. ( 0..^ T ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) )   =>    |- ( ph -> prod_ a e. ( 0..^ ( T + 1 ) ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( ( T + 1 ) x. N ) ) sum_ d e. ( ( 1 ... N ) (repr ` ( T + 1 ) ) m ) ( prod_ a e. ( 0..^ ( T + 1 ) ) ( ( L ` a ) ` ( d ` a ) ) x. ( Z ^ m ) ) )
Theorem	breprexp 30711*	Express the S th power of the finite series in terms of the number of representations of integers m as sums of S terms. This is a general formulation which allows logarithmic weighting of the sums (see https://mathoverflow.net/questions/253246) and a mix of different smoothing functions taken into account in L. See breprexpnat 30712 for the simple case presented in the proposition of [Nathanson] p. 123. (Contributed by Thierry Arnoux, 6-Dec-2021.)
|- ( ph -> N e. NN0 )   &    |- ( ph -> S e. NN0 )   &    |- ( ph -> Z e. CC )   &    |- ( ph -> L : ( 0..^ S ) --> ( CC ^m NN ) )   =>    |- ( ph -> prod_ a e. ( 0..^ S ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( S x. N ) ) sum_ c e. ( ( 1 ... N ) (repr ` S ) m ) ( prod_ a e. ( 0..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
Theorem	breprexpnat 30712*	Express the S th power of the finite series in terms of the number of representations of integers m as sums of S terms of elements of A, bounded by N. Proposition of [Nathanson] p. 123. (Contributed by Thierry Arnoux, 11-Dec-2021.)
|- ( ph -> N e. NN0 )   &    |- ( ph -> S e. NN0 )   &    |- ( ph -> Z e. CC )   &    |- ( ph -> A C_ NN )   &    |- P = sum_ b e. ( A i^i ( 1 ... N ) ) ( Z ^ b )   &    |- R = ( # ` ( ( A i^i ( 1 ... N ) ) (repr ` S ) m ) )   =>    |- ( ph -> ( P ^ S ) = sum_ m e. ( 0 ... ( S x. N ) ) ( R x. ( Z ^ m ) ) )
20.3.26.2  Vinogradov Trigonometric Sums and the Circle Method
Syntax	cvts 30713	The Vinogradov trigonometric sums.
class vts
Definition	df-vts 30714*	Define the Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 1-Dec-2021.)
|- vts = ( l e. ( CC ^m NN ) , n e. NN0 |-> ( x e. CC |-> sum_ a e. ( 1 ... n ) ( ( l ` a ) x. ( exp ` ( ( _i x. ( 2 x. pi ) ) x. ( a x. x ) ) ) ) ) )
Theorem	vtsval 30715*	Value of the Vinogradov trigonometric sums (Contributed by Thierry Arnoux, 1-Dec-2021.)
|- ( ph -> N e. NN0 )   &    |- ( ph -> X e. CC )   &    |- ( ph -> L : NN --> CC )   =>    |- ( ph -> ( ( Lvts N ) ` X ) = sum_ a e. ( 1 ... N ) ( ( L ` a ) x. ( exp ` ( ( _i x. ( 2 x. pi ) ) x. ( a x. X ) ) ) ) )
Theorem	vtscl 30716	Closure of the Vinogradov trigonometric sums (Contributed by Thierry Arnoux, 14-Dec-2021.)
|- ( ph -> N e. NN0 )   &    |- ( ph -> X e. CC )   &    |- ( ph -> L : NN --> CC )   =>    |- ( ph -> ( ( Lvts N ) ` X ) e. CC )
Theorem	vtsprod 30717*	Express the Vinogradov trigonometric sums to the power of S (Contributed by Thierry Arnoux, 12-Dec-2021.)
|- ( ph -> N e. NN0 )   &    |- ( ph -> X e. CC )   &    |- ( ph -> S e. NN0 )   &    |- ( ph -> L : ( 0..^ S ) --> ( CC ^m NN ) )   =>    |- ( ph -> prod_ a e. ( 0..^ S ) ( ( ( L ` a )vts N ) ` X ) = sum_ m e. ( 0 ... ( S x. N ) ) sum_ c e. ( ( 1 ... N ) (repr ` S ) m ) ( prod_ a e. ( 0..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( exp ` ( ( _i x. ( 2 x. pi ) ) x. ( m x. X ) ) ) ) )
Theorem	circlemeth 30718*	The Hardy, Littlewood and Ramanujan Circle Method, in a generic form, with different weighting / smoothing functions. (Contributed by Thierry Arnoux, 13-Dec-2021.)
|- ( ph -> N e. NN0 )   &    |- ( ph -> S e. NN )   &    |- ( ph -> L : ( 0..^ S ) --> ( CC ^m NN ) )   =>    |- ( ph -> sum_ c e. ( NN (repr ` S ) N ) prod_ a e. ( 0..^ S ) ( ( L ` a ) ` ( c ` a ) ) = S. ( 0 (,) 1 ) ( prod_ a e. ( 0..^ S ) ( ( ( L ` a )vts N ) ` x ) x. ( exp ` ( ( _i x. ( 2 x. pi ) ) x. ( -u N x. x ) ) ) ) _d x )
Theorem	circlemethnat 30719*	The Hardy, Littlewood and Ramanujan Circle Method, Chapter 5.1 of [Nathanson] p. 123. This expresses R, the number of different ways a nonnegative integer N can be represented as the sum of at most S integers in the set A as an integral of Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 13-Dec-2021.)
|- R = ( # ` ( A (repr ` S ) N ) )   &    |- F = ( ( ( (𝟭 ` NN ) ` A )vts N ) ` x )   &    |- N e. NN0   &    |- A C_ NN   &    |- S e. NN   =>    |- R = S. ( 0 (,) 1 ) ( ( F ^ S ) x. ( exp ` ( ( _i x. ( 2 x. pi ) ) x. ( -u N x. x ) ) ) ) _d x
Theorem	circlevma 30720*	The Circle Method, where the Vinogradov sums are weighted using the von Mangoldt function, as it appears as proposition 1.1 of [Helfgott] p. 5. (Contributed by Thierry Arnoux, 13-Dec-2021.)
|- ( ph -> N e. NN0 )   =>    |- ( ph -> sum_ n e. ( NN (repr ` 3 ) N ) ( (Λ ` ( n ` 0 ) ) x. ( (Λ ` ( n ` 1 ) ) x. (Λ ` ( n ` 2 ) ) ) ) = S. ( 0 (,) 1 ) ( ( ( (Λvts N ) ` x ) ^ 3 ) x. ( exp ` ( ( _i x. ( 2 x. pi ) ) x. ( -u N x. x ) ) ) ) _d x )
Theorem	circlemethhgt 30721*	The circle method, where the Vinogradov sums are weighted using the Von Mangoldt function and smoothed using functions H and K. Statement 7.49 of [Helfgott] p. 69. At this point there is no further constraint on the smoothing functions. (Contributed by Thierry Arnoux, 22-Dec-2021.)
|- ( ph -> H : NN --> RR )   &    |- ( ph -> K : NN --> RR )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> sum_ n e. ( NN (repr ` 3 ) N ) ( ( (Λ ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) x. ( ( (Λ ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) x. ( (Λ ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) ) ) = S. ( 0 (,) 1 ) ( ( ( ( (Λ oF x. H )vts N ) ` x ) x. ( ( ( (Λ oF x. K )vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. pi ) ) x. ( -u N x. x ) ) ) ) _d x )
20.3.26.3  The Ternary Goldbach Conjecture: Final Statement
Axiom	ax-hgt749 30722*	Statement 7.49 of [Helfgott] p. 70. For a sufficiently big odd N, this postulates the existence of smoothing functions h (eta star) and k (eta plus) such that the lower bound for the circle integral is big enough. (Contributed by Thierry Arnoux, 15-Dec-2021.)
|- A. n e. { z e. ZZ | -. 2 || z } ( (; 1 0 ^; 2 7 ) <_ n -> E. h e. ( ( 0 [,) +oo ) ^m NN ) E. k e. ( ( 0 [,) +oo ) ^m NN ) ( A. m e. NN ( k ` m ) <_ ( 1 period_ 0_ 7_ 9_ 9_ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 period_ 4_ 1 4 ) /\ ( ( 0 period_ 0_ 0_ 0_ 4_ 2_ 2_ 4 8 ) x. ( n ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( (Λ oF x. h )vts n ) ` x ) x. ( ( ( (Λ oF x. k )vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. pi ) ) x. ( -u n x. x ) ) ) ) _d x ) )
Axiom	ax-ros335 30723	Theorem 12. of [RosserSchoenfeld] p. 71. Theorem chpo1ubb 25170 states that the ψ function is bounded by a linear term; this axiom postulates an upper bound for that linear term. This is stated as an axiom until a formal proof can be provided. (Contributed by Thierry Arnoux, 28-Dec-2021.)
|- A. x e. RR+ (ψ ` x ) < ( ( 1 period_ 0_ 3_ 8_ 8 3 ) x. x )
Axiom	ax-ros336 30724	Theorem 13. of [RosserSchoenfeld] p. 71. Theorem chpchtlim 25168 states that the ψ and theta function are asymtotic to each other; this axiom postulates an upper bound for their difference. This is stated as an axiom until a formal proof can be provided. (Contributed by Thierry Arnoux, 28-Dec-2021.)
|- A. x e. RR+ ( (ψ ` x ) - ( theta ` x ) ) < ( ( 1 period_ 4_ 2_ 6 2 ) x. ( sqr ` x ) )
Theorem	hgt750lemc 30725*	An upper bound to the summatory function of the von Mangoldt function. (Contributed by Thierry Arnoux, 29-Dec-2021.)
|- ( ph -> N e. NN )   =>    |- ( ph -> sum_ j e. ( 1 ... N ) (Λ ` j ) < ( ( 1 period_ 0_ 3_ 8_ 8 3 ) x. N ) )
Theorem	hgt750lemd 30726*	An upper bound to the summatory function of the von Mangoldt function on non-primes. (Contributed by Thierry Arnoux, 29-Dec-2021.)
|- ( ph -> N e. NN )   &    |- ( ph -> (; 1 0 ^; 2 7 ) <_ N )   =>    |- ( ph -> sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) (Λ ` i ) < ( ( 1 period_ 4_ 2_ 6 3 ) x. ( sqr ` N ) ) )
Theorem	hgt749d 30727*	A deduction version of ax-hgt749 30722. (Contributed by Thierry Arnoux, 15-Dec-2021.)
|- O = { z e. ZZ | -. 2 || z }   &    |- ( ph -> N e. O )   &    |- ( ph -> (; 1 0 ^; 2 7 ) <_ N )   =>    |- ( ph -> E. h e. ( ( 0 [,) +oo ) ^m NN ) E. k e. ( ( 0 [,) +oo ) ^m NN ) ( A. m e. NN ( k ` m ) <_ ( 1 period_ 0_ 7_ 9_ 9_ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 period_ 4_ 1 4 ) /\ ( ( 0 period_ 0_ 0_ 0_ 4_ 2_ 2_ 4 8 ) x. ( N ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( (Λ oF x. h )vts N ) ` x ) x. ( ( ( (Λ oF x. k )vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. pi ) ) x. ( -u N x. x ) ) ) ) _d x ) )
Theorem	logdivsqrle 30728	Conditions for ( ( log x ) / ( sqrt x ) ) to be decreasing. (Contributed by Thierry Arnoux, 20-Dec-2021.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> ( exp ` 2 ) <_ A )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( ( log ` B ) / ( sqr ` B ) ) <_ ( ( log ` A ) / ( sqr ` A ) ) )
Theorem	hgt750lem 30729	Lemma for tgoldbachgtd 30740. (Contributed by Thierry Arnoux, 17-Dec-2021.)
|- ( ( N e. NN0 /\ (; 1 0 ^; 2 7 ) <_ N ) -> ( ( 7 period_ 3_ 4 8 ) x. ( ( log ` N ) / ( sqr ` N ) ) ) < ( 0 period_ 0_ 0_ 0_ 4_ 2_ 2_ 4 8 ) )
Theorem	hgt750lem2 30730	Decimal multiplication galore! (Contributed by Thierry Arnoux, 26-Dec-2021.)
|- ( 3 x. ( ( ( ( 1 period_ 0_ 7_ 9_ 9_ 5 5 ) ^ 2 ) x. ( 1 period_ 4_ 1 4 ) ) x. ( ( 1 period_ 4_ 2_ 6 3 ) x. ( 1 period_ 0_ 3_ 8_ 8 3 ) ) ) ) < ( 7 period_ 3_ 4 8 )
Theorem	hgt750lemf 30731*	Lemma for the statement 7.50 of [Helfgott] p. 69. (Contributed by Thierry Arnoux, 1-Jan-2022.)
|- ( ph -> A e. Fin )   &    |- ( ph -> P e. RR )   &    |- ( ph -> Q e. RR )   &    |- ( ph -> H : NN --> ( 0 [,) +oo ) )   &    |- ( ph -> K : NN --> ( 0 [,) +oo ) )   &    |- ( ( ph /\ n e. A ) -> ( n ` 0 ) e. NN )   &    |- ( ( ph /\ n e. A ) -> ( n ` 1 ) e. NN )   &    |- ( ( ph /\ n e. A ) -> ( n ` 2 ) e. NN )   &    |- ( ( ph /\ m e. NN ) -> ( K ` m ) <_ P )   &    |- ( ( ph /\ m e. NN ) -> ( H ` m ) <_ Q )   =>    |- ( ph -> sum_ n e. A ( ( (Λ ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) x. ( ( (Λ ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) x. ( (Λ ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) ) ) <_ ( ( ( P ^ 2 ) x. Q ) x. sum_ n e. A ( (Λ ` ( n ` 0 ) ) x. ( (Λ ` ( n ` 1 ) ) x. (Λ ` ( n ` 2 ) ) ) ) ) )
Theorem	hgt750lemg 30732*	Lemma for the statement 7.50 of [Helfgott] p. 69. Applying a permutation T to the three factors of a product does not change the result. (Contributed by Thierry Arnoux, 1-Jan-2022.)
|- F = ( c e. R |-> ( c o. T ) )   &    |- ( ph -> T : ( 0..^ 3 ) -1-1-onto-> ( 0..^ 3 ) )   &    |- ( ph -> N : ( 0..^ 3 ) --> NN )   &    |- ( ph -> L : NN --> RR )   &    |- ( ph -> N e. R )   =>    |- ( ph -> ( ( L ` ( ( F ` N ) ` 0 ) ) x. ( ( L ` ( ( F ` N ) ` 1 ) ) x. ( L ` ( ( F ` N ) ` 2 ) ) ) ) = ( ( L ` ( N ` 0 ) ) x. ( ( L ` ( N ` 1 ) ) x. ( L ` ( N ` 2 ) ) ) ) )
Theorem	oddprm2 30733*	Two ways to write the set of odd primes. (Contributed by Thierry Arnoux, 27-Dec-2021.)
|- O = { z e. ZZ | -. 2 || z }   =>    |- ( Prime \ { 2 } ) = ( O i^i Prime )
Theorem	hgt750lemb 30734*	An upper bound on the contribution of the non-prime terms in the Statement 7.50 of [Helfgott] p. 69. (Contributed by Thierry Arnoux, 28-Dec-2021.)
|- O = { z e. ZZ | -. 2 || z }   &    |- ( ph -> N e. NN )   &    |- ( ph -> 2 <_ N )   &    |- A = { c e. ( NN (repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) }   =>    |- ( ph -> sum_ n e. A ( (Λ ` ( n ` 0 ) ) x. ( (Λ ` ( n ` 1 ) ) x. (Λ ` ( n ` 2 ) ) ) ) <_ ( ( log ` N ) x. ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) (Λ ` i ) x. sum_ j e. ( 1 ... N ) (Λ ` j ) ) ) )
Theorem	hgt750lema 30735*	An upper bound on the contribution of the non-prime terms in the Statement 7.50 of [Helfgott] p. 69. (Contributed by Thierry Arnoux, 1-Jan-2022.)
|- O = { z e. ZZ | -. 2 || z }   &    |- ( ph -> N e. NN )   &    |- ( ph -> 2 <_ N )   &    |- A = { c e. ( NN (repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) }   &    |- F = ( d e. { c e. ( NN (repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } |-> ( d o. if ( a = 0 , ( _I |` ( 0..^ 3 ) ) , ( (pmTrsp ` ( 0..^ 3 ) ) ` { a , 0 } ) ) ) )   =>    |- ( ph -> sum_ n e. ( ( NN (repr ` 3 ) N ) \ ( ( O i^i Prime ) (repr ` 3 ) N ) ) ( (Λ ` ( n ` 0 ) ) x. ( (Λ ` ( n ` 1 ) ) x. (Λ ` ( n ` 2 ) ) ) ) <_ ( 3 x. sum_ n e. A ( (Λ ` ( n ` 0 ) ) x. ( (Λ ` ( n ` 1 ) ) x. (Λ ` ( n ` 2 ) ) ) ) ) )
Theorem	hgt750leme 30736*	An upper bound on the contribution of the non-prime terms in the Statement 7.50 of [Helfgott] p. 69. (Contributed by Thierry Arnoux, 29-Dec-2021.)
|- O = { z e. ZZ | -. 2 || z }   &    |- ( ph -> N e. NN )   &    |- ( ph -> (; 1 0 ^; 2 7 ) <_ N )   &    |- ( ph -> H : NN --> ( 0 [,) +oo ) )   &    |- ( ph -> K : NN --> ( 0 [,) +oo ) )   &    |- ( ( ph /\ m e. NN ) -> ( K ` m ) <_ ( 1 period_ 0_ 7_ 9_ 9_ 5 5 ) )   &    |- ( ( ph /\ m e. NN ) -> ( H ` m ) <_ ( 1 period_ 4_ 1 4 ) )   =>    |- ( ph -> sum_ n e. ( ( NN (repr ` 3 ) N ) \ ( ( O i^i Prime ) (repr ` 3 ) N ) ) ( ( (Λ ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) x. ( ( (Λ ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) x. ( (Λ ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) ) ) <_ ( ( ( 7 period_ 3_ 4 8 ) x. ( ( log ` N ) / ( sqr ` N ) ) ) x. ( N ^ 2 ) ) )
Theorem	tgoldbachgnn 30737*	Lemma for tgoldbachgtd 30740. (Contributed by Thierry Arnoux, 15-Dec-2021.)
|- O = { z e. ZZ | -. 2 || z }   &    |- ( ph -> N e. O )   &    |- ( ph -> (; 1 0 ^; 2 7 ) <_ N )   =>    |- ( ph -> N e. NN )
Theorem	tgoldbachgtde 30738*	Lemma for tgoldbachgtd 30740. (Contributed by Thierry Arnoux, 15-Dec-2021.)
|- O = { z e. ZZ | -. 2 || z }   &    |- ( ph -> N e. O )   &    |- ( ph -> (; 1 0 ^; 2 7 ) <_ N )   &    |- ( ph -> H : NN --> ( 0 [,) +oo ) )   &    |- ( ph -> K : NN --> ( 0 [,) +oo ) )   &    |- ( ( ph /\ m e. NN ) -> ( K ` m ) <_ ( 1 period_ 0_ 7_ 9_ 9_ 5 5 ) )   &    |- ( ( ph /\ m e. NN ) -> ( H ` m ) <_ ( 1 period_ 4_ 1 4 ) )   &    |- ( ph -> ( ( 0 period_ 0_ 0_ 0_ 4_ 2_ 2_ 4 8 ) x. ( N ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( (Λ oF x. H )vts N ) ` x ) x. ( ( ( (Λ oF x. K )vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. pi ) ) x. ( -u N x. x ) ) ) ) _d x )   =>    |- ( ph -> 0 < sum_ n e. ( ( O i^i Prime ) (repr ` 3 ) N ) ( ( (Λ ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) x. ( ( (Λ ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) x. ( (Λ ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) ) ) )
Theorem	tgoldbachgtda 30739*	Lemma for tgoldbachgtd 30740. (Contributed by Thierry Arnoux, 15-Dec-2021.)
|- O = { z e. ZZ | -. 2 || z }   &    |- ( ph -> N e. O )   &    |- ( ph -> (; 1 0 ^; 2 7 ) <_ N )   &    |- ( ph -> H : NN --> ( 0 [,) +oo ) )   &    |- ( ph -> K : NN --> ( 0 [,) +oo ) )   &    |- ( ( ph /\ m e. NN ) -> ( K ` m ) <_ ( 1 period_ 0_ 7_ 9_ 9_ 5 5 ) )   &    |- ( ( ph /\ m e. NN ) -> ( H ` m ) <_ ( 1 period_ 4_ 1 4 ) )   &    |- ( ph -> ( ( 0 period_ 0_ 0_ 0_ 4_ 2_ 2_ 4 8 ) x. ( N ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( (Λ oF x. H )vts N ) ` x ) x. ( ( ( (Λ oF x. K )vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. pi ) ) x. ( -u N x. x ) ) ) ) _d x )   =>    |- ( ph -> 0 < ( # ` ( ( O i^i Prime ) (repr ` 3 ) N ) ) )
Theorem	tgoldbachgtd 30740*	Odd integers greater than (; 1 0 ^; 2 7 ) have at least a representation as a sum of three odd primes. Final statement in section 7.4 of [Helfgott] p. 70 (Contributed by Thierry Arnoux, 15-Dec-2021.)
|- O = { z e. ZZ | -. 2 || z }   &    |- ( ph -> N e. O )   &    |- ( ph -> (; 1 0 ^; 2 7 ) <_ N )   =>    |- ( ph -> 0 < ( # ` ( ( O i^i Prime ) (repr ` 3 ) N ) ) )
Theorem	tgoldbachgt 30741*	Odd integers greater than (; 1 0 ^; 2 7 ) have at least a representation as a sum of three odd primes. Final statement in section 7.4 of [Helfgott] p. 70 , expressed using the set G of odd numbers which can be written as a sum of three odd primes. (Contributed by Thierry Arnoux, 22-Dec-2021.)
|- O = { z e. ZZ | -. 2 || z }   &    |- G = { z e. O | E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. O /\ q e. O /\ r e. O ) /\ z = ( ( p + q ) + r ) ) }   =>    |- E. m e. NN ( m <_ (; 1 0 ^; 2 7 ) /\ A. n e. O ( m < n -> n e. G ) )
20.3.27  Elementary Geometry
20.3.27.1  Two-dimension geometry This definition has been superseded by DimTarskiG≥ and is no longer needed in the main part of set.mm. It is only kept here for reference.
Syntax	cstrkg2d 30742	Extends class notation with the class of geometries fulfilling the planarity axioms.
class TarskiG2D
Definition	df-trkg2d 30743*	Define the class of geometries fulfilling the lower dimension axiom, Axiom A8 of [Schwabhauser] p. 12, and the upper dimension axiom, Axiom A9 of [Schwabhauser] p. 13, for dimension 2. (Contributed by Thierry Arnoux, 14-Mar-2019.) (New usage is discouraged.)
|- TarskiG2D = { f | [. ( Base ` f ) / p ]. [. ( dist ` f ) / d ]. [. (Itv ` f ) / i ]. ( E. x e. p E. y e. p E. z e. p -. ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) /\ A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( ( ( x d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) ) /\ u =/= v ) -> ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) ) }
Theorem	istrkg2d 30744*	Property of fulfilling dimension 2 axiom. (Contributed by Thierry Arnoux, 29-May-2019.) (New usage is discouraged.) (Proof modification is discouraged.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   =>    |- ( G e. TarskiG2D <-> ( G e. _V /\ ( E. x e. P E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) /\ A. x e. P A. y e. P A. z e. P A. u e. P A. v e. P ( ( ( ( x .- u ) = ( x .- v ) /\ ( y .- u ) = ( y .- v ) /\ ( z .- u ) = ( z .- v ) ) /\ u =/= v ) -> ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) )
Theorem	axtglowdim2OLD 30745*	Lower dimension axiom for dimension 2, Axiom A8 of [Schwabhauser] p. 13. There exist 3 non-colinear points. (Contributed by Thierry Arnoux, 29-May-2019.) (New usage is discouraged.) (Proof modification is discouraged.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG2D )   =>    |- ( ph -> E. x e. P E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) )
Theorem	axtgupdim2OLD 30746	Upper dimension axiom for dimension 2, Axiom A9 of [Schwabhauser] p. 13. (Contributed by Thierry Arnoux, 29-May-2019.) (New usage is discouraged.) (Proof modification is discouraged.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> U e. P )   &    |- ( ph -> V e. P )   &    |- ( ph -> U =/= V )   &    |- ( ph -> ( X .- U ) = ( X .- V ) )   &    |- ( ph -> ( Y .- U ) = ( Y .- V ) )   &    |- ( ph -> ( Z .- U ) = ( Z .- V ) )   &    |- ( ph -> G e. TarskiG2D )   =>    |- ( ph -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) )
20.3.27.2  Outer Five Segment (not used, no need to move to main)
Syntax	cafs 30747	Declare the syntax for the outer five segment configuration.
class AFS
Definition	df-afs 30748*	The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom (axtg5seg 25364). See df-ofs 32090. Definition 2.10 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 21-Sep-2013.) (Modified by Thierry Arnoux, 15-Mar-2019.)
|- AFS = ( g e. TarskiG |-> { <. e , f >. | [. ( Base ` g ) / p ]. [. ( dist ` g ) / h ]. [. (Itv ` g ) / i ]. E. a e. p E. b e. p E. c e. p E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) ) } )
Theorem	afsval 30749*	Value of the AFS relation for a given geometry structure. (Contributed by Thierry Arnoux, 20-Mar-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   =>    |- ( ph -> (AFS ` G ) = { <. e , f >. | E. a e. P E. b e. P E. c e. P E. d e. P E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) } )
Theorem	brafs 30750	Binary relation form of the outer five segment predicate. (Contributed by Scott Fenton, 21-Sep-2013.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- O = (AFS ` G )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> X e. P )   &    |- ( ph -> Y e. P )   &    |- ( ph -> Z e. P )   &    |- ( ph -> W e. P )   =>    |- ( ph -> ( <. <. A , B >. , <. C , D >. >. O <. <. X , Y >. , <. Z , W >. >. <-> ( ( B e. ( A I C ) /\ Y e. ( X I Z ) ) /\ ( ( A .- B ) = ( X .- Y ) /\ ( B .- C ) = ( Y .- Z ) ) /\ ( ( A .- D ) = ( X .- W ) /\ ( B .- D ) = ( Y .- W ) ) ) ) )
Theorem	tg5segofs 30751	Rephrase axtg5seg 25364 using the outer five segment predicate. Theorem 2.10 of [Schwabhauser] p. 28. (Contributed by Thierry Arnoux, 23-Mar-2019.)
|- P = ( Base ` G )   &    |- .- = ( dist ` G )   &    |- I = (Itv ` G )   &    |- ( ph -> G e. TarskiG )   &    |- ( ph -> A e. P )   &    |- ( ph -> B e. P )   &    |- ( ph -> C e. P )   &    |- ( ph -> D e. P )   &    |- ( ph -> E e. P )   &    |- ( ph -> F e. P )   &    |- O = (AFS ` G )   &    |- ( ph -> H e. P )   &    |- ( ph -> I e. P )   &    |- ( ph -> <. <. A , B >. , <. C , D >. >. O <. <. E , F >. , <. H , I >. >. )   &    |- ( ph -> A =/= B )   =>    |- ( ph -> ( C .- D ) = ( H .- I ) )
20.4  Mathbox for Jonathan Ben-Naim Note: On 4-Sep-2016 and after, 745 unused theorems were deleted from this mathbox, and 359 theorems used only once or twice were merged into their referencing theorems. The originals can be recovered from set.mm versions prior to this date.
Syntax	w-bnj17 30752	Extend wff notation with the 4-way conjunction. (New usage is discouraged.)
wff ( ph /\ ps /\ ch /\ th )
Definition	df-bnj17 30753	Define the 4-way conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ( ph /\ ps /\ ch /\ th ) <-> ( ( ph /\ ps /\ ch ) /\ th ) )
Syntax	c-bnj14 30754	Extend class notation with the function giving: the class of all elements of A that are "smaller" than X according to R. (New usage is discouraged.)
class pred ( X , A , R )
Definition	df-bnj14 30755*	Define the function giving: the class of all elements of A that are "smaller" than X according to R. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- pred ( X , A , R ) = { y e. A | y R X }
Syntax	w-bnj13 30756	Extend wff notation with the following predicate: R is set-like on A. (New usage is discouraged.)
wff R Se A
Definition	df-bnj13 30757*	Define the following predicate: R is set-like on A. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( R Se A <-> A. x e. A pred ( x , A , R ) e. _V )
Syntax	w-bnj15 30758	Extend wff notation with the following predicate: R is both well-founded and set-like on A. (New usage is discouraged.)
wff R FrSe A
Definition	df-bnj15 30759	Define the following predicate: R is both well-founded and set-like on A. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( R FrSe A <-> ( R Fr A /\ R Se A ) )
Syntax	c-bnj18 30760	Extend class notation with the function giving: the transitive closure of X in A by R. (New usage is discouraged.)
class trCl ( X , A , R )
Definition	df-bnj18 30761*	Define the function giving: the transitive closure of X in A by R. This definition has been designed for facilitating verification that it is eliminable and that the $d restrictions are sound and complete. For a more readable definition see bnj882 30996. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- trCl ( X , A , R ) = U_ f e. { f | E. n e. ( om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = pred ( X , A , R ) /\ A. i e. om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) ) } U_ i e. dom f ( f ` i )
Syntax	w-bnj19 30762	Extend wff notation with the following predicate: B is transitive for A and R. (New usage is discouraged.)
wff TrFo ( B , A , R )
Definition	df-bnj19 30763*	Define the following predicate: B is transitive for A and R. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( TrFo ( B , A , R ) <-> A. x e. B pred ( x , A , R ) C_ B )
20.4.1  First-order logic and set theory
Theorem	bnj170 30764	/\-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.)
|- ( ( ph /\ ps /\ ch ) <-> ( ( ps /\ ch ) /\ ph ) )
Theorem	bnj240 30765	/\-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ps -> ps' )   &    |- ( ch -> ch' )   =>    |- ( ( ph /\ ps /\ ch ) -> ( ps' /\ ch' ) )
Theorem	bnj248 30766	/\-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ( ph /\ ps /\ ch /\ th ) <-> ( ( ( ph /\ ps ) /\ ch ) /\ th ) )
Theorem	bnj250 30767	/\-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ( ph /\ ps /\ ch /\ th ) <-> ( ph /\ ( ( ps /\ ch ) /\ th ) ) )
Theorem	bnj251 30768	/\-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ( ph /\ ps /\ ch /\ th ) <-> ( ph /\ ( ps /\ ( ch /\ th ) ) ) )
Theorem	bnj252 30769	/\-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ( ph /\ ps /\ ch /\ th ) <-> ( ph /\ ( ps /\ ch /\ th ) ) )
Theorem	bnj253 30770	/\-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ( ph /\ ps /\ ch /\ th ) <-> ( ( ph /\ ps ) /\ ch /\ th ) )
Theorem	bnj255 30771	/\-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ( ph /\ ps /\ ch /\ th ) <-> ( ph /\ ps /\ ( ch /\ th ) ) )
Theorem	bnj256 30772	/\-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ( ph /\ ps /\ ch /\ th ) <-> ( ( ph /\ ps ) /\ ( ch /\ th ) ) )
Theorem	bnj257 30773	/\-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ( ph /\ ps /\ ch /\ th ) <-> ( ph /\ ps /\ th /\ ch ) )
Theorem	bnj258 30774	/\-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ( ph /\ ps /\ ch /\ th ) <-> ( ( ph /\ ps /\ th ) /\ ch ) )
Theorem	bnj268 30775	/\-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ( ph /\ ps /\ ch /\ th ) <-> ( ph /\ ch /\ ps /\ th ) )
Theorem	bnj290 30776	/\-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ( ph /\ ps /\ ch /\ th ) <-> ( ph /\ ch /\ th /\ ps ) )
Theorem	bnj291 30777	/\-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ( ph /\ ps /\ ch /\ th ) <-> ( ( ph /\ ch /\ th ) /\ ps ) )
Theorem	bnj312 30778	/\-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ( ph /\ ps /\ ch /\ th ) <-> ( ps /\ ph /\ ch /\ th ) )
Theorem	bnj334 30779	/\-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.)
|- ( ( ph /\ ps /\ ch /\ th ) <-> ( ch /\ ph /\ ps /\ th ) )
Theorem	bnj345 30780	/\-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.)
|- ( ( ph /\ ps /\ ch /\ th ) <-> ( th /\ ph /\ ps /\ ch ) )
Theorem	bnj422 30781	/\-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.)
|- ( ( ph /\ ps /\ ch /\ th ) <-> ( ch /\ th /\ ph /\ ps ) )
Theorem	bnj432 30782	/\-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ( ph /\ ps /\ ch /\ th ) <-> ( ( ch /\ th ) /\ ( ph /\ ps ) ) )
Theorem	bnj446 30783	/\-manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ( ph /\ ps /\ ch /\ th ) <-> ( ( ps /\ ch /\ th ) /\ ph ) )
Theorem	bnj23 30784*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.)
|- B = { x e. A | -. ph }   =>    |- ( A. z e. B -. z R y -> A. w e. A ( w R y -> [. w / x ]. ph ) )
Theorem	bnj31 30785	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ph -> E. x e. A ps )   &    |- ( ps -> ch )   =>    |- ( ph -> E. x e. A ch )
Theorem	bnj62 30786*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( [. z / x ]. x Fn A <-> z Fn A )
Theorem	bnj89 30787*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- Z e. _V   =>    |- ( [. Z / y ]. E! x ph <-> E! x [. Z / y ]. ph )
Theorem	bnj90 30788*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.)
|- Y e. _V   =>    |- ( [. Y / x ]. z Fn x <-> z Fn Y )
Theorem	bnj101 30789	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- E. x ph   &    |- ( ph -> ps )   =>    |- E. x ps
Theorem	bnj105 30790	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- 1o e. _V
Theorem	bnj115 30791	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( et <-> A. n e. D ( ta -> th ) )   =>    |- ( et <-> A. n ( ( n e. D /\ ta ) -> th ) )
Theorem	bnj132 30792*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (New usage is discouraged.)
|- ( ph <-> E. x ( ps -> ch ) )   =>    |- ( ph <-> ( ps -> E. x ch ) )
Theorem	bnj133 30793	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ph <-> E. x ps )   &    |- ( ch <-> ps )   =>    |- ( ph <-> E. x ch )
Theorem	bnj142OLD 30794	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.) (Proof modification is discouraged.) Obsolete as of 29-Dec-2018. This is now incorporated into the proof of fnsnb 6432.
|- ( F Fn { A } -> ( u e. F -> u = <. A , ( F ` A ) >. ) )
Theorem	bnj145OLD 30795	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) (Proof modification is discouraged.) Obsolete as of 29-Dec-2018. This is now incorporated into the proof of fnsnb 6432.
|- A e. _V   &    |- ( F ` A ) e. _V   =>    |- ( F Fn { A } -> F = { <. A , ( F ` A ) >. } )
Theorem	bnj156 30796	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ze0 <-> ( f Fn 1o /\ ph' /\ ps' ) )   &    |- ( ze1 <-> [. g / f ]. ze0 )   &    |- ( ph1 <-> [. g / f ]. ph' )   &    |- ( ps1 <-> [. g / f ]. ps' )   =>    |- ( ze1 <-> ( g Fn 1o /\ ph1 /\ ps1 ) )
Theorem	bnj158 30797*	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- D = ( om \ { (/) } )   =>    |- ( m e. D -> E. p e. om m = suc p )
Theorem	bnj168 30798*	First-order logic and set theory. Revised to remove dependence on ax-reg 8497. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Revised by NM, 21-Dec-2016.) (New usage is discouraged.)
|- D = ( om \ { (/) } )   =>    |- ( ( n =/= 1o /\ n e. D ) -> E. m e. D n = suc m )
Theorem	bnj206 30799	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- ( ph' <-> [. M / n ]. ph )   &    |- ( ps' <-> [. M / n ]. ps )   &    |- ( ch' <-> [. M / n ]. ch )   &    |- M e. _V   =>    |- ( [. M / n ]. ( ph /\ ps /\ ch ) <-> ( ph' /\ ps' /\ ch' ) )
Theorem	bnj216 30800	First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
|- B e. _V   =>    |- ( A = suc B -> B e. A )