Prove coprimality of aks

set.mm

@@ -646567,6 +646567,22 @@ fixed reference functional determined by this vector (corresponding to
       AUNWGXFWIYKWSWTWQVN $.
   $}
 
+  ${
+    aks4d1lem1.1 $e |- ( ph -> N e. ( ZZ>= ` 3 ) ) $.
+    aks4d1lem1.2 $e |- B = ( |^ ` ( ( 2 logb N ) ^ 5 ) ) $.
+    $( Technical lemma to reduce proof size.  (Contributed by metakunt,
+       14-Nov-2024.) $)
+    aks4d1lem1 $p |- ( ph -> ( B e. NN /\ 9 < B ) ) $=
+      ( cn wcel c9 clt wbr c2 co c5 cfv cc0 cr a1i c3 syl c1 clogb cceil cz 2re
+      cexp wa 2pos cuz eluzelz zred 0red 3re 3pos cle eluzle ltletrd 1red ltned
+      1lt2 necomd relogbcld cn0 5nn0 reexpcld ceilcld 9re 9pos 3lexlogpow5ineq4
+      ceilge lttrd jca elnnz sylibr eleq1i wceq breqtrrd ) ABFGZHBIJAKCUALZMUEL
+      ZUBNZFGZVQAVTUCGZOVTIJZUFWAAWBWCAVSAVRMAKCKPGAUDQOKIJAUGQACACRUHNGZCUCGDR
+      CUISUJZAORCAUKZRPGAULQWEORIJAUMQAWDRCUNJDRCUOSZUPATKATKAUQTKIJAUSQURUTVAM
+      VBGAVCQVDZVEZAOHVTWFHPGAVFQZAVTWIUJZOHIJAVGQAHVSVTWJWHWKACWEWGVHAVSPGVSVT
+      UNJWHVSVISUPZVJVKVTVLVMBVTFEVNVMAHVTBIWLBVTVOAEQVPVK $.
+  $}
+
   ${
     $d A k $.  $d N k $.  $d k ph $.
     aks4d1p1p1.1 $e |- ( ph -> A e. RR+ ) $.
@@ -647681,6 +647697,246 @@ fixed reference functional determined by this vector (corresponding to
       FUVOUVPYQWN $.
   $}
 
+  ${
+    aks4d1p8d1.1 $e |- ( ph -> P e. Prime ) $.
+    aks4d1p8d1.2 $e |- ( ph -> M e. NN ) $.
+    aks4d1p8d1.3 $e |- ( ph -> N e. NN ) $.
+    aks4d1p8d1.4 $e |- ( ph -> P || M ) $.
+    aks4d1p8d1.5 $e |- ( ph -> -. P || N ) $.
+    $( If a prime divides one number ` M ` , but not another number ` N ` ,
+       then it divides the quotient of ` M ` and the gcd of ` M ` and ` N ` .
+       (Contributed by Thierry Arnoux, 10-Nov-2024.) $)
+    aks4d1p8d1 $p |- ( ph -> P || ( M / ( M gcd N ) ) ) $=
+      ( cgcd co cmul cdvds wbr wcel cn nnzd syl2anc cz wa cdiv cprime prmnn syl
+      gcdnncl wn c1 wceq intnand wb dvdsgcdb syl3anc mtbid coprm biimpa gcddvds
+      syl21anc simpld coprmdvds2d nnproddivdvdsd mpbid ) ABCDJKZLKCMNBCVBUAKMNA
+      BVBCABABUBOZBPOEBUCUDZQZAVBACPODPOVBPOFGCDUERZQZACFQZAVCVBSOZBVBMNZUFZBVB
+      JKUGUHZEVGABCMNZBDMNZTZVJAVNVMIUIABSOCSOZDSOZVOVJUJVEVHADGQZBCDUKULUMVCVI
+      TVKVLBVBUNUOUQHAVBCMNZVBDMNZAVPVQVSVTTVHVRCDUPRURUSABVBCVDVFFUTVA $.
+  $}
+
+  ${
+    $d P p $.  $d Q p $.  $d R p $.  $d p ph $.
+    aks4d1p8d2.1 $e |- ( ph -> R e. NN ) $.
+    aks4d1p8d2.2 $e |- ( ph -> N e. NN ) $.
+    aks4d1p8d2.3 $e |- ( ph -> P e. Prime ) $.
+    aks4d1p8d2.4 $e |- ( ph -> Q e. Prime ) $.
+    aks4d1p8d2.5 $e |- ( ph -> P || R ) $.
+    aks4d1p8d2.6 $e |- ( ph -> Q || R ) $.
+    aks4d1p8d2.7 $e |- ( ph -> -. P || N ) $.
+    aks4d1p8d2.8 $e |- ( ph -> Q || N ) $.
+    $( Any prime power dividing a positive integer is less than that integer if
+       that integer has another prime factor.  (Contributed by metakunt,
+       13-Nov-2024.) $)
+    aks4d1p8d2 $p |- ( ph -> ( P ^ ( P pCnt R ) ) < R ) $=
+      ( cpc co wcel c1 wbr cdvds wn vp cexp cmul cprime cn prmnn nnred reexpcld
+      syl pccld remulcld clt recnd mulid1d nnrpd nn0zd rpexpcld prmgt1 ltmul2dd
+      1red eqbrtrrd cle nnzd zexpcld cgcd gcdcomd wceq cv wral wrex wa cc0 0lt1
+      a1i 0red ltnled mpbid exp1d eqcomd oveq2d cz 1zzd syl2anc eqtrd adantr wb
+      breq1 adantl bicomd biimpd mpd pm2.65da neqcomd pcelnn mpbird prmdvdsexpb
+      syl3anc notbid nnexpcld pceq0 breq12d simpr oveq1d rspcime rexnal pc2dvds
+      pcid coprm pcdvds coprmdvds2d wi zmulcld dvdsle ltletrd ) ABBDNOZUBOZXPCU
+      COZDABXOABABUDPZBUEPHBUFUIZUGABDHFUJZUHZAXPCYAACACUDPZCUEPICUFUIZUGZUKADF
+      UGAXPQUCOXPXQULAXPAXPYAUMUNAQCXPAUTZYDABXOABXSUOAXOXTUPUQAYBQCULRICURUIUS
+      VAAXQDSRZXQDVBRZAXPCDABXOABXSVCXTVDZACYCVCZADFVCAXPCVEOCXPVEOZQAXPCYHYIVF
+      ACXPSRZTZYJQVGZAYLUAVHZCNOZYNXPNOZVBRZUAUDVIZTZAYQTZUAUDVJZYSAYTUACUDAYNC
+      VGZVKZYTCCNOZCXPNOZVBRZTZAUUGUUBAUUGQVLVBRZTZAVLQULRZUUIUUJAVMVNAVLQAVOYE
+      VPVQAUUFUUHAUUDQUUEVLVBAUUDCCQUBOZNOZQACUUKCNAUUKCACACYDUMVRVSVTAYBQWAPUU
+      LQVGIAWBQCXGWCWDAUUEVLVGZYLAYLCBVGZTABCABCVGZBESRZAUUOVKZCESRZUUPAUURUUOM
+      WEUUQUURUUPUUQUUPUURUUOUUPUURWFABCESWGWHWIWJWKAUUPTUUOLWEWLWMAYKUUNAYBXRX
+      OUEPZYKUUNWFIHAUUSBDSRZJAXRDUEPZUUSUUTWFHFBDWNWCWOCBXOWPWQWRWOAYBXPUEPUUM
+      YLWFIABXOXSXTWSCXPWTWCWOXAWRWOWEUUCYQUUFUUCYOUUDYPUUEVBUUCYNCCNAUUBXBZXCU
+      UCYNCXPNUVBXCXAWRWOIXDUUAYSWFAYQUAUDXEVNVQAYKYRACWAPXPWAPZYKYRWFYIYHCXPUA
+      XFWCWRWOAYBUVCYLYMWFIYHCXPXHWCVQWDAXRUVAXPDSRHFBDXIWCKXJAXQWAPUVAYFYGXKAX
+      PCYHYIXLFXQDXMWCWKXN $.
+  $}
+
+  ${
+    aks4d1p8d3.1 $e |- ( ph -> N e. NN ) $.
+    aks4d1p8d3.2 $e |- ( ph -> P e. Prime ) $.
+    aks4d1p8d3.3 $e |- ( ph -> P || N ) $.
+    $( The remainder of a division with its maximal prime power is coprime with
+       that prime power.  (Contributed by metakunt, 13-Nov-2024.) $)
+    aks4d1p8d3 $p |- ( ph ->
+     ( ( N / ( P ^ ( P pCnt N ) ) ) gcd ( P ^ ( P pCnt N ) ) ) = 1 ) $=
+      ( co cgcd c1 cdvds wbr cz wcel cn syl2anc cc0 wb syl nnzd clt cexp cprime
+      cpc cdiv pcdvds prmnn pccld zexpcld zcnd 0red 1red zred 0lt1 prmgt1 lttrd
+      wne a1i ltned necomd nn0zd expne0d dvdsval2 syl3anc mpbid gcdcomd wceq wn
+      pcndvds2 coprm pcelnn mpbird rpexp eqtrd ) ACBBCUCGZUAGZUDGZVOHGVOVPHGZIA
+      VPVOAVOCJKZVPLMZABUBMZCNMZVREDBCUEOAVOLMVOPUPCLMVRVSQABVNABAVTBNMEBUFRSZA
+      BCEDUGZUHZABVNABWBUIAPBAPBAUJZAPIBWEAUKABWBULPITKAUMUQAVTIBTKEBUNRUOURUSA
+      VNWCUTVAACDSVOCVBVCVDZWDVEAVQIVFZBVPHGIVFZABVPJKVGZWHAVTWAWIEDBCVHOAVTVSW
+      IWHQEWFBVPVIOVDABLMVSVNNMZWGWHQWBWFAWJBCJKZFAVTWAWJWKQEDBCVJOVKBVPVNVLVCV
+      KVM $.
+  $}
+
+  ${
+    $d A p r y $.  $d A r x y $.  $d B o $.  $d B r x y $.  $d N k p $.
+    $d N p r $.  $d R k p $.  $d R p r y $.  $d k p ph $.  $d o ph $.
+    $d B f $.  $d N p q $.  $d R p q $.  $d f ph $.  $d ph q $.
+    aks4d1p8.1 $e |- ( ph -> N e. ( ZZ>= ` 3 ) ) $.
+    aks4d1p8.2 $e |- A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e.
+     ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) $.
+    aks4d1p8.3 $e |- B = ( |^ ` ( ( 2 logb N ) ^ 5 ) ) $.
+    aks4d1p8.4 $e |- R = inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) $.
+    $( Show that ` N ` and ` R ` are coprime for AKS existence theorem, with
+       eliminated hypothesis.  (Contributed by Thierry Arnoux, 10-Nov-2024.) $)
+    aks4d1p8 $p |- ( ph -> ( N gcd R ) = 1 ) $=
+      ( c1 co clt wbr wcel cle adantr c2 cc0 vp vx vy vo vf vq cgcd wa cdvds wn
+      cdiv cv cprime cfz crab cr cinf wceq a1i wss wral ssrab2 cn elfznn adantl
+      nnred ex ssrdv sstrd cfn c0 wne fzfid ssfid aks4d1p3 rabn0 sylibr fiminre
+      wrex syl3anc breq1 notbid 1zzd cz clogb c5 cexp cceil cfv c3 zred ltletrd
+      syl 1red ltned necomd relogbcld cn0 ad4antr wb ad2antrr wi dvdsval2 mpbid
+      nnzd cmul nncnd mulid2d sylbir jca dvdsle syl2anc eqbrtrd nnrpd lemuldivd
+      lttrd ltled letrd mpbird elfzd simplr zexpcld eqcomd cfl ad3antrrr simprl
+      c9 recnd cc crp redivcld ltnled breq1d infrefilb 3expa mpd elrab3 con2bid
+      con3d r19.29a 2re 2pos cuz eluzelz 0red 3re 3pos eluzle 1lt2 5nn0 ceilcld
+      reexpcld eqeltrd simplrl prmnn nnne0d aks4d1p4 simpld anass anbi1i imbi1i
+      mpbi imp remulcld elfzle2 9pos eqeltrrd 3lexlogpow5ineq4 ceilged breqtrrd
+      9re nnge1d lemulge11d ledivmul2d anasss pccld zcnd nn0zd expne0d divcan1d
+      cpc pcdvds cmin cprod elnnz flcld gtned logb1 2z leidd 0lt1 1lt9 logblebd
+      0zd elnn0z nnnn0d zsubcld fprodzcl zmulcld eleq1d aks4d1p8d3 exp0d pcelnn
+      flge nngt0d prmgt1 ltexp2d eqbrtrrd ltmulgt11d rpexpcld expge1d nnledivrp
+      ltdivmul2d simprr simplrr simpr prmdvdsncoprmbd bicomd biimpd coprmdvds2d
+      aks4d1p8d2 simprd ad5antr pm2.21dd lbinfle ltdiv2d div1d breqtrd pm2.65da
+      elrabd 1rp aks4d1p7 aks4d1p5 ) ABCDEFGHIJKALFDUGMZNOZUHZDUYNUKMBUIOZUJZUY
+      QUYPUAULZDUIOZUYSFUIOUJZUHZUYRUAUMUYPUYSUMPZUHZVUBUHZUYQDDUYSUKMZQOZVUEUY
+      QUHZDGULZBUIOZUJZGLCUNMZUOZUPNUQZVUFQDVUNURZVUHKUSVUHVUMUPUTZUBULUCULQOUC
+      VUMVAUBVUMVSZVUFVUMPVUNVUFQOVUEVUPUYQVUDVUPVUBUYPVUPVUCAVUPUYOAVUMVULUPVU
+      MVULUTAVUKGVULVBUSZAUDVULUPAUDULZVULPZVUSUPPAVUTUHVUSVUTVUSVCPAVUSCVDVEVF
+      VGVHVIZRRRRVUEVUQUYQVUDVUQVUBUYPVUQVUCAVUQUYOAVUPVUMVJPZVUMVKVLZVUQVVAAVU
+      LVUMALCVMVURVNZAVUKGVULVSVVCABCEFGHIJVOVUKGVULVPVQUBUCVUMVRVTRRRRVUHVUKVU
+      FBUIOZUJZGVUFVULVUIVUFURVUJVVEVUIVUFBUIWAWBVUHVUFLCVUHWCACWDPZUYOVUCVUBUY
+      QACSFWEMZWFWGMZWHWIZWDCVVJURAJUSZAVVIAVVHWFASFSUPPAUUAUSZTSNOAUUBUSZAFAFW
+      JUUCWIPZFWDPZHWJFUUDWMZWKZATWJFAUUEZWJUPPAUUFUSVVQTWJNOAUUGUSAVVNWJFQOHWJ
+      FUUHWMZWLZALSALSAWNZLSNOAUUIUSWOWPZWQWFWRPAUUJUSUULZUUKUUMZWSVUHUYTVUFWDP
+      ZVUDUYTVUAUYQUUNZVUHUYSWDPZUYSTVLZDWDPZUYTVWEWTVUHUYSVUDUYSVCPZVUBUYQVUCV
+      WJUYPUYSUUOVEZXAZXEZVUDVWHVUBUYQVUDUYSVWKUUPZXAVUDUYTUHZVUAUHZUYQUHZVWIXB
+      VUHVWIXBVWQDVWPDVCPZUYQAVWRUYOVUCUYTVUAADVULPZVWRAVWSDBUIOZUJZABCDEFGHIJK
+      UUQZUURZDCVDWMZWSZRZXEVWQVUHVWIVWPVUEUYQVUDUYTVUAUUSZUUTZUVAUVBUYSDXCVTXD
+      VUHLUYSXFMZDQOLVUFQOVUHVXIUYSDQVUHUYSVUHUYSVWLXGXHVUHVWGVWRUHZUYTUYSDQOZV
+      UHVWGVWRVWMVUHVWQVWRVXHVXFXIXJVWFVXJUYTVXKUYSDXKUVCXLXMVUHLDUYSVUHWNVUEDU
+      PPZUYQVUDVXLVUBUYPVXLVUCAVXLUYOADVXDVFZRRRZRZVUHUYSVWLXNZXOXDVUEVUFCQOZUY
+      QVUDVXQVUBVUDVXQDCUYSXFMZQOVUDDCVXRAVXLUYOVUCVXMXAZVUDCAVVGUYOVUCVWDXAZWK
+      ZVUDCUYSVYAVUDUYSVWKVFZUVDUYPDCQOZVUCAVYCUYOAVWSVYCVXCDLCUVEWMRRZVUDCUYSV
+      YAVYBUYPTCQOZVUCAVYEUYOATCVVRACVWDWKZATYGCVVRYGUPPAUVKUSZVYFTYGNOAUVFUSAY
+      GVVJCNAYGVVIVVJVYGVWCACVVJUPVVKVYFUVGAFVVQVVSUVHAVVIVWCUVIWLVVKUVJZXPZXQR
+      RVUDUYSVWKUVLZUVMXRVUDDCUYSVXSVYAVUDUYSVWKXNZUVNXSRRXTVUHVWTVVFVUEVWTUYQV
+      UEDDUYSUYSDUWAMZWGMZUKMZVYMXFMZBUIVUEVYODVUEDVYMVUEDVXNYHZVUEVYMVUEUYSVYL
+      VUEUYSVUDVWJVUBVWKRZXEVUEUYSDUYPVUCVUBYAZVUDUYTVUAVWRVXEUVOZUVPZYBZUVQZVU
+      EUYSVYLVUEUYSVYQXGZVUDVWHVUBVWNRVUEVYLVYTUVRZUVSZUVTYCVUEVYNVYMBVUEVYMDUI
+      OZVYNWDPZVUEVUCVWRWUFVYRVYSUYSDUWBXLZVUEVYMWDPZVYMTVLVWIWUFWUGWTWUAWUEVUE
+      DVYSXEVYMDXCVTXDZWUAABWDPZUYOVUCVUBAWUKFSCWEMZYDWIZWGMZLVVHSWGMYDWIZUNMZF
+      EULZWGMZLUWCMZEUWDZXFMZWDPAWUNWUTAFWUMAFAFVCPZVVOTFNOZUHZAVVOWVCVVPVVTXJW
+      VBWVDWTAFUWEUSXSZXEZAWUMWRPZWUMWDPZTWUMQOZUHZAWVHWVIAWULASCVVLVVMVYFVYIVW
+      BWQZUWFATWULQOZWVIATSLWEMZWULQAWVMTASYIPSTVLSLVLWVMTURASVVLYHATSVVRVVMUWG
+      VWBSUWHVTYCASLCSWDPAUWIUSASVVLUWJVWATLNOAUWKUSVYFVYIALCVWAVYFALYGCVWAVYGV
+      YFLYGNOAUWLUSVYHXPXQUWMXMAWULUPPTWDPZWVLWVIWTWVKAUWNZWULTUXDXLXDXJWVGWVJW
+      TAWUMUWOUSXSYBAWUPWUSEALWUOVMAWUQWUPPZUHZWURLWVQFWUQAVVOWVPWVFRWVQWUQWVPW
+      UQVCPAWUQWUOVDVEUWPYBWVQWCUWQUWRUWSABWVAWDBWVAURAIUSUWTXSYEVUEUYSDVYSVYRV
+      UDUYTVUAYFZUXAVUEVYNBUIOZVYNVUMPZUJZVUEVUNVYNQOZUJZWWAVUEDVYNQOZUJZWWCVUE
+      VYNDNOZWWEVUEWWFDDVYMXFMNOZVUELVYMNOWWGVUEUYSTWGMZLVYMNVUEUYSWUCUXBVUETVY
+      LNOWWHVYMNOVUEVYLVUEVYLVCPZUYTWVRVUEVUCVWRWWIUYTWTVYRVYSUYSDUXCXLXSUXEVUE
+      UYSTVYLVUDUYSUPPVUBVYBRZAWVNUYOVUCVUBWVOYEWUDVUDLUYSNOZVUBVUCWWKUYPUYSUXF
+      VERZUXGXDUXHVUEVYMDVUEVYMWUAWKZVUDDYJPZVUBUYPWWNVUCAWWNUYOADVXDXNRRRZUXIX
+      DVUEDDVYMVXNVXNVUEUYSVYLVUDUYSYJPVUBVYKRWUDUXJZUXMXSVUEVYNDVUEDVYMVXNWWMW
+      UEYKZVXNYLXDVUEWWDWWBVUEDVUNVYNQVUOVUEKUSZYMWBXDVUEVUPVVBWWCWWAXBVUDVUPVU
+      BUYPVUPVUCAVUPUYOAVUMVULUPVURAUEVULUPAUEULZVULPZWWSUPPAWWTUHWWSWWTWWSVCPA
+      WWSCVDVEVFVGVHVIRRRZVUDVVBVUBUYPVVBVUCAVVBUYOVVDRRRZVUPVVBUHZWVTWWBWXCWVT
+      WWBVUPVVBWVTWWBVYNVUMYNYOVGYSXLYPVUEVYNVULPZWVSWWAWTVUEVYNLCVUEWCZVUDVVGV
+      UBVXTRZWUJVUELVYMXFMZDQOLVYNQOVUEWXGVYMDQVUEVYMWUBXHVUEWUFVYMDQOZWUHVUEWU
+      IVWRWUFWXHXBWUAVYSVYMDXKXLYPZXMVUELDVYMUYPLUPPZVUCVUBAWXJUYOVWARXAZVXNWWP
+      XOXDVUEVYNDCWWQVXNVUDCUPPVUBVYARZVUELVYMQOZVYNDQOZVUEUYSVYLWWJVYTVUDLUYSQ
+      OVUBVYJRUXKZVUEVWRVYMYJPWXMWXNWTVYSWWPDVYMUXLXLXDVUDVYCVUBVYDRZXRXTWXDWVT
+      WVSVUKWVSUJGVYNVULVUIVYNURVUJWVSVUIVYNBUIWAWBYQYRWMXSVUEVYMBUIOZVYMVUMPZU
+      JZVUEVUNVYMQOZUJZWXSVUEDVYMQOZUJZWYAVUEVYMDNOZWYCVUEUFULZFUIOZWYEDUIOZUHZ
+      WYDUFUMVUEWYEUMPZUHZWYHUHUYSWYEDFVUEVWRWYIWYHVYSXAVUEWVBWYIWYHVUEVWPWVBVX
+      GVWOWVBVUAVUDWVBUYTUYPWVBVUCAWVBUYOWVERRRRXIZXAVUEVUCWYIWYHVYRXAVUEWYIWYH
+      YAVUEUYTWYIWYHWVRXAWYJWYFWYGUXNWYJVUAWYHVUDUYTVUAWYIUXORWYJWYFWYGYFUYAVUE
+      UYNLVLZWYHUFUMVSZVUELUYNVUELUYNWXKUYPUYOVUCVUBAUYOUXPXAWOWPVUEWYLWYMVUEWY
+      MWYLVUEFDUFWYKVYSUXQUXRUXSYPYTVUEVYMDWWMVXNYLXDVUEWYBWXTVUEDVUNVYMQWWRYMW
+      BXDVUEVUPVVBWYAWXSXBWXAWXBWXCWXRWXTWXCWXRWXTVUPVVBWXRWXTVYMVUMYNYOVGYSXLY
+      PVUEWXRWXQVUEVYMVULPWXRWXQUJZWTVUEVYMLCWXEWXFWUAWXOVUEVYMDCWWMVXNWXLWXIWX
+      PXRXTVUKWYNGVYMVULVUIVYMURVUJWXQVUIVYMBUIWAWBYQWMYRXSUXTXMRVUHVWQVXAVXHAV
+      XAUYOVUCUYTVUAUYQAVWSVXAVXBUYBUYCXIUYDUYJUBUCVUFVUMUYEVTXMVUHVUFDNOVUGUJV
+      UHVUFDLUKMZDNVUHWWKVUFWYONOVUEWWKUYQWWLRVUHLUYSDLYJPVUHUYKUSVXPVUEWWNUYQW
+      WORUYFXDVUHDVUEDYIPUYQVYPRUYGUYHVUHVUFDVUEVUFUPPZUYQVUDWYPVUBVUDDUYSVXSVY
+      BVWNYKRRVXOYLXDUYIAVUBUAUMVSUYOABCDEFGUAHIJKUYLRYTRUYM $.
+  $}
+
+  ${
+    $d A r $.  $d B r $.  $d N k x z $.  $d N r $.  $d R k x z $.  $d R r $.
+    $d k ph x z $.
+    aks4d1p9.1 $e |- ( ph -> N e. ( ZZ>= ` 3 ) ) $.
+    aks4d1p9.2 $e |- A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e.
+     ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) $.
+    aks4d1p9.3 $e |- B = ( |^ ` ( ( 2 logb N ) ^ 5 ) ) $.
+    aks4d1p9.4 $e |- R = inf ( { r e. ( 1 ... B ) | -. r || A } , RR , < ) $.
+    $( Show that the order is bound by the squared binary logarithm.
+       (Contributed by metakunt, 14-Nov-2024.) $)
+    aks4d1p9 $p |- ( ph -> ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` R ) ` N ) ) $=
+      ( c2 co wbr cdvds wcel cz cc0 c1 adantr vx vz clogb cexp codz cfv clt cle
+      wn wa cfl cr wb 2re a1i 2pos c3 cuz eluzelz syl zred 0red 3re 3pos eluzle
+      ltletrd 1red 1lt2 ltned necomd relogbcld resqcld cn cgcd w3a cfz aks4d1p4
+      wceq simpld elfznn aks4d1p8 3jca nnzd flge syl2anc biimpd imp wi cmin cn0
+      odzcl nnnn0d zexpcld 1zzd zsubcld cv cprod cmul c9 aks4d1lem1 nnred flcld
+      nngt0d cc wne 2cnd gtned logb1 2z leidd 0lt1 nnge1d logblebd eqbrtrrd 0zd
+      mpbid jca elnn0z sylibr fzfid adantl zmulcld eleq1d mpbird iddvds odzdvds
+      cmpt fveq2 breq1d wral ssidd fmpttd fprodfvdvdsd simpr elfzd eqidd oveq2d
+      fprodzcl oveq1d fvmptd rspcdva breq12d dvdsmultr2d breqtrrd dvdstrd mpdan
+      prodeq2dv ex simprd pm2.65da ltnled ) ALFUCMZLUDMZFDUEUFUFZUGNUUNUUMUHNZU
+      IAUUODBONZAUUOUJZUUNUUMUKUFZUHNZUUPAUUOUUSAUUOUUSAUUMULPUUNQPZUUOUUSUMAUU
+      LALFLULPAUNUOZRLUGNAUPUOZAFAFUQURUFPZFQPZHUQFUSUTZVAZARUQFAVBZUQULPAVCUOU
+      VFRUQUGNAVDUOAUVCUQFUHNHUQFVEUTVFASLASLAVGZSLUGNAVHUOVIVJZVKZVLZAUUNADVMP
+      ZUVDFDVNMSVRZVOZUUNVMPAUVLUVDUVMADSCVPMPZUVLAUVOUUPUIZABCDEFGHIJKVQZVSDCV
+      TUTZUVEABCDEFGHIJKWAWBZFDWKUTZWCZUUMUUNWDWEWFWGUUQUUSUUPAUUSUUPWHUUOAUUSU
+      UPAUUSUJZDFUUNUDMZSWIMZBADQPUUSADUVRWCTUWBUWCSUWBFUUNAUVDUUSUVETZAUUNWJPZ
+      UUSAUUNUVTWLZTWMUWBWNZWOZABQPZUUSAUWJFLCUCMZUKUFZUDMZSUURVPMZFEWPZUDMZSWI
+      MZEWQZWRMZQPAUWMUWRAFUWLUVEAUWLQPZRUWLUHNZUJUWLWJPZAUWTUXAAUWKALCUVAUVBAC
+      ACVMPWSCUGNACFHJWTVSZXAZACUXCXCZUVIVKZXBARUWKUHNZUXAALSUCMZRUWKUHALXDPZLR
+      XEZLSXEZVOUXHRVRAUXIUXJUXKAXFARLUVGUVBXGUVIWBLXHUTALSCLQPAXIUOALUVAXJUVHR
+      SUGNAXKUOUXDUXEACUXCXLXMXNAUWKULPRQPUXGUXAUMUXFAXOUWKRWDWEXPXQUWLXRXSZWMA
+      UWNUWQEASUURXTZAUWOUWNPZUJZUWPSUXOFUWOAUVDUXNUVETUXNUWOWJPAUXNUWOUWOUURVT
+      ZWLYAWMUXOWNWOYRYBABUWSQBUWSVRZAIUOYCYDTADUWDONZUUSAUXRUUNUUNONZAUUTUXSUW
+      AUUNYEUTAUVNUWFUXRUXSUMUVSUWGFUUNDYFWEYDTUWBUWDUWSBOUWBUWDUWMUWRUWIUWBFUW
+      LUWEAUXBUUSUXLTWMUWBUWNUWQEUWBSUURXTUWBUXNUJZUWPSUXTFUWOUWBUVDUXNUWETUXTU
+      WOUXNUWOVMPUWBUXPYAWLWMUXTWNWOZYRUWBUUNUAUWNFUAWPZUDMZSWIMZYGZUFZUWNUWOUY
+      EUFZEWQZONZUWDUWRONUWBUBWPZUYEUFZUYHONZUYIUBUWNUUNUYJUUNVRUYKUYFUYHOUYJUU
+      NUYEYHYIAUYLUBUWNYJUUSAUBUWNUWNEUYEUXMAUWNYKAUAUWNUYDQAUYBUWNPZUJZUYCSUYN
+      FUYBAUVDUYMUVETUYNUYBUYMUYBVMPAUYBUURVTYAWLWMUYNWNWOYLYMTUWBUUNSUURUWHUWB
+      UUMUWBUULAUULULPUUSUVJTVLXBAUUTUUSUWATASUUNUHNUUSAUUNUVTXLTAUUSYNYOZUUAUW
+      BUYFUWDUYHUWROUWBUAUUNUYDUWDUWNUYEQUWBUYEYPUWBUYBUUNVRZUJZUYCUWCSWIUYQUYB
+      UUNFUDUWBUYPYNYQYSUYOUWIYTUWBUWNUYGUWQEUXTUAUWOUYDUWQUWNUYEQUXTUYEYPUXTUY
+      BUWOVRZUJZUYCUWPSWIUYSUYBUWOFUDUXTUYRYNYQYSUWBUXNYNUYAYTUUGUUBXPUUCUXQUWB
+      IUOUUDUUEUUHTWGUUFAUVPUUOAUVOUVPUVQUUITUUJAUUMUUNUVKAUUNUVTXAUUKYD $.
+  $}
+
+  ${
+    $d B a h $.  $d B h k $.  $d B h r $.  $d N a b c $.  $d N a b h $.
+    $d N b c k $.  $d N c r $.  $d a ph $.  $d ph r $.
+    aks4d1.1 $e |- ( ph -> N e. ( ZZ>= ` 3 ) ) $.
+    aks4d1.2 $e |- B = ( |^ ` ( ( 2 logb N ) ^ 5 ) ) $.
+    $( Lemma 4.1 from ~ https://www3.nd.edu/%7eandyp/notes/AKS.pdf , existence
+       of a polynomially bounded number by the digit size of ` N ` that asserts
+       the polynomial subspace that we need to search to guarantee that ` N `
+       is prime.  Eventually we want to show that the polynomial searching
+       space is bounded by degree ` B ` .  (Contributed by metakunt,
+       14-Nov-2024.) $)
+    aks4d1 $p |- ( ph -> E. r e. ( 1 ... B ) ( ( N gcd r ) = 1 /\
+    ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` r ) ` N ) ) ) $=
+      ( vb va vk cv co c1 wceq cexp cfv clt wbr cmin cmul cdvds vh vc cgcd codz
+      c2 clogb wa cfl cfz cprod wn crab cr cinf oveq2 oveq1d cbvprodv oveq2i id
+      wcel a1i breq12d notbid cbvrabv infeq1i simpld adantl eqeq1d fveq2 fveq1d
+      aks4d1p4 breq2d anbi12d aks4d1p8 aks4d1p9 jca rspcedvd ) ACDJZUCKZLMZUECU
+      FKUENKZCVRUDOZOZPQZUGCUAJZCUEBUFKUHONKZLWAUHOUIKZCUBJZNKZLRKZUBUJZSKZTQZU
+      KZUALBUIKZULZUMPUNZUCKZLMZWACWQUDOZOZPQZUGDWQWOAWQWOUTWQWFWGCGJZNKZLRKZGU
+      JZSKZTQUKAXGBWQHCIEXFWGCHJZNKZLRKZHUJWFSWGXEXJGHXCXHMXDXILRXCXHCNUOUPUQUR
+      ZFUMWPIJZXGTQZUKZIWOULPWNXNUAIWOWEXLMZWMXMXOWEXLWLXGTXOUSWLXGMXOWKXFWFSWG
+      WJXEUBGWHXCMWIXDLRWHXCCNUOUPUQURVAVBVCVDVEZVKVFAVRWQMZUGZVTWSWDXBXRVSWRLX
+      QVSWRMAVRWQCUCUOVGVHXRWCXAWAPXRCWBWTXQWBWTMAVRWQUDVIVGVJVLVMAWSXBAXGBWQHC
+      IEXKFXPVNAXGBWQHCIEXKFXPVOVPVQ $.
+  $}
+
   ${
     $( The value of 5 choose 2.  (Contributed by metakunt, 8-Jun-2024.) $)
     5bc2eq10 $p |- ( 5 _C 2 ) = ; 1 0 $=