:: GROUPP_1 semantic presentation begin theorem :: GROUPP_1:1 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "(" "for" (Set (Var "r")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "p")) ($#k1_newton :::"|^"::: ) (Set (Var "r")))) ")" )) "holds" (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "s")) "is" ($#v1_int_2 :::"prime"::: ) ) & (Bool (Set (Var "s")) ($#r1_int_1 :::"divides"::: ) (Set (Var "n"))) & (Bool (Set (Var "s")) ($#r1_hidden :::"<>"::: ) (Set (Var "p"))) ")" )))) ; theorem :: GROUPP_1:2 (Bool "for" (Set (Var "p")) "being" ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_int_1 :::"divides"::: ) (Set (Set (Var "p")) ($#k1_newton :::"|^"::: ) (Set (Var "m"))))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_newton :::"|^"::: ) (Set (Var "r")))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) ")" )))) ; theorem :: GROUPP_1:3 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) ($#k5_group_1 :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G"))))))) ; theorem :: GROUPP_1:4 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" ) ($#k5_group_1 :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G"))))))) ; theorem :: GROUPP_1:5 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k6_group_1 :::"ord"::: ) (Set "(" (Set (Var "a")) ($#k2_group_1 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_group_1 :::"ord"::: ) (Set (Var "a")))))) ; theorem :: GROUPP_1:6 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k6_group_1 :::"ord"::: ) (Set "(" (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_group_1 :::"ord"::: ) (Set (Var "a")))))) ; theorem :: GROUPP_1:7 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N")) "is" ($#v1_group_3 :::"normal"::: ) ) & (Bool (Set (Var "b")) ($#r1_struct_0 :::"in"::: ) (Set (Var "N")))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_struct_0 :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k5_group_1 :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "n")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "g")))) ")" )))))) ; theorem :: GROUPP_1:8 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "G")) ($#k5_group_6 :::"./."::: ) (Set (Var "N")) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "N"))))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "S")) ($#k5_group_1 :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "n")) ")" ) ($#k13_group_2 :::"*"::: ) (Set (Var "N"))))))))) ; theorem :: GROUPP_1:9 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "a")) ($#k13_group_2 :::"*"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k13_group_2 :::"*"::: ) (Set (Var "H"))))) "holds" (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "h")))) & (Bool (Set (Var "h")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H"))) ")" ))))) ; theorem :: GROUPP_1:10 (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N")) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set ($#k10_group_5 :::"center"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "G")) ($#k5_group_6 :::"./."::: ) (Set (Var "N"))) "is" ($#v1_gr_cy_1 :::"cyclic"::: ) )) "holds" (Bool (Set (Var "G")) "is" ($#v5_group_1 :::"commutative"::: ) ))) ; theorem :: GROUPP_1:11 (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N")) ($#r1_hidden :::"="::: ) (Set ($#k10_group_5 :::"center"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "G")) ($#k5_group_6 :::"./."::: ) (Set (Var "N"))) "is" ($#v1_gr_cy_1 :::"cyclic"::: ) )) "holds" (Bool (Set (Var "G")) "is" ($#v5_group_1 :::"commutative"::: ) ))) ; theorem :: GROUPP_1:12 (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k7_group_1 :::"card"::: ) (Set (Var "H"))) ($#r1_hidden :::"<>"::: ) (Set ($#k7_group_1 :::"card"::: ) (Set (Var "G"))))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool "not" (Set (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H"))))))) ; definitionlet "p" be ($#m1_hidden :::"Nat":::); let "G" be ($#l3_algstr_0 :::"Group":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); attr "a" is "p" :::"-power"::: means :: GROUPP_1:def 1 (Bool "ex" (Set (Var "r")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set ($#k6_group_1 :::"ord"::: ) "a") ($#r1_hidden :::"="::: ) (Set "p" ($#k1_newton :::"|^"::: ) (Set (Var "r"))))); end; :: deftheorem defines :::"-power"::: GROUPP_1:def 1 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "a")) "is" (Set (Var "p")) ($#v1_groupp_1 :::"-power"::: ) ) "iff" (Bool "ex" (Set (Var "r")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set ($#k6_group_1 :::"ord"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_newton :::"|^"::: ) (Set (Var "r"))))) ")" )))); theorem :: GROUPP_1:13 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "G"))) "is" (Set (Var "m")) ($#v1_groupp_1 :::"-power"::: ) ))) ; registrationlet "G" be ($#l3_algstr_0 :::"Group":::); let "m" be ($#m1_hidden :::"Nat":::); cluster "m" ($#v1_groupp_1 :::"-power"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G"); end; registrationlet "p" be ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::); let "G" be ($#l3_algstr_0 :::"Group":::); let "a" be (Set (Const "p")) ($#v1_groupp_1 :::"-power"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); cluster (Set "a" ($#k2_group_1 :::"""::: ) ) -> "p" ($#v1_groupp_1 :::"-power"::: ) ; end; theorem :: GROUPP_1:14 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "p")) "being" ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "a")) ($#k2_group_3 :::"|^"::: ) (Set (Var "b"))) "is" (Set (Var "p")) ($#v1_groupp_1 :::"-power"::: ) )) "holds" (Bool (Set (Var "a")) "is" (Set (Var "p")) ($#v1_groupp_1 :::"-power"::: ) )))) ; registrationlet "p" be ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::); let "G" be ($#l3_algstr_0 :::"Group":::); let "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); let "a" be (Set (Const "p")) ($#v1_groupp_1 :::"-power"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); cluster (Set "a" ($#k2_group_3 :::"|^"::: ) "b") -> "p" ($#v1_groupp_1 :::"-power"::: ) ; end; registrationlet "p" be ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::); let "G" be ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::); let "a", "b" be (Set (Const "p")) ($#v1_groupp_1 :::"-power"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); cluster (Set "a" ($#k6_algstr_0 :::"*"::: ) "b") -> "p" ($#v1_groupp_1 :::"-power"::: ) ; end; registrationlet "p" be ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::); let "G" be ($#v8_struct_0 :::"finite"::: ) (Set (Const "p")) ($#v2_group_10 :::"-group"::: ) ($#l3_algstr_0 :::"Group":::); cluster -> "p" ($#v1_groupp_1 :::"-power"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G"); end; theorem :: GROUPP_1:15 (Bool "for" (Set (Var "p")) "being" ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "H")) "is" (Set (Var "p")) ($#v2_group_10 :::"-group"::: ) ) & (Bool (Set (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H")))) "holds" (Bool (Set (Var "a")) "is" (Set (Var "p")) ($#v1_groupp_1 :::"-power"::: ) ))))) ; registrationlet "p" be ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::); let "G" be ($#v8_struct_0 :::"finite"::: ) (Set (Const "p")) ($#v2_group_10 :::"-group"::: ) ($#l3_algstr_0 :::"Group":::); cluster -> "p" ($#v2_group_10 :::"-group"::: ) for ($#m1_group_2 :::"Subgroup"::: ) "of" "G"; end; theorem :: GROUPP_1:16 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "p")) "being" ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G"))) "is" (Set (Var "p")) ($#v2_group_10 :::"-group"::: ) ))) ; registrationlet "p" be ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::); let "G" be ($#l3_algstr_0 :::"Group":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) "p" ($#v2_group_10 :::"-group"::: ) for ($#m1_group_2 :::"Subgroup"::: ) "of" "G"; end; registrationlet "p" be ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::); let "G" be ($#v8_struct_0 :::"finite"::: ) ($#l3_algstr_0 :::"Group":::); let "G1" be (Set (Const "p")) ($#v2_group_10 :::"-group"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); let "G2" be ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); cluster (Set "G1" ($#k9_group_2 :::"/\"::: ) "G2") -> "p" ($#v2_group_10 :::"-group"::: ) ; cluster (Set "G2" ($#k9_group_2 :::"/\"::: ) "G1") -> "p" ($#v2_group_10 :::"-group"::: ) ; end; theorem :: GROUPP_1:17 (Bool "for" (Set (Var "p")) "being" ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l3_algstr_0 :::"Group":::) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Var "a")) "is" (Set (Var "p")) ($#v1_groupp_1 :::"-power"::: ) ) ")" )) "holds" (Bool (Set (Var "G")) "is" (Set (Var "p")) ($#v2_group_10 :::"-group"::: ) ))) ; registrationlet "p" be ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::); let "G" be ($#v8_struct_0 :::"finite"::: ) (Set (Const "p")) ($#v2_group_10 :::"-group"::: ) ($#l3_algstr_0 :::"Group":::); let "N" be ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); cluster (Set "G" ($#k5_group_6 :::"./."::: ) "N") -> "p" ($#v2_group_10 :::"-group"::: ) ; end; theorem :: GROUPP_1:18 (Bool "for" (Set (Var "p")) "being" ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N")) "is" (Set (Var "p")) ($#v2_group_10 :::"-group"::: ) ) & (Bool (Set (Set (Var "G")) ($#k5_group_6 :::"./."::: ) (Set (Var "N"))) "is" (Set (Var "p")) ($#v2_group_10 :::"-group"::: ) )) "holds" (Bool (Set (Var "G")) "is" (Set (Var "p")) ($#v2_group_10 :::"-group"::: ) )))) ; theorem :: GROUPP_1:19 (Bool "for" (Set (Var "p")) "being" ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "," (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "H1")) "is" (Set (Var "p")) ($#v2_group_10 :::"-group"::: ) ) & (Bool (Set (Var "H2")) "is" (Set (Var "p")) ($#v2_group_10 :::"-group"::: ) ) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k7_group_4 :::"*"::: ) (Set (Var "H2"))))) "holds" (Bool (Set (Var "H")) "is" (Set (Var "p")) ($#v2_group_10 :::"-group"::: ) )))) ; theorem :: GROUPP_1:20 (Bool "for" (Set (Var "p")) "being" ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "," (Set (Var "N")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N")) "is" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G"))) & (Bool (Set (Var "H")) "is" (Set (Var "p")) ($#v2_group_10 :::"-group"::: ) ) & (Bool (Set (Var "N")) "is" (Set (Var "p")) ($#v2_group_10 :::"-group"::: ) )) "holds" (Bool "ex" (Set (Var "P")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k7_group_4 :::"*"::: ) (Set (Var "N")))) & (Bool (Set (Var "P")) "is" (Set (Var "p")) ($#v2_group_10 :::"-group"::: ) ) ")" ))))) ; theorem :: GROUPP_1:21 (Bool "for" (Set (Var "p")) "being" ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N1")) "is" (Set (Var "p")) ($#v2_group_10 :::"-group"::: ) ) & (Bool (Set (Var "N2")) "is" (Set (Var "p")) ($#v2_group_10 :::"-group"::: ) )) "holds" (Bool "ex" (Set (Var "N")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k7_group_4 :::"*"::: ) (Set (Var "N2")))) & (Bool (Set (Var "N")) "is" (Set (Var "p")) ($#v2_group_10 :::"-group"::: ) ) ")" ))))) ; registrationlet "p" be ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::); let "G" be ($#v8_struct_0 :::"finite"::: ) (Set (Const "p")) ($#v2_group_10 :::"-group"::: ) ($#l3_algstr_0 :::"Group":::); let "H" be ($#v8_struct_0 :::"finite"::: ) ($#l3_algstr_0 :::"Group":::); let "g" be ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Const "G")) "," (Set (Const "H")); cluster (Set ($#k10_group_6 :::"Image"::: ) "g") -> "p" ($#v2_group_10 :::"-group"::: ) ; end; theorem :: GROUPP_1:22 (Bool "for" (Set (Var "p")) "being" ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) "st" (Bool (Bool (Set (Var "G")) "," (Set (Var "H")) ($#r2_group_6 :::"are_isomorphic"::: ) ) & (Bool (Set (Var "G")) "is" (Set (Var "p")) ($#v2_group_10 :::"-group"::: ) )) "holds" (Bool (Set (Var "H")) "is" (Set (Var "p")) ($#v2_group_10 :::"-group"::: ) ))) ; definitionlet "p" be ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::); let "G" be ($#l3_algstr_0 :::"Group":::); assume (Bool (Set (Const "G")) "is" (Set (Const "p")) ($#v2_group_10 :::"-group"::: ) ) ; func :::"expon"::: "(" "G" "," "p" ")" -> ($#m1_hidden :::"Nat":::) means :: GROUPP_1:def 2 (Bool (Set ($#k7_struct_0 :::"card"::: ) "G") ($#r1_hidden :::"="::: ) (Set "p" ($#k1_newton :::"|^"::: ) it)); end; :: deftheorem defines :::"expon"::: GROUPP_1:def 2 : (Bool "for" (Set (Var "p")) "being" ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "st" (Bool (Bool (Set (Var "G")) "is" (Set (Var "p")) ($#v2_group_10 :::"-group"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_groupp_1 :::"expon"::: ) "(" (Set (Var "G")) "," (Set (Var "p")) ")" )) "iff" (Bool (Set ($#k7_struct_0 :::"card"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_newton :::"|^"::: ) (Set (Var "b3")))) ")" )))); definitionlet "p" be ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::); let "G" be ($#l3_algstr_0 :::"Group":::); :: original: :::"expon"::: redefine func :::"expon"::: "(" "G" "," "p" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; theorem :: GROUPP_1:23 (Bool "for" (Set (Var "p")) "being" ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G")) "is" (Set (Var "p")) ($#v2_group_10 :::"-group"::: ) )) "holds" (Bool (Set ($#k2_groupp_1 :::"expon"::: ) "(" (Set (Var "H")) "," (Set (Var "p")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_groupp_1 :::"expon"::: ) "(" (Set (Var "G")) "," (Set (Var "p")) ")" ))))) ; theorem :: GROUPP_1:24 (Bool "for" (Set (Var "p")) "being" ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) "st" (Bool (Bool (Set (Var "G")) "is" (Set (Var "p")) ($#v2_group_10 :::"-group"::: ) ) & (Bool (Set ($#k2_groupp_1 :::"expon"::: ) "(" (Set (Var "G")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")))))) ; theorem :: GROUPP_1:25 (Bool "for" (Set (Var "p")) "being" ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) "st" (Bool (Bool (Set (Var "G")) "is" (Set (Var "p")) ($#v2_group_10 :::"-group"::: ) ) & (Bool (Set ($#k2_groupp_1 :::"expon"::: ) "(" (Set (Var "G")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set (Var "G")) "is" ($#v1_gr_cy_1 :::"cyclic"::: ) ))) ; theorem :: GROUPP_1:26 (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "p")) "being" ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G")) "is" (Set (Var "p")) ($#v2_group_10 :::"-group"::: ) ) & (Bool (Set ($#k2_groupp_1 :::"expon"::: ) "(" (Set (Var "G")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Num 2)) & (Bool (Set ($#k6_group_1 :::"ord"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_newton :::"|^"::: ) (Num 2)))) "holds" (Bool (Set (Var "G")) "is" ($#v5_group_1 :::"commutative"::: ) )))) ; begin definitionlet "p" be ($#m1_hidden :::"Nat":::); let "G" be ($#l3_algstr_0 :::"Group":::); attr "G" is "p" :::"-commutative-group-like"::: means :: GROUPP_1:def 3 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "G" "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k5_group_1 :::"|^"::: ) "p") ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) "p" ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k5_group_1 :::"|^"::: ) "p" ")" )))); end; :: deftheorem defines :::"-commutative-group-like"::: GROUPP_1:def 3 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" (Set (Var "p")) ($#v2_groupp_1 :::"-commutative-group-like"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k5_group_1 :::"|^"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "p")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k5_group_1 :::"|^"::: ) (Set (Var "p")) ")" )))) ")" ))); definitionlet "p" be ($#m1_hidden :::"Nat":::); let "G" be ($#l3_algstr_0 :::"Group":::); attr "G" is "p" :::"-commutative-group"::: means :: GROUPP_1:def 4 (Bool "(" (Bool "G" "is" "p" ($#v2_group_10 :::"-group"::: ) ) & (Bool "G" "is" "p" ($#v2_groupp_1 :::"-commutative-group-like"::: ) ) ")" ); end; :: deftheorem defines :::"-commutative-group"::: GROUPP_1:def 4 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" (Set (Var "p")) ($#v3_groupp_1 :::"-commutative-group"::: ) ) "iff" (Bool "(" (Bool (Set (Var "G")) "is" (Set (Var "p")) ($#v2_group_10 :::"-group"::: ) ) & (Bool (Set (Var "G")) "is" (Set (Var "p")) ($#v2_groupp_1 :::"-commutative-group-like"::: ) ) ")" ) ")" ))); registrationlet "p" be ($#m1_hidden :::"Nat":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) "p" ($#v3_groupp_1 :::"-commutative-group"::: ) -> "p" ($#v2_group_10 :::"-group"::: ) "p" ($#v2_groupp_1 :::"-commutative-group-like"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) "p" ($#v2_group_10 :::"-group"::: ) "p" ($#v2_groupp_1 :::"-commutative-group-like"::: ) -> "p" ($#v3_groupp_1 :::"-commutative-group"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; end; theorem :: GROUPP_1:27 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "p")) "being" ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G"))) "is" (Set (Var "p")) ($#v2_groupp_1 :::"-commutative-group-like"::: ) ))) ; registrationlet "p" be ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v1_group_1 :::"unital"::: ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v1_gr_cy_1 :::"cyclic"::: ) "p" ($#v3_groupp_1 :::"-commutative-group"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; end; registrationlet "p" be ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::); let "G" be ($#v8_struct_0 :::"finite"::: ) (Set (Const "p")) ($#v2_groupp_1 :::"-commutative-group-like"::: ) ($#l3_algstr_0 :::"Group":::); cluster -> "p" ($#v2_groupp_1 :::"-commutative-group-like"::: ) for ($#m1_group_2 :::"Subgroup"::: ) "of" "G"; end; registrationlet "p" be ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) "p" ($#v2_group_10 :::"-group"::: ) -> "p" ($#v3_groupp_1 :::"-commutative-group"::: ) for ($#l3_algstr_0 :::"multMagma"::: ) ; end; theorem :: GROUPP_1:28 (Bool "for" (Set (Var "p")) "being" ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) "st" (Bool (Bool (Set ($#k7_group_1 :::"card"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Var "p")))) "holds" (Bool (Set (Var "G")) "is" (Set (Var "p")) ($#v3_groupp_1 :::"-commutative-group"::: ) ))) ; registrationlet "p" be ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::); let "G" be ($#l3_algstr_0 :::"Group":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_struct_0 :::"finite"::: ) ($#v1_group_1 :::"unital"::: ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) "p" ($#v3_groupp_1 :::"-commutative-group"::: ) for ($#m1_group_2 :::"Subgroup"::: ) "of" "G"; end; registrationlet "p" be ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::); let "G" be ($#v8_struct_0 :::"finite"::: ) ($#l3_algstr_0 :::"Group":::); let "H1" be (Set (Const "p")) ($#v2_groupp_1 :::"-commutative-group-like"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); let "H2" be ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); cluster (Set "H1" ($#k9_group_2 :::"/\"::: ) "H2") -> "p" ($#v2_groupp_1 :::"-commutative-group-like"::: ) ; cluster (Set "H2" ($#k9_group_2 :::"/\"::: ) "H1") -> "p" ($#v2_groupp_1 :::"-commutative-group-like"::: ) ; end; registrationlet "p" be ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::); let "G" be ($#v8_struct_0 :::"finite"::: ) (Set (Const "p")) ($#v2_groupp_1 :::"-commutative-group-like"::: ) ($#l3_algstr_0 :::"Group":::); let "N" be ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Const "G")); cluster (Set "G" ($#k5_group_6 :::"./."::: ) "N") -> "p" ($#v2_groupp_1 :::"-commutative-group-like"::: ) ; end; theorem :: GROUPP_1:29 (Bool "for" (Set (Var "p")) "being" ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G")) "is" (Set (Var "p")) ($#v2_groupp_1 :::"-commutative-group-like"::: ) )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k5_group_1 :::"|^"::: ) (Set "(" (Set (Var "p")) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set "(" (Set (Var "p")) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k5_group_1 :::"|^"::: ) (Set "(" (Set (Var "p")) ($#k1_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ))))))) ; theorem :: GROUPP_1:30 (Bool "for" (Set (Var "p")) "being" ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "," (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "H1")) "is" (Set (Var "p")) ($#v3_groupp_1 :::"-commutative-group"::: ) ) & (Bool (Set (Var "H2")) "is" (Set (Var "p")) ($#v3_groupp_1 :::"-commutative-group"::: ) ) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H1")) ($#k7_group_4 :::"*"::: ) (Set (Var "H2"))))) "holds" (Bool (Set (Var "H")) "is" (Set (Var "p")) ($#v3_groupp_1 :::"-commutative-group"::: ) )))) ; theorem :: GROUPP_1:31 (Bool "for" (Set (Var "p")) "being" ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "N")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N")) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set ($#k10_group_5 :::"center"::: ) (Set (Var "G")))) & (Bool (Set (Var "H")) "is" (Set (Var "p")) ($#v3_groupp_1 :::"-commutative-group"::: ) ) & (Bool (Set (Var "N")) "is" (Set (Var "p")) ($#v3_groupp_1 :::"-commutative-group"::: ) )) "holds" (Bool "ex" (Set (Var "P")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k7_group_4 :::"*"::: ) (Set (Var "N")))) & (Bool (Set (Var "P")) "is" (Set (Var "p")) ($#v3_groupp_1 :::"-commutative-group"::: ) ) ")" )))))) ; theorem :: GROUPP_1:32 (Bool "for" (Set (Var "p")) "being" ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "N1")) "," (Set (Var "N2")) "being" ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "N2")) "is" ($#m1_group_6 :::"Subgroup"::: ) "of" (Set ($#k10_group_5 :::"center"::: ) (Set (Var "G")))) & (Bool (Set (Var "N1")) "is" (Set (Var "p")) ($#v3_groupp_1 :::"-commutative-group"::: ) ) & (Bool (Set (Var "N2")) "is" (Set (Var "p")) ($#v3_groupp_1 :::"-commutative-group"::: ) )) "holds" (Bool "ex" (Set (Var "N")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_group_3 :::"normal"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N1")) ($#k7_group_4 :::"*"::: ) (Set (Var "N2")))) & (Bool (Set (Var "N")) "is" (Set (Var "p")) ($#v3_groupp_1 :::"-commutative-group"::: ) ) ")" ))))) ; theorem :: GROUPP_1:33 (Bool "for" (Set (Var "p")) "being" ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#l3_algstr_0 :::"Group":::) "st" (Bool (Bool (Set (Var "G")) "," (Set (Var "H")) ($#r1_group_6 :::"are_isomorphic"::: ) ) & (Bool (Set (Var "G")) "is" (Set (Var "p")) ($#v2_groupp_1 :::"-commutative-group-like"::: ) )) "holds" (Bool (Set (Var "H")) "is" (Set (Var "p")) ($#v2_groupp_1 :::"-commutative-group-like"::: ) ))) ; theorem :: GROUPP_1:34 (Bool "for" (Set (Var "p")) "being" ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) "st" (Bool (Bool (Set (Var "G")) "," (Set (Var "H")) ($#r2_group_6 :::"are_isomorphic"::: ) ) & (Bool (Set (Var "G")) "is" (Set (Var "p")) ($#v3_groupp_1 :::"-commutative-group"::: ) )) "holds" (Bool (Set (Var "H")) "is" (Set (Var "p")) ($#v3_groupp_1 :::"-commutative-group"::: ) ))) ; registrationlet "p" be ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::); let "G" be ($#v8_struct_0 :::"finite"::: ) (Set (Const "p")) ($#v2_groupp_1 :::"-commutative-group-like"::: ) ($#l3_algstr_0 :::"Group":::); let "H" be ($#v8_struct_0 :::"finite"::: ) ($#l3_algstr_0 :::"Group":::); let "g" be ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Const "G")) "," (Set (Const "H")); cluster (Set ($#k10_group_6 :::"Image"::: ) "g") -> "p" ($#v2_groupp_1 :::"-commutative-group-like"::: ) ; end; theorem :: GROUPP_1:35 (Bool "for" (Set (Var "p")) "being" ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) "st" (Bool (Bool (Set (Var "G")) "is" (Set (Var "p")) ($#v2_group_10 :::"-group"::: ) ) & (Bool (Set ($#k2_groupp_1 :::"expon"::: ) "(" (Set (Var "G")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "G")) "is" (Set (Var "p")) ($#v3_groupp_1 :::"-commutative-group"::: ) ))) ; theorem :: GROUPP_1:36 (Bool "for" (Set (Var "p")) "being" ($#v1_int_2 :::"prime"::: ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) "st" (Bool (Bool (Set (Var "G")) "is" (Set (Var "p")) ($#v2_group_10 :::"-group"::: ) ) & (Bool (Set ($#k2_groupp_1 :::"expon"::: ) "(" (Set (Var "G")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set (Var "G")) "is" (Set (Var "p")) ($#v3_groupp_1 :::"-commutative-group"::: ) ))) ;