【摘要】以數学的观点和方法求解和验证一次同余方程组的解和用Vlookup函数进行验证有一定的区别，本文介绍了一种以计算机辅助证明初等数论部分结论的方法.
【关键词】Vlookup函数；同余方程组；解
【资助项目】丽江师范高等专科学校特色课程《小学数学课堂教学技能训练》建设项目.
方程组（1）是一元一次同余方程组的最简形式，其求解对更加复杂的一元一次同余方程组具有重要意义.为了验证其解，构造两个此形式的方程组（2）和（3）.
x≡b1（modm1），x≡b2（modm2）. （1）
x≡7（mod10），x≡4（mod8）. （2）
x≡7（mod10），x≡5（mod8）. （3）
一、基本结论
定理 一次同余方程组（1）有解的充要条件是（m1，m2）|（b1-b2），且在有解条件下有唯一解.
二、用Vlookup验证定理结论
步骤1：令F列为自然序列，进行赋值F1=0，F2=1，F3=2，…，F100=99，F101=100.
步骤2：令A列为x≡7（mod10）的解，即A1=F1*10+7，A2=F2*10+7，其后进行自动填充.
步骤3：令B列为x≡4（mod8）的解，即A1=F1*8+4，A2=F2*8+4，其后进行自动填充.
步骤4：做Vlookup函数验证x≡7（mod10）和x≡4（mod8）是否有公共解，若有则可判定其解为方程组（2）的解，若无，可适当增大自然序列的最大值进行补充验证，再次验证后不能改变解的状态可猜测方程组无解.
令C1=Vlookup（B1，$A$1：$A$101，1，0），回车返回错误值，再次验证也无法得解.
步骤5：重复步骤3和4验证方程组（3）的解.其中，令B列为x≡5（mod8）的解.应用Vlookup函数验证可返回其解为37，77，117，157，197，…，797，….
步骤6：将上述解筛选出来并以数值形式粘贴至sheet2，计算可知77-37=117-77=157-117=…=797-757=…=40.
由此可猜想方程组（3）的解是以40为模的，而可以验证40=[10，8].
步骤7：猜测上述最小正整数解37的出处.37=7+10y0，37=5+8y1，易知y0=3，y1=4，而y≡3mod8（10，8） 和y≡4mod10（10，8）刚好是同余方程102y≡7-52mod8（10，8） 的唯一解.由此猜测（验证）一次同余方程组（1）的解为
x≡b1+m1y0（mod[m1，m2]），
其中y0为m1（m1，m2）y≡b1-b2（m1，m2）modm2（m1，m2）的解.
说明：① 上述结论可以推广到更多的方程上，也就可以得到孙子定理的结论了.② 应用计算机证明数论结论，只能选择一定的上限，虽说上限可以尽量大，但不能做到对所有数值均成立，故此证明从数学角度来说有一定缺陷.
三、实例演示
求解x≡3（mod7），x≡5（mod11）. 易知（7，11）=1，[11，7]=77，故只需求解7y≡-2（mod11），易得其解为y≡5（mod11），故原方程组的解为x≡3+7×5（mod[11，7]），即x≡38（mod77）.
【参考文献】
[1]王金明.初等数论[M].北京：人民教育出版社，2002：158-170.