Path	Lines of Code
metamath/valid/aime-1983-p9.mm	9
metamath/valid/aime-1984-p15.mm	15
metamath/valid/aime-1984-p5.mm	11
metamath/valid/aime-1987-p8.mm	9
metamath/valid/aime-1988-p3.mm	9
metamath/valid/aime-1988-p4.mm	11
metamath/valid/aime-1990-p2.mm	7
metamath/valid/aime-1991-p1.mm	11
metamath/valid/aime-1991-p6.mm	9
metamath/valid/aime-1994-p4.mm	9
metamath/valid/aime-1996-p5.mm	21
metamath/valid/aime-1997-p12.mm	9
metamath/valid/aimeI-2000-p7.mm	16
metamath/valid/aimeI-2001-p3.mm	15
metamath/valid/aimeII-2020-p6.mm	13
metamath/valid/algebra-2complexrootspoly-xsqp49eqxp7itxpn7i.mm	20
metamath/valid/algebra-2rootsintpoly-am10tap11eqasqpam110.mm	19
metamath/valid/algebra-2rootspoly-apatapbeq2asqp2ab.mm	12
metamath/valid/algebra-2varlineareq-xpeeq7-2xpeeq3-eeq11-xeqn4.mm	31
metamath/valid/algebra-3rootspoly-amdtamctambeqnasqmbpctapcbtdpasqmbpctapcbta.mm	25
metamath/valid/algebra-amgm-faxinrrp2msqrt2geq2mxm1div2x.mm	7
metamath/valid/algebra-amgm-prod1toneq1-sum1tongeqn.mm	10
metamath/valid/algebra-amgm-sqrtxymulxmyeqxpy-xpygeq4.mm	11
metamath/valid/algebra-amgm-sumasqdivbsqgeqsumbdiva.mm	10
metamath/valid/algebra-apb4leq8ta4pb4.mm	9
metamath/valid/algebra-binomnegdiscrineq-10alt28asqp1.mm	23
metamath/valid/algebra-manipexpr-2erprsqpesqeqnrpnesq.mm	14
metamath/valid/algebra-manipexpr-apbeq2cceqiacpbceqm2.mm	16
metamath/valid/algebra-sqineq-2at2pclta2c2p41pc.mm	31
metamath/valid/algebra-sqineq-2unitcircatblt1.mm	10
metamath/valid/algebra-sqineq-36azm9asqle36zsq.mm	25
metamath/valid/algebra-sqineq-4bap1lt4bsqpap1sq.mm	34
metamath/valid/algebra-xmysqpymzsqpzmxsqeqxyz-xpypzp6dvdx3y3z3.mm	11
metamath/valid/amc12-2000-p11.mm	29
metamath/valid/amc12-2000-p15.mm	10
metamath/valid/amc12-2000-p5.mm	20
metamath/valid/amc12-2001-p2.mm	18
metamath/valid/amc12-2001-p9.mm	28
metamath/valid/amc12a-2002-p1.mm	12
metamath/valid/amc12a-2002-p12.mm	6
metamath/valid/amc12a-2002-p21.mm	11
metamath/valid/amc12a-2003-p1.mm	25
metamath/valid/amc12a-2003-p24.mm	31
metamath/valid/amc12a-2003-p25.mm	9
metamath/valid/amc12a-2008-p15.mm	9
metamath/valid/amc12a-2008-p2.mm	9
metamath/valid/amc12a-2008-p4.mm	7
metamath/valid/amc12a-2008-p8.mm	11
metamath/valid/amc12a-2009-p15.mm	9
metamath/valid/amc12a-2009-p2.mm	7
metamath/valid/amc12a-2009-p25.mm	11
metamath/valid/amc12a-2009-p5.mm	9
metamath/valid/amc12a-2009-p9.mm	14
metamath/valid/amc12a-2010-p10.mm	15
metamath/valid/amc12a-2010-p11.mm	11
metamath/valid/amc12a-2010-p22.mm	8
metamath/valid/amc12a-2011-p18.mm	10
metamath/valid/amc12a-2013-p7.mm	11
metamath/valid/amc12a-2013-p8.mm	13
metamath/valid/amc12a-2015-p10.mm	12
metamath/valid/amc12a-2016-p2.mm	9
metamath/valid/amc12a-2016-p3.mm	9
metamath/valid/amc12a-2017-p2.mm	12
metamath/valid/amc12a-2017-p7.mm	11
metamath/valid/amc12a-2019-p21.mm	9
metamath/valid/amc12a-2019-p9.mm	11
metamath/valid/amc12a-2020-p13.mm	16
metamath/valid/amc12a-2020-p22.mm	8
metamath/valid/amc12a-2021-p7.mm	9
metamath/valid/amc12b-2002-p11.mm	13
metamath/valid/amc12b-2002-p3.mm	34
metamath/valid/amc12b-2002-p6.mm	12
metamath/valid/amc12b-2003-p17.mm	27
metamath/valid/amc12b-2003-p6.mm	43
metamath/valid/amc12b-2003-p9.mm	36
metamath/valid/amc12b-2004-p3.mm	53
metamath/valid/amc12b-2020-p5.mm	11
metamath/valid/amc12b-2021-p21.mm	8
metamath/valid/imo-1961-p1.mm	18
metamath/valid/imo-1962-p4.mm	9
metamath/valid/imo-1964-p1-1.mm	9
metamath/valid/imo-1964-p1-2.mm	8
metamath/valid/imo-1965-p1.mm	12
metamath/valid/imo-1966-p4.mm	10
metamath/valid/imo-1966-p5.mm	19
metamath/valid/imo-1967-p3.mm	13
metamath/valid/imo-1973-p3.mm	10
metamath/valid/imo-1974-p5.mm	13
metamath/valid/imo-1977-p5.mm	14
metamath/valid/imo-1978-p5.mm	9
metamath/valid/imo-1979-p1.mm	10
metamath/valid/imo-1984-p2.mm	13
metamath/valid/imo-1987-p4.mm	8
metamath/valid/imo-1987-p6.mm	12
metamath/valid/imo-1988-p6.mm	10
metamath/valid/imo-1990-p3.mm	9
metamath/valid/imo-1993-p5.mm	7
metamath/valid/imo-2006-p6.mm	10
metamath/valid/induction-divisibility-3div2tooddnp1.mm	32
metamath/valid/induction-divisibility-3divnto3m2n.mm	43
metamath/valid/induction-divisibility-9div10tonm1.mm	25
metamath/valid/induction-ineq-nsqlefactn.mm	37
metamath/valid/induction-seq-mul2pnp1.mm	51
metamath/valid/induction-sum-1oktkp1.mm	40
metamath/valid/induction-sum-odd.mm	28
metamath/valid/induction-sum2kp1npqsqm1.mm	33
metamath/valid/mathd-algebra-10.mm	7
metamath/valid/mathd-algebra-101.mm	9
metamath/valid/mathd-algebra-104.mm	9
metamath/valid/mathd-algebra-109.mm	11
metamath/valid/mathd-algebra-11.mm	12
metamath/valid/mathd-algebra-110.mm	9
metamath/valid/mathd-algebra-116.mm	10
metamath/valid/mathd-algebra-119.mm	11
metamath/valid/mathd-algebra-123.mm	11
metamath/valid/mathd-algebra-126.mm	11
metamath/valid/mathd-algebra-13.mm	10
metamath/valid/mathd-algebra-131.mm	13
metamath/valid/mathd-algebra-132.mm	11
metamath/valid/mathd-algebra-140.mm	12
metamath/valid/mathd-algebra-144.mm	15
metamath/valid/mathd-algebra-149.mm	7
metamath/valid/mathd-algebra-15.mm	8
metamath/valid/mathd-algebra-151.mm	28
metamath/valid/mathd-algebra-159.mm	34
metamath/valid/mathd-algebra-181.mm	10
metamath/valid/mathd-algebra-182.mm	8
metamath/valid/mathd-algebra-185.mm	8
metamath/valid/mathd-algebra-190.mm	7
metamath/valid/mathd-algebra-192.mm	23
metamath/valid/mathd-algebra-206.mm	13
metamath/valid/mathd-algebra-214.mm	10
metamath/valid/mathd-algebra-22.mm	7
metamath/valid/mathd-algebra-224.mm	7
metamath/valid/mathd-algebra-234.mm	9
metamath/valid/mathd-algebra-245.mm	36
metamath/valid/mathd-algebra-247.mm	18
metamath/valid/mathd-algebra-251.mm	14
metamath/valid/mathd-algebra-267.mm	11
metamath/valid/mathd-algebra-28.mm	10
metamath/valid/mathd-algebra-282.mm	10
metamath/valid/mathd-algebra-31.mm	40
metamath/valid/mathd-algebra-323.mm	9
metamath/valid/mathd-algebra-327.mm	9
metamath/valid/mathd-algebra-35.mm	9
metamath/valid/mathd-algebra-37.mm	11
metamath/valid/mathd-algebra-393.mm	7
metamath/valid/mathd-algebra-405.mm	9
metamath/valid/mathd-algebra-410.mm	10
metamath/valid/mathd-algebra-421.mm	16
metamath/valid/mathd-algebra-422.mm	5
metamath/valid/mathd-algebra-43.mm	12
metamath/valid/mathd-algebra-433.mm	8
metamath/valid/mathd-algebra-437.mm	14
metamath/valid/mathd-algebra-451.mm	5
metamath/valid/mathd-algebra-455.mm	17
metamath/valid/mathd-algebra-462.mm	7
metamath/valid/mathd-algebra-48.mm	9
metamath/valid/mathd-algebra-480.mm	12
metamath/valid/mathd-algebra-482.mm	14
metamath/valid/mathd-algebra-493.mm	8
metamath/valid/mathd-algebra-509.mm	7
metamath/valid/mathd-algebra-51.mm	11
metamath/valid/mathd-algebra-510.mm	11
metamath/valid/mathd-algebra-536.mm	7
metamath/valid/mathd-algebra-547.mm	9
metamath/valid/mathd-algebra-55.mm	9
metamath/valid/mathd-algebra-568.mm	8
metamath/valid/mathd-algebra-59.mm	9
metamath/valid/mathd-algebra-616.mm	9
metamath/valid/mathd-algebra-67.mm	9
metamath/valid/mathd-algebra-69.mm	11
metamath/valid/mathd-algebra-73.mm	13
metamath/valid/mathd-algebra-77.mm	12
metamath/valid/mathd-algebra-89.mm	8
metamath/valid/mathd-algebra-96.mm	14
metamath/valid/mathd-numbertheory-101.mm	7
metamath/valid/mathd-numbertheory-102.mm	7
metamath/valid/mathd-numbertheory-109.mm	8
metamath/valid/mathd-numbertheory-110.mm	12
metamath/valid/mathd-numbertheory-126.mm	12
metamath/valid/mathd-numbertheory-13.mm	14
metamath/valid/mathd-numbertheory-132.mm	7
metamath/valid/mathd-numbertheory-136.mm	9
metamath/valid/mathd-numbertheory-149.mm	7
metamath/valid/mathd-numbertheory-155.mm	7
metamath/valid/mathd-numbertheory-156.mm	8
metamath/valid/mathd-numbertheory-169.mm	7
metamath/valid/mathd-numbertheory-188.mm	14
metamath/valid/mathd-numbertheory-198.mm	7
metamath/valid/mathd-numbertheory-200.mm	7
metamath/valid/mathd-numbertheory-202.mm	7
metamath/valid/mathd-numbertheory-211.mm	8
metamath/valid/mathd-numbertheory-22.mm	10
metamath/valid/mathd-numbertheory-221.mm	7
metamath/valid/mathd-numbertheory-232.mm	16
metamath/valid/mathd-numbertheory-236.mm	7
metamath/valid/mathd-numbertheory-24.mm	7
metamath/valid/mathd-numbertheory-252.mm	7
metamath/valid/mathd-numbertheory-257.mm	9
metamath/valid/mathd-numbertheory-269.mm	7
metamath/valid/mathd-numbertheory-284.mm	10
metamath/valid/mathd-numbertheory-30.mm	7
metamath/valid/mathd-numbertheory-301.mm	8
metamath/valid/mathd-numbertheory-303.mm	7
metamath/valid/mathd-numbertheory-32.mm	7
metamath/valid/mathd-numbertheory-326.mm	9
metamath/valid/mathd-numbertheory-33.mm	10
metamath/valid/mathd-numbertheory-335.mm	9
metamath/valid/mathd-numbertheory-35.mm	7
metamath/valid/mathd-numbertheory-37.mm	7
metamath/valid/mathd-numbertheory-370.mm	9
metamath/valid/mathd-numbertheory-403.mm	7
metamath/valid/mathd-numbertheory-405.mm	17
metamath/valid/mathd-numbertheory-412.mm	11
metamath/valid/mathd-numbertheory-42.mm	14
metamath/valid/mathd-numbertheory-43.mm	10
metamath/valid/mathd-numbertheory-45.mm	7
metamath/valid/mathd-numbertheory-458.mm	9
metamath/valid/mathd-numbertheory-461.mm	8
metamath/valid/mathd-numbertheory-466.mm	7
metamath/valid/mathd-numbertheory-48.mm	10
metamath/valid/mathd-numbertheory-530.mm	11
metamath/valid/mathd-numbertheory-543.mm	7
metamath/valid/mathd-numbertheory-629.mm	9
metamath/valid/mathd-numbertheory-64.mm	10
metamath/valid/mathd-numbertheory-640.mm	7
metamath/valid/mathd-numbertheory-668.mm	16
metamath/valid/mathd-numbertheory-690.mm	12
metamath/valid/mathd-numbertheory-709.mm	10
metamath/valid/mathd-numbertheory-739.mm	7
metamath/valid/mathd-numbertheory-780.mm	13
metamath/valid/mathd-numbertheory-81.mm	7
metamath/valid/mathd-numbertheory-84.mm	7
metamath/valid/mathd-numbertheory-92.mm	9
metamath/valid/mathd-numbertheory-961.mm	7
metamath/valid/numbertheory-2dvd4expn.mm	9
metamath/valid/numbertheory-aneqprodakp4-anmsqrtanp1eq2.mm	11
metamath/valid/numbertheory-nckeqnm1ckpnm1ckm1.mm	10
metamath/valid/numbertheory-prmdvsneqnsqmodpeq0.mm	76
metamath/valid/numbertheory-sqmod3in01d.mm	8
metamath/valid/numbertheory-sqmod4in01d.mm	37
metamath/valid/numbertheory-sumkmulnckeqnmul2pownm1.mm	8
metamath/valid/numbertheory-xsqpysqintdenomeq.mm	46