:: INT_3 semantic presentation begin definitionredefine func :::"multint"::: means :: INT_3:def 1 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k35_binop_2 :::"multreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))); end; :: deftheorem defines :::"multint"::: INT_3:def 1 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set ($#k4_numbers :::"INT"::: ) ) "," (Set ($#k4_numbers :::"INT"::: ) ))) "," (Set ($#k4_numbers :::"INT"::: ) ))))) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k46_binop_2 :::"multint"::: ) )) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k35_binop_2 :::"multreal"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) ")" )); definitionredefine func :::"compint"::: means :: INT_3:def 2 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k31_binop_2 :::"compreal"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))); end; :: deftheorem defines :::"compint"::: INT_3:def 2 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set ($#k4_numbers :::"INT"::: ) ) "," (Set ($#k4_numbers :::"INT"::: ) ))))) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k43_binop_2 :::"compint"::: ) )) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k31_binop_2 :::"compreal"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))) ")" )); definitionfunc :::"INT.Ring"::: -> ($#l6_algstr_0 :::"doubleLoopStr"::: ) equals :: INT_3:def 3 (Set ($#g6_algstr_0 :::"doubleLoopStr"::: ) "(#" (Set ($#k4_numbers :::"INT"::: ) ) "," (Set ($#k44_binop_2 :::"addint"::: ) ) "," (Set ($#k46_binop_2 :::"multint"::: ) ) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Num 1) "," (Set ($#k4_numbers :::"INT"::: ) ) ")" ")" ) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k4_numbers :::"INT"::: ) ) ")" ")" ) "#)" ); end; :: deftheorem defines :::"INT.Ring"::: INT_3:def 3 : (Bool (Set ($#k1_int_3 :::"INT.Ring"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g6_algstr_0 :::"doubleLoopStr"::: ) "(#" (Set ($#k4_numbers :::"INT"::: ) ) "," (Set ($#k44_binop_2 :::"addint"::: ) ) "," (Set ($#k46_binop_2 :::"multint"::: ) ) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Num 1) "," (Set ($#k4_numbers :::"INT"::: ) ) ")" ")" ) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k4_numbers :::"INT"::: ) ) ")" ")" ) "#)" )); registration cluster (Set ($#k1_int_3 :::"INT.Ring"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v36_algstr_0 :::"strict"::: ) ; end; registration cluster (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k1_int_3 :::"INT.Ring"::: ) )) -> ($#v5_membered :::"integer-membered"::: ) ; end; registrationlet "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_int_3 :::"INT.Ring"::: ) ); let "c", "d" be ($#m1_hidden :::"Integer":::); identify ; identify ; end; registration cluster (Set ($#k1_int_3 :::"INT.Ring"::: ) ) -> ($#v4_vectsp_1 :::"well-unital"::: ) ; end; registration cluster (Set ($#k1_int_3 :::"INT.Ring"::: ) ) -> ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ; end; registrationlet "a" be ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_int_3 :::"INT.Ring"::: ) ); let "b" be ($#m1_hidden :::"Integer":::); identify ; end; definitionlet "a" be ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_int_3 :::"INT.Ring"::: ) ); :: original: :::"|."::: redefine func :::"abs"::: "a" -> ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_int_3 :::"INT.Ring"::: ) ) equals :: INT_3:def 4 "a" if (Bool "a" ($#r1_xxreal_0 :::">="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_int_3 :::"INT.Ring"::: ) ))) otherwise (Set ($#k4_algstr_0 :::"-"::: ) "a"); end; :: deftheorem defines :::"abs"::: INT_3:def 4 : (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_int_3 :::"INT.Ring"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_int_3 :::"INT.Ring"::: ) )))) "implies" (Bool (Set ($#k2_int_3 :::"abs"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "a")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_int_3 :::"INT.Ring"::: ) ))))) "implies" (Bool (Set ($#k2_int_3 :::"abs"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "a")))) ")" ")" )); definitionfunc :::"absint"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k1_int_3 :::"INT.Ring"::: ) )) "," (Set ($#k5_numbers :::"NAT"::: ) ) means :: INT_3:def 5 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_int_3 :::"INT.Ring"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_euclid :::"absreal"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))); end; :: deftheorem defines :::"absint"::: INT_3:def 5 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k1_int_3 :::"INT.Ring"::: ) )) "," (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k3_int_3 :::"absint"::: ) )) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_int_3 :::"INT.Ring"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_euclid :::"absreal"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))) ")" )); theorem :: INT_3:1 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_int_3 :::"INT.Ring"::: ) ) "holds" (Bool (Set (Set ($#k3_int_3 :::"absint"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k2_int_3 :::"abs"::: ) (Set (Var "a"))))) ; theorem :: INT_3:2 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "q1")) "," (Set (Var "q2")) "," (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_int_3 :::"INT.Ring"::: ) ) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_int_3 :::"INT.Ring"::: ) ))) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "q1")) ($#k8_group_1 :::"*"::: ) (Set (Var "b")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "r1")))) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_int_3 :::"INT.Ring"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r1"))) & (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k2_int_3 :::"abs"::: ) (Set (Var "b")))) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "q2")) ($#k8_group_1 :::"*"::: ) (Set (Var "b")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "r2")))) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_int_3 :::"INT.Ring"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r2"))) & (Bool (Set (Var "r2")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k2_int_3 :::"abs"::: ) (Set (Var "b"))))) "holds" (Bool "(" (Bool (Set (Var "q1")) ($#r1_hidden :::"="::: ) (Set (Var "q2"))) & (Bool (Set (Var "r1")) ($#r1_hidden :::"="::: ) (Set (Var "r2"))) ")" )) ; definitionlet "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_int_3 :::"INT.Ring"::: ) ); assume (Bool (Set (Const "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_int_3 :::"INT.Ring"::: ) ))) ; func "a" :::"div"::: "b" -> ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_int_3 :::"INT.Ring"::: ) ) means :: INT_3:def 6 (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_int_3 :::"INT.Ring"::: ) ) "st" (Bool "(" (Bool "a" ($#r1_hidden :::"="::: ) (Set (Set "(" it ($#k8_group_1 :::"*"::: ) "b" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "r")))) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_int_3 :::"INT.Ring"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k2_int_3 :::"abs"::: ) "b")) ")" )); end; :: deftheorem defines :::"div"::: INT_3:def 6 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_int_3 :::"INT.Ring"::: ) ) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_int_3 :::"INT.Ring"::: ) )))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_int_3 :::"INT.Ring"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k4_int_3 :::"div"::: ) (Set (Var "b")))) "iff" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_int_3 :::"INT.Ring"::: ) ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b3")) ($#k8_group_1 :::"*"::: ) (Set (Var "b")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "r")))) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_int_3 :::"INT.Ring"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k2_int_3 :::"abs"::: ) (Set (Var "b")))) ")" )) ")" ))); definitionlet "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_int_3 :::"INT.Ring"::: ) ); assume (Bool (Set (Const "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_int_3 :::"INT.Ring"::: ) ))) ; func "a" :::"mod"::: "b" -> ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_int_3 :::"INT.Ring"::: ) ) means :: INT_3:def 7 (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_int_3 :::"INT.Ring"::: ) ) "st" (Bool "(" (Bool "a" ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "q")) ($#k8_group_1 :::"*"::: ) "b" ")" ) ($#k3_rlvect_1 :::"+"::: ) it)) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_int_3 :::"INT.Ring"::: ) )) ($#r1_xxreal_0 :::"<="::: ) it) & (Bool it ($#r1_xxreal_0 :::"<"::: ) (Set ($#k2_int_3 :::"abs"::: ) "b")) ")" )); end; :: deftheorem defines :::"mod"::: INT_3:def 7 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_int_3 :::"INT.Ring"::: ) ) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_int_3 :::"INT.Ring"::: ) )))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_int_3 :::"INT.Ring"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k5_int_3 :::"mod"::: ) (Set (Var "b")))) "iff" (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_int_3 :::"INT.Ring"::: ) ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "q")) ($#k8_group_1 :::"*"::: ) (Set (Var "b")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b3")))) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_int_3 :::"INT.Ring"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b3"))) & (Bool (Set (Var "b3")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k2_int_3 :::"abs"::: ) (Set (Var "b")))) ")" )) ")" ))); theorem :: INT_3:3 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_int_3 :::"INT.Ring"::: ) ) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_int_3 :::"INT.Ring"::: ) )))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k4_int_3 :::"div"::: ) (Set (Var "b")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "b")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k5_int_3 :::"mod"::: ) (Set (Var "b")) ")" )))) ; begin definitionlet "I" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; attr "I" is :::"Euclidian"::: means :: INT_3:def 8 (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "I") "," (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "I" "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) "I"))) "holds" (Bool "ex" (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" "I" "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "q")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "r")))) & (Bool "(" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "I")) "or" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "r"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b")))) ")" ) ")" )))); end; :: deftheorem defines :::"Euclidian"::: INT_3:def 8 : (Bool "for" (Set (Var "I")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#v1_int_3 :::"Euclidian"::: ) ) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "I"))) "," (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "I"))))) "holds" (Bool "ex" (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "I")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "q")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "r")))) & (Bool "(" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "I")))) "or" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "r"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b")))) ")" ) ")" )))) ")" )); registration cluster (Set ($#k1_int_3 :::"INT.Ring"::: ) ) -> ($#v1_int_3 :::"Euclidian"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v36_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#v1_int_3 :::"Euclidian"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; definitionmode EuclidianRing is ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#v1_int_3 :::"Euclidian"::: ) ($#l6_algstr_0 :::"Ring":::); end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) bbbadV7_STRUCT_0() ($#v13_algstr_0 :::"right_complementable"::: ) ($#v36_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#v1_int_3 :::"Euclidian"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; definitionlet "E" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_int_3 :::"Euclidian"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; mode :::"DegreeFunction"::: "of" "E" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "E") "," (Set ($#k5_numbers :::"NAT"::: ) ) means :: INT_3:def 9 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "E" "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) "E"))) "holds" (Bool "ex" (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" "E" "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "q")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "r")))) & (Bool "(" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "E")) "or" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "r"))) ($#r1_xxreal_0 :::"<"::: ) (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "b")))) ")" ) ")" ))); end; :: deftheorem defines :::"DegreeFunction"::: INT_3:def 9 : (Bool "for" (Set (Var "E")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_int_3 :::"Euclidian"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "E"))) "," (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_int_3 :::"DegreeFunction"::: ) "of" (Set (Var "E"))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "E"))))) "holds" (Bool "ex" (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "E")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "q")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "r")))) & (Bool "(" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "E")))) "or" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "r"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "b")))) ")" ) ")" ))) ")" ))); theorem :: INT_3:4 (Bool "for" (Set (Var "E")) "being" ($#l6_algstr_0 :::"EuclidianRing":::) "holds" (Bool (Set (Var "E")) "is" ($#l6_algstr_0 :::"gcdDomain":::))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#v1_int_3 :::"Euclidian"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#v3_gcd_1 :::"gcd-like"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; definition:: original: :::"absint"::: redefine func :::"absint"::: -> ($#m1_int_3 :::"DegreeFunction"::: ) "of" (Set ($#k1_int_3 :::"INT.Ring"::: ) ); end; theorem :: INT_3:5 (Bool "for" (Set (Var "F")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) "holds" (Bool (Set (Var "F")) "is" ($#v1_int_3 :::"Euclidian"::: ) )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_int_3 :::"Euclidian"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; theorem :: INT_3:6 (Bool "for" (Set (Var "F")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) "," (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Var "f")) "is" ($#m1_int_3 :::"DegreeFunction"::: ) "of" (Set (Var "F"))))) ; begin definitionlet "n" be ($#m1_hidden :::"Nat":::); assume (Bool (Set (Const "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ; func :::"multint"::: "n" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k7_card_1 :::"Segm"::: ) "n" ")" ) means :: INT_3:def 10 (Bool "for" (Set (Var "k")) "," (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) "n") "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "k")) "," (Set (Var "l")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "k")) ($#k24_binop_2 :::"*"::: ) (Set (Var "l")) ")" ) ($#k4_nat_d :::"mod"::: ) "n"))); end; :: deftheorem defines :::"multint"::: INT_3:def 10 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k7_card_1 :::"Segm"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k7_int_3 :::"multint"::: ) (Set (Var "n")))) "iff" (Bool "for" (Set (Var "k")) "," (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "b2")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "k")) "," (Set (Var "l")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "k")) ($#k24_binop_2 :::"*"::: ) (Set (Var "l")) ")" ) ($#k4_nat_d :::"mod"::: ) (Set (Var "n"))))) ")" ))); definitionlet "n" be ($#m1_hidden :::"Nat":::); assume (Bool (Set (Const "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ; func :::"compint"::: "n" -> ($#m1_subset_1 :::"UnOp":::) "of" (Set "(" ($#k7_card_1 :::"Segm"::: ) "n" ")" ) means :: INT_3:def 11 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) "n") "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "n" ($#k21_binop_2 :::"-"::: ) (Set (Var "k")) ")" ) ($#k6_int_1 :::"mod"::: ) "n"))); end; :: deftheorem defines :::"compint"::: INT_3:def 11 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set "(" ($#k7_card_1 :::"Segm"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k8_int_3 :::"compint"::: ) (Set (Var "n")))) "iff" (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Set (Var "n"))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k21_binop_2 :::"-"::: ) (Set (Var "k")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set (Var "n"))))) ")" ))); theorem :: INT_3:7 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Set (Var "n"))) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "a")) ($#k23_binop_2 :::"+"::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "implies" (Bool (Set (Set "(" ($#k3_gr_cy_1 :::"addint"::: ) (Set (Var "n")) ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k23_binop_2 :::"+"::: ) (Set (Var "b")))) ")" & "(" (Bool (Bool (Set (Set "(" ($#k3_gr_cy_1 :::"addint"::: ) (Set (Var "n")) ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k23_binop_2 :::"+"::: ) (Set (Var "b"))))) "implies" (Bool (Set (Set (Var "a")) ($#k23_binop_2 :::"+"::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) ")" & "(" (Bool (Bool (Set (Set (Var "a")) ($#k23_binop_2 :::"+"::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::">="::: ) (Set (Var "n")))) "implies" (Bool (Set (Set "(" ($#k3_gr_cy_1 :::"addint"::: ) (Set (Var "n")) ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k23_binop_2 :::"+"::: ) (Set (Var "b")) ")" ) ($#k21_binop_2 :::"-"::: ) (Set (Var "n")))) ")" & "(" (Bool (Bool (Set (Set "(" ($#k3_gr_cy_1 :::"addint"::: ) (Set (Var "n")) ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k23_binop_2 :::"+"::: ) (Set (Var "b")) ")" ) ($#k21_binop_2 :::"-"::: ) (Set (Var "n"))))) "implies" (Bool (Set (Set (Var "a")) ($#k23_binop_2 :::"+"::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::">="::: ) (Set (Var "n"))) ")" ")" ))) ; theorem :: INT_3:8 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool "(" (Bool (Set (Set (Var "k")) ($#k24_binop_2 :::"*"::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "a")) ($#k24_binop_2 :::"*"::: ) (Set (Var "b")))) & (Bool (Set (Set (Var "a")) ($#k24_binop_2 :::"*"::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "k")) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ($#k24_binop_2 :::"*"::: ) (Set (Var "n")))) ")" ) "iff" (Bool (Set (Set "(" ($#k7_int_3 :::"multint"::: ) (Set (Var "n")) ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k24_binop_2 :::"*"::: ) (Set (Var "b")) ")" ) ($#k21_binop_2 :::"-"::: ) (Set "(" (Set (Var "k")) ($#k24_binop_2 :::"*"::: ) (Set (Var "n")) ")" ))) ")" )))) ; theorem :: INT_3:9 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Set (Var "n"))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set "(" ($#k8_int_3 :::"compint"::: ) (Set (Var "n")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Set "(" ($#k8_int_3 :::"compint"::: ) (Set (Var "n")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set "(" ($#k8_int_3 :::"compint"::: ) (Set (Var "n")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k21_binop_2 :::"-"::: ) (Set (Var "a")))) ")" & "(" (Bool (Bool (Set (Set "(" ($#k8_int_3 :::"compint"::: ) (Set (Var "n")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k21_binop_2 :::"-"::: ) (Set (Var "a"))))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" ))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"INT.Ring"::: "n" -> ($#l6_algstr_0 :::"doubleLoopStr"::: ) equals :: INT_3:def 12 (Set ($#g6_algstr_0 :::"doubleLoopStr"::: ) "(#" (Set "(" ($#k7_card_1 :::"Segm"::: ) "n" ")" ) "," (Set "(" ($#k3_gr_cy_1 :::"addint"::: ) "n" ")" ) "," (Set "(" ($#k7_int_3 :::"multint"::: ) "n" ")" ) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Num 1) "," (Set "(" ($#k7_card_1 :::"Segm"::: ) "n" ")" ) ")" ")" ) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k7_card_1 :::"Segm"::: ) "n" ")" ) ")" ")" ) "#)" ); end; :: deftheorem defines :::"INT.Ring"::: INT_3:def 12 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k9_int_3 :::"INT.Ring"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#g6_algstr_0 :::"doubleLoopStr"::: ) "(#" (Set "(" ($#k7_card_1 :::"Segm"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k3_gr_cy_1 :::"addint"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k7_int_3 :::"multint"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Num 1) "," (Set "(" ($#k7_card_1 :::"Segm"::: ) (Set (Var "n")) ")" ) ")" ")" ) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k7_card_1 :::"Segm"::: ) (Set (Var "n")) ")" ) ")" ")" ) "#)" ))); registrationlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::); cluster (Set ($#k9_int_3 :::"INT.Ring"::: ) "n") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v36_algstr_0 :::"strict"::: ) ; end; theorem :: INT_3:10 (Bool "(" (Bool (Set ($#k9_int_3 :::"INT.Ring"::: ) (Num 1)) "is" ($#v6_struct_0 :::"degenerated"::: ) ) & (Bool (Set ($#k9_int_3 :::"INT.Ring"::: ) (Num 1)) "is" ($#l6_algstr_0 :::"Ring":::)) & (Bool (Set ($#k9_int_3 :::"INT.Ring"::: ) (Num 1)) "is" ($#v33_algstr_0 :::"almost_left_invertible"::: ) ) & (Bool (Set ($#k9_int_3 :::"INT.Ring"::: ) (Num 1)) "is" ($#v1_group_1 :::"unital"::: ) ) & (Bool (Set ($#k9_int_3 :::"INT.Ring"::: ) (Num 1)) "is" ($#v5_vectsp_1 :::"distributive"::: ) ) & (Bool (Set ($#k9_int_3 :::"INT.Ring"::: ) (Num 1)) "is" ($#v5_group_1 :::"commutative"::: ) ) ")" ) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_struct_0 :::"degenerated"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v36_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; theorem :: INT_3:11 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k9_int_3 :::"INT.Ring"::: ) (Set (Var "n"))) "is" ($#v6_struct_0 :::"degenerated"::: ) )) & (Bool (Set ($#k9_int_3 :::"INT.Ring"::: ) (Set (Var "n"))) "is" ($#v5_group_1 :::"commutative"::: ) ($#l6_algstr_0 :::"Ring":::)) ")" )) ; theorem :: INT_3:12 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool "(" (Bool (Set ($#k9_int_3 :::"INT.Ring"::: ) (Set (Var "p"))) "is" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ) "iff" (Bool (Set (Var "p")) "is" ($#m1_hidden :::"Prime":::)) ")" )) ; registration cluster bbbadV7_ORDINAL1() ($#v1_int_2 :::"prime"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "p" be ($#m1_hidden :::"Prime":::); cluster (Set ($#k9_int_3 :::"INT.Ring"::: ) "p") -> ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ; end; theorem :: INT_3:13 (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set ($#k1_int_3 :::"INT.Ring"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ; theorem :: INT_3:14 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set "(" ($#k9_int_3 :::"INT.Ring"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; begin registration cluster (Set ($#k1_int_3 :::"INT.Ring"::: ) ) -> ($#v8_struct_0 :::"infinite"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"infinite"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v36_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end;