:: INT_6 semantic presentation begin registrationlet "f" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::); let "n" be ($#m1_hidden :::"Nat":::); cluster (Set "f" ($#k16_finseq_1 :::"|"::: ) "n") -> ($#v1_valued_0 :::"complex-valued"::: ) ; end; registrationlet "f" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::); let "n" be ($#m1_hidden :::"Nat":::); cluster (Set "f" ($#k16_finseq_1 :::"|"::: ) "n") -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "f" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::); let "n" be ($#m1_hidden :::"Nat":::); cluster (Set "f" ($#k1_rfinseq :::"/^"::: ) "n") -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "i" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k5_finseq_1 :::"<*"::: ) "i" ($#k5_finseq_1 :::"*>"::: ) ) -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "f", "g" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "f" ($#k7_finseq_1 :::"^"::: ) "g") -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; theorem :: INT_6:1 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "f1")) ($#k1_valued_1 :::"+"::: ) (Set (Var "f2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_nat_1 :::"min"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1")) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f2")) ")" ) ")" ))) ; theorem :: INT_6:2 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "f1")) ($#k45_valued_1 :::"-"::: ) (Set (Var "f2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_nat_1 :::"min"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1")) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f2")) ")" ) ")" ))) ; theorem :: INT_6:3 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "f1")) ($#k18_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_nat_1 :::"min"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1")) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f2")) ")" ) ")" ))) ; theorem :: INT_6:4 (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "m1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "m2"))))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "m1"))))) "holds" (Bool (Set (Set "(" (Set (Var "m1")) ($#k18_valued_1 :::"(#)"::: ) (Set (Var "m2")) ")" ) ($#k16_finseq_1 :::"|"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "m1")) ($#k16_finseq_1 :::"|"::: ) (Set (Var "k")) ")" ) ($#k18_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "m2")) ($#k16_finseq_1 :::"|"::: ) (Set (Var "k")) ")" ))))) ; registrationlet "F" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set ($#k16_rvsum_1 :::"Sum"::: ) "F") -> ($#v1_int_1 :::"integer"::: ) ; cluster (Set ($#k19_rvsum_1 :::"Product"::: ) "F") -> ($#v1_int_1 :::"integer"::: ) ; end; theorem :: INT_6:5 (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k16_finseq_1 :::"|"::: ) (Set (Var "i")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k9_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k16_finseq_1 :::"|"::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ))))) ; theorem :: INT_6:6 (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (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 ($#k6_numbers :::"0"::: ) )) ")" ))) "holds" (Bool (Set ($#k19_rvsum_1 :::"Product"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: INT_6:7 (Bool "for" (Set (Var "n")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k6_int_1 :::"mod"::: ) (Set (Var "n")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k6_int_1 :::"mod"::: ) (Set (Var "n")) ")" ) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "n"))))) ; theorem :: INT_6:8 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_int_1 :::"divides"::: ) (Set (Var "j")))) "holds" (Bool (Set (Set (Var "k")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "i"))) ($#r1_int_1 :::"divides"::: ) (Set (Set (Var "k")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "j"))))) ; theorem :: INT_6:9 (Bool "for" (Set (Var "m")) "being" (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::) (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 "m")))) & (Bool (Set (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k19_rvsum_1 :::"Product"::: ) (Set (Var "m")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )) "is" ($#m1_hidden :::"Integer":::)))) ; theorem :: INT_6:10 (Bool "for" (Set (Var "m")) "being" (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::) (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 "m"))))) "holds" (Bool "ex" (Set (Var "z")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Set (Var "z")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k19_rvsum_1 :::"Product"::: ) (Set (Var "m"))))))) ; theorem :: INT_6:11 (Bool "for" (Set (Var "m")) "being" (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "m")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "m")))) & (Bool (Set (Var "j")) ($#r1_hidden :::"<>"::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k19_rvsum_1 :::"Product"::: ) (Set (Var "m")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set "(" (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")) ")" ) ")" )) "is" ($#m1_hidden :::"Integer":::)))) ; theorem :: INT_6:12 (Bool "for" (Set (Var "m")) "being" (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "m")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "m")))) & (Bool (Set (Var "j")) ($#r1_hidden :::"<>"::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "z")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Set (Var "z")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k19_rvsum_1 :::"Product"::: ) (Set (Var "m")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")) ")" )))))) ; begin theorem :: INT_6:13 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" (Bool (Set ($#k1_int_2 :::"abs"::: ) (Set (Var "i"))) ($#r1_int_1 :::"divides"::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_int_1 :::"divides"::: ) (Set ($#k1_int_2 :::"abs"::: ) (Set (Var "i")))) ")" )) ; theorem :: INT_6:14 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set (Var "i")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k3_int_2 :::"gcd"::: ) (Set "(" ($#k1_int_2 :::"abs"::: ) (Set (Var "j")) ")" )))) ; theorem :: INT_6:15 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "i")) "," (Set (Var "j")) ($#r1_int_2 :::"are_relative_prime"::: ) )) "holds" (Bool (Set (Set (Var "i")) ($#k2_int_2 :::"lcm"::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set ($#k1_int_2 :::"abs"::: ) (Set "(" (Set (Var "i")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "j")) ")" )))) ; theorem :: INT_6:16 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set "(" (Set (Var "i")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "j")) ")" ) ($#k3_int_2 :::"gcd"::: ) (Set "(" (Set (Var "i")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_int_2 :::"abs"::: ) (Set (Var "i")) ")" ) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "j")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "k")) ")" )))) ; theorem :: INT_6:17 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set "(" (Set (Var "i")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "j")) ")" ) ($#k3_int_2 :::"gcd"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_int_2 :::"abs"::: ) (Set (Var "i"))))) ; theorem :: INT_6:18 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set (Var "i")) ($#k3_int_2 :::"gcd"::: ) (Set "(" (Set (Var "j")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "i")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "j")) ")" ) ($#k3_int_2 :::"gcd"::: ) (Set (Var "k"))))) ; theorem :: INT_6:19 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "i")) "," (Set (Var "j")) ($#r1_int_2 :::"are_relative_prime"::: ) )) "holds" (Bool (Set (Set (Var "i")) ($#k3_int_2 :::"gcd"::: ) (Set "(" (Set (Var "j")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k3_int_2 :::"gcd"::: ) (Set (Var "k"))))) ; theorem :: INT_6:20 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "i")) "," (Set (Var "j")) ($#r1_int_2 :::"are_relative_prime"::: ) )) "holds" (Bool (Set (Set (Var "i")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "j"))) ($#r1_int_1 :::"divides"::: ) (Set (Set (Var "i")) ($#k2_int_2 :::"lcm"::: ) (Set (Var "j"))))) ; theorem :: INT_6:21 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "i")) "," (Set (Var "j")) ($#r1_int_2 :::"are_relative_prime"::: ) ) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Var "i"))) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Var "j")))) "holds" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Set (Var "i")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "j"))))) ; theorem :: INT_6:22 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "i")) "," (Set (Var "j")) ($#r1_int_2 :::"are_relative_prime"::: ) )) "holds" (Bool "ex" (Set (Var "s")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Set (Var "s")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "i"))) "," (Num 1) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Var "j"))))) ; begin notationlet "f" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::); antonym :::"multiplicative-trivial"::: "f" for :::"non-empty"::: ; end; definitionlet "f" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::); redefine attr "f" is :::"non-empty"::: means :: INT_6:def 1 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" "not" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "f")) "or" "not" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )); end; :: deftheorem defines :::"multiplicative-trivial"::: INT_6:def 1 : (Bool "for" (Set (Var "f")) "being" (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "f")) "is" ($#v2_relat_1 :::"multiplicative-trivial"::: ) )) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" "not" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) "or" "not" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v2_relat_1 :::"multiplicative-trivial"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#~v2_relat_1 "non" ($#v2_relat_1 :::"multiplicative-trivial"::: ) ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_FINSET_1() ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) ($#v1_partfun3 :::"positive-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: INT_6:23 (Bool "for" (Set (Var "m")) "being" ($#v2_relat_1 :::"multiplicative-trivial"::: ) (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k19_rvsum_1 :::"Product"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; definitionlet "f" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::); attr "f" is :::"Chinese_Remainder"::: means :: INT_6:def 2 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "f")) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "f")) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j")))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "," (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_int_2 :::"are_relative_prime"::: ) )); end; :: deftheorem defines :::"Chinese_Remainder"::: INT_6:def 2 : (Bool "for" (Set (Var "f")) "being" (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_int_6 :::"Chinese_Remainder"::: ) ) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "," (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_int_2 :::"are_relative_prime"::: ) )) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_FINSET_1() ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) ($#v1_partfun3 :::"positive-yielding"::: ) ($#v1_int_6 :::"Chinese_Remainder"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionmode CR_Sequence is (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_partfun3 :::"positive-yielding"::: ) ($#v1_int_6 :::"Chinese_Remainder"::: ) ($#m1_hidden :::"FinSequence":::); end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v1_partfun3 :::"positive-yielding"::: ) ($#v1_int_6 :::"Chinese_Remainder"::: ) -> ($#~v2_relat_1 "non" ($#v2_relat_1 :::"multiplicative-trivial"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v2_relat_1 :::"multiplicative-trivial"::: ) (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: INT_6:24 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"CR_Sequence":::) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k16_finseq_1 :::"|"::: ) (Set (Var "m"))) "is" ($#m1_hidden :::"CR_Sequence":::)))) ; registrationlet "m" be ($#m1_hidden :::"CR_Sequence":::); cluster (Set ($#k19_rvsum_1 :::"Product"::: ) "m") -> ($#v7_ordinal1 :::"natural"::: ) ($#v2_xxreal_0 :::"positive"::: ) ; end; theorem :: INT_6:25 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"CR_Sequence":::) (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 "m"))))) "holds" (Bool "for" (Set (Var "mm")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "mm")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k19_rvsum_1 :::"Product"::: ) (Set (Var "m")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )))) "holds" (Bool (Set (Var "mm")) "," (Set (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_int_2 :::"are_relative_prime"::: ) )))) ; begin definitionlet "u" be ($#m1_hidden :::"Integer":::); let "m" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::); func :::"mod"::: "(" "u" "," "m" ")" -> ($#m1_hidden :::"FinSequence":::) means :: INT_6:def 3 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "m")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set "u" ($#k6_int_1 :::"mod"::: ) (Set "(" "m" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"mod"::: INT_6:def 3 : (Bool "for" (Set (Var "u")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "m")) "being" (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_int_6 :::"mod"::: ) "(" (Set (Var "u")) "," (Set (Var "m")) ")" )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "m")))) & (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 "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k6_int_1 :::"mod"::: ) (Set "(" (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ) ")" )))); registrationlet "u" be ($#m1_hidden :::"Integer":::); let "m" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set ($#k1_int_6 :::"mod"::: ) "(" "u" "," "m" ")" ) -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; definitionlet "m" be ($#m1_hidden :::"CR_Sequence":::); mode :::"CR_coefficients"::: "of" "m" -> ($#m1_hidden :::"FinSequence":::) means :: INT_6:def 4 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "m")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) it))) "holds" (Bool "ex" (Set (Var "s")) "," (Set (Var "mm")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool "(" (Bool (Set (Var "mm")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k19_rvsum_1 :::"Product"::: ) "m" ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" "m" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) & (Bool (Set (Set (Var "s")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "mm"))) "," (Num 1) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set "m" ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" ($#k19_rvsum_1 :::"Product"::: ) "m" ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" "m" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ")" ))) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"CR_coefficients"::: INT_6:def 4 : (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"CR_Sequence":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_int_6 :::"CR_coefficients"::: ) "of" (Set (Var "m"))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "m")))) & (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 "b2"))))) "holds" (Bool "ex" (Set (Var "s")) "," (Set (Var "mm")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool "(" (Bool (Set (Var "mm")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k19_rvsum_1 :::"Product"::: ) (Set (Var "m")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) & (Bool (Set (Set (Var "s")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "mm"))) "," (Num 1) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" ($#k19_rvsum_1 :::"Product"::: ) (Set (Var "m")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ")" ))) ")" )) ")" ) ")" ) ")" ))); registrationlet "m" be ($#m1_hidden :::"CR_Sequence":::); cluster -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) for ($#m1_int_6 :::"CR_coefficients"::: ) "of" "m"; end; theorem :: INT_6:26 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"CR_Sequence":::) (Bool "for" (Set (Var "c")) "being" ($#m1_int_6 :::"CR_coefficients"::: ) "of" (Set (Var "m")) (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 "c"))))) "holds" (Bool (Set (Set (Var "c")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "," (Num 1) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))))) ; theorem :: INT_6:27 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"CR_Sequence":::) (Bool "for" (Set (Var "c")) "being" ($#m1_int_6 :::"CR_coefficients"::: ) "of" (Set (Var "m")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "c")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "c")))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j")))) "holds" (Bool (Set (Set (Var "c")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "," (Set ($#k6_numbers :::"0"::: ) ) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))))) ; theorem :: INT_6:28 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"CR_Sequence":::) (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#m1_int_6 :::"CR_coefficients"::: ) "of" (Set (Var "m")) (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 "c1"))))) "holds" (Bool (Set (Set (Var "c1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "," (Set (Set (Var "c2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))))) ; theorem :: INT_6:29 (Bool "for" (Set (Var "u")) "being" (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"CR_Sequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "u"))))) "holds" (Bool "for" (Set (Var "c")) "being" ($#m1_int_6 :::"CR_coefficients"::: ) "of" (Set (Var "m")) (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 "m"))))) "holds" (Bool (Set ($#k16_rvsum_1 :::"Sum"::: ) (Set "(" (Set (Var "u")) ($#k18_valued_1 :::"(#)"::: ) (Set (Var "c")) ")" )) "," (Set (Set (Var "u")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))))))) ; theorem :: INT_6:30 (Bool "for" (Set (Var "u")) "being" (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"CR_Sequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "u"))))) "holds" (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#m1_int_6 :::"CR_coefficients"::: ) "of" (Set (Var "m")) "holds" (Bool (Set ($#k16_rvsum_1 :::"Sum"::: ) (Set "(" (Set (Var "u")) ($#k18_valued_1 :::"(#)"::: ) (Set (Var "c1")) ")" )) "," (Set ($#k16_rvsum_1 :::"Sum"::: ) (Set "(" (Set (Var "u")) ($#k18_valued_1 :::"(#)"::: ) (Set (Var "c2")) ")" )) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set ($#k19_rvsum_1 :::"Product"::: ) (Set (Var "m"))))))) ; definitionlet "u" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::); let "m" be ($#m1_hidden :::"CR_Sequence":::); assume (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Const "m"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Const "u")))) ; func :::"to_int"::: "(" "u" "," "m" ")" -> ($#m1_hidden :::"Integer":::) means :: INT_6:def 5 (Bool "for" (Set (Var "c")) "being" ($#m1_int_6 :::"CR_coefficients"::: ) "of" "m" "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k16_rvsum_1 :::"Sum"::: ) (Set "(" "u" ($#k18_valued_1 :::"(#)"::: ) (Set (Var "c")) ")" ) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" ($#k19_rvsum_1 :::"Product"::: ) "m" ")" )))); end; :: deftheorem defines :::"to_int"::: INT_6:def 5 : (Bool "for" (Set (Var "u")) "being" (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"CR_Sequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "u"))))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_int_6 :::"to_int"::: ) "(" (Set (Var "u")) "," (Set (Var "m")) ")" )) "iff" (Bool "for" (Set (Var "c")) "being" ($#m1_int_6 :::"CR_coefficients"::: ) "of" (Set (Var "m")) "holds" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k16_rvsum_1 :::"Sum"::: ) (Set "(" (Set (Var "u")) ($#k18_valued_1 :::"(#)"::: ) (Set (Var "c")) ")" ) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" ($#k19_rvsum_1 :::"Product"::: ) (Set (Var "m")) ")" )))) ")" )))); theorem :: INT_6:31 (Bool "for" (Set (Var "u")) "being" (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"CR_Sequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "u"))))) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_int_6 :::"to_int"::: ) "(" (Set (Var "u")) "," (Set (Var "m")) ")" )) & (Bool (Set ($#k2_int_6 :::"to_int"::: ) "(" (Set (Var "u")) "," (Set (Var "m")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k19_rvsum_1 :::"Product"::: ) (Set (Var "m")))) ")" ))) ; theorem :: INT_6:32 (Bool "for" (Set (Var "u")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"CR_Sequence":::) (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 "m"))))) "holds" (Bool (Set (Var "u")) "," (Set (Set "(" ($#k1_int_6 :::"mod"::: ) "(" (Set (Var "u")) "," (Set (Var "m")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))))) ; theorem :: INT_6:33 (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"CR_Sequence":::) (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 "m"))))) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_int_6 :::"mod"::: ) "(" (Set (Var "u")) "," (Set (Var "m")) ")" ")" ) ($#k4_rvsum_1 :::"+"::: ) (Set "(" ($#k1_int_6 :::"mod"::: ) "(" (Set (Var "v")) "," (Set (Var "m")) ")" ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "," (Set (Set (Var "u")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "v"))) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))))) ; theorem :: INT_6:34 (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"CR_Sequence":::) (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 "m"))))) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_int_6 :::"mod"::: ) "(" (Set (Var "u")) "," (Set (Var "m")) ")" ")" ) ($#k18_valued_1 :::"(#)"::: ) (Set "(" ($#k1_int_6 :::"mod"::: ) "(" (Set (Var "v")) "," (Set (Var "m")) ")" ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "," (Set (Set (Var "u")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "v"))) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))))) ; theorem :: INT_6:35 (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"CR_Sequence":::) (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 "m"))))) "holds" (Bool (Set ($#k2_int_6 :::"to_int"::: ) "(" (Set "(" (Set "(" ($#k1_int_6 :::"mod"::: ) "(" (Set (Var "u")) "," (Set (Var "m")) ")" ")" ) ($#k4_rvsum_1 :::"+"::: ) (Set "(" ($#k1_int_6 :::"mod"::: ) "(" (Set (Var "v")) "," (Set (Var "m")) ")" ")" ) ")" ) "," (Set (Var "m")) ")" ) "," (Set (Set (Var "u")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "v"))) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))))) ; theorem :: INT_6:36 (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"CR_Sequence":::) (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 "m"))))) "holds" (Bool (Set ($#k2_int_6 :::"to_int"::: ) "(" (Set "(" (Set "(" ($#k1_int_6 :::"mod"::: ) "(" (Set (Var "u")) "," (Set (Var "m")) ")" ")" ) ($#k8_rvsum_1 :::"-"::: ) (Set "(" ($#k1_int_6 :::"mod"::: ) "(" (Set (Var "v")) "," (Set (Var "m")) ")" ")" ) ")" ) "," (Set (Var "m")) ")" ) "," (Set (Set (Var "u")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "v"))) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))))) ; theorem :: INT_6:37 (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"CR_Sequence":::) (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 "m"))))) "holds" (Bool (Set ($#k2_int_6 :::"to_int"::: ) "(" (Set "(" (Set "(" ($#k1_int_6 :::"mod"::: ) "(" (Set (Var "u")) "," (Set (Var "m")) ")" ")" ) ($#k18_valued_1 :::"(#)"::: ) (Set "(" ($#k1_int_6 :::"mod"::: ) "(" (Set (Var "v")) "," (Set (Var "m")) ")" ")" ) ")" ) "," (Set (Var "m")) ")" ) "," (Set (Set (Var "u")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "v"))) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))))) ; theorem :: INT_6:38 (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"CR_Sequence":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "u")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "v")))) & (Bool (Set (Set (Var "u")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "v"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k19_rvsum_1 :::"Product"::: ) (Set (Var "m"))))) "holds" (Bool (Set ($#k2_int_6 :::"to_int"::: ) "(" (Set "(" (Set "(" ($#k1_int_6 :::"mod"::: ) "(" (Set (Var "u")) "," (Set (Var "m")) ")" ")" ) ($#k4_rvsum_1 :::"+"::: ) (Set "(" ($#k1_int_6 :::"mod"::: ) "(" (Set (Var "v")) "," (Set (Var "m")) ")" ")" ) ")" ) "," (Set (Var "m")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "v")))))) ; theorem :: INT_6:39 (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"CR_Sequence":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "u")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "v")))) & (Bool (Set (Set (Var "u")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "v"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k19_rvsum_1 :::"Product"::: ) (Set (Var "m"))))) "holds" (Bool (Set ($#k2_int_6 :::"to_int"::: ) "(" (Set "(" (Set "(" ($#k1_int_6 :::"mod"::: ) "(" (Set (Var "u")) "," (Set (Var "m")) ")" ")" ) ($#k8_rvsum_1 :::"-"::: ) (Set "(" ($#k1_int_6 :::"mod"::: ) "(" (Set (Var "v")) "," (Set (Var "m")) ")" ")" ) ")" ) "," (Set (Var "m")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "v")))))) ; theorem :: INT_6:40 (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"CR_Sequence":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "u")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "v")))) & (Bool (Set (Set (Var "u")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "v"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k19_rvsum_1 :::"Product"::: ) (Set (Var "m"))))) "holds" (Bool (Set ($#k2_int_6 :::"to_int"::: ) "(" (Set "(" (Set "(" ($#k1_int_6 :::"mod"::: ) "(" (Set (Var "u")) "," (Set (Var "m")) ")" ")" ) ($#k18_valued_1 :::"(#)"::: ) (Set "(" ($#k1_int_6 :::"mod"::: ) "(" (Set (Var "v")) "," (Set (Var "m")) ")" ")" ) ")" ) "," (Set (Var "m")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "v")))))) ; begin theorem :: INT_6:41 (Bool "for" (Set (Var "u")) "being" (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"CR_Sequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "m"))))) "holds" (Bool "ex" (Set (Var "z")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "z"))) & (Bool (Set (Var "z")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k19_rvsum_1 :::"Product"::: ) (Set (Var "m")))) & (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 "u"))))) "holds" (Bool (Set (Var "z")) "," (Set (Set (Var "u")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" )))) ; theorem :: INT_6:42 (Bool "for" (Set (Var "u")) "being" (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"CR_Sequence":::) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "z1"))) & (Bool (Set (Var "z1")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k19_rvsum_1 :::"Product"::: ) (Set (Var "m")))) & (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 "m"))))) "holds" (Bool (Set (Var "z1")) "," (Set (Set (Var "u")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "z2"))) & (Bool (Set (Var "z2")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k19_rvsum_1 :::"Product"::: ) (Set (Var "m")))) & (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 "m"))))) "holds" (Bool (Set (Var "z2")) "," (Set (Set (Var "u")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_int_1 :::"are_congruent_mod"::: ) (Set (Set (Var "m")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" )) "holds" (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Var "z2")))))) ;