:: RATFUNC1 semantic presentation begin theorem :: RATFUNC1:1 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "q")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "p")) ")" )))))) ; theorem :: RATFUNC1:2 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)))) "holds" (Bool (Set ($#k5_finseq_5 :::"Ins"::: ) "(" (Set "(" ($#k1_polynom3 :::"Del"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "j")) "," (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "f")))))) ; theorem :: RATFUNC1:3 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k3_group_4 :::"Product"::: ) (Set "(" ($#k1_polynom3 :::"Del"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ")" ) ")" )))))) ; registrationlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "x", "y" be ($#~v9_struct_0 "non" ($#v9_struct_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); cluster (Set "x" ($#k3_vectsp_1 :::"/"::: ) "y") -> ($#~v9_struct_0 "non" ($#v9_struct_0 :::"zero"::: ) ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v30_algstr_0 :::"almost_left_cancelable"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v31_algstr_0 :::"almost_right_cancelable"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; registrationlet "x", "y" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k4_xxreal_0 :::"max"::: ) "(" "x" "," "y" ")" ) -> ($#v1_int_1 :::"integer"::: ) ; cluster (Set ($#k3_xxreal_0 :::"min"::: ) "(" "x" "," "y" ")" ) -> ($#v1_int_1 :::"integer"::: ) ; end; theorem :: RATFUNC1:4 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set "(" (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "y")) ")" ) "," (Set "(" (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "z")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k4_xxreal_0 :::"max"::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" ")" )))) ; begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "p" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); attr "p" is :::"zero"::: means :: RATFUNC1:def 1 (Bool "p" ($#r2_funct_2 :::"="::: ) (Set ($#k9_polynom3 :::"0_."::: ) "L")); attr "p" is :::"constant"::: means :: RATFUNC1:def 2 (Bool (Set ($#k2_hurwitz :::"deg"::: ) "p") ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )); end; :: deftheorem defines :::"zero"::: RATFUNC1:def 1 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v1_ratfunc1 :::"zero"::: ) ) "iff" (Bool (Set (Var "p")) ($#r2_funct_2 :::"="::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")))) ")" ))); :: deftheorem defines :::"constant"::: RATFUNC1:def 2 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v2_ratfunc1 :::"constant"::: ) ) "iff" (Bool (Set ($#k2_hurwitz :::"deg"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))); registrationlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; cluster bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set ($#k5_numbers :::"NAT"::: ) )) bbbadV5_RELAT_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#v1_partfun1 :::"total"::: ) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) ($#v1_algseq_1 :::"finite-Support"::: ) ($#~v1_ratfunc1 "non" ($#v1_ratfunc1 :::"zero"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))))); end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; cluster (Set ($#k9_polynom3 :::"0_."::: ) "L") -> ($#v1_ratfunc1 :::"zero"::: ) ($#v2_ratfunc1 :::"constant"::: ) ; end; registrationlet "L" be ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; cluster (Set ($#k10_polynom3 :::"1_."::: ) "L") -> ($#~v1_ratfunc1 "non" ($#v1_ratfunc1 :::"zero"::: ) ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; cluster (Set ($#k10_polynom3 :::"1_."::: ) "L") -> ($#v2_ratfunc1 :::"constant"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) ($#v1_algseq_1 :::"finite-Support"::: ) ($#v1_ratfunc1 :::"zero"::: ) -> ($#v2_ratfunc1 :::"constant"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))))); end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) ($#v1_algseq_1 :::"finite-Support"::: ) ($#~v2_ratfunc1 "non" ($#v2_ratfunc1 :::"constant"::: ) ) -> ($#~v1_ratfunc1 "non" ($#v1_ratfunc1 :::"zero"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))))); end; registrationlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; cluster bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set ($#k5_numbers :::"NAT"::: ) )) bbbadV5_RELAT_1((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#v1_partfun1 :::"total"::: ) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L")) ($#v1_algseq_1 :::"finite-Support"::: ) ($#~v2_ratfunc1 "non" ($#v2_ratfunc1 :::"constant"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L"))))); end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "z" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); let "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k3_hurwitz :::"rpoly"::: ) "(" "k" "," "z" ")" ) -> ($#~v1_ratfunc1 "non" ($#v1_ratfunc1 :::"zero"::: ) ) ; end; registrationlet "L" be ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k14_polynom3 :::"Polynom-Ring"::: ) "L") -> ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ; end; registrationlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k14_polynom3 :::"Polynom-Ring"::: ) "L") -> ($#v1_vectsp_2 :::"domRing-like"::: ) ; end; theorem :: RATFUNC1:5 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k3_polynom5 :::"*"::: ) (Set (Var "p")) ")" ) ($#k11_polynom3 :::"*'"::: ) (Set (Var "q"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "a")) ($#k3_polynom5 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k11_polynom3 :::"*'"::: ) (Set (Var "q")) ")" )))))) ; theorem :: RATFUNC1:6 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "p")) ($#k11_polynom3 :::"*'"::: ) (Set "(" (Set (Var "a")) ($#k3_polynom5 :::"*"::: ) (Set (Var "q")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "a")) ($#k3_polynom5 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k11_polynom3 :::"*'"::: ) (Set (Var "q")) ")" )))))) ; registrationlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p" be ($#~v1_ratfunc1 "non" ($#v1_ratfunc1 :::"zero"::: ) ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); let "a" be ($#~v9_struct_0 "non" ($#v9_struct_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); cluster (Set "a" ($#k3_polynom5 :::"*"::: ) "p") -> ($#~v1_ratfunc1 "non" ($#v1_ratfunc1 :::"zero"::: ) ) ; end; registrationlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p1", "p2" be ($#~v1_ratfunc1 "non" ($#v1_ratfunc1 :::"zero"::: ) ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); cluster (Set "p1" ($#k11_polynom3 :::"*'"::: ) "p2") -> ($#~v1_ratfunc1 "non" ($#v1_ratfunc1 :::"zero"::: ) ) ; end; theorem :: RATFUNC1:7 (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p3")) "being" ($#~v1_ratfunc1 "non" ($#v1_ratfunc1 :::"zero"::: ) ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Set (Var "p1")) ($#k11_polynom3 :::"*'"::: ) (Set (Var "p3"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "p2")) ($#k11_polynom3 :::"*'"::: ) (Set (Var "p3"))))) "holds" (Bool (Set (Var "p1")) ($#r2_funct_2 :::"="::: ) (Set (Var "p2")))))) ; registrationlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "p" be ($#~v1_ratfunc1 "non" ($#v1_ratfunc1 :::"zero"::: ) ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); cluster (Set ($#k2_hurwitz :::"degree"::: ) "p") -> ($#v7_ordinal1 :::"natural"::: ) ; end; theorem :: RATFUNC1:8 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_group_1 :::"unital"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k2_hurwitz :::"deg"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))))) ; theorem :: RATFUNC1:9 (Bool "for" (Set (Var "L")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) "iff" (Bool (Set ($#k3_hurwitz :::"rpoly"::: ) "(" (Num 1) "," (Set (Var "x")) ")" ) ($#r1_hurwitz :::"divides"::: ) (Set (Var "p"))) ")" )))) ; theorem :: RATFUNC1:10 (Bool "for" (Set (Var "L")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" "not" (Bool (Set ($#k3_hurwitz :::"rpoly"::: ) "(" (Num 1) "," (Set (Var "x")) ")" ) ($#r1_hurwitz :::"divides"::: ) (Set (Set (Var "p")) ($#k13_polynom3 :::"*'"::: ) (Set (Var "q")))) "or" (Bool (Set ($#k3_hurwitz :::"rpoly"::: ) "(" (Num 1) "," (Set (Var "x")) ")" ) ($#r1_hurwitz :::"divides"::: ) (Set (Var "p"))) "or" (Bool (Set ($#k3_hurwitz :::"rpoly"::: ) "(" (Num 1) "," (Set (Var "x")) ")" ) ($#r1_hurwitz :::"divides"::: ) (Set (Var "q"))) ")" )))) ; theorem :: RATFUNC1:11 (Bool "for" (Set (Var "L")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set (Var "L")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k3_hurwitz :::"rpoly"::: ) "(" (Num 1) "," (Set (Var "z")) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L"))))))) ; theorem :: RATFUNC1:12 (Bool "for" (Set (Var "L")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set (Var "L")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k3_hurwitz :::"rpoly"::: ) "(" (Num 1) "," (Set (Var "z")) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "f"))))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) "iff" (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k3_hurwitz :::"rpoly"::: ) "(" (Num 1) "," (Set (Var "x")) ")" )) ")" )) ")" ))))) ; begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p1", "p2" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); pred "x" :::"is_a_common_root_of"::: "p1" "," "p2" means :: RATFUNC1:def 3 (Bool "(" (Bool "x" ($#r1_polynom5 :::"is_a_root_of"::: ) "p1") & (Bool "x" ($#r1_polynom5 :::"is_a_root_of"::: ) "p2") ")" ); end; :: deftheorem defines :::"is_a_common_root_of"::: RATFUNC1:def 3 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_ratfunc1 :::"is_a_common_root_of"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_polynom5 :::"is_a_root_of"::: ) (Set (Var "p1"))) & (Bool (Set (Var "x")) ($#r1_polynom5 :::"is_a_root_of"::: ) (Set (Var "p2"))) ")" ) ")" )))); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p1", "p2" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); pred "p1" "," "p2" :::"have_a_common_root"::: means :: RATFUNC1:def 4 (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool (Set (Var "x")) ($#r1_ratfunc1 :::"is_a_common_root_of"::: ) "p1" "," "p2")); end; :: deftheorem defines :::"have_a_common_root"::: RATFUNC1:def 4 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "p1")) "," (Set (Var "p2")) ($#r2_ratfunc1 :::"have_a_common_root"::: ) ) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Var "x")) ($#r1_ratfunc1 :::"is_a_common_root_of"::: ) (Set (Var "p1")) "," (Set (Var "p2")))) ")" ))); notationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p1", "p2" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); synonym "p1" "," "p2" :::"have_common_roots"::: for "p1" "," "p2" :::"have_a_common_root"::: ; antonym "p1" "," "p2" :::"have_no_common_roots"::: for "p1" "," "p2" :::"have_a_common_root"::: ; end; theorem :: RATFUNC1:13 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_group_1 :::"unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_polynom5 :::"is_a_root_of"::: ) (Set (Var "p")))) "holds" (Bool (Set (Var "x")) ($#r1_polynom5 :::"is_a_root_of"::: ) (Set ($#k5_vfunct_1 :::"-"::: ) (Set (Var "p"))))))) ; theorem :: RATFUNC1:14 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_group_1 :::"unital"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_ratfunc1 :::"is_a_common_root_of"::: ) (Set (Var "p1")) "," (Set (Var "p2")))) "holds" (Bool (Set (Var "x")) ($#r1_polynom5 :::"is_a_root_of"::: ) (Set (Set (Var "p1")) ($#k8_polynom3 :::"+"::: ) (Set (Var "p2"))))))) ; theorem :: RATFUNC1:15 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_group_1 :::"unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_ratfunc1 :::"is_a_common_root_of"::: ) (Set (Var "p1")) "," (Set (Var "p2")))) "holds" (Bool (Set (Var "x")) ($#r1_polynom5 :::"is_a_root_of"::: ) (Set ($#k5_vfunct_1 :::"-"::: ) (Set "(" (Set (Var "p1")) ($#k8_polynom3 :::"+"::: ) (Set (Var "p2")) ")" )))))) ; theorem :: RATFUNC1:16 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_group_1 :::"unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_ratfunc1 :::"is_a_common_root_of"::: ) (Set (Var "p")) "," (Set (Var "q")))) "holds" (Bool (Set (Var "x")) ($#r1_polynom5 :::"is_a_root_of"::: ) (Set (Set (Var "p")) ($#k8_polynom3 :::"+"::: ) (Set (Var "q"))))))) ; theorem :: RATFUNC1:17 (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "p1")) ($#r1_hurwitz :::"divides"::: ) (Set (Var "p2"))) & (Bool (Set (Var "p1")) "is" ($#v1_polynom5 :::"with_roots"::: ) )) "holds" (Bool (Set (Var "p1")) "," (Set (Var "p2")) ($#r2_ratfunc1 :::"have_common_roots"::: ) ))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p", "q" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); func :::"Common_Roots"::: "(" "p" "," "q" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "L" equals :: RATFUNC1:def 5 "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" "L" : (Bool (Set (Var "x")) ($#r1_ratfunc1 :::"is_a_common_root_of"::: ) "p" "," "q") "}" ; end; :: deftheorem defines :::"Common_Roots"::: RATFUNC1:def 5 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k1_ratfunc1 :::"Common_Roots"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool (Set (Var "x")) ($#r1_ratfunc1 :::"is_a_common_root_of"::: ) (Set (Var "p")) "," (Set (Var "q"))) "}" ))); begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "p" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); func :::"Leading-Coefficient"::: "p" -> ($#m1_subset_1 :::"Element":::) "of" "L" equals :: RATFUNC1:def 6 (Set "p" ($#k1_normsp_1 :::"."::: ) (Set "(" (Set "(" ($#k1_algseq_1 :::"len"::: ) "p" ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )); end; :: deftheorem defines :::"Leading-Coefficient"::: RATFUNC1:def 6 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_ratfunc1 :::"Leading-Coefficient"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ))))); notationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "p" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); synonym :::"LC"::: "p" for :::"Leading-Coefficient"::: "p"; end; registrationlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p" be ($#~v1_ratfunc1 "non" ($#v1_ratfunc1 :::"zero"::: ) ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); cluster (Set ($#k2_ratfunc1 :::"Leading-Coefficient"::: ) "p") -> ($#~v9_struct_0 "non" ($#v9_struct_0 :::"zero"::: ) ) ; end; theorem :: RATFUNC1:18 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_ratfunc1 :::"LC"::: ) (Set "(" (Set (Var "a")) ($#k3_polynom5 :::"*"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k2_ratfunc1 :::"LC"::: ) (Set (Var "p")) ")" )))))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); attr "p" is :::"normalized"::: means :: RATFUNC1:def 7 (Bool (Set ($#k2_ratfunc1 :::"LC"::: ) "p") ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "L")); end; :: deftheorem defines :::"normalized"::: RATFUNC1:def 7 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v3_ratfunc1 :::"normalized"::: ) ) "iff" (Bool (Set ($#k2_ratfunc1 :::"LC"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "L")))) ")" ))); registrationlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p" be ($#~v1_ratfunc1 "non" ($#v1_ratfunc1 :::"zero"::: ) ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); cluster (Set (Set "(" (Set "(" ($#k5_struct_0 :::"1."::: ) "L" ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set "(" ($#k2_ratfunc1 :::"LC"::: ) "p" ")" ) ")" ) ($#k3_polynom5 :::"*"::: ) "p") -> ($#v3_ratfunc1 :::"normalized"::: ) ; end; registrationlet "L" be ($#l6_algstr_0 :::"Field":::); let "p" be ($#~v1_ratfunc1 "non" ($#v1_ratfunc1 :::"zero"::: ) ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); cluster (Set ($#k7_polynom5 :::"NormPolynomial"::: ) "p") -> ($#v3_ratfunc1 :::"normalized"::: ) ; end; begin definitionlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; mode :::"rational_function"::: "of" "L" -> ($#m1_hidden :::"set"::: ) means :: RATFUNC1:def 8 (Bool "ex" (Set (Var "p1")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" "L"(Bool "ex" (Set (Var "p2")) "being" ($#~v1_ratfunc1 "non" ($#v1_ratfunc1 :::"zero"::: ) ) ($#m1_subset_1 :::"Polynomial":::) "of" "L" "st" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k4_tarski :::"]"::: ) )))); end; :: deftheorem defines :::"rational_function"::: RATFUNC1:def 8 : (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Var "L"))) "iff" (Bool "ex" (Set (Var "p1")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L"))(Bool "ex" (Set (Var "p2")) "being" ($#~v1_ratfunc1 "non" ($#v1_ratfunc1 :::"zero"::: ) ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k4_tarski :::"]"::: ) )))) ")" ))); definitionlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; let "p1" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); let "p2" be ($#~v1_ratfunc1 "non" ($#v1_ratfunc1 :::"zero"::: ) ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); :: original: :::"["::: redefine func :::"[":::"p1" "," "p2":::"]"::: -> ($#m1_ratfunc1 :::"rational_function"::: ) "of" "L"; end; definitionlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; let "z" be ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Const "L")); :: original: :::"`1"::: redefine func "z" :::"`1"::: -> ($#m1_subset_1 :::"Polynomial":::) "of" "L"; :: original: :::"`2"::: redefine func "z" :::"`2"::: -> ($#~v1_ratfunc1 "non" ($#v1_ratfunc1 :::"zero"::: ) ) ($#m1_subset_1 :::"Polynomial":::) "of" "L"; end; definitionlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; let "z" be ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Const "L")); attr "z" is :::"zero"::: means :: RATFUNC1:def 9 (Bool (Set "z" ($#k4_ratfunc1 :::"`1"::: ) ) ($#r2_funct_2 :::"="::: ) (Set ($#k9_polynom3 :::"0_."::: ) "L")); end; :: deftheorem defines :::"zero"::: RATFUNC1:def 9 : (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) (Bool "for" (Set (Var "z")) "being" ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "z")) "is" ($#v4_ratfunc1 :::"zero"::: ) ) "iff" (Bool (Set (Set (Var "z")) ($#k4_ratfunc1 :::"`1"::: ) ) ($#r2_funct_2 :::"="::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")))) ")" ))); registrationlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; cluster ($#~v4_ratfunc1 "non" ($#v4_ratfunc1 :::"zero"::: ) ) for ($#m1_ratfunc1 :::"rational_function"::: ) "of" "L"; end; theorem :: RATFUNC1:19 (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) (Bool "for" (Set (Var "z")) "being" ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Var "L")) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k3_ratfunc1 :::"["::: ) (Set "(" (Set (Var "z")) ($#k4_ratfunc1 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "z")) ($#k5_ratfunc1 :::"`2"::: ) ")" ) ($#k3_ratfunc1 :::"]"::: ) )))) ; definitionlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_group_1 :::"unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "z" be ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Const "L")); attr "z" is :::"irreducible"::: means :: RATFUNC1:def 10 (Bool (Set "z" ($#k4_ratfunc1 :::"`1"::: ) ) "," (Set "z" ($#k5_ratfunc1 :::"`2"::: ) ) ($#r2_ratfunc1 :::"have_no_common_roots"::: ) ); end; :: deftheorem defines :::"irreducible"::: RATFUNC1:def 10 : (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_group_1 :::"unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "z")) "being" ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "z")) "is" ($#v5_ratfunc1 :::"irreducible"::: ) ) "iff" (Bool (Set (Set (Var "z")) ($#k4_ratfunc1 :::"`1"::: ) ) "," (Set (Set (Var "z")) ($#k5_ratfunc1 :::"`2"::: ) ) ($#r2_ratfunc1 :::"have_no_common_roots"::: ) ) ")" ))); notationlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_group_1 :::"unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "z" be ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Const "L")); antonym :::"reducible"::: "z" for :::"irreducible"::: ; end; definitionlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_group_1 :::"unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "z" be ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Const "L")); attr "z" is :::"normalized"::: means :: RATFUNC1:def 11 (Bool "(" (Bool "z" "is" ($#v5_ratfunc1 :::"irreducible"::: ) ) & (Bool (Set "z" ($#k5_ratfunc1 :::"`2"::: ) ) "is" ($#v3_ratfunc1 :::"normalized"::: ) ) ")" ); end; :: deftheorem defines :::"normalized"::: RATFUNC1:def 11 : (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_group_1 :::"unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "z")) "being" ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "z")) "is" ($#v6_ratfunc1 :::"normalized"::: ) ) "iff" (Bool "(" (Bool (Set (Var "z")) "is" ($#v5_ratfunc1 :::"irreducible"::: ) ) & (Bool (Set (Set (Var "z")) ($#k5_ratfunc1 :::"`2"::: ) ) "is" ($#v3_ratfunc1 :::"normalized"::: ) ) ")" ) ")" ))); registrationlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_group_1 :::"unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster ($#v6_ratfunc1 :::"normalized"::: ) -> ($#v5_ratfunc1 :::"irreducible"::: ) for ($#m1_ratfunc1 :::"rational_function"::: ) "of" "L"; end; registrationlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "z" be ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Const "L")); cluster (Set ($#k2_ratfunc1 :::"Leading-Coefficient"::: ) (Set "(" "z" ($#k5_ratfunc1 :::"`2"::: ) ")" )) -> ($#~v9_struct_0 "non" ($#v9_struct_0 :::"zero"::: ) ) ; end; definitionlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "z" be ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Const "L")); func :::"NormRationalFunction"::: "z" -> ($#m1_ratfunc1 :::"rational_function"::: ) "of" "L" equals :: RATFUNC1:def 12 (Set ($#k3_ratfunc1 :::"["::: ) (Set "(" (Set "(" (Set "(" ($#k5_struct_0 :::"1."::: ) "L" ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set "(" ($#k2_ratfunc1 :::"LC"::: ) (Set "(" "z" ($#k5_ratfunc1 :::"`2"::: ) ")" ) ")" ) ")" ) ($#k3_polynom5 :::"*"::: ) (Set "(" "z" ($#k4_ratfunc1 :::"`1"::: ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k5_struct_0 :::"1."::: ) "L" ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set "(" ($#k2_ratfunc1 :::"LC"::: ) (Set "(" "z" ($#k5_ratfunc1 :::"`2"::: ) ")" ) ")" ) ")" ) ($#k3_polynom5 :::"*"::: ) (Set "(" "z" ($#k5_ratfunc1 :::"`2"::: ) ")" ) ")" ) ($#k3_ratfunc1 :::"]"::: ) ); end; :: deftheorem defines :::"NormRationalFunction"::: RATFUNC1:def 12 : (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "z")) "being" ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Var "L")) "holds" (Bool (Set ($#k6_ratfunc1 :::"NormRationalFunction"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k3_ratfunc1 :::"["::: ) (Set "(" (Set "(" (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set "(" ($#k2_ratfunc1 :::"LC"::: ) (Set "(" (Set (Var "z")) ($#k5_ratfunc1 :::"`2"::: ) ")" ) ")" ) ")" ) ($#k3_polynom5 :::"*"::: ) (Set "(" (Set (Var "z")) ($#k4_ratfunc1 :::"`1"::: ) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set "(" ($#k2_ratfunc1 :::"LC"::: ) (Set "(" (Set (Var "z")) ($#k5_ratfunc1 :::"`2"::: ) ")" ) ")" ) ")" ) ($#k3_polynom5 :::"*"::: ) (Set "(" (Set (Var "z")) ($#k5_ratfunc1 :::"`2"::: ) ")" ) ")" ) ($#k3_ratfunc1 :::"]"::: ) )))); notationlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "z" be ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Const "L")); synonym :::"NormRatF"::: "z" for :::"NormRationalFunction"::: "z"; end; registrationlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "z" be ($#~v4_ratfunc1 "non" ($#v4_ratfunc1 :::"zero"::: ) ) ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Const "L")); cluster (Set ($#k6_ratfunc1 :::"NormRationalFunction"::: ) "z") -> ($#~v4_ratfunc1 "non" ($#v4_ratfunc1 :::"zero"::: ) ) ; end; definitionlet "L" be ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; func :::"0._"::: "L" -> ($#m1_ratfunc1 :::"rational_function"::: ) "of" "L" equals :: RATFUNC1:def 13 (Set ($#k3_ratfunc1 :::"["::: ) (Set "(" ($#k9_polynom3 :::"0_."::: ) "L" ")" ) "," (Set "(" ($#k10_polynom3 :::"1_."::: ) "L" ")" ) ($#k3_ratfunc1 :::"]"::: ) ); func :::"1._"::: "L" -> ($#m1_ratfunc1 :::"rational_function"::: ) "of" "L" equals :: RATFUNC1:def 14 (Set ($#k3_ratfunc1 :::"["::: ) (Set "(" ($#k10_polynom3 :::"1_."::: ) "L" ")" ) "," (Set "(" ($#k10_polynom3 :::"1_."::: ) "L" ")" ) ($#k3_ratfunc1 :::"]"::: ) ); end; :: deftheorem defines :::"0._"::: RATFUNC1:def 13 : (Bool "for" (Set (Var "L")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) "holds" (Bool (Set ($#k7_ratfunc1 :::"0._"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k3_ratfunc1 :::"["::: ) (Set "(" ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")) ")" ) "," (Set "(" ($#k10_polynom3 :::"1_."::: ) (Set (Var "L")) ")" ) ($#k3_ratfunc1 :::"]"::: ) ))); :: deftheorem defines :::"1._"::: RATFUNC1:def 14 : (Bool "for" (Set (Var "L")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) "holds" (Bool (Set ($#k8_ratfunc1 :::"1._"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k3_ratfunc1 :::"["::: ) (Set "(" ($#k10_polynom3 :::"1_."::: ) (Set (Var "L")) ")" ) "," (Set "(" ($#k10_polynom3 :::"1_."::: ) (Set (Var "L")) ")" ) ($#k3_ratfunc1 :::"]"::: ) ))); registrationlet "L" be ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k7_ratfunc1 :::"0._"::: ) "L") -> ($#v6_ratfunc1 :::"normalized"::: ) ; end; registrationlet "L" be ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; cluster (Set ($#k8_ratfunc1 :::"1._"::: ) "L") -> ($#~v4_ratfunc1 "non" ($#v4_ratfunc1 :::"zero"::: ) ) ; end; registrationlet "L" be ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k8_ratfunc1 :::"1._"::: ) "L") -> ($#v5_ratfunc1 :::"irreducible"::: ) ; end; registrationlet "L" be ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster ($#~v4_ratfunc1 "non" ($#v4_ratfunc1 :::"zero"::: ) ) ($#v5_ratfunc1 :::"irreducible"::: ) for ($#m1_ratfunc1 :::"rational_function"::: ) "of" "L"; end; registrationlet "L" be ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); cluster (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k3_hurwitz :::"rpoly"::: ) "(" (Num 1) "," "x" ")" ")" ) "," (Set "(" ($#k3_hurwitz :::"rpoly"::: ) "(" (Num 1) "," "x" ")" ")" ) ($#k4_tarski :::"]"::: ) ) -> ($#~v4_ratfunc1 "non" ($#v4_ratfunc1 :::"zero"::: ) ) ($#v5_ratfunc1 :::"reducible"::: ) for ($#m1_ratfunc1 :::"rational_function"::: ) "of" "L"; end; registrationlet "L" be ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster ($#~v4_ratfunc1 "non" ($#v4_ratfunc1 :::"zero"::: ) ) ($#v5_ratfunc1 :::"reducible"::: ) for ($#m1_ratfunc1 :::"rational_function"::: ) "of" "L"; end; registrationlet "L" be ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster ($#v6_ratfunc1 :::"normalized"::: ) for ($#m1_ratfunc1 :::"rational_function"::: ) "of" "L"; end; registrationlet "L" be ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; cluster (Set ($#k7_ratfunc1 :::"0._"::: ) "L") -> ($#v4_ratfunc1 :::"zero"::: ) ; end; registrationlet "L" be ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k8_ratfunc1 :::"1._"::: ) "L") -> ($#v6_ratfunc1 :::"normalized"::: ) ; end; definitionlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p", "q" be ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Const "L")); func "p" :::"+"::: "q" -> ($#m1_ratfunc1 :::"rational_function"::: ) "of" "L" equals :: RATFUNC1:def 15 (Set ($#k3_ratfunc1 :::"["::: ) (Set "(" (Set "(" (Set "(" "p" ($#k4_ratfunc1 :::"`1"::: ) ")" ) ($#k11_polynom3 :::"*'"::: ) (Set "(" "q" ($#k5_ratfunc1 :::"`2"::: ) ")" ) ")" ) ($#k2_normsp_1 :::"+"::: ) (Set "(" (Set "(" "p" ($#k5_ratfunc1 :::"`2"::: ) ")" ) ($#k11_polynom3 :::"*'"::: ) (Set "(" "q" ($#k4_ratfunc1 :::"`1"::: ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" "p" ($#k5_ratfunc1 :::"`2"::: ) ")" ) ($#k11_polynom3 :::"*'"::: ) (Set "(" "q" ($#k5_ratfunc1 :::"`2"::: ) ")" ) ")" ) ($#k3_ratfunc1 :::"]"::: ) ); end; :: deftheorem defines :::"+"::: RATFUNC1:def 15 : (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "p")) ($#k9_ratfunc1 :::"+"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k3_ratfunc1 :::"["::: ) (Set "(" (Set "(" (Set "(" (Set (Var "p")) ($#k4_ratfunc1 :::"`1"::: ) ")" ) ($#k11_polynom3 :::"*'"::: ) (Set "(" (Set (Var "q")) ($#k5_ratfunc1 :::"`2"::: ) ")" ) ")" ) ($#k2_normsp_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_ratfunc1 :::"`2"::: ) ")" ) ($#k11_polynom3 :::"*'"::: ) (Set "(" (Set (Var "q")) ($#k4_ratfunc1 :::"`1"::: ) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "p")) ($#k5_ratfunc1 :::"`2"::: ) ")" ) ($#k11_polynom3 :::"*'"::: ) (Set "(" (Set (Var "q")) ($#k5_ratfunc1 :::"`2"::: ) ")" ) ")" ) ($#k3_ratfunc1 :::"]"::: ) )))); definitionlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p", "q" be ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Const "L")); func "p" :::"*'"::: "q" -> ($#m1_ratfunc1 :::"rational_function"::: ) "of" "L" equals :: RATFUNC1:def 16 (Set ($#k3_ratfunc1 :::"["::: ) (Set "(" (Set "(" "p" ($#k4_ratfunc1 :::"`1"::: ) ")" ) ($#k11_polynom3 :::"*'"::: ) (Set "(" "q" ($#k4_ratfunc1 :::"`1"::: ) ")" ) ")" ) "," (Set "(" (Set "(" "p" ($#k5_ratfunc1 :::"`2"::: ) ")" ) ($#k11_polynom3 :::"*'"::: ) (Set "(" "q" ($#k5_ratfunc1 :::"`2"::: ) ")" ) ")" ) ($#k3_ratfunc1 :::"]"::: ) ); end; :: deftheorem defines :::"*'"::: RATFUNC1:def 16 : (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "p")) ($#k10_ratfunc1 :::"*'"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k3_ratfunc1 :::"["::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k4_ratfunc1 :::"`1"::: ) ")" ) ($#k11_polynom3 :::"*'"::: ) (Set "(" (Set (Var "q")) ($#k4_ratfunc1 :::"`1"::: ) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "p")) ($#k5_ratfunc1 :::"`2"::: ) ")" ) ($#k11_polynom3 :::"*'"::: ) (Set "(" (Set (Var "q")) ($#k5_ratfunc1 :::"`2"::: ) ")" ) ")" ) ($#k3_ratfunc1 :::"]"::: ) )))); theorem :: RATFUNC1:20 (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#~v9_struct_0 "non" ($#v9_struct_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k3_ratfunc1 :::"["::: ) (Set "(" (Set (Var "a")) ($#k3_polynom5 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k4_ratfunc1 :::"`1"::: ) ")" ) ")" ) "," (Set "(" (Set (Var "a")) ($#k3_polynom5 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k5_ratfunc1 :::"`2"::: ) ")" ) ")" ) ($#k3_ratfunc1 :::"]"::: ) ) "is" ($#v5_ratfunc1 :::"irreducible"::: ) ) "iff" (Bool (Set (Var "p")) "is" ($#v5_ratfunc1 :::"irreducible"::: ) ) ")" )))) ; begin theorem :: RATFUNC1:21 (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "z")) "being" ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Var "L")) (Bool "ex" (Set (Var "z1")) "being" ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Var "L"))(Bool "ex" (Set (Var "z2")) "being" ($#~v1_ratfunc1 "non" ($#v1_ratfunc1 :::"zero"::: ) ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k3_ratfunc1 :::"["::: ) (Set "(" (Set (Var "z2")) ($#k13_polynom3 :::"*'"::: ) (Set "(" (Set (Var "z1")) ($#k4_ratfunc1 :::"`1"::: ) ")" ) ")" ) "," (Set "(" (Set (Var "z2")) ($#k13_polynom3 :::"*'"::: ) (Set "(" (Set (Var "z1")) ($#k5_ratfunc1 :::"`2"::: ) ")" ) ")" ) ($#k3_ratfunc1 :::"]"::: ) )) & (Bool (Set (Var "z1")) "is" ($#v5_ratfunc1 :::"irreducible"::: ) ) & (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set (Var "L")) ")" ) "st" (Bool "(" (Bool (Set (Var "z2")) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_ratfunc1 :::"is_a_common_root_of"::: ) (Set (Set (Var "z")) ($#k4_ratfunc1 :::"`1"::: ) ) "," (Set (Set (Var "z")) ($#k5_ratfunc1 :::"`2"::: ) )) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k3_hurwitz :::"rpoly"::: ) "(" (Num 1) "," (Set (Var "x")) ")" )) ")" )) ")" ) ")" )) ")" ))))) ; definitionlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "z" be ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Const "L")); func :::"NF"::: "z" -> ($#m1_ratfunc1 :::"rational_function"::: ) "of" "L" means :: RATFUNC1:def 17 (Bool "ex" (Set (Var "z1")) "being" ($#m1_ratfunc1 :::"rational_function"::: ) "of" "L"(Bool "ex" (Set (Var "z2")) "being" ($#~v1_ratfunc1 "non" ($#v1_ratfunc1 :::"zero"::: ) ) ($#m1_subset_1 :::"Polynomial":::) "of" "L" "st" (Bool "(" (Bool "z" ($#r1_hidden :::"="::: ) (Set ($#k3_ratfunc1 :::"["::: ) (Set "(" (Set (Var "z2")) ($#k13_polynom3 :::"*'"::: ) (Set "(" (Set (Var "z1")) ($#k4_ratfunc1 :::"`1"::: ) ")" ) ")" ) "," (Set "(" (Set (Var "z2")) ($#k13_polynom3 :::"*'"::: ) (Set "(" (Set (Var "z1")) ($#k5_ratfunc1 :::"`2"::: ) ")" ) ")" ) ($#k3_ratfunc1 :::"]"::: ) )) & (Bool (Set (Var "z1")) "is" ($#v5_ratfunc1 :::"irreducible"::: ) ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_ratfunc1 :::"NormRationalFunction"::: ) (Set (Var "z1")))) & (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) "L" ")" ) "st" (Bool "(" (Bool (Set (Var "z2")) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_ratfunc1 :::"is_a_common_root_of"::: ) (Set "z" ($#k4_ratfunc1 :::"`1"::: ) ) "," (Set "z" ($#k5_ratfunc1 :::"`2"::: ) )) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k3_hurwitz :::"rpoly"::: ) "(" (Num 1) "," (Set (Var "x")) ")" )) ")" )) ")" ) ")" )) ")" ))) if (Bool (Bool "not" "z" "is" ($#v4_ratfunc1 :::"zero"::: ) )) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k7_ratfunc1 :::"0._"::: ) "L")); end; :: deftheorem defines :::"NF"::: RATFUNC1:def 17 : (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "z")) "," (Set (Var "b3")) "being" ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Var "L")) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "z")) "is" ($#v4_ratfunc1 :::"zero"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k11_ratfunc1 :::"NF"::: ) (Set (Var "z")))) "iff" (Bool "ex" (Set (Var "z1")) "being" ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Var "L"))(Bool "ex" (Set (Var "z2")) "being" ($#~v1_ratfunc1 "non" ($#v1_ratfunc1 :::"zero"::: ) ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k3_ratfunc1 :::"["::: ) (Set "(" (Set (Var "z2")) ($#k13_polynom3 :::"*'"::: ) (Set "(" (Set (Var "z1")) ($#k4_ratfunc1 :::"`1"::: ) ")" ) ")" ) "," (Set "(" (Set (Var "z2")) ($#k13_polynom3 :::"*'"::: ) (Set "(" (Set (Var "z1")) ($#k5_ratfunc1 :::"`2"::: ) ")" ) ")" ) ($#k3_ratfunc1 :::"]"::: ) )) & (Bool (Set (Var "z1")) "is" ($#v5_ratfunc1 :::"irreducible"::: ) ) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_ratfunc1 :::"NormRationalFunction"::: ) (Set (Var "z1")))) & (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set (Var "L")) ")" ) "st" (Bool "(" (Bool (Set (Var "z2")) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_ratfunc1 :::"is_a_common_root_of"::: ) (Set (Set (Var "z")) ($#k4_ratfunc1 :::"`1"::: ) ) "," (Set (Set (Var "z")) ($#k5_ratfunc1 :::"`2"::: ) )) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k3_hurwitz :::"rpoly"::: ) "(" (Num 1) "," (Set (Var "x")) ")" )) ")" )) ")" ) ")" )) ")" ))) ")" ) ")" & "(" (Bool (Bool (Set (Var "z")) "is" ($#v4_ratfunc1 :::"zero"::: ) )) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k11_ratfunc1 :::"NF"::: ) (Set (Var "z")))) "iff" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k7_ratfunc1 :::"0._"::: ) (Set (Var "L")))) ")" ) ")" ")" ))); registrationlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "z" be ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Const "L")); cluster (Set ($#k11_ratfunc1 :::"NF"::: ) "z") -> ($#v5_ratfunc1 :::"irreducible"::: ) ($#v6_ratfunc1 :::"normalized"::: ) ; end; registrationlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "z" be ($#~v4_ratfunc1 "non" ($#v4_ratfunc1 :::"zero"::: ) ) ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Const "L")); cluster (Set ($#k11_ratfunc1 :::"NF"::: ) "z") -> ($#~v4_ratfunc1 "non" ($#v4_ratfunc1 :::"zero"::: ) ) ; end; theorem :: RATFUNC1:22 (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "z")) "being" ($#~v4_ratfunc1 "non" ($#v4_ratfunc1 :::"zero"::: ) ) ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "z1")) "being" ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "z2")) "being" ($#~v1_ratfunc1 "non" ($#v1_ratfunc1 :::"zero"::: ) ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k3_ratfunc1 :::"["::: ) (Set "(" (Set (Var "z2")) ($#k13_polynom3 :::"*'"::: ) (Set "(" (Set (Var "z1")) ($#k4_ratfunc1 :::"`1"::: ) ")" ) ")" ) "," (Set "(" (Set (Var "z2")) ($#k13_polynom3 :::"*'"::: ) (Set "(" (Set (Var "z1")) ($#k5_ratfunc1 :::"`2"::: ) ")" ) ")" ) ($#k3_ratfunc1 :::"]"::: ) )) & (Bool (Set (Var "z1")) "is" ($#v5_ratfunc1 :::"irreducible"::: ) ) & (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set (Var "L")) ")" ) "st" (Bool "(" (Bool (Set (Var "z2")) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_ratfunc1 :::"is_a_common_root_of"::: ) (Set (Set (Var "z")) ($#k4_ratfunc1 :::"`1"::: ) ) "," (Set (Set (Var "z")) ($#k5_ratfunc1 :::"`2"::: ) )) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k3_hurwitz :::"rpoly"::: ) "(" (Num 1) "," (Set (Var "x")) ")" )) ")" )) ")" ) ")" ))) "holds" (Bool (Set ($#k11_ratfunc1 :::"NF"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_ratfunc1 :::"NormRationalFunction"::: ) (Set (Var "z1")))))))) ; theorem :: RATFUNC1:23 (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) "holds" (Bool (Set ($#k11_ratfunc1 :::"NF"::: ) (Set "(" ($#k7_ratfunc1 :::"0._"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_ratfunc1 :::"0._"::: ) (Set (Var "L"))))) ; theorem :: RATFUNC1:24 (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) "holds" (Bool (Set ($#k11_ratfunc1 :::"NF"::: ) (Set "(" ($#k8_ratfunc1 :::"1._"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_ratfunc1 :::"1._"::: ) (Set (Var "L"))))) ; theorem :: RATFUNC1:25 (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "z")) "being" ($#~v4_ratfunc1 "non" ($#v4_ratfunc1 :::"zero"::: ) ) ($#v5_ratfunc1 :::"irreducible"::: ) ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Var "L")) "holds" (Bool (Set ($#k11_ratfunc1 :::"NF"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_ratfunc1 :::"NormRationalFunction"::: ) (Set (Var "z")))))) ; theorem :: RATFUNC1:26 (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "z")) "being" ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k11_ratfunc1 :::"NF"::: ) (Set ($#k3_ratfunc1 :::"["::: ) (Set "(" (Set "(" ($#k3_hurwitz :::"rpoly"::: ) "(" (Num 1) "," (Set (Var "x")) ")" ")" ) ($#k13_polynom3 :::"*'"::: ) (Set "(" (Set (Var "z")) ($#k4_ratfunc1 :::"`1"::: ) ")" ) ")" ) "," (Set "(" (Set "(" ($#k3_hurwitz :::"rpoly"::: ) "(" (Num 1) "," (Set (Var "x")) ")" ")" ) ($#k13_polynom3 :::"*'"::: ) (Set "(" (Set (Var "z")) ($#k5_ratfunc1 :::"`2"::: ) ")" ) ")" ) ($#k3_ratfunc1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k11_ratfunc1 :::"NF"::: ) (Set (Var "z"))))))) ; theorem :: RATFUNC1:27 (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "z")) "being" ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Var "L")) "holds" (Bool (Set ($#k11_ratfunc1 :::"NF"::: ) (Set "(" ($#k11_ratfunc1 :::"NF"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_ratfunc1 :::"NF"::: ) (Set (Var "z")))))) ; theorem :: RATFUNC1:28 (Bool "for" (Set (Var "L")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "z")) "being" ($#~v4_ratfunc1 "non" ($#v4_ratfunc1 :::"zero"::: ) ) ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "z")) "is" ($#v5_ratfunc1 :::"irreducible"::: ) ) "iff" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "a")) ($#k3_polynom5 :::"*"::: ) (Set "(" (Set (Var "z")) ($#k4_ratfunc1 :::"`1"::: ) ")" ) ")" ) "," (Set "(" (Set (Var "a")) ($#k3_polynom5 :::"*"::: ) (Set "(" (Set (Var "z")) ($#k5_ratfunc1 :::"`2"::: ) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k11_ratfunc1 :::"NF"::: ) (Set (Var "z")))) ")" )) ")" ))) ; begin definitionlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "z" be ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Const "L")); func :::"degree"::: "z" -> ($#m1_hidden :::"Integer":::) equals :: RATFUNC1:def 18 (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set "(" ($#k2_hurwitz :::"degree"::: ) (Set "(" (Set "(" ($#k11_ratfunc1 :::"NF"::: ) "z" ")" ) ($#k4_ratfunc1 :::"`1"::: ) ")" ) ")" ) "," (Set "(" ($#k2_hurwitz :::"degree"::: ) (Set "(" (Set "(" ($#k11_ratfunc1 :::"NF"::: ) "z" ")" ) ($#k5_ratfunc1 :::"`2"::: ) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"degree"::: RATFUNC1:def 18 : (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "z")) "being" ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Var "L")) "holds" (Bool (Set ($#k12_ratfunc1 :::"degree"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set "(" ($#k2_hurwitz :::"degree"::: ) (Set "(" (Set "(" ($#k11_ratfunc1 :::"NF"::: ) (Set (Var "z")) ")" ) ($#k4_ratfunc1 :::"`1"::: ) ")" ) ")" ) "," (Set "(" ($#k2_hurwitz :::"degree"::: ) (Set "(" (Set "(" ($#k11_ratfunc1 :::"NF"::: ) (Set (Var "z")) ")" ) ($#k5_ratfunc1 :::"`2"::: ) ")" ) ")" ) ")" )))); notationlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "z" be ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Const "L")); synonym :::"deg"::: "z" for :::"degree"::: "z"; end; theorem :: RATFUNC1:29 (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "z")) "being" ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Var "L")) "holds" (Bool (Set ($#k12_ratfunc1 :::"degree"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set "(" ($#k2_hurwitz :::"degree"::: ) (Set "(" (Set (Var "z")) ($#k4_ratfunc1 :::"`1"::: ) ")" ) ")" ) "," (Set "(" ($#k2_hurwitz :::"degree"::: ) (Set "(" (Set (Var "z")) ($#k5_ratfunc1 :::"`2"::: ) ")" ) ")" ) ")" )))) ; theorem :: RATFUNC1:30 (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "z")) "being" ($#~v4_ratfunc1 "non" ($#v4_ratfunc1 :::"zero"::: ) ) ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "z")) "is" ($#v5_ratfunc1 :::"irreducible"::: ) ) "iff" (Bool (Set ($#k12_ratfunc1 :::"degree"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set "(" ($#k2_hurwitz :::"degree"::: ) (Set "(" (Set (Var "z")) ($#k4_ratfunc1 :::"`1"::: ) ")" ) ")" ) "," (Set "(" ($#k2_hurwitz :::"degree"::: ) (Set "(" (Set (Var "z")) ($#k5_ratfunc1 :::"`2"::: ) ")" ) ")" ) ")" )) ")" ))) ; begin definitionlet "L" be ($#l6_algstr_0 :::"Field":::); let "z" be ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Const "L")); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func :::"eval"::: "(" "z" "," "x" ")" -> ($#m1_subset_1 :::"Element":::) "of" "L" equals :: RATFUNC1:def 19 (Set (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" "z" ($#k4_ratfunc1 :::"`1"::: ) ")" ) "," "x" ")" ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" "z" ($#k5_ratfunc1 :::"`2"::: ) ")" ) "," "x" ")" ")" )); end; :: deftheorem defines :::"eval"::: RATFUNC1:def 19 : (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "z")) "being" ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k13_ratfunc1 :::"eval"::: ) "(" (Set (Var "z")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" (Set (Var "z")) ($#k4_ratfunc1 :::"`1"::: ) ")" ) "," (Set (Var "x")) ")" ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" (Set (Var "z")) ($#k5_ratfunc1 :::"`2"::: ) ")" ) "," (Set (Var "x")) ")" ")" )))))); theorem :: RATFUNC1:31 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k13_ratfunc1 :::"eval"::: ) "(" (Set "(" ($#k7_ratfunc1 :::"0._"::: ) (Set (Var "L")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))))) ; theorem :: RATFUNC1:32 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k13_ratfunc1 :::"eval"::: ) "(" (Set "(" ($#k8_ratfunc1 :::"1._"::: ) (Set (Var "L")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "L")))))) ; theorem :: RATFUNC1:33 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" (Set (Var "p")) ($#k5_ratfunc1 :::"`2"::: ) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) & (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" (Set (Var "q")) ($#k5_ratfunc1 :::"`2"::: ) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "holds" (Bool (Set ($#k13_ratfunc1 :::"eval"::: ) "(" (Set "(" (Set (Var "p")) ($#k9_ratfunc1 :::"+"::: ) (Set (Var "q")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k13_ratfunc1 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k13_ratfunc1 :::"eval"::: ) "(" (Set (Var "q")) "," (Set (Var "x")) ")" ")" )))))) ; theorem :: RATFUNC1:34 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" (Set (Var "p")) ($#k5_ratfunc1 :::"`2"::: ) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) & (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" (Set (Var "q")) ($#k5_ratfunc1 :::"`2"::: ) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "holds" (Bool (Set ($#k13_ratfunc1 :::"eval"::: ) "(" (Set "(" (Set (Var "p")) ($#k10_ratfunc1 :::"*'"::: ) (Set (Var "q")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k13_ratfunc1 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k13_ratfunc1 :::"eval"::: ) "(" (Set (Var "q")) "," (Set (Var "x")) ")" ")" )))))) ; theorem :: RATFUNC1:35 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "being" ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" (Set (Var "p")) ($#k5_ratfunc1 :::"`2"::: ) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "holds" (Bool (Set ($#k13_ratfunc1 :::"eval"::: ) "(" (Set "(" ($#k6_ratfunc1 :::"NormRationalFunction"::: ) (Set (Var "p")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_ratfunc1 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ))))) ; theorem :: RATFUNC1:36 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "being" ($#m1_ratfunc1 :::"rational_function"::: ) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" "not" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" (Set (Var "p")) ($#k5_ratfunc1 :::"`2"::: ) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) "or" (Bool (Set (Var "x")) ($#r1_ratfunc1 :::"is_a_common_root_of"::: ) (Set (Set (Var "p")) ($#k4_ratfunc1 :::"`1"::: ) ) "," (Set (Set (Var "p")) ($#k5_ratfunc1 :::"`2"::: ) )) "or" (Bool (Set ($#k13_ratfunc1 :::"eval"::: ) "(" (Set "(" ($#k11_ratfunc1 :::"NF"::: ) (Set (Var "p")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_ratfunc1 :::"eval"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" )) ")" )))) ;