HomeHome Metamath Proof Explorer
Theorem List (p. 237 of 322)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Color key:    Metamath Proof Explorer  Metamath Proof Explorer
(1-21498)
  Hilbert Space Explorer  Hilbert Space Explorer
(21499-23021)
  Users' Mathboxes  Users' Mathboxes
(23022-32154)
 

Theorem List for Metamath Proof Explorer - 23601-23700   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theorempr01ssre 23601 The range of the indicator function is a subset of  RR. (Contributed by Thierry Arnoux, 14-Aug-2017.)
 |-  { 0 ,  1 }  C_  RR
 
Theoremind1 23602 Value of the indicator function where it is  1. (Contributed by Thierry Arnoux, 14-Aug-2017.)
 |-  (
 ( O  e.  V  /\  A  C_  O  /\  X  e.  A )  ->  ( ( (D7ED; `  O ) `  A ) `  X )  =  1
 )
 
Theoremind0 23603 Value of the indicator function where it is  0. (Contributed by Thierry Arnoux, 14-Aug-2017.)
 |-  (
 ( O  e.  V  /\  A  C_  O  /\  X  e.  ( O  \  A ) )  ->  ( ( (D7ED; `  O ) `  A ) `  X )  =  0
 )
 
Theoremind1a 23604 Value of the indicator function where it is  1. (Contributed by Thierry Arnoux, 22-Aug-2017.)
 |-  (
 ( O  e.  V  /\  A  C_  O  /\  X  e.  O )  ->  ( ( ( (D7ED; `  O ) `  A ) `  X )  =  1  <->  X  e.  A ) )
 
Theoremindpi1 23605 Preimage of the singleton  { 1 } by the indicator function. See i1f1lem 19044. (Contributed by Thierry Arnoux, 21-Aug-2017.)
 |-  (
 ( O  e.  V  /\  A  C_  O )  ->  ( `' ( (D7ED; `  O ) `  A ) " { 1 } )  =  A )
 
Theoremindsum 23606* Finite sum of a product with the indicator function / cross-product with the indicator function. (Contributed by Thierry Arnoux, 14-Aug-2017.)
 |-  ( ph  ->  O  e.  Fin )   &    |-  ( ph  ->  A  C_  O )   &    |-  ( ( ph  /\  x  e.  O ) 
 ->  B  e.  CC )   =>    |-  ( ph  ->  sum_ x  e.  O  ( ( ( (D7ED; `  O ) `  A ) `  x )  x.  B )  =  sum_ x  e.  A  B )
 
Theoremindf1o 23607 The bijection between a power set and the set of indicator functions. (Contributed by Thierry Arnoux, 14-Aug-2017.)
 |-  ( O  e.  V  ->  (D7ED; `  O ) : ~P O
 -1-1-onto-> ( { 0 ,  1 }  ^m  O ) )
 
Theoremindpreima 23608 A function with range  { 0 ,  1 } as an indicator of the preimage of  { 1 } (Contributed by Thierry Arnoux, 23-Aug-2017.)
 |-  (
 ( O  e.  V  /\  F : O --> { 0 ,  1 } )  ->  F  =  ( (D7ED; `  O ) `  ( `' F " { 1 } ) ) )
 
Theoremindf1ofs 23609* The bijection between finite subsets and the indicator functions with finite support. (Contributed by Thierry Arnoux, 22-Aug-2017.)
 |-  ( O  e.  V  ->  ( (D7ED; `  O )  |` 
 Fin ) : ( ~P O  i^i  Fin )
 -1-1-onto-> { f  e.  ( { 0 ,  1 }  ^m  O )  |  ( `' f " { 1 } )  e.  Fin } )
 
18.3.41  Probability Theory
 
Syntaxcprb 23610 Extend class notation to include the class of probability measures.
 class Prob
 
Definitiondf-prob 23611 Define the class of probability measures as the set of measures with total measure 1. (Contributed by Thierry Arnoux, 14-Sep-2016.)
 |- Prob  =  { p  e.  U. ran measures  |  ( p `  U. dom  p )  =  1 }
 
Theoremelprob 23612 The property of being a probability measure (Contributed by Thierry Arnoux, 8-Dec-2016.)
 |-  ( P  e. Prob  <->  ( P  e.  U.
 ran measures  /\  ( P `  U.
 dom  P )  =  1 ) )
 
Theoremdomprobmeas 23613 A probability measure is a measure on its domain. (Contributed by Thierry Arnoux, 23-Dec-2016.)
 |-  ( P  e. Prob  ->  P  e.  (measures `  dom  P ) )
 
Theoremdomprobsiga 23614 The domain of a probability measure is a sigma-algebra. (Contributed by Thierry Arnoux, 23-Dec-2016.)
 |-  ( P  e. Prob  ->  dom  P  e.  U. ran sigAlgebra )
 
Theoremprobtot 23615 The Probbiliy of the universe set is 1 (Second axiom of Kolmogorov) (Contributed by Thierry Arnoux, 8-Dec-2016.)
 |-  ( P  e. Prob  ->  ( P `
  U. dom  P )  =  1 )
 
Theoremprob01 23616 A Probbiliy is bounded in [ 0 , 1 ] (First axiom of Kolmogorov) (Contributed by Thierry Arnoux, 25-Dec-2016.)
 |-  (
 ( P  e. Prob  /\  A  e.  dom  P )  ->  ( P `  A )  e.  ( 0 [,] 1 ) )
 
Theoremprobnul 23617 The Probbiliy of the empty event set is 0. (Contributed by Thierry Arnoux, 25-Dec-2016.)
 |-  ( P  e. Prob  ->  ( P `
  (/) )  =  0 )
 
Theoremunveldomd 23618 The universe is an element of the domain of the probability, the universe (entire probability space) being  U.
dom  P in our construction. (Contributed by Thierry Arnoux, 22-Jan-2017.)
 |-  ( ph  ->  P  e. Prob )   =>    |-  ( ph  ->  U. dom  P  e.  dom 
 P )
 
Theoremunveldom 23619 The universe is an element of the domain of the probability, the universe (entire probability space) being  U.
dom  P in our construction. (Contributed by Thierry Arnoux, 22-Jan-2017.)
 |-  ( P  e. Prob  ->  U. dom  P  e.  dom  P )
 
Theoremnuleldmp 23620 The empty set is an element of the domain of the probability. (Contributed by Thierry Arnoux, 22-Jan-2017.)
 |-  ( P  e. Prob  ->  (/)  e.  dom  P )
 
Theoremprobcun 23621* The probability of the union of a countable disjoint set of events is the sum of their probabilities. (Third axiom of Kolmogorov) Here, the  sum_ construct cannot be used as it can handle infinite indexing set only if they are subsets of 
ZZ, which is not the case here. (Contributed by Thierry Arnoux, 25-Dec-2016.)
 |-  (
 ( P  e. Prob  /\  A  e.  ~P dom  P  /\  ( A  ~<_  om  /\ Disj  x  e.  A x ) ) 
 ->  ( P `  U. A )  = Σ* x  e.  A ( P `  x ) )
 
Theoremprobun 23622 The probability of the union two incompatible events is the sum of their probabilities. (Contributed by Thierry Arnoux, 25-Dec-2016.)
 |-  (
 ( P  e. Prob  /\  A  e.  dom  P  /\  B  e.  dom  P )  ->  ( ( A  i^i  B )  =  (/)  ->  ( P `  ( A  u.  B ) )  =  ( ( P `  A )  +  ( P `  B ) ) ) )
 
Theoremprobdif 23623 The probabiliy of the difference of two event sets (Contributed by Thierry Arnoux, 12-Dec-2016.)
 |-  (
 ( P  e. Prob  /\  A  e.  dom  P  /\  B  e.  dom  P )  ->  ( P `  ( A 
 \  B ) )  =  ( ( P `
  A )  -  ( P `  ( A  i^i  B ) ) ) )
 
Theoremprobinc 23624 A probabiliy law is increasing with regard to event set inclusion. (Contributed by Thierry Arnoux, 10-Feb-2017.)
 |-  (
 ( ( P  e. Prob  /\  A  e.  dom  P  /\  B  e.  dom  P )  /\  A  C_  B )  ->  ( P `  A )  <_  ( P `
  B ) )
 
Theoremprobdsb 23625 The probability of the complement of a set. That is, the probability that the event  A does not occur. (Contributed by Thierry Arnoux, 15-Dec-2016.)
 |-  (
 ( P  e. Prob  /\  A  e.  dom  P )  ->  ( P `  ( U. dom  P  \  A ) )  =  ( 1  -  ( P `  A ) ) )
 
Theoremprobmeasd 23626 A probability measure is a measure. (Contributed by Thierry Arnoux, 2-Feb-2017.)
 |-  ( ph  ->  P  e. Prob )   =>    |-  ( ph  ->  P  e.  U. ran measures )
 
Theoremprobvalrnd 23627 The value of a probability is a a real number. (Contributed by Thierry Arnoux, 2-Feb-2017.)
 |-  ( ph  ->  P  e. Prob )   &    |-  ( ph  ->  A  e.  dom  P )   =>    |-  ( ph  ->  ( P `  A )  e. 
 RR )
 
Theoremprobtotrnd 23628 The probability of the universe set is finite. (Contributed by Thierry Arnoux, 2-Feb-2017.)
 |-  ( ph  ->  P  e. Prob )   =>    |-  ( ph  ->  ( P `  U.
 dom  P )  e.  RR )
 
Theoremtotprobd 23629* Law of total probability, deduction form. (Contributed by Thierry Arnoux, 25-Dec-2016.)
 |-  ( ph  ->  P  e. Prob )   &    |-  ( ph  ->  A  e.  dom  P )   &    |-  ( ph  ->  B  e.  ~P dom  P )   &    |-  ( ph  ->  U. B  =  U. dom  P )   &    |-  ( ph  ->  B  ~<_  om )   &    |-  ( ph  -> Disj  b  e.  B b )   =>    |-  ( ph  ->  ( P `  A )  = Σ* b  e.  B ( P `
  ( b  i^i 
 A ) ) )
 
Theoremtotprob 23630* Law of total probability (Contributed by Thierry Arnoux, 25-Dec-2016.)
 |-  (
 ( P  e. Prob  /\  A  e.  dom  P  /\  ( U. B  =  U. dom  P  /\  B  e.  ~P
 dom  P  /\  ( B  ~<_ 
 om  /\ Disj  b  e.  B b ) ) ) 
 ->  ( P `  A )  = Σ* b  e.  B ( P `  ( b  i^i  A ) ) )
 
TheoremprobfinmeasbOLD 23631* Build a probability measure from a finite measure (Contributed by Thierry Arnoux, 17-Dec-2016.)
 |-  (
 ( M  e.  (measures `  S )  /\  ( M `  U. S )  e.  RR+ )  ->  ( x  e.  S  |->  ( ( M `  x ) /𝑒  ( M `  U. S ) ) )  e. Prob
 )
 
Theoremprobfinmeasb 23632 Build a probability measure from a finite measure (Contributed by Thierry Arnoux, 31-Jan-2017.)
 |-  (
 ( M  e.  (measures `  S )  /\  ( M `  U. S )  e.  RR+ )  ->  ( M𝑓/𝑐 /𝑒  ( M ` 
 U. S ) )  e. Prob )
 
Theoremprobmeasb 23633* Build a probability from a measure and a set with finite measure (Contributed by Thierry Arnoux, 25-Dec-2016.)
 |-  (
 ( M  e.  (measures `  S )  /\  A  e.  S  /\  ( M `
  A )  e.  RR+ )  ->  ( x  e.  S  |->  ( ( M `  ( x  i^i  A ) ) 
 /  ( M `  A ) ) )  e. Prob )
 
18.3.42  Conditional Probabilities
 
Syntaxccprob 23634 Extends class notation with the conditional probability builder.
 class cprob
 
Definitiondf-cndprob 23635* Define the conditional probability. (Contributed by Thierry Arnoux, 14-Sep-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
 |- cprob  =  ( p  e. Prob  |->  ( a  e.  dom  p ,  b  e.  dom  p  |->  ( ( p `  (
 a  i^i  b )
 )  /  ( p `  b ) ) ) )
 
Theoremcndprobval 23636 The value of the conditional probability , i.e. the probability for the event  A, given  B, under the probability law  P. (Contributed by Thierry Arnoux, 21-Jan-2017.)
 |-  (
 ( P  e. Prob  /\  A  e.  dom  P  /\  B  e.  dom  P )  ->  ( (cprob `  P ) `  <. A ,  B >. )  =  ( ( P `  ( A  i^i  B ) ) 
 /  ( P `  B ) ) )
 
Theoremcndprobin 23637 An identity linking conditional probability and intersection. (Contributed by Thierry Arnoux, 13-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
 |-  (
 ( ( P  e. Prob  /\  A  e.  dom  P  /\  B  e.  dom  P )  /\  ( P `  B )  =/=  0
 )  ->  ( (
 (cprob `  P ) `  <. A ,  B >. )  x.  ( P `
  B ) )  =  ( P `  ( A  i^i  B ) ) )
 
Theoremcndprob01 23638 The conditional probability has values in  [ 0 ,  1 ]. (Contributed by Thierry Arnoux, 13-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
 |-  (
 ( ( P  e. Prob  /\  A  e.  dom  P  /\  B  e.  dom  P )  /\  ( P `  B )  =/=  0
 )  ->  ( (cprob `  P ) `  <. A ,  B >. )  e.  (
 0 [,] 1 ) )
 
Theoremcndprobtot 23639 The conditional probability given a certain event is one. (Contributed by Thierry Arnoux, 20-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
 |-  (
 ( P  e. Prob  /\  A  e.  dom  P  /\  ( P `  A )  =/=  0 )  ->  (
 (cprob `  P ) `  <. U. dom  P ,  A >. )  =  1 )
 
Theoremcndprobnul 23640 The conditional probability given empty event is zero. (Contributed by Thierry Arnoux, 20-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
 |-  (
 ( P  e. Prob  /\  A  e.  dom  P  /\  ( P `  A )  =/=  0 )  ->  (
 (cprob `  P ) `  <. (/) ,  A >. )  =  0 )
 
Theoremcndprobprob 23641* The conditional probability defines a probability law. (Contributed by Thierry Arnoux, 23-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
 |-  (
 ( P  e. Prob  /\  B  e.  dom  P  /\  ( P `  B )  =/=  0 )  ->  (
 a  e.  dom  P  |->  ( (cprob `  P ) `  <. a ,  B >. ) )  e. Prob )
 
Theorembayesth 23642 Bayes Theorem (Contributed by Thierry Arnoux, 20-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.)
 |-  (
 ( ( P  e. Prob  /\  A  e.  dom  P  /\  B  e.  dom  P )  /\  ( P `  A )  =/=  0  /\  ( P `  B )  =/=  0 )  ->  ( (cprob `  P ) `  <. A ,  B >. )  =  ( ( ( (cprob `  P ) `  <. B ,  A >. )  x.  ( P `
  A ) ) 
 /  ( P `  B ) ) )
 
18.3.43  Real Valued Random Variables
 
Syntaxcrrv 23643 Extend class notation with the class of real valued random variables.
 class rRndVar
 
Definitiondf-rrv 23644 In its generic definition, a random variable is a measurable function from a probability space to a Borel set. Here, we specifically target real-valued random variables, i.e. measurable function from a probability space to the Borel sigma algebra on the set of real numbers. (Contributed by Thierry Arnoux, 20-Sep-2016.) (Revised by Thierry Arnoux, 25-Jan-2017.)
 |- rRndVar  =  ( p  e. Prob  |->  (MblFnM `  <. dom  p , 𝔅 >.
 ) )
 
Theoremrrvmbfm 23645 A real-valued random variable is a measurable function from its sample space to the Borel Sigma Algebra. (Contributed by Thierry Arnoux, 25-Jan-2017.)
 |-  ( ph  ->  P  e. Prob )   =>    |-  ( ph  ->  ( X  e.  (rRndVar `  P )  <->  X  e.  (MblFnM ` 
 <. dom  P , 𝔅
 >. ) ) )
 
Theoremisrrvv 23646* Elementhood to the set of real-valued random variables with respect to the probability  P. (Contributed by Thierry Arnoux, 25-Jan-2017.)
 |-  ( ph  ->  P  e. Prob )   =>    |-  ( ph  ->  ( X  e.  (rRndVar `  P )  <->  ( X : U. dom  P --> RR  /\  A. y  e. 𝔅  ( `' X "
 y )  e.  dom  P ) ) )
 
Theoremrrvvf 23647 A real-valued random variable is a function. (Contributed by Thierry Arnoux, 25-Jan-2017.)
 |-  ( ph  ->  P  e. Prob )   &    |-  ( ph  ->  X  e.  (rRndVar `  P ) )   =>    |-  ( ph  ->  X : U. dom  P --> RR )
 
Theoremrrvfn 23648 A real-valued random variable is a function over the universe. (Contributed by Thierry Arnoux, 25-Jan-2017.)
 |-  ( ph  ->  P  e. Prob )   &    |-  ( ph  ->  X  e.  (rRndVar `  P ) )   =>    |-  ( ph  ->  X  Fn  U. dom  P )
 
Theoremrrvdm 23649 The domain of a random variable is the universe. (Contributed by Thierry Arnoux, 25-Jan-2017.)
 |-  ( ph  ->  P  e. Prob )   &    |-  ( ph  ->  X  e.  (rRndVar `  P ) )   =>    |-  ( ph  ->  dom 
 X  =  U. dom  P )
 
Theoremrrvrnss 23650 The range of a random variable as a subset of  RR. (Contributed by Thierry Arnoux, 6-Feb-2017.)
 |-  ( ph  ->  P  e. Prob )   &    |-  ( ph  ->  X  e.  (rRndVar `  P ) )   =>    |-  ( ph  ->  ran 
 X  C_  RR )
 
Theoremrrvf2 23651 A real-valued random variable is a function. (Contributed by Thierry Arnoux, 25-Jan-2017.)
 |-  ( ph  ->  P  e. Prob )   &    |-  ( ph  ->  X  e.  (rRndVar `  P ) )   =>    |-  ( ph  ->  X : dom  X --> RR )
 
Theoremrrvdmss 23652 The domain of a random variable. This is useful to shorten proofs. (Contributed by Thierry Arnoux, 25-Jan-2017.)
 |-  ( ph  ->  P  e. Prob )   &    |-  ( ph  ->  X  e.  (rRndVar `  P ) )   =>    |-  ( ph  ->  U.
 dom  P  C_  dom  X )
 
Theoremrrvfinvima 23653* For a real-value random variable  X, any open interval in 
RR is the image of a measurable set. (Contributed by Thierry Arnoux, 25-Jan-2017.)
 |-  ( ph  ->  P  e. Prob )   &    |-  ( ph  ->  X  e.  (rRndVar `  P ) )   =>    |-  ( ph  ->  A. y  e. 𝔅  ( `' X "
 y )  e.  dom  P )
 
Theorem0rrv 23654* The constant function equal to zero is a random variable. (Contributed by Thierry Arnoux, 16-Jan-2017.) (Revised by Thierry Arnoux, 30-Jan-2017.)
 |-  ( ph  ->  P  e. Prob )   =>    |-  ( ph  ->  ( x  e. 
 U. dom  P  |->  0 )  e.  (rRndVar `  P ) )
 
Theoremrrvmulc 23655 A random variable multiplied by a constant is a random variable. (Contributed by Thierry Arnoux, 17-Jan-2017.) (Revised by Thierry Arnoux, 22-May-2017.)
 |-  ( ph  ->  P  e. Prob )   &    |-  ( ph  ->  X  e.  (rRndVar `  P ) )   &    |-  ( ph  ->  C  e.  RR )   =>    |-  ( ph  ->  ( X𝑓/𝑐  x.  C )  e.  (rRndVar `  P ) )
 
18.3.44  Preimage set mapping operator
 
Syntaxcorvc 23656 Extend class notation to include the preimage set mapping operator.
 classRV/𝑐 R
 
Definitiondf-orvc 23657* Define the preimage set mapping operator. In probability theory, the notation  P ( X  =  A ) denotes the probability that a random variable  X takes the value  A. We introduce here an operator which enables to write this in Metamath as  ( P `  ( XRV/𝑐  _I  A ) ), and keep a similar notation. Because with this notation  ( XRV/𝑐  _I  A ) is a set, we can also apply it to conditional probabilities, like in  ( P `  ( XRV/𝑐  _I  A )  |  ( YRV/𝑐  _I  B ) ) ).

The oRVC operator transforms a relation  R into an operation taking a random variable  X and a constant  C, and returning the preimage through  X of the equivalence class of  C.

The most commonly used relations are: - equality:  { X  =  A } as  ( XRV/𝑐  _I  A ) cf. ideq 4836- elementhood:  { X  e.  A } as  ( XRV/𝑐  _E  A ) cf. epel 4308- less-than:  { X  <_  A } as  ( XRV/𝑐  <_  A )

Even though it is primarily designed to be used within probability theory and with random variables, this operator is defined on generic functions, and could be used in other fields, e.g. for continuous functions. (Contributed by Thierry Arnoux, 15-Jan-2017.)

 |-RV/𝑐 R  =  ( x  e.  { x  |  Fun  x } ,  a  e.  _V  |->  ( `' x " { y  |  y R a } )
 )
 
Theoremorvcval 23658* Value of the preimage mapping operator applied on a given random variable and constant (Contributed by Thierry Arnoux, 19-Jan-2017.)
 |-  ( ph  ->  Fun  X )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  A  e.  W )   =>    |-  ( ph  ->  ( XRV/𝑐 R A )  =  ( `' X " { y  |  y R A }
 ) )
 
Theoremorvcval2 23659* Another way to express the value of the preimage mapping operator (Contributed by Thierry Arnoux, 19-Jan-2017.)
 |-  ( ph  ->  Fun  X )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  A  e.  W )   =>    |-  ( ph  ->  ( XRV/𝑐 R A )  =  {
 z  e.  dom  X  |  ( X `  z
 ) R A }
 )
 
Theoremelorvc 23660* Elementhood of a preimage (Contributed by Thierry Arnoux, 21-Jan-2017.)
 |-  ( ph  ->  Fun  X )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  A  e.  W )   =>    |-  ( ( ph  /\  z  e.  dom  X )  ->  ( z  e.  ( XRV/𝑐 R A )  <->  ( X `  z ) R A ) )
 
Theoremorvcval4 23661* The value of the preimage mapping operator can be restricted to preimages in the base set of the topology. Cf. orvcval 23658 (Contributed by Thierry Arnoux, 21-Jan-2017.)
 |-  ( ph  ->  S  e.  U. ran sigAlgebra )   &    |-  ( ph  ->  J  e.  Top )   &    |-  ( ph  ->  X  e.  (MblFnM ` 
 <. S ,  (sigaGen `  J ) >. ) )   &    |-  ( ph  ->  A  e.  V )   =>    |-  ( ph  ->  ( XRV/𝑐 R A )  =  ( `' X " { y  e.  U. J  |  y R A } )
 )
 
Theoremorvcoel 23662* If the relation produces open sets, preimage maps by a measurable function are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017.)
 |-  ( ph  ->  S  e.  U. ran sigAlgebra )   &    |-  ( ph  ->  J  e.  Top )   &    |-  ( ph  ->  X  e.  (MblFnM ` 
 <. S ,  (sigaGen `  J ) >. ) )   &    |-  ( ph  ->  A  e.  V )   &    |-  ( ph  ->  { y  e.  U. J  |  y R A }  e.  J )   =>    |-  ( ph  ->  ( XRV/𝑐 R A )  e.  S )
 
Theoremorvccel 23663* If the relation produces closed sets, preimage maps by a measurable function are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017.)
 |-  ( ph  ->  S  e.  U. ran sigAlgebra )   &    |-  ( ph  ->  J  e.  Top )   &    |-  ( ph  ->  X  e.  (MblFnM ` 
 <. S ,  (sigaGen `  J ) >. ) )   &    |-  ( ph  ->  A  e.  V )   &    |-  ( ph  ->  { y  e.  U. J  |  y R A }  e.  ( Clsd `  J )
 )   =>    |-  ( ph  ->  ( XRV/𝑐 R A )  e.  S )
 
Theoremelorrvc 23664* Elementhood of a preimage for a real-valued random variable. (Contributed by Thierry Arnoux, 21-Jan-2017.)
 |-  ( ph  ->  P  e. Prob )   &    |-  ( ph  ->  X  e.  (rRndVar `  P ) )   &    |-  ( ph  ->  A  e.  V )   =>    |-  ( ( ph  /\  z  e.  U. dom  P ) 
 ->  ( z  e.  ( XRV/𝑐 R A )  <->  ( X `  z ) R A ) )
 
Theoremorrvcval4 23665* The value of the preimage mapping operator can be restricted to preimages of subsets of RR. (Contributed by Thierry Arnoux, 21-Jan-2017.)
 |-  ( ph  ->  P  e. Prob )   &    |-  ( ph  ->  X  e.  (rRndVar `  P ) )   &    |-  ( ph  ->  A  e.  V )   =>    |-  ( ph  ->  ( XRV/𝑐 R A )  =  ( `' X " { y  e.  RR  |  y R A } ) )
 
Theoremorrvcoel 23666* If the relation produces open sets, preimage maps of a random variable are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017.)
 |-  ( ph  ->  P  e. Prob )   &    |-  ( ph  ->  X  e.  (rRndVar `  P ) )   &    |-  ( ph  ->  A  e.  V )   &    |-  ( ph  ->  { y  e.  RR  |  y R A }  e.  ( topGen `
  ran  (,) ) )   =>    |-  ( ph  ->  ( XRV/𝑐 R A )  e.  dom  P )
 
Theoremorrvccel 23667* If the relation produces closed sets, preimage maps are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017.)
 |-  ( ph  ->  P  e. Prob )   &    |-  ( ph  ->  X  e.  (rRndVar `  P ) )   &    |-  ( ph  ->  A  e.  V )   &    |-  ( ph  ->  { y  e.  RR  |  y R A }  e.  ( Clsd `  ( topGen `  ran  (,) ) ) )   =>    |-  ( ph  ->  ( XRV/𝑐 R A )  e.  dom  P )
 
Theoremorvcgteel 23668 Preimage maps produced by the "greater than or equal" relation are measurable sets. (Contributed by Thierry Arnoux, 5-Feb-2017.)
 |-  ( ph  ->  P  e. Prob )   &    |-  ( ph  ->  X  e.  (rRndVar `  P ) )   &    |-  ( ph  ->  A  e.  RR )   =>    |-  ( ph  ->  ( XRV/𝑐 `' 
 <_  A )  e.  dom  P )
 
18.3.45  Distribution Functions
 
Theoremorvcelval 23669 Preimage maps produced by the "elementhood" relation (Contributed by Thierry Arnoux, 6-Feb-2017.)
 |-  ( ph  ->  P  e. Prob )   &    |-  ( ph  ->  X  e.  (rRndVar `  P ) )   &    |-  ( ph  ->  A  e. 𝔅 )   =>    |-  ( ph  ->  ( XRV/𝑐  _E  A )  =  ( `' X " A ) )
 
Theoremorvcelel 23670 Preimage maps produced by the "elementhood" relation are measurable sets. (Contributed by Thierry Arnoux, 5-Feb-2017.)
 |-  ( ph  ->  P  e. Prob )   &    |-  ( ph  ->  X  e.  (rRndVar `  P ) )   &    |-  ( ph  ->  A  e. 𝔅 )   =>    |-  ( ph  ->  ( XRV/𝑐  _E  A )  e.  dom  P )
 
Theoremdstrvval 23671* The value of the distribution of a random variable. (Contributed by Thierry Arnoux, 9-Feb-2017.)
 |-  ( ph  ->  P  e. Prob )   &    |-  ( ph  ->  X  e.  (rRndVar `  P ) )   &    |-  ( ph  ->  D  =  ( a  e. 𝔅 
 |->  ( P `  ( XRV/𝑐  _E  a ) ) ) )   &    |-  ( ph  ->  A  e. 𝔅 )   =>    |-  ( ph  ->  ( D `  A )  =  ( P `  ( `' X " A ) ) )
 
Theoremdstrvprob 23672* The distribution of a random variable is a probability law (TODO: could be shortened using dstrvval 23671) (Contributed by Thierry Arnoux, 10-Feb-2017.)
 |-  ( ph  ->  P  e. Prob )   &    |-  ( ph  ->  X  e.  (rRndVar `  P ) )   &    |-  ( ph  ->  D  =  ( a  e. 𝔅 
 |->  ( P `  ( XRV/𝑐  _E  a ) ) ) )   =>    |-  ( ph  ->  D  e. Prob )
 
18.3.46  Cumulative Distribution Functions
 
Theoremorvclteel 23673 Preimage maps produced by the "lower than or equal" relation are measurable sets. (Contributed by Thierry Arnoux, 4-Feb-2017.)
 |-  ( ph  ->  P  e. Prob )   &    |-  ( ph  ->  X  e.  (rRndVar `  P ) )   &    |-  ( ph  ->  A  e.  RR )   =>    |-  ( ph  ->  ( XRV/𝑐  <_  A )  e.  dom  P )
 
Theoremdstfrvel 23674 Elementhood of preimage maps produced by the "lower than or equal" relation. (Contributed by Thierry Arnoux, 13-Feb-2017.)
 |-  ( ph  ->  P  e. Prob )   &    |-  ( ph  ->  X  e.  (rRndVar `  P ) )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  U. dom  P )   &    |-  ( ph  ->  ( X `  B )  <_  A )   =>    |-  ( ph  ->  B  e.  ( XRV/𝑐  <_  A ) )
 
Theoremdstfrvunirn 23675* The limit of all preimage maps by the "lower than or equal" relation is the universe. (Contributed by Thierry Arnoux, 12-Feb-2017.)
 |-  ( ph  ->  P  e. Prob )   &    |-  ( ph  ->  X  e.  (rRndVar `  P ) )   =>    |-  ( ph  ->  U.
 ran  ( n  e. 
 NN  |->  ( XRV/𝑐  <_  n ) )  = 
 U. dom  P )
 
Theoremorvclteinc 23676 Preimage maps produced by the "lower than or equal" relation are increasing. (Contributed by Thierry Arnoux, 11-Feb-2017.)
 |-  ( ph  ->  P  e. Prob )   &    |-  ( ph  ->  X  e.  (rRndVar `  P ) )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A 
 <_  B )   =>    |-  ( ph  ->  ( XRV/𝑐  <_  A )  C_  ( XRV/𝑐  <_  B ) )
 
Theoremdstfrvinc 23677* A cumulative distribution function is non-decreasing. (Contributed by Thierry Arnoux, 11-Feb-2017.)
 |-  ( ph  ->  P  e. Prob )   &    |-  ( ph  ->  X  e.  (rRndVar `  P ) )   &    |-  ( ph  ->  F  =  ( x  e.  RR  |->  ( P `  ( XRV/𝑐  <_  x ) ) ) )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <_  B )   =>    |-  ( ph  ->  ( F `  A )  <_  ( F `  B ) )
 
Theoremdstfrvclim1 23678* The limit of the cumulative distribution function is one. (Contributed by Thierry Arnoux, 12-Feb-2017.) (Revised by Thierry Arnoux, 11-Jul-2017.)
 |-  ( ph  ->  P  e. Prob )   &    |-  ( ph  ->  X  e.  (rRndVar `  P ) )   &    |-  ( ph  ->  F  =  ( x  e.  RR  |->  ( P `  ( XRV/𝑐  <_  x ) ) ) )   =>    |-  ( ph  ->  F  ~~>  1 )
 
18.3.47  Probabilities - example
 
Theoremcoinfliplem 23679 Division in the extended real numbers can be used for the coin-flip example. (Contributed by Thierry Arnoux, 15-Jan-2017.)
 |-  H  e.  _V   &    |-  T  e.  _V   &    |-  H  =/=  T   &    |-  P  =  ( ( #  |`  ~P { H ,  T }
 )𝑓/𝑐  / 
 2 )   &    |-  X  =  { <. H ,  1 >. ,  <. T ,  0
 >. }   =>    |-  P  =  ( ( #  |`  ~P { H ,  T } )𝑓/𝑐 /𝑒  2 )
 
Theoremcoinflipprob 23680 The  P we defined for coin-flip is a probability law. (Contributed by Thierry Arnoux, 15-Jan-2017.)
 |-  H  e.  _V   &    |-  T  e.  _V   &    |-  H  =/=  T   &    |-  P  =  ( ( #  |`  ~P { H ,  T }
 )𝑓/𝑐  / 
 2 )   &    |-  X  =  { <. H ,  1 >. ,  <. T ,  0
 >. }   =>    |-  P  e. Prob
 
Theoremcoinflipspace 23681 The space of our coin-flip probability (Contributed by Thierry Arnoux, 15-Jan-2017.)
 |-  H  e.  _V   &    |-  T  e.  _V   &    |-  H  =/=  T   &    |-  P  =  ( ( #  |`  ~P { H ,  T }
 )𝑓/𝑐  / 
 2 )   &    |-  X  =  { <. H ,  1 >. ,  <. T ,  0
 >. }   =>    |- 
 dom  P  =  ~P { H ,  T }
 
Theoremcoinflipuniv 23682 The universe of our coin-flip probability is  { H ,  T }. (Contributed by Thierry Arnoux, 15-Jan-2017.)
 |-  H  e.  _V   &    |-  T  e.  _V   &    |-  H  =/=  T   &    |-  P  =  ( ( #  |`  ~P { H ,  T }
 )𝑓/𝑐  / 
 2 )   &    |-  X  =  { <. H ,  1 >. ,  <. T ,  0
 >. }   =>    |- 
 U. dom  P  =  { H ,  T }
 
Theoremcoinfliprv 23683 The  X we defined for coin-flip is a random variable. (Contributed by Thierry Arnoux, 12-Jan-2017.)
 |-  H  e.  _V   &    |-  T  e.  _V   &    |-  H  =/=  T   &    |-  P  =  ( ( #  |`  ~P { H ,  T }
 )𝑓/𝑐  / 
 2 )   &    |-  X  =  { <. H ,  1 >. ,  <. T ,  0
 >. }   =>    |-  X  e.  (rRndVar `  P )
 
Theoremcoinflippv 23684 The probability of heads is one-half. (Contributed by Thierry Arnoux, 15-Jan-2017.)
 |-  H  e.  _V   &    |-  T  e.  _V   &    |-  H  =/=  T   &    |-  P  =  ( ( #  |`  ~P { H ,  T }
 )𝑓/𝑐  / 
 2 )   &    |-  X  =  { <. H ,  1 >. ,  <. T ,  0
 >. }   =>    |-  ( P `  { H } )  =  (
 1  /  2 )
 
Theoremcoinflippvt 23685 The probability of tails is one-half. (Contributed by Thierry Arnoux, 5-Feb-2017.)
 |-  H  e.  _V   &    |-  T  e.  _V   &    |-  H  =/=  T   &    |-  P  =  ( ( #  |`  ~P { H ,  T }
 )𝑓/𝑐  / 
 2 )   &    |-  X  =  { <. H ,  1 >. ,  <. T ,  0
 >. }   =>    |-  ( P `  { T } )  =  (
 1  /  2 )
 
18.4  Mathbox for Mario Carneiro
 
18.4.1  Miscellaneous stuff
 
Theoremquartfull 23686 The quartic equation, written out in full. This actually makes a fairly good Metamath stress test. Note that the length of this formula could be shortened significantly if the intermediate expressions were expanded and simplified, but it's not like this theorem will be used anyway. (Contributed by Mario Carneiro, 6-May-2015.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  D  e.  CC )   &    |-  ( ph  ->  X  e.  CC )   &    |-  ( ph  ->  ( ( ( ( (
 -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) )  =/=  0 )   &    |-  ( ph  ->  -u ( ( ( ( 2  x.  ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) )  +  ( ( ( ( ( -u (
 2  x.  ( ( B  -  ( ( 3  /  8 )  x.  ( A ^
 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) )  +  ( ( ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 2 )  +  (; 1 2  x.  (
 ( D  -  (
 ( C  x.  A )  /  4 ) )  +  ( ( ( ( A ^ 2
 )  x.  B ) 
 / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) )  /  ( ( ( ( ( -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) ) )  /  3
 )  =/=  0 )   =>    |-  ( ph  ->  ( ( ( ( X ^ 4
 )  +  ( A  x.  ( X ^
 3 ) ) )  +  ( ( B  x.  ( X ^
 2 ) )  +  ( ( C  x.  X )  +  D ) ) )  =  0  <->  ( ( X  =  ( ( -u ( A  /  4
 )  -  ( ( sqr `  -u ( ( ( ( 2  x.  ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) )  +  (
 ( ( ( (
 -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) )  +  ( ( ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 2 )  +  (; 1 2  x.  (
 ( D  -  (
 ( C  x.  A )  /  4 ) )  +  ( ( ( ( A ^ 2
 )  x.  B ) 
 / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) )  /  ( ( ( ( ( -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) ) )  /  3
 ) )  /  2
 ) )  +  ( sqr `  ( ( -u ( ( ( sqr `  -u ( ( ( ( 2  x.  ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) )  +  ( ( ( ( ( -u (
 2  x.  ( ( B  -  ( ( 3  /  8 )  x.  ( A ^
 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) )  +  ( ( ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 2 )  +  (; 1 2  x.  (
 ( D  -  (
 ( C  x.  A )  /  4 ) )  +  ( ( ( ( A ^ 2
 )  x.  B ) 
 / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) )  /  ( ( ( ( ( -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) ) )  /  3
 ) )  /  2
 ) ^ 2 )  -  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  / 
 2 ) )  +  ( ( ( ( C  -  ( ( A  x.  B ) 
 /  2 ) )  +  ( ( A ^ 3 )  / 
 8 ) )  / 
 4 )  /  (
 ( sqr `  -u ( ( ( ( 2  x.  ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) )  +  (
 ( ( ( (
 -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) )  +  ( ( ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 2 )  +  (; 1 2  x.  (
 ( D  -  (
 ( C  x.  A )  /  4 ) )  +  ( ( ( ( A ^ 2
 )  x.  B ) 
 / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) )  /  ( ( ( ( ( -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) ) )  /  3
 ) )  /  2
 ) ) ) ) )  \/  X  =  ( ( -u ( A  /  4 )  -  ( ( sqr `  -u (
 ( ( ( 2  x.  ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) )  +  (
 ( ( ( (
 -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) )  +  ( ( ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 2 )  +  (; 1 2  x.  (
 ( D  -  (
 ( C  x.  A )  /  4 ) )  +  ( ( ( ( A ^ 2
 )  x.  B ) 
 / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) )  /  ( ( ( ( ( -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) ) )  /  3
 ) )  /  2
 ) )  -  ( sqr `  ( ( -u ( ( ( sqr `  -u ( ( ( ( 2  x.  ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) )  +  ( ( ( ( ( -u (
 2  x.  ( ( B  -  ( ( 3  /  8 )  x.  ( A ^
 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) )  +  ( ( ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 2 )  +  (; 1 2  x.  (
 ( D  -  (
 ( C  x.  A )  /  4 ) )  +  ( ( ( ( A ^ 2
 )  x.  B ) 
 / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) )  /  ( ( ( ( ( -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) ) )  /  3
 ) )  /  2
 ) ^ 2 )  -  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  / 
 2 ) )  +  ( ( ( ( C  -  ( ( A  x.  B ) 
 /  2 ) )  +  ( ( A ^ 3 )  / 
 8 ) )  / 
 4 )  /  (
 ( sqr `  -u ( ( ( ( 2  x.  ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) )  +  (
 ( ( ( (
 -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) )  +  ( ( ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 2 )  +  (; 1 2  x.  (
 ( D  -  (
 ( C  x.  A )  /  4 ) )  +  ( ( ( ( A ^ 2
 )  x.  B ) 
 / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) )  /  ( ( ( ( ( -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) ) )  /  3
 ) )  /  2
 ) ) ) ) ) )  \/  ( X  =  ( ( -u ( A  /  4
 )  +  ( ( sqr `  -u ( ( ( ( 2  x.  ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) )  +  (
 ( ( ( (
 -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) )  +  ( ( ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 2 )  +  (; 1 2  x.  (
 ( D  -  (
 ( C  x.  A )  /  4 ) )  +  ( ( ( ( A ^ 2
 )  x.  B ) 
 / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) )  /  ( ( ( ( ( -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) ) )  /  3
 ) )  /  2
 ) )  +  ( sqr `  ( ( -u ( ( ( sqr `  -u ( ( ( ( 2  x.  ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) )  +  ( ( ( ( ( -u (
 2  x.  ( ( B  -  ( ( 3  /  8 )  x.  ( A ^
 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) )  +  ( ( ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 2 )  +  (; 1 2  x.  (
 ( D  -  (
 ( C  x.  A )  /  4 ) )  +  ( ( ( ( A ^ 2
 )  x.  B ) 
 / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) )  /  ( ( ( ( ( -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) ) )  /  3
 ) )  /  2
 ) ^ 2 )  -  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  / 
 2 ) )  -  ( ( ( ( C  -  ( ( A  x.  B ) 
 /  2 ) )  +  ( ( A ^ 3 )  / 
 8 ) )  / 
 4 )  /  (
 ( sqr `  -u ( ( ( ( 2  x.  ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) )  +  (
 ( ( ( (
 -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) )  +  ( ( ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 2 )  +  (; 1 2  x.  (
 ( D  -  (
 ( C  x.  A )  /  4 ) )  +  ( ( ( ( A ^ 2
 )  x.  B ) 
 / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) )  /  ( ( ( ( ( -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) ) )  /  3
 ) )  /  2
 ) ) ) ) )  \/  X  =  ( ( -u ( A  /  4 )  +  ( ( sqr `  -u (
 ( ( ( 2  x.  ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) )  +  (
 ( ( ( (
 -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) )  +  ( ( ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 2 )  +  (; 1 2  x.  (
 ( D  -  (
 ( C  x.  A )  /  4 ) )  +  ( ( ( ( A ^ 2
 )  x.  B ) 
 / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) )  /  ( ( ( ( ( -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) ) )  /  3
 ) )  /  2
 ) )  -  ( sqr `  ( ( -u ( ( ( sqr `  -u ( ( ( ( 2  x.  ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) )  +  ( ( ( ( ( -u (
 2  x.  ( ( B  -  ( ( 3  /  8 )  x.  ( A ^
 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) )  +  ( ( ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 2 )  +  (; 1 2  x.  (
 ( D  -  (
 ( C  x.  A )  /  4 ) )  +  ( ( ( ( A ^ 2
 )  x.  B ) 
 / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) )  /  ( ( ( ( ( -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) ) )  /  3
 ) )  /  2
 ) ^ 2 )  -  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  / 
 2 ) )  -  ( ( ( ( C  -  ( ( A  x.  B ) 
 /  2 ) )  +  ( ( A ^ 3 )  / 
 8 ) )  / 
 4 )  /  (
 ( sqr `  -u ( ( ( ( 2  x.  ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) )  +  (
 ( ( ( (
 -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) )  +  ( ( ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 2 )  +  (; 1 2  x.  (
 ( D  -  (
 ( C  x.  A )  /  4 ) )  +  ( ( ( ( A ^ 2
 )  x.  B ) 
 / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) )  /  ( ( ( ( ( -u ( 2  x.  ( ( B  -  ( ( 3  / 
 8 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) )  +  ( sqr `  (
 ( ( ( -u ( 2  x.  (
 ( B  -  (
 ( 3  /  8
 )  x.  ( A ^ 2 ) ) ) ^ 3 ) )  -  (; 2 7  x.  (
 ( ( C  -  ( ( A  x.  B )  /  2
 ) )  +  (
 ( A ^ 3
 )  /  8 )
 ) ^ 2 ) ) )  +  (; 7 2  x.  ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) )  x.  ( ( D  -  ( ( C  x.  A )  /  4
 ) )  +  (
 ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^
 4 ) ) ) ) ) ) ) ^ 2 )  -  ( 4  x.  (
 ( ( ( B  -  ( ( 3 
 /  8 )  x.  ( A ^ 2
 ) ) ) ^
 2 )  +  (; 1 2  x.  ( ( D  -  ( ( C  x.  A )  / 
 4 ) )  +  ( ( ( ( A ^ 2 )  x.  B )  / ; 1 6 )  -  ( ( 3  / ;; 2 5 6 )  x.  ( A ^ 4
 ) ) ) ) ) ) ^ 3
 ) ) ) ) )  /  2 ) 
 ^ c  ( 1 
 /  3 ) ) ) )  /  3
 ) )  /  2
 ) ) ) ) ) ) ) ) )
 
18.4.2  Zeta function
 
Syntaxczeta 23687 The Riemann zeta function.
 class  zeta
 
Definitiondf-zeta 23688* Define the Riemann zeta function. This definition uses a series expansion of the alternating zeta function ~? zetaalt that is convergent everywhere except  1, but going from the alternating zeta function to the regular zeta function requires dividing by  1  -  2 ^ ( 1  -  s ), which has zeroes other than  1. To extract the correct value of the zeta function at these points, we extend the divided alternating zeta function by continuity. (Contributed by Mario Carneiro, 18-Jul-2014.)
 |-  zeta  =  ( iota_ f  e.  (
 ( CC  \  {
 1 } ) -cn-> CC ) A. s  e.  ( CC  \  { 1 } ) ( ( 1  -  ( 2  ^ c  ( 1  -  s
 ) ) )  x.  ( f `  s
 ) )  =  sum_ n  e.  NN0  ( sum_ k  e.  ( 0 ... n ) ( ( ( -u 1 ^ k
 )  x.  ( n  _C  k ) )  x.  ( ( k  +  1 )  ^ c  s ) )  /  ( 2 ^ ( n  +  1 )
 ) ) )
 
Theoremzetacvg 23689* The zeta series is convergent. (Contributed by Mario Carneiro, 18-Jul-2014.)
 |-  ( ph  ->  S  e.  CC )   &    |-  ( ph  ->  1  <  ( Re `  S ) )   &    |-  ( ( ph  /\  k  e.  NN )  ->  ( F `  k
 )  =  ( k 
 ^ c  -u S ) )   =>    |-  ( ph  ->  seq  1
 (  +  ,  F )  e.  dom  ~~>  )
 
18.4.3  Gamma function
 
Syntaxclgam 23690 Logarithm of the Gamma function.
 class  log  _G
 
Syntaxcgam 23691 The Gamma function.
 class  _G
 
Definitiondf-lgam 23692* Define the log-Gamma function. We can work with this form of the gamma function a bit easier than the equivalent expression for the gamma function itself, and moreover this function is not actually equal to  log ( _G ( x ) ) because the branch cuts are placed differently (we do have  exp ( log  _G ( x ) )  =  _G ( x ), though). This definition is attributed to Euler, and unlike the usual integral definition is defined on the entire complex plane except the nonpositive integers  ZZ  \  NN, where the function has simple poles. (Contributed by Mario Carneiro, 12-Jul-2014.)
 |-  log  _G  =  ( z  e.  ( CC  \  ( ZZ  \  NN ) ) 
 |->  (  ~~>  `  ( n  e.  NN  |->  ( ( ( z  x.  ( log `  n ) )  -  ( log `  z )
 )  -  sum_ m  e.  ( 1 ... n ) ( log `  (
 ( z  /  m )  +  1 )
 ) ) ) ) )
 
Definitiondf-gam 23693 Define the Gamma function. See df-lgam 23692 for more information about the reason for this definition in terms of the log-gamma function. (Contributed by Mario Carneiro, 12-Jul-2014.)
 |-  _G  =  ( exp  o.  log  _G )
 
Theoremeldmgm 23694 Elementhood in the set of non-nonpositive integers. (Contributed by Mario Carneiro, 12-Jul-2014.)
 |-  ( A  e.  ( CC  \  ( ZZ  \  NN ) )  <->  ( A  e.  CC  /\  -.  -u A  e.  NN0 ) )
 
Theoremdmgmaddn0 23695 If  A is not a nonpositive integer, then  A  +  N is nonzero for any nonnegative integer  N. (Contributed by Mario Carneiro, 12-Jul-2014.)
 |-  (
 ( A  e.  ( CC  \  ( ZZ  \  NN ) )  /\  N  e.  NN0 )  ->  ( A  +  N )  =/=  0 )
 
Theoremdmgmseqn0 23696* If  A is not a nonpositive integer, then  prod_ m  e.  ( 1 ... N
) A  +  m is nonzero for any  N. (Contributed by Mario Carneiro, 12-Jul-2014.)
 |-  S  =  seq  0 (  x. 
 ,  ( m  e. 
 _V  |->  ( A  +  m ) ) )   =>    |-  ( ( A  e.  ( CC  \  ( ZZ  \  NN ) )  /\  N  e.  NN0 )  ->  ( S `  N )  =/=  0 )
 
18.4.4  Derangements and the Subfactorial
 
Theoremderanglem 23697* Lemma for derangements. (Contributed by Mario Carneiro, 19-Jan-2015.)
 |-  ( A  e.  Fin  ->  { f  |  ( f : A -1-1-onto-> A  /\  ph ) }  e.  Fin )
 
Theoremderangval 23698* Define the derangement function, which counts the number of bijections from a set to itself such that no element is mapped to itself. (Contributed by Mario Carneiro, 19-Jan-2015.)
 |-  D  =  ( x  e.  Fin  |->  ( # `  { f  |  ( f : x -1-1-onto-> x  /\  A. y  e.  x  ( f `  y
 )  =/=  y ) } ) )   =>    |-  ( A  e.  Fin 
 ->  ( D `  A )  =  ( # `  { f  |  ( f : A -1-1-onto-> A  /\  A. y  e.  A  ( f `  y
 )  =/=  y ) } ) )
 
Theoremderangf 23699* The derangement number is a function from finite sets to nonnegative integers. (Contributed by Mario Carneiro, 19-Jan-2015.)
 |-  D  =  ( x  e.  Fin  |->  ( # `  { f  |  ( f : x -1-1-onto-> x  /\  A. y  e.  x  ( f `  y
 )  =/=  y ) } ) )   =>    |-  D : Fin --> NN0
 
Theoremderang0 23700* The derangement number of the empty set. (Contributed by Mario Carneiro, 19-Jan-2015.)
 |-  D  =  ( x  e.  Fin  |->  ( # `  { f  |  ( f : x -1-1-onto-> x  /\  A. y  e.  x  ( f `  y
 )  =/=  y ) } ) )   =>    |-  ( D `  (/) )  =  1
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18