:: GR_CY_3  semantic presentation begin  
theorem :: GR_CY_3:1 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"Prime":::)  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "k"))  ($#r1_nat_d :::"divides"::: )  (Set (Set (Var "p"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "q")))) "or" (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Num 1)) "or" (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set (Var "p"))) "or" (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set (Var "q"))) "or" (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "q"))))  ")" ))) ; 
 definitionlet "p" be   ($#m1_hidden :::"Nat":::); attr "p" is  :::"Safe":::  means :: GR_CY_3:def 1 (Bool  "ex" (Set (Var "sgp")) "being"   ($#m1_hidden :::"Prime":::) "st" (Bool (Set (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "sgp")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_hidden :::"="::: )  "p")); end; 




:: deftheorem    defines :::"Safe"::: GR_CY_3:def 1 :  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "p")) "is"   ($#v1_gr_cy_3 :::"Safe"::: )  ) "iff" (Bool  "ex" (Set (Var "sgp")) "being"   ($#m1_hidden :::"Prime":::) "st" (Bool (Set (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "sgp")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "p"))))  ")" )); 
 registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  bbbadV1_ORDINAL1() bbbadV2_ORDINAL1() bbbadV3_ORDINAL1() bbbadV7_ORDINAL1() bbbadV1_XCMPLX_0() bbbadV1_XREAL_0()   ($#v1_int_1 :::"integer"::: )     ($#v1_int_2 :::"prime"::: )     ($#v1_xxreal_0 :::"ext-real"::: )     ($#v2_xxreal_0 :::"positive"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_finset_1 :::"finite"::: )     ($#v1_card_1 :::"cardinal"::: )     ($#v1_gr_cy_3 :::"Safe"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: GR_CY_3:2 (Bool  "for" (Set (Var "p")) "being"   ($#v1_gr_cy_3 :::"Safe"::: )    ($#m1_hidden :::"Prime":::) "holds"  (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::">="::: )  (Num 5))) ; 
 
theorem :: GR_CY_3:3 (Bool  "for" (Set (Var "p")) "being"   ($#v1_gr_cy_3 :::"Safe"::: )    ($#m1_hidden :::"Prime":::) "holds"  (Bool (Set (Set (Var "p"))  ($#k4_nat_d :::"mod"::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: GR_CY_3:4 (Bool  "for" (Set (Var "p")) "being"   ($#v1_gr_cy_3 :::"Safe"::: )    ($#m1_hidden :::"Prime":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Num 7))) "holds"  (Bool (Set (Set (Var "p"))  ($#k4_nat_d :::"mod"::: )  (Num 3))  ($#r1_hidden :::"="::: )  (Num 2))) ; 
 
theorem :: GR_CY_3:5 (Bool  "for" (Set (Var "p")) "being"   ($#v1_gr_cy_3 :::"Safe"::: )    ($#m1_hidden :::"Prime":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Num 5))) "holds"  (Bool (Set (Set (Var "p"))  ($#k4_nat_d :::"mod"::: )  (Num 4))  ($#r1_hidden :::"="::: )  (Num 3))) ; 
 
theorem :: GR_CY_3:6 (Bool  "for" (Set (Var "p")) "being"   ($#v1_gr_cy_3 :::"Safe"::: )    ($#m1_hidden :::"Prime":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Num 7))) "holds"  (Bool (Set (Set (Var "p"))  ($#k4_nat_d :::"mod"::: )  (Num 6))  ($#r1_hidden :::"="::: )  (Num 5))) ; 
 
theorem :: GR_CY_3:7 (Bool  "for" (Set (Var "p")) "being"   ($#v1_gr_cy_3 :::"Safe"::: )    ($#m1_hidden :::"Prime":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::">"::: )  (Num 7))) "holds"  (Bool (Set (Set (Var "p"))  ($#k4_nat_d :::"mod"::: )  (Num 12))  ($#r1_hidden :::"="::: )  (Num 11))) ; 
 
theorem :: GR_CY_3:8 (Bool  "for" (Set (Var "p")) "being"   ($#v1_gr_cy_3 :::"Safe"::: )    ($#m1_hidden :::"Prime":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::">"::: )  (Num 5)) "or" (Bool (Set (Set (Var "p"))  ($#k4_nat_d :::"mod"::: )  (Num 8))  ($#r1_hidden :::"="::: )  (Num 3)) "or" (Bool (Set (Set (Var "p"))  ($#k4_nat_d :::"mod"::: )  (Num 8))  ($#r1_hidden :::"="::: )  (Num 7))  ")" )) ; 
 definitionlet "p" be   ($#m1_hidden :::"Nat":::); attr "p" is  :::"Sophie_Germain":::  means :: GR_CY_3:def 2 (Bool (Set (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  "p" ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1)) "is"   ($#m1_hidden :::"Prime":::)); end; 




:: deftheorem    defines :::"Sophie_Germain"::: GR_CY_3:def 2 :  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "p")) "is"   ($#v2_gr_cy_3 :::"Sophie_Germain"::: )  ) "iff" (Bool (Set (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "p")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1)) "is"   ($#m1_hidden :::"Prime":::))  ")" )); 
 registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  bbbadV1_ORDINAL1() bbbadV2_ORDINAL1() bbbadV3_ORDINAL1() bbbadV7_ORDINAL1() bbbadV1_XCMPLX_0() bbbadV1_XREAL_0()   ($#v1_int_1 :::"integer"::: )     ($#v1_int_2 :::"prime"::: )     ($#v1_xxreal_0 :::"ext-real"::: )     ($#v2_xxreal_0 :::"positive"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_finset_1 :::"finite"::: )     ($#v1_card_1 :::"cardinal"::: )     ($#v2_gr_cy_3 :::"Sophie_Germain"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: GR_CY_3:9 (Bool  "for" (Set (Var "p")) "being"   ($#v2_gr_cy_3 :::"Sophie_Germain"::: )    ($#m1_hidden :::"Prime":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::">"::: )  (Num 2)) "or" (Bool (Set (Set (Var "p"))  ($#k4_nat_d :::"mod"::: )  (Num 4))  ($#r1_hidden :::"="::: )  (Num 1)) "or" (Bool (Set (Set (Var "p"))  ($#k4_nat_d :::"mod"::: )  (Num 4))  ($#r1_hidden :::"="::: )  (Num 3))  ")" )) ; 
 
theorem :: GR_CY_3:10 (Bool  "for" (Set (Var "p")) "being"   ($#v1_gr_cy_3 :::"Safe"::: )    ($#m1_hidden :::"Prime":::) (Bool  "ex" (Set (Var "q")) "being"   ($#v2_gr_cy_3 :::"Sophie_Germain"::: )    ($#m1_hidden :::"Prime":::) "st" (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "q")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))))) ; 
 
theorem :: GR_CY_3:11 (Bool  "for" (Set (Var "p")) "being"   ($#v1_gr_cy_3 :::"Safe"::: )    ($#m1_hidden :::"Prime":::) (Bool  "ex" (Set (Var "q")) "being"   ($#v2_gr_cy_3 :::"Sophie_Germain"::: )    ($#m1_hidden :::"Prime":::) "st" (Bool (Set   ($#k1_euler_1 :::"Euler"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "q")))))) ; 
 
theorem :: GR_CY_3:12 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#v1_gr_cy_3 :::"Safe"::: )    ($#m1_hidden :::"Prime":::)  (Bool  "for" (Set (Var "N")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "p1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "p2"))) & (Bool (Set (Var "N"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p2"))))) "holds"  (Bool  "ex" (Set (Var "q1")) "," (Set (Var "q2")) "being"   ($#v2_gr_cy_3 :::"Sophie_Germain"::: )    ($#m1_hidden :::"Prime":::) "st" (Bool (Set   ($#k1_euler_1 :::"Euler"::: )  (Set (Var "N")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 4)  ($#k4_nat_1 :::"*"::: )  (Set (Var "q1")) ")" )  ($#k4_nat_1 :::"*"::: )  (Set (Var "q2"))))))) ; 
 
theorem :: GR_CY_3:13 (Bool  "for" (Set (Var "p")) "being"   ($#v1_gr_cy_3 :::"Safe"::: )    ($#m1_hidden :::"Prime":::) (Bool  "ex" (Set (Var "q")) "being"   ($#v2_gr_cy_3 :::"Sophie_Germain"::: )    ($#m1_hidden :::"Prime":::) "st" (Bool (Set   ($#k7_group_1 :::"card"::: )  (Set  "("  ($#k3_int_7 :::"Z/Z*"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "q")))))) ; 
 
theorem :: GR_CY_3:14 (Bool  "for" (Set (Var "G")) "being"   ($#v8_struct_0 :::"finite"::: )     ($#v1_gr_cy_1 :::"cyclic"::: )    ($#l3_algstr_0 :::"Group":::)  (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set   ($#k7_group_1 :::"card"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "m"))))) "holds"  (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st"  (Bool  "("  (Bool (Set   ($#k6_group_1 :::"ord"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set   ($#k5_group_4 :::"gr"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "a")) ($#k6_domain_1 :::"}"::: ) )) "is"   ($#v15_algstr_0 :::"strict"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set (Var "G")))  ")" )))) ; 
 
theorem :: GR_CY_3:15 (Bool  "for" (Set (Var "p")) "being"   ($#v1_gr_cy_3 :::"Safe"::: )    ($#m1_hidden :::"Prime":::) (Bool  "ex" (Set (Var "q")) "being"   ($#v2_gr_cy_3 :::"Sophie_Germain"::: )    ($#m1_hidden :::"Prime":::)(Bool  "ex" (Set (Var "H1")) "," (Set (Var "H2")) "," (Set (Var "Hq")) "," (Set (Var "H2q")) "being"   ($#v15_algstr_0 :::"strict"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set   ($#k3_int_7 :::"Z/Z*"::: )  (Set (Var "p"))) "st"  (Bool  "("  (Bool (Set   ($#k7_group_1 :::"card"::: )  (Set (Var "H1")))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set   ($#k7_group_1 :::"card"::: )  (Set (Var "H2")))  ($#r1_hidden :::"="::: )  (Num 2)) & (Bool (Set   ($#k7_group_1 :::"card"::: )  (Set (Var "Hq")))  ($#r1_hidden :::"="::: )  (Set (Var "q"))) & (Bool (Set   ($#k7_group_1 :::"card"::: )  (Set (Var "H2q")))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "q")))) & (Bool  "("   "for" (Set (Var "H")) "being"   ($#v15_algstr_0 :::"strict"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set   ($#k3_int_7 :::"Z/Z*"::: )  (Set (Var "p")))  "holds"  (Bool  "("  (Bool (Set (Var "H"))  ($#r1_group_2 :::"="::: )  (Set (Var "H1"))) "or" (Bool (Set (Var "H"))  ($#r1_group_2 :::"="::: )  (Set (Var "H2"))) "or" (Bool (Set (Var "H"))  ($#r1_group_2 :::"="::: )  (Set (Var "Hq"))) "or" (Bool (Set (Var "H"))  ($#r1_group_2 :::"="::: )  (Set (Var "H2q")))  ")" )  ")" )  ")" )))) ; 
 definitionlet "n" be   ($#m1_hidden :::"Nat":::); func  :::"Mersenne"::: "n" ->   ($#m1_hidden :::"Nat":::) equals :: GR_CY_3:def 3 (Set (Set  "(" (Num 2)  ($#k2_newton :::"|^"::: )  "n" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1)); end; 





:: deftheorem    defines :::"Mersenne"::: GR_CY_3:def 3 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k1_gr_cy_3 :::"Mersenne"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k2_newton :::"|^"::: )  (Set (Var "n")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1)))); 
 
theorem :: GR_CY_3:16 (Bool (Set   ($#k1_gr_cy_3 :::"Mersenne"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) ; 
 
theorem :: GR_CY_3:17 (Bool (Set   ($#k1_gr_cy_3 :::"Mersenne"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Num 1)) ; 
 
theorem :: GR_CY_3:18 (Bool (Set   ($#k1_gr_cy_3 :::"Mersenne"::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Num 3)) ; 
 
theorem :: GR_CY_3:19 (Bool (Set   ($#k1_gr_cy_3 :::"Mersenne"::: )  (Num 3))  ($#r1_hidden :::"="::: )  (Num 7)) ; 
 
theorem :: GR_CY_3:20 (Bool (Set   ($#k1_gr_cy_3 :::"Mersenne"::: )  (Num 5))  ($#r1_hidden :::"="::: )  (Num 31)) ; 
 
theorem :: GR_CY_3:21 (Bool (Set   ($#k1_gr_cy_3 :::"Mersenne"::: )  (Num 7))  ($#r1_hidden :::"="::: )  (Num 127)) ; 
 
theorem :: GR_CY_3:22 (Bool (Set   ($#k1_gr_cy_3 :::"Mersenne"::: )  (Num 11))  ($#r1_hidden :::"="::: )  (Set (Num 23)  ($#k4_nat_1 :::"*"::: )  (Num 89))) ; 
 
theorem :: GR_CY_3:23 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Prime":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Num 2))) "holds"  (Bool (Set (Set  "("  ($#k1_gr_cy_3 :::"Mersenne"::: )  (Set (Var "p")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set  "(" (Num 2)  ($#k4_nat_1 :::"*"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: GR_CY_3:24 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Prime":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"<>"::: )  (Num 2))) "holds"  (Bool (Set (Set  "("  ($#k1_gr_cy_3 :::"Mersenne"::: )  (Set (Var "p")) ")" )  ($#k4_nat_d :::"mod"::: )  (Num 8))  ($#r1_hidden :::"="::: )  (Num 7))) ; 
 
theorem :: GR_CY_3:25 (Bool  "for" (Set (Var "p")) "being"   ($#v2_gr_cy_3 :::"Sophie_Germain"::: )    ($#m1_hidden :::"Prime":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::">"::: )  (Num 2)) & (Bool (Set (Set (Var "p"))  ($#k4_nat_d :::"mod"::: )  (Num 4))  ($#r1_hidden :::"="::: )  (Num 3))) "holds"  (Bool  "ex" (Set (Var "q")) "being"   ($#v1_gr_cy_3 :::"Safe"::: )    ($#m1_hidden :::"Prime":::) "st" (Bool (Set (Var "q"))  ($#r1_nat_d :::"divides"::: )  (Set   ($#k1_gr_cy_3 :::"Mersenne"::: )  (Set (Var "p")))))) ; 
 
theorem :: GR_CY_3:26 (Bool  "for" (Set (Var "p")) "being"   ($#v2_gr_cy_3 :::"Sophie_Germain"::: )    ($#m1_hidden :::"Prime":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::">"::: )  (Num 2)) & (Bool (Set (Set (Var "p"))  ($#k4_nat_d :::"mod"::: )  (Num 4))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool  "ex" (Set (Var "q")) "being"   ($#v1_gr_cy_3 :::"Safe"::: )    ($#m1_hidden :::"Prime":::) "st" (Bool (Set (Set  "("  ($#k1_gr_cy_3 :::"Mersenne"::: )  (Set (Var "p")) ")" )  ($#k4_nat_d :::"mod"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "q"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 2))))) ; 
 
theorem :: GR_CY_3:27 (Bool  "for" (Set (Var "a")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Num 1))  ($#r1_int_1 :::"divides"::: )  (Set (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "n")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1)))) ; 
 
theorem :: GR_CY_3:28 (Bool  "for" (Set (Var "a")) "," (Set (Var "p")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::">"::: )  (Num 1)) & (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "p")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1)) "is"   ($#m1_hidden :::"Prime":::))) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Num 2)) & (Bool (Set (Var "p")) "is"   ($#m1_hidden :::"Prime":::))  ")" )) ; 
 
theorem :: GR_CY_3:29 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::">"::: )  (Num 1)) & (Bool (Set   ($#k1_gr_cy_3 :::"Mersenne"::: )  (Set (Var "p"))) "is"   ($#m1_hidden :::"Prime":::))) "holds"  (Bool (Set (Var "p")) "is"   ($#m1_hidden :::"Prime":::))) ; 
 
theorem :: GR_CY_3:30 (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "x")) ")" )  ($#k6_int_1 :::"mod"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k6_int_1 :::"mod"::: )  (Set (Var "n")) ")" )  ($#k1_newton :::"|^"::: )  (Set (Var "x")) ")" )  ($#k6_int_1 :::"mod"::: )  (Set (Var "n")))))) ; 
 
theorem :: GR_CY_3:31 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "n"))  ($#r1_int_2 :::"are_relative_prime"::: )  ) & (Bool (Set (Var "x")) "," (Set (Var "y"))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "n")))) "holds"  (Bool (Set (Var "y")) "," (Set (Var "n"))  ($#r1_int_2 :::"are_relative_prime"::: )  )) ; 
 
theorem :: GR_CY_3:32 (Bool  "for" (Set (Var "a")) "," (Set (Var "x")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Prime":::)  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "p"))  ($#r1_int_2 :::"are_relative_prime"::: )  ) & (Bool (Set (Var "a")) "," (Set (Set (Var "x"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "x")))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "p")))) "holds"  (Bool (Set (Var "x")) "," (Set (Var "p"))  ($#r1_int_2 :::"are_relative_prime"::: )  ))) ; 
 
theorem :: GR_CY_3:33 (Bool  "for" (Set (Var "a")) "," (Set (Var "x")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Prime":::)  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "p"))  ($#r1_int_2 :::"are_relative_prime"::: )  ) & (Bool (Set (Var "a")) "," (Set (Set (Var "x"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "x")))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "p")))) "holds"  (Bool (Set (Var "x")) "," (Set (Var "p"))  ($#r1_int_2 :::"are_relative_prime"::: )  ))) ; 
 
theorem :: GR_CY_3:34 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "n")) "," (Set (Var "x")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "n"))) & (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Set (Var "x"))) "," (Set (Set (Var "b"))  ($#k1_newton :::"|^"::: )  (Set (Var "x")))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "n"))))) ; 
 
theorem :: GR_CY_3:35 (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Prime":::)  "holds"  (Bool  "("   "not" (Bool (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a")) ")" )  ($#k6_int_1 :::"mod"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Num 1)) "or" (Bool (Set (Var "a")) "," (Num 1)  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "n"))) "or" (Bool (Set (Var "a")) "," (Set   ($#k4_xcmplx_0 :::"-"::: )  (Num 1))  ($#r2_int_1 :::"are_congruent_mod"::: )  (Set (Var "n")))  ")" ))) ; 
 begin  
theorem :: GR_CY_3:36 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"Prime":::) "holds"  (Bool (Set   ($#k3_int_7 :::"Z/Z*"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_uniroots :::"MultGroup"::: )  (Set  "("  ($#k9_int_3 :::"INT.Ring"::: )  (Set (Var "p")) ")" )))) ; 
 registrationlet "F" be   ($#v5_group_1 :::"commutative"::: )    ($#l6_algstr_0 :::"Skew-Field":::); 
cluster (Set   ($#k1_uniroots :::"MultGroup"::: )  "F") ->   ($#v5_group_1 :::"commutative"::: )   ; 
end; 
theorem :: GR_CY_3:37 (Bool  "for" (Set (Var "F")) "being"   ($#v5_group_1 :::"commutative"::: )    ($#l6_algstr_0 :::"Skew-Field":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_uniroots :::"MultGroup"::: )  (Set (Var "F")) ")" )  (Bool  "for" (Set (Var "x1")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "F"))  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "x1")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k2_group_1 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "x1"))  ($#k11_algstr_0 :::"""::: )  ))))) ; 
 
theorem :: GR_CY_3:38 (Bool  "for" (Set (Var "F")) "being"   ($#v5_group_1 :::"commutative"::: )    ($#l6_algstr_0 :::"Skew-Field":::)  (Bool  "for" (Set (Var "G")) "being"   ($#v8_struct_0 :::"finite"::: )     ($#m1_group_2 :::"Subgroup"::: )   "of" (Set   ($#k1_uniroots :::"MultGroup"::: )  (Set (Var "F"))) "holds"  (Bool (Set (Var "G")) "is"   ($#v1_gr_cy_1 :::"cyclic"::: )    ($#l3_algstr_0 :::"Group":::)))) ;