:: GR_CY_2 semantic presentation begin theorem :: GR_CY_2:1 (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 "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k6_group_1 :::"ord"::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Num 1)) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k5_group_1 :::"|^"::: ) (Set (Var "k"))))) "holds" (Bool (Set (Var "k")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))))) ; theorem :: GR_CY_2:2 (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 (Var "a")) ($#r1_struct_0 :::"in"::: ) (Set ($#k5_group_4 :::"gr"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ))))) ; theorem :: GR_CY_2:3 (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "G1")) "being" ($#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 "a1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G1")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "a1")))) "holds" (Bool (Set ($#k5_group_4 :::"gr"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_group_4 :::"gr"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a1")) ($#k6_domain_1 :::"}"::: ) ))))))) ; theorem :: GR_CY_2: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")) "holds" (Bool (Set ($#k5_group_4 :::"gr"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) )) "is" ($#v1_gr_cy_1 :::"cyclic"::: ) ($#l3_algstr_0 :::"Group":::)))) ; theorem :: GR_CY_2:5 (Bool "for" (Set (Var "G")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i"))))) ")" ) "iff" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k5_group_4 :::"gr"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "b")) ($#k6_domain_1 :::"}"::: ) ))) ")" ))) ; theorem :: GR_CY_2:6 (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k5_group_1 :::"|^"::: ) (Set (Var "p"))))) ")" ) "iff" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k5_group_4 :::"gr"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "b")) ($#k6_domain_1 :::"}"::: ) ))) ")" ))) ; theorem :: GR_CY_2:7 (Bool "for" (Set (Var "G")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v8_struct_0 :::"finite"::: ) ) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k5_group_4 :::"gr"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) )))) "holds" (Bool "for" (Set (Var "G1")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "G1")) ($#r1_group_2 :::"="::: ) (Set ($#k5_group_4 :::"gr"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "p")) ")" ) ($#k6_domain_1 :::"}"::: ) ))))))) ; theorem :: GR_CY_2:8 (Bool "for" (Set (Var "n")) "," (Set (Var "p")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k5_group_4 :::"gr"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ))) & (Bool (Set ($#k7_group_1 :::"card"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "s"))))) "holds" (Bool (Set ($#k6_group_1 :::"ord"::: ) (Set "(" (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "s")))))) ; theorem :: GR_CY_2:9 (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 "s")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "s")) ($#r1_nat_d :::"divides"::: ) (Set (Var "k")))) "holds" (Bool (Set (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "k"))) ($#r1_struct_0 :::"in"::: ) (Set ($#k5_group_4 :::"gr"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "s")) ")" ) ($#k6_domain_1 :::"}"::: ) )))))) ; theorem :: GR_CY_2:10 (Bool "for" (Set (Var "s")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k7_group_1 :::"card"::: ) (Set "(" ($#k5_group_4 :::"gr"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "s")) ")" ) ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_group_1 :::"card"::: ) (Set "(" ($#k5_group_4 :::"gr"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "k")) ")" ) ($#k6_domain_1 :::"}"::: ) ) ")" ))) & (Bool (Set (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "k"))) ($#r1_struct_0 :::"in"::: ) (Set ($#k5_group_4 :::"gr"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "s")) ")" ) ($#k6_domain_1 :::"}"::: ) )))) "holds" (Bool (Set ($#k5_group_4 :::"gr"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "s")) ")" ) ($#k6_domain_1 :::"}"::: ) )) ($#r1_group_2 :::"="::: ) (Set ($#k5_group_4 :::"gr"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "k")) ")" ) ($#k6_domain_1 :::"}"::: ) )))))) ; theorem :: GR_CY_2:11 (Bool "for" (Set (Var "n")) "," (Set (Var "p")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "G1")) "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 ($#k7_group_1 :::"card"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k5_group_4 :::"gr"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ))) & (Bool (Set ($#k7_group_1 :::"card"::: ) (Set (Var "G1"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Var "G1")) ($#r1_hidden :::"="::: ) (Set ($#k5_group_4 :::"gr"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "k")) ")" ) ($#k6_domain_1 :::"}"::: ) )))) "holds" (Bool (Set (Var "n")) ($#r1_nat_d :::"divides"::: ) (Set (Set (Var "k")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "p")))))))) ; theorem :: GR_CY_2:12 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#v8_struct_0 :::"finite"::: ) ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k5_group_4 :::"gr"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) ))) & (Bool (Set ($#k7_group_1 :::"card"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Var "n")))) "holds" (Bool "(" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set ($#k5_group_4 :::"gr"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "a")) ($#k5_group_1 :::"|^"::: ) (Set (Var "k")) ")" ) ($#k6_domain_1 :::"}"::: ) ))) "iff" (Bool (Set (Set (Var "k")) ($#k6_nat_d :::"gcd"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" )))) ; theorem :: GR_CY_2:13 (Bool "for" (Set (Var "Gc")) "being" ($#v1_gr_cy_1 :::"cyclic"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "Gc")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Gc")) "st" (Bool (Bool (Set (Var "Gc")) ($#r1_hidden :::"="::: ) (Set ($#k5_group_4 :::"gr"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "g")) ($#k6_domain_1 :::"}"::: ) ))) & (Bool (Set (Var "g")) ($#r1_struct_0 :::"in"::: ) (Set (Var "H")))) "holds" (Bool (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Gc"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "Gc"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g3_algstr_0 :::"multMagma"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H"))) "," (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "H"))) "#)" ))))) ; theorem :: GR_CY_2:14 (Bool "for" (Set (Var "Gc")) "being" ($#v1_gr_cy_1 :::"cyclic"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Gc")) "st" (Bool (Bool (Set (Var "Gc")) ($#r1_hidden :::"="::: ) (Set ($#k5_group_4 :::"gr"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "g")) ($#k6_domain_1 :::"}"::: ) )))) "holds" (Bool "(" (Bool (Set (Var "Gc")) "is" ($#v8_struct_0 :::"finite"::: ) ) "iff" (Bool "ex" (Set (Var "i")) "," (Set (Var "i1")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool "(" (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "i1"))) & (Bool (Set (Set (Var "g")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_group_1 :::"|^"::: ) (Set (Var "i1")))) ")" )) ")" ))) ; registrationlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::); cluster -> ($#v7_ordinal1 :::"natural"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k4_gr_cy_1 :::"INT.Group"::: ) "n" ")" )); end; theorem :: GR_CY_2:15 (Bool "for" (Set (Var "Gc")) "being" ($#v8_struct_0 :::"finite"::: ) ($#v15_algstr_0 :::"strict"::: ) ($#v1_gr_cy_1 :::"cyclic"::: ) ($#l3_algstr_0 :::"Group":::) "holds" (Bool (Set ($#k4_gr_cy_1 :::"INT.Group"::: ) (Set "(" ($#k7_group_1 :::"card"::: ) (Set (Var "Gc")) ")" )) "," (Set (Var "Gc")) ($#r2_group_6 :::"are_isomorphic"::: ) )) ; theorem :: GR_CY_2:16 (Bool "for" (Set (Var "Gc")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#v1_gr_cy_1 :::"cyclic"::: ) ($#l3_algstr_0 :::"Group":::) "st" (Bool (Bool (Set (Var "Gc")) "is" ($#v8_struct_0 :::"infinite"::: ) )) "holds" (Bool (Set ($#k2_gr_cy_1 :::"INT.Group"::: ) ) "," (Set (Var "Gc")) ($#r2_group_6 :::"are_isomorphic"::: ) )) ; theorem :: GR_CY_2:17 (Bool "for" (Set (Var "Gc")) "," (Set (Var "Hc")) "being" ($#v8_struct_0 :::"finite"::: ) ($#v15_algstr_0 :::"strict"::: ) ($#v1_gr_cy_1 :::"cyclic"::: ) ($#l3_algstr_0 :::"Group":::) "st" (Bool (Bool (Set ($#k7_group_1 :::"card"::: ) (Set (Var "Hc"))) ($#r1_hidden :::"="::: ) (Set ($#k7_group_1 :::"card"::: ) (Set (Var "Gc"))))) "holds" (Bool (Set (Var "Hc")) "," (Set (Var "Gc")) ($#r2_group_6 :::"are_isomorphic"::: ) )) ; theorem :: GR_CY_2:18 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "F")) "," (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 "F"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set ($#k7_group_1 :::"card"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Var "p")) "is" ($#v1_int_2 :::"prime"::: ) )) "holds" (Bool (Set (Var "F")) "," (Set (Var "G")) ($#r2_group_6 :::"are_isomorphic"::: ) ))) ; theorem :: GR_CY_2:19 (Bool "for" (Set (Var "F")) "," (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 "F"))) ($#r1_hidden :::"="::: ) (Num 2)) & (Bool (Set ($#k7_group_1 :::"card"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Num 2))) "holds" (Bool (Set (Var "F")) "," (Set (Var "G")) ($#r2_group_6 :::"are_isomorphic"::: ) )) ; theorem :: GR_CY_2:20 (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 :::"="::: ) (Num 2))) "holds" (Bool "for" (Set (Var "H")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r1_group_2 :::"="::: ) (Set ($#k6_group_2 :::"(1)."::: ) (Set (Var "G")))) "or" (Bool (Set (Var "H")) ($#r1_hidden :::"="::: ) (Set (Var "G"))) ")" ))) ; theorem :: GR_CY_2:21 (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 :::"="::: ) (Num 2))) "holds" (Bool (Set (Var "G")) "is" ($#v1_gr_cy_1 :::"cyclic"::: ) ($#l3_algstr_0 :::"Group":::))) ; theorem :: GR_CY_2:22 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"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" ($#v1_gr_cy_1 :::"cyclic"::: ) ) & (Bool (Set ($#k7_group_1 :::"card"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Var "n")))) "holds" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r1_nat_d :::"divides"::: ) (Set (Var "n")))) "holds" (Bool "ex" (Set (Var "G1")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set ($#k7_group_1 :::"card"::: ) (Set (Var "G1"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool "(" "for" (Set (Var "G2")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k7_group_1 :::"card"::: ) (Set (Var "G2"))) ($#r1_hidden :::"="::: ) (Set (Var "p")))) "holds" (Bool (Set (Var "G2")) ($#r1_group_2 :::"="::: ) (Set (Var "G1"))) ")" ) ")" ))))) ; theorem :: GR_CY_2:23 (Bool "for" (Set (Var "Gc")) "being" ($#v1_gr_cy_1 :::"cyclic"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Gc")) "st" (Bool (Bool (Set (Var "Gc")) ($#r1_hidden :::"="::: ) (Set ($#k5_group_4 :::"gr"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "g")) ($#k6_domain_1 :::"}"::: ) )))) "holds" (Bool "for" (Set (Var "G")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "Gc")) "st" (Bool (Bool (Set (Var "g")) ($#r1_struct_0 :::"in"::: ) (Set ($#k10_group_6 :::"Image"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "f")) "is" ($#v2_funct_2 :::"onto"::: ) ))))) ; theorem :: GR_CY_2:24 (Bool "for" (Set (Var "Gc")) "being" ($#v8_struct_0 :::"finite"::: ) ($#v15_algstr_0 :::"strict"::: ) ($#v1_gr_cy_1 :::"cyclic"::: ) ($#l3_algstr_0 :::"Group":::) "st" (Bool (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set ($#k7_group_1 :::"card"::: ) (Set (Var "Gc"))) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "k")))))) "holds" (Bool "ex" (Set (Var "g1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Gc")) "st" (Bool "(" (Bool (Set ($#k6_group_1 :::"ord"::: ) (Set (Var "g1"))) ($#r1_hidden :::"="::: ) (Num 2)) & (Bool "(" "for" (Set (Var "g2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "Gc")) "st" (Bool (Bool (Set ($#k6_group_1 :::"ord"::: ) (Set (Var "g2"))) ($#r1_hidden :::"="::: ) (Num 2))) "holds" (Bool (Set (Var "g1")) ($#r1_hidden :::"="::: ) (Set (Var "g2"))) ")" ) ")" ))) ; registrationlet "G" be ($#l3_algstr_0 :::"Group":::); cluster (Set ($#k10_group_5 :::"center"::: ) "G") -> ($#v1_group_3 :::"normal"::: ) ; end; theorem :: GR_CY_2:25 (Bool "for" (Set (Var "Gc")) "being" ($#v8_struct_0 :::"finite"::: ) ($#v15_algstr_0 :::"strict"::: ) ($#v1_gr_cy_1 :::"cyclic"::: ) ($#l3_algstr_0 :::"Group":::) "st" (Bool (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set ($#k7_group_1 :::"card"::: ) (Set (Var "Gc"))) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "k")))))) "holds" (Bool "ex" (Set (Var "H")) "being" ($#m1_group_2 :::"Subgroup"::: ) "of" (Set (Var "Gc")) "st" (Bool "(" (Bool (Set ($#k7_group_1 :::"card"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Num 2)) & (Bool (Set (Var "H")) "is" ($#v1_gr_cy_1 :::"cyclic"::: ) ($#l3_algstr_0 :::"Group":::)) ")" ))) ; theorem :: GR_CY_2:26 (Bool "for" (Set (Var "F")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "G")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "F")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v1_gr_cy_1 :::"cyclic"::: ) )) "holds" (Bool (Set ($#k10_group_6 :::"Image"::: ) (Set (Var "g"))) "is" ($#v1_gr_cy_1 :::"cyclic"::: ) )))) ; theorem :: GR_CY_2:27 (Bool "for" (Set (Var "G")) "," (Set (Var "F")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"Group":::) "st" (Bool (Bool (Set (Var "G")) "," (Set (Var "F")) ($#r2_group_6 :::"are_isomorphic"::: ) ) & (Bool (Set (Var "G")) "is" ($#v1_gr_cy_1 :::"cyclic"::: ) )) "holds" (Bool (Set (Var "F")) "is" ($#v1_gr_cy_1 :::"cyclic"::: ) )) ;