metamath/valid/induction-ineq-nsqlefactn.mm (37 lines of code) (raw):

${ $d N x $. $d ph x y $. induction-ineq-nsqlefactn.0 $e |- ( ph -> N e. ( ZZ>= ` 4 ) ) $. $( (Contributed by Stanislas Polu, 12-Oct-2020.) $) induction-ineq-nsqlefactn $p |- ( ph -> ( N ^ 2 ) <_ ( ! ` N ) ) $= ( c4 cfv wcel c2 cexp co cfa cle wbr c1 wceq cmul a1i cr ad2antlr syl c3 vx vy cuz cv caddc oveq1 fveq2 breq12d cdc c6 4cn sqvali 4t4e16 eqtri 1nn0 6nn decnncl nnrei 2nn0 4nn 6nn0 4nn0 6lt10 decltc ltleii eqbrtri eqcomi breqtrd 1lt2 fac4 wa eluzelz peano2zd zred cn0 eluznn0 mpancom faccld cc0 peano2nn0 nnred adantl nn0ge0d adantr leidd cmin cz 2z zmulcld cn eluznn mpan nnm1nn0 faccl eluzelre remulcld 1red nnge1d leadd2dd eluzelcn 2timesd breqtrrd fac3 2re 6re eqeltri 2lt6 breqtrri 3nn0 df-4 oveq1i 3cn ax-1cn pncan3oi lesub1dd 4re eluzle syl5eqbrr facwordi syl3anc letrd lemul1ad cc npcan sylancl facp1 zcn oveq2d fveq2d eqtr3d lemul12ad zcnd sqvald eqcomd nncnd mulcomd 3brtr3d eqtrd zzkindd mpdan ) ABDUCEZFBGHIZBJEZKLZCAUAUDZGHIZUUEJEZKLDGHIZDJEZKLUBU DZGHIZUUJJEZKLZUUJMUEIZGHIZUUNJEZKLUUDUAUBBDUUEDNUUFUUHUUGUUIKUUEDGHUFUUEDJ UGUHUUEUUJNUUFUUKUUGUULKUUEUUJGHUFUUEUUJJUGUHUUEUUNNUUFUUOUUGUUPKUUEUUNGHUF UUEUUNJUGUHUUEBNUUFUUBUUGUUCKUUEBGHUFUUEBJUGUHAUUHGDUIZUUIKUUHUUQKLAUUHMUJU IZUUQKUUHDDOIUURDUKULUMUNUURUUQUURMUJUOUPUQURUUQGDUSUTUQURMGUJDUOUSVAVBVCVI VDVEVFPUUQUUINAUUIUUQVJVGPVHAUUJUUAFZVKZUUMVKZUUNUUNOIZUUNUULOIZUUOUUPKUVAU UNUUNUUNUULUUSUUNQFAUUMUUSUUNUUSUUJDUUJVLZVMZVNRZUVFUVFUUSUULQFAUUMUUSUULUU SUUJDVOFZUUSUUJVOFZUVGUUSVBPUUJDVPVQZVRZWARUUTVSUUNKLUUMUUTUUNUUSUUNVOFZAUU SUVHUVKUVIUUJVTSWBWCWDZUVLUVAUUNUVFWEUVAUUNUUJMWFIZJEZUUJOIZUULKUVAUUNGUUJO IZUVOUVFUUTUVPQFUUMUUTUVPUUTGUUJGWGFUUTWHPUUSUUJWGFZAUVDWBWIVNWDUVAUVNUUJUU TUVNQFUUMUUTUVNUUTUVMVOFZUVNWJFZUUSUVRAUUSUUJWJFZUVRDWJFUUSUVTUTUUJDWKWLZUU JWMSZWBZUVMWNZSWAWDUUSUUJQFAUUMDUUJWOZRZWPUVAUUNUUJUUJUEIZUVPKUVAMUUJUUJUVA WQUWFUWFUUSMUUJKLAUUMUUSUUJUWAWRRWSUUSUVPUWGNAUUMUUSUUJDUUJWTXARXBUUSUVPUVO KLAUUMUUSGUVNUUJGQFUUSXDPZUUSUVNUUSUVRUVSUWBUWDSWAZUWEUUSUUJUVIWCUUSGTJEZUV NUWHUWJQFUUSUWJUJQXCXEXFPUWIGUWJKLUUSGUJUWJKGUJXDXEXGVEXCXHPUUSTVOFZUVRTUVM KLUWJUVNKLUWKUUSXIPUWBUUSTDMWFIZUVMKUWLTMUEIZMWFITDUWMMWFXJXKTMXLXMXNUNUUSD UUJMDQFUUSXPPUWEUUSWQDUUJXQXOXRTUVMXSXTYAYBRYAUUTUVOUULNUUMUUTUVNUVMMUEIZOI ZUVOUULUUTUWNUUJUVNOUUSUWNUUJNZAUUSUVQUWPUVDUVQUUJYCFMYCFUWPUUJYGXMUUJMYDYE SWBZYHUUTUWNJEZUWOUULUUTUVRUWRUWONUWCUVMYFSUUTUWNUUJJUWQYIYJYJWDVHYKUVAUUOU VBUUTUUOUVBNUUMUUTUUNUUSUUNYCFAUUSUUNUVEYLZWBYMWDYNUVAUUPUVCUUSUUPUVCNAUUMU USUUPUULUUNOIZUVCUUSUVHUUPUWTNUVIUUJYFSUUSUULUUNUUSUULUVJYOUWSYPYRRYNYQYSYT $. $}