metamath/valid/amc12b-2002-p3.mm

${
  amc12b-2002-p3.0 $e |- ( ph -> N e. NN ) $.
  amc12b-2002-p3.1 $e |- ( ph -> ( ( ( N ^ 2 ) - ( 3 x. N ) ) + 2 ) e. Prime ) 
$.
  $( (Contributed by Kunhao Zheng, 22-Apr-2021.) $)
  amc12b-2002-p3 $p |- ( ph -> N = 3 ) $=
( c1 cmin co c2 cmul wceq c3 wcel caddc cneg a1i cz cdiv wa zsubcld cc0 2cn 
cprime ceven cexp nncnd 1cnd negsubd oveq12d eqcomd negcld ax-1cn mul2negib 
2cnd mulid2i negdid 1p2e3 negeqi syl6eq quadfact3d sqcld 3cn mulcld addassd 
mulneg1d oveq2d eqtr2d oveq1d eqtr4d 3eqtr2d eqeltrd nnzd 1zzd zmulcld codd cc 
2z wo zeoALTV syl iseven peano2zm adantr zcnd simpl wne 2ne0 divassd zcn 
divsubdird 2div2e1 oveq2i simpr sylbi isodd2 subcld div23d jca wb mpbird wi 
jaoi evenprm2 biimpd imp mp2and eqeq1d biimpa 0cnd addcan2d addid2i biimpar 
eqeq2d bitr3d sqvald mulcomd eqtr3d eqtrd orbi2d bitrd syldan nnne0d neneqd 
subdird mul0ord subeq0ad orcomd ord mt3d mpdan ) ABEFGZBHFGZIGZHJZBKJZAYLUB 
LZYLUCLZYMAYLBHUDGZKBIGZFGZHMGZUBAYLBENZMGZBHNZMGZIGZYQKNZBIGZHMGMGZYTAUUEY 
LAUUBYJUUDYKIABEABCUEZAUFZUGABHUUIAUMZUGUHUIAUUFHUUAUUCBAEUUJUJAHUUKUJUUIUU 
AUUCIGHJAEHHUKUAUAHUAUNULOAUUAUUCMGZEHMGZNZUUFAUUNUULAEHUUJUUKUOUIUUMKUPUQU 
RUSAUUHYQUUGMGZHMGZYTAUUPUUHAYQUUGHABUUIUTZAUUFBAKKVOLAVAOZUJUUIVBUUKVCUIAY 
SUUOHMAUUOYQYRNZMGYSAUUGUUSYQMAKBUURUUIVDVEAYQYRUUQAKBUURUUIVBZUGVFVGVHVIZD 
VJAYPYLPLZYLHQGZPLZRZAUVBUVDAYJYKABEABCVKZAVLSABHUVFHPLZAVPOSVMABUCLZBVNLZV 
QZUVDABPLZUVJUVFBVRVSUVHUVDUVIUVHUVKBHQGZPLZRZUVDBVTUVNUVCYJYKHQGZIGPUVNYJY 
KHUVNYJUVKYJPLUVMBWAZWBZWCUVNYKUVNBHUVKUVMWDUVGUVNVPOSWCUVNUMHTWEZUVNWFOWGU 
VNYJUVOUVQUVNUVOUVLEFGZPUVNUVOUVLHHQGZFGZUVSUVKUVOUWAJUVMUVKBHHBWHZUVKUMZUW 
CUVRUVKWFOZWIWBUVTEUVLFWJWKURUVNUVLEUVKUVMWLUVNVLSVJVMVJWMUVIUVKYJHQGZPLZRZ 
UVDBWNUWGUVCUWEYKIGZPUVKUVCUWHJUWFUVKYJYKHUVKYJUVPWCUVKBHUWBUWCWOUWCUWDWPWB 
UWGUWEYKUVKUWFWLUWGBHUVKUWFWDUVGUWGVPOSVMVJWMXAVSWQYPUVEWRAYLVTOWSYOYPRYMWT 
AYOYPYMYOYPYMYLXBXCXDOXEAYMYTHJZYNAYMUWIAYLYTHUVAXFXGAUWIYSTJZYNAUWJUWIAYTT 
HMGZJUWJUWIAYSTHAYQYRUUQUUTWOAXHUUKXIAUWKHYTUWKHJAHUAXJOXLXMXKAUWJBTJZYNVQZ 
YNAUWJBBKFGZIGZTJZUWMAUWJRYSUWOTAYSUWOJUWJAYSBBIGZYRFGZUWOAYQUWQYRFABUUIXNV 
GAUWOUWRAUWNBIGUWOUWRAUWNBABKUUIUURWOZUUIXOABKBUUIUURUUIYCXPUIXQWBAUWJWLXPA 
UWPUWMAUWPUWLUWNTJZVQUWMABUWNUUIUWSYDAUWTYNUWLABKUUIUURYEXRXSXGXTAUWMRZYNUW 
LUXABTABTWEUWMABCYAWBYBUXAYNUWLUXAUWLYNAUWMWLYFYGYHXTXTXTYI $.
$}