The log file "job155.log" was opened 13-Feb-2020 5:08 PM. MM> submit job155.cmd/silent MM> ! 3atlem4 is used as reference for CPU speed calibration MM> prove 3atlem4 Entering the Proof Assistant. HELP PROOF_ASSISTANT for help, EXIT to exit. You will be working on statement (from "SHOW STATEMENT 3atlem4"): 155429 3at.l $e |- .<_ = ( le ` K ) $. 155430 3at.j $e |- .\/ = ( join ` K ) $. 155431 3at.a $e |- A = ( Atoms ` K ) $. 155435 3atlem4 $p |- ( ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( S e. A /\ T e. A ) ) /\ ( -. R .<_ ( P .\/ Q ) /\ P =/= Q ) /\ ( ( P .\/ Q ) .\/ R ) .<_ ( ( S .\/ T ) .\/ R ) ) -> ( ( P .\/ Q ) .\/ R ) = ( ( S .\/ T ) .\/ R ) ) $= ... $. Note: The proof you are starting with is already complete. MM-PA> minimize_with * /allow_new_axioms * /no_new_axioms_from ax-* /time Bytes refer to compressed proof size, steps to uncompressed length. Scanning forward through statements... No shorter proof was found. (Other mathboxes were not checked. Use / INCLUDE_MATHBOXES to include them.) MINIMIZE_WITH run time = 30.76 sec for "3atlem4" MM-PA> _exit_pa /force Exiting the Proof Assistant. Type EXIT again to exit Metamath. MM> ! start of main run MM> prove fourierdlem111 Entering the Proof Assistant. HELP PROOF_ASSISTANT for help, EXIT to exit. You will be working on statement (from "SHOW STATEMENT fourierdlem111"): $d A m n $. $d B m $. $d D i m y $. $d D s t i y $. $d x D i s y $. $d i F n s t y $. $d x F n $. $d i G s x $. $d L s t $. $d x L $. $d i M m p $. $d M s t y $. $d x M $. $d Q i p $. $d Q s t y $. $d x Q $. $d R s t $. $d x R $. $d T s x $. $d i W m p $. $d W s x y $. $d i X m n y $. $d X p $. $d X s t $. $d x X $. $d ph i m n y $. $d ph s t $. $d ph x $. 138946 fourierdlem111.a $e |- A = ( n e. NN0 |-> ( S. ( -u _pi (,) _pi ) ( ( F ` t ) x. ( cos ` ( n x. t ) ) ) _d t / _pi ) ) $. 138947 fourierdlem111.b $e |- B = ( n e. NN |-> ( S. ( -u _pi (,) _pi ) ( ( F ` t ) x. ( sin ` ( n x. t ) ) ) _d t / _pi ) ) $. 138948 fourierdlem111.s $e |- S = ( m e. NN |-> ( ( ( A ` 0 ) / 2 ) + sum_ n e. ( 1 ... m ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) ) $. 138949 fourierdlem111.d $e |- D = ( n e. NN |-> ( y e. RR |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) ) $. 138950 fourierdlem111.p $e |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = -u _pi /\ ( p ` m ) = _pi ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) $. 138951 fourierdlem111.m $e |- ( ph -> M e. NN ) $. 138952 fourierdlem111.q $e |- ( ph -> Q e. ( P ` M ) ) $. 138953 fourierdlem111.x $e |- ( ph -> X e. RR ) $. 138954 fourierdlem111.6 $e |- ( ph -> F : RR --> RR ) $. 138955 fourierdlem111.fper $e |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) ) $. 138956 fourierdlem111.g $e |- G = ( x e. RR |-> ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) ) $. 138957 fourierdlem111.fcn $e |- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) ) $. 138958 fourierdlem111.r $e |- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) ) $. 138959 fourierdlem111.l $e |- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) ) $. 138960 fourierdlem111.t $e |- T = ( 2 x. _pi ) $. 138961 fourierdlem111.o $e |- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( -u _pi - X ) /\ ( p ` m ) = ( _pi - X ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) $. 138962 fourierdlem111.14 $e |- W = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) ) $. 138963 fourierdlem111 $p |- ( ( ph /\ n e. NN ) -> ( S ` n ) = ( S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s + S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s ) ) $= ... $. Note: The proof you are starting with is already complete. MM-PA> minimize_with * /allow_new_axioms * /no_new_axioms_from ax-* /time Bytes refer to compressed proof size, steps to uncompressed length. Scanning forward through statements... Proof of "fourierdlem111" decreased from 17818 to 17812 bytes using "a1i". Proof of "fourierdlem111" decreased from 17812 to 17776 bytes using "mp1i". Proof of "fourierdlem111" decreased from 17776 to 17727 bytes using "adantl". Proof of "fourierdlem111" decreased from 17727 to 17719 bytes using "sylan". Proof of "fourierdlem111" decreased from 17719 to 17715 bytes using "syl2an". Proof of "fourierdlem111" stayed at 17715 bytes using "jca31". (Uncompressed steps decreased from 610147 to 610087). Proof of "fourierdlem111" stayed at 17715 bytes using "jctil". (Uncompressed steps decreased from 610087 to 609911). Proof of "fourierdlem111" stayed at 17715 bytes using "sylancl". (Uncompressed steps decreased from 609911 to 609765). Proof of "fourierdlem111" decreased from 17715 to 17695 bytes using "sylancr". Proof of "fourierdlem111" decreased from 17695 to 17670 bytes using "sylanbrc". Proof of "fourierdlem111" decreased from 17670 to 17659 bytes using "mp2an". Proof of "fourierdlem111" decreased from 17659 to 17643 bytes using "adantll". Proof of "fourierdlem111" stayed at 17643 bytes using "ad2antrr". (Uncompressed steps decreased from 608974 to 608272). Proof of "fourierdlem111" decreased from 17643 to 17641 bytes using "ad2antlr". Proof of "fourierdlem111" decreased from 17641 to 17631 bytes using "simp1bi". Proof of "fourierdlem111" decreased from 17631 to 17615 bytes using "syl3anbrc" . Proof of "fourierdlem111" decreased from 17615 to 17592 bytes using "mp3an12". Proof of "fourierdlem111" decreased from 17592 to 17578 bytes using "weq". Proof of "fourierdlem111" decreased from 17578 to 17527 bytes using "chvarv". Proof of "fourierdlem111" decreased from 17527 to 17519 bytes using "3eqtr4i". Proof of "fourierdlem111" decreased from 17519 to 17484 bytes using "eqtrd". Proof of "fourierdlem111" decreased from 17484 to 17453 bytes using "eqtr2d". Proof of "fourierdlem111" decreased from 17453 to 17439 bytes using "eqtr3d". Proof of "fourierdlem111" decreased from 17439 to 17415 bytes using "eqtr4d". Proof of "fourierdlem111" decreased from 17415 to 17400 bytes using "3eqtrd". Proof of "fourierdlem111" decreased from 17400 to 17399 bytes using "3eqtrrd". Proof of "fourierdlem111" stayed at 17399 bytes using "3eqtr3d". (Uncompressed steps decreased from 603645 to 603616). Proof of "fourierdlem111" decreased from 17399 to 17395 bytes using "3eqtr4d". Proof of "fourierdlem111" decreased from 17395 to 17394 bytes using "3eqtr4rd". Proof of "fourierdlem111" decreased from 17394 to 17354 bytes using "syl6eqr". Proof of "fourierdlem111" decreased from 17354 to 17319 bytes using "sylan9eqr" . Proof of "fourierdlem111" decreased from 17319 to 17302 bytes using "3eqtr3a". Proof of "fourierdlem111" decreased from 17302 to 17253 bytes using "eqeltrrd". Proof of "fourierdlem111" decreased from 17253 to 17191 bytes using "eleqtrrd". Proof of "fourierdlem111" decreased from 17191 to 17142 bytes using "3eltr3d". Proof of "fourierdlem111" decreased from 17142 to 17120 bytes using "vtoclga". Proof of "fourierdlem111" decreased from 17120 to 17026 bytes using "sseldi". Proof of "fourierdlem111" decreased from 17026 to 17019 bytes using "syl6ss". Proof of "fourierdlem111" decreased from 17019 to 17008 bytes using "sseqtr4d". Proof of "fourierdlem111" decreased from 17008 to 16993 bytes using "3brtr4d". Proof of "fourierdlem111" decreased from 16993 to 16955 bytes using "cbvmptv". Proof of "fourierdlem111" decreased from 16955 to 16948 bytes using "resabs1d". Proof of "fourierdlem111" decreased from 16948 to 16941 bytes using "resmptd". Proof of "fourierdlem111" decreased from 16941 to 16940 bytes using "feqresmpt" . Proof of "fourierdlem111" decreased from 16940 to 16921 bytes using "ffvelrnda" . Proof of "fourierdlem111" decreased from 16921 to 16872 bytes using "ffvelrnd". Proof of "fourierdlem111" decreased from 16872 to 16837 bytes using "fmptd". Proof of "fourierdlem111" decreased from 16837 to 16834 bytes using "0red". Proof of "fourierdlem111" decreased from 16834 to 16827 bytes using "recni". Proof of "fourierdlem111" decreased from 16827 to 16718 bytes using "recnd". Proof of "fourierdlem111" decreased from 16718 to 16714 bytes using "readdcld". Proof of "fourierdlem111" decreased from 16714 to 16658 bytes using "ltadd2dd". Proof of "fourierdlem111" decreased from 16658 to 16640 bytes using "ltsub1dd". Proof of "fourierdlem111" decreased from 16640 to 16633 bytes using "0zd". Proof of "fourierdlem111" decreased from 16633 to 16627 bytes using "0ltpnf". Proof of "fourierdlem111" decreased from 16627 to 16610 bytes using "elioore". Proof of "fourierdlem111" decreased from 16610 to 16604 bytes using "ioossre". Proof of "fourierdlem111" decreased from 16604 to 16583 bytes using "elicc2i". Proof of "fourierdlem111" decreased from 16583 to 16553 bytes using "cbvitgv". Proof of "fourierdlem111" decreased from 16553 to 16546 bytes using "picn".