:: POLYEQ_4 semantic presentation begin theorem :: POLYEQ_4:1 (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set (Var "b")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "c")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: POLYEQ_4:2 (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set (Var "b")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "c")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: POLYEQ_4:3 (Bool "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" "not" (Bool (Set (Set (Var "c")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) "or" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )) ; theorem :: POLYEQ_4:4 (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) "is" ($#v1_abian :::"even"::: ) ) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Set (Var "x")) ($#k2_newton :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_power :::"-root"::: ) (Set (Var "a")))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "n")) ($#k2_power :::"-root"::: ) (Set (Var "a")) ")" ))))) ; theorem :: POLYEQ_4:5 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k4_polyeq_1 :::"Polynom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "a")) ")" )))) ; theorem :: POLYEQ_4:6 (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k4_polyeq_1 :::"Polynom"::: ) "(" (Set (Var "a")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: POLYEQ_4:7 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) "is" ($#v1_abian :::"odd"::: ) ) & (Bool (Set ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k4_polyeq_1 :::"Polynom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set "(" (Set (Var "x")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ")" ))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ")" ))))) ; theorem :: POLYEQ_4:8 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "b")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "c")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) "is" ($#v1_abian :::"even"::: ) ) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k4_polyeq_1 :::"Polynom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set "(" (Set (Var "x")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ")" )))) & (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ")" )))) & (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ")" ))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ")" ))))) ; theorem :: POLYEQ_4:9 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) "is" ($#v1_abian :::"odd"::: ) ) & (Bool (Set ($#k4_polyeq_1 :::"Polynom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "x")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "a")) ")" ) ")" ))))) ; theorem :: POLYEQ_4:10 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "b")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) "is" ($#v1_abian :::"even"::: ) ) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set ($#k4_polyeq_1 :::"Polynom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "x")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "a")) ")" ) ")" ))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "a")) ")" ) ")" ) ")" ))))) ; theorem :: POLYEQ_4:11 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k2_newton :::"|^"::: ) (Num 3) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k2_newton :::"|^"::: ) (Num 5) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k2_newton :::"|^"::: ) (Num 5) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k2_newton :::"|^"::: ) (Num 4) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k2_newton :::"|^"::: ) (Num 2) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k2_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k2_newton :::"|^"::: ) (Num 4) ")" ) ")" ))) ")" )) ; theorem :: POLYEQ_4:12 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set (Var "b")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k8_polyeq_1 :::"Polynom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Num 1)))) & (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "b")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "b")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" )))) ; definitionlet "a", "b", "c", "d", "e", "f", "x" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; func :::"Polynom"::: "(" "a" "," "b" "," "c" "," "d" "," "e" "," "f" "," "x" ")" -> ($#m1_hidden :::"set"::: ) equals :: POLYEQ_4:def 1 (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" "a" ($#k3_xcmplx_0 :::"*"::: ) (Set "(" "x" ($#k1_newton :::"|^"::: ) (Num 5) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" "b" ($#k3_xcmplx_0 :::"*"::: ) (Set "(" "x" ($#k1_newton :::"|^"::: ) (Num 4) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" "c" ($#k3_xcmplx_0 :::"*"::: ) (Set "(" "x" ($#k1_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" "d" ($#k3_xcmplx_0 :::"*"::: ) (Set "(" "x" ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" "e" ($#k3_xcmplx_0 :::"*"::: ) "x" ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) "f"); end; :: deftheorem defines :::"Polynom"::: POLYEQ_4:def 1 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "x")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_polyeq_4 :::"Polynom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k1_newton :::"|^"::: ) (Num 5) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k1_newton :::"|^"::: ) (Num 4) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k1_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "d")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "e")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "f"))))); registrationlet "a", "b", "c", "d", "e", "f", "x" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k1_polyeq_4 :::"Polynom"::: ) "(" "a" "," "b" "," "c" "," "d" "," "e" "," "f" "," "x" ")" ) -> ($#v1_xcmplx_0 :::"complex"::: ) ; end; registrationlet "a", "b", "c", "d", "e", "f", "x" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k1_polyeq_4 :::"Polynom"::: ) "(" "a" "," "b" "," "c" "," "d" "," "e" "," "f" "," "x" ")" ) -> ($#v1_xreal_0 :::"real"::: ) ; end; theorem :: POLYEQ_4:13 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "b")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 5) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k1_polyeq_4 :::"Polynom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "b")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 5) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ))) & (Bool (Set (Var "y2")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "b")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 5) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ))) & (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Num 1)))) & (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "y1")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" ($#k1_quin_1 :::"delta"::: ) "(" (Num 1) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "y1")) ")" ) "," (Num 1) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2)))) & (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "y2")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" ($#k1_quin_1 :::"delta"::: ) "(" (Num 1) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "y2")) ")" ) "," (Num 1) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2)))) & (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "y1")) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" ($#k1_quin_1 :::"delta"::: ) "(" (Num 1) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "y1")) ")" ) "," (Num 1) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "y2")) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" ($#k1_quin_1 :::"delta"::: ) "(" (Num 1) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "y2")) ")" ) "," (Num 1) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2))))) ; theorem :: POLYEQ_4:14 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set (Var "x")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "not" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2))) ")" ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2))) ")" )) ; theorem :: POLYEQ_4:15 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set "(" (Set (Var "x")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) "is" ($#v1_abian :::"odd"::: ) ) & (Bool "not" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ))) ")" ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ))) ")" ))) ; theorem :: POLYEQ_4:16 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set "(" (Set (Var "x")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "q")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) "is" ($#v1_abian :::"even"::: ) ) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool "not" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ))) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ))) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ))) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ))) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ))) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ))) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ))) ")" ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q")) ")" ) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ))) ")" ))) ; theorem :: POLYEQ_4:17 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set "(" (Set (Var "x")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "y")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "n")) "is" ($#v1_abian :::"even"::: ) ) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "not" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ))) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ))) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ))) ")" ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ))) ")" ))) ; theorem :: POLYEQ_4:18 (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "b")) "," (Set (Var "y")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set (Var "x")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) "is" ($#v1_abian :::"odd"::: ) ) & (Bool (Set (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "not" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set (Var "p")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "b")) ")" ))) ")" ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set (Var "p")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "a")) ")" ))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; theorem :: POLYEQ_4:19 (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "b")) "," (Set (Var "y")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set (Var "x")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) "is" ($#v1_abian :::"even"::: ) ) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Set (Var "p")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "p")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "not" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set (Var "p")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "b")) ")" ))) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set (Var "p")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "b")) ")" ) ")" ))) ")" )) & (Bool "not" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set (Var "p")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "a")) ")" ))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set (Var "p")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "a")) ")" ) ")" ))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; theorem :: POLYEQ_4:20 (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "p")) "," (Set (Var "y")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set (Var "x")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Var "n")) "is" ($#v1_abian :::"odd"::: ) ) & (Bool (Set (Set (Var "p")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set (Var "p")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "a")) ")" ))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set (Var "a")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "p")) ")" ) ")" ))) ")" ))) ; theorem :: POLYEQ_4:21 (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "p")) "," (Set (Var "y")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Set (Var "x")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Var "n")) "is" ($#v1_abian :::"even"::: ) ) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Set (Var "p")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "not" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set (Var "p")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "a")) ")" ))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set (Var "a")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "p")) ")" ) ")" ))) ")" ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set (Var "p")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "a")) ")" ) ")" ))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "q")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "n")) ($#k1_power :::"-root"::: ) (Set "(" (Set (Var "a")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "p")) ")" ) ")" ) ")" ))) ")" ))) ; theorem :: POLYEQ_4:22 (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Set (Var "a")) ($#k4_power :::"to_power"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: POLYEQ_4:23 (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Set (Var "a")) ($#k4_power :::"to_power"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: POLYEQ_4:24 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k6_power :::"log"::: ) "(" (Set (Var "a")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: POLYEQ_4:25 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k6_power :::"log"::: ) "(" (Set (Var "a")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "a")))) ;