今天看了一篇 勒让德 通过反证法证明 三角形内角和不大于180°的一篇文章
具体内容不赘述 想了解的一搜就能搜到

证明过程中用到了一个引理：
△ABC和△A'B’C’中  AB=A’B’  AC=A’C’  ∠A＞∠A’ 要证的结论是BC＞B’C’
文章中用了显然的写法 没做具体证明

这个结论确实很显然（余弦定理加余弦函数在 0-180°之间的单调性） 一眼可以得出结论
但仔细想好像不是那么回事
余弦定理 的证明依赖勾股定理
勾股定理的证明 是不是依赖于第五公设？（这个记不准了）
如果是的话那就涉嫌循环论证了
因为三角形内角和 180°跟第五公设是等价的 这个我很确定

我的问题是：
余弦定理或者勾股定理 在不用到第五公设（也就是三角形内角和180°）的前提下 是成立的么？
抑或如果不用余弦定理
那个引理有比较好的 在不需要第五公设这个结论的证明方式么？

用反证法证明 三角形内角和不大于180° 这个证明已经几百年了
我相信里面应该没有涉及用到第五公设循环论证的问题
谁能解答一下
或者帮忙找一下勒让德证明过程中是怎么处理这个引理的
--
修改:knup FROM 111.199.185.*
FROM 111.199.185.*

想到了一个方法
里面应该没有伪证或者用到了第五公设以及等价命题
因为刨了欧氏几何里的根基（平行公理以及推论）不能用
所以证明起来如履薄冰
到底有没有伪证不敢十分确定
大家仔细帮忙检查一下
我会写的非常详细

引理1：△ABC中∠B=∠C 求证AB=AC
证明：∵∠B=∠C ∠C=∠B BC=CB
∴△ABC≌△ACB
∴AB=AC
这里用到了全等三角形的ASA定理
这个定理的基石是“两条直线相交有且只有一个交点” 不涉及第五公设
如果从顶点做底边垂线或者角分线 去证是不行的
因为会用到内角和180°的结论（第五公设的等价命题）

引理2：△ABC中 AB=AC 求证∠B=∠C
证明：
∵AB=AC ∠A=∠A AC=AB
∴△ABC≌△ACB
∴∠B=∠C
这里用到了全等三角形的SAS定理
基石是两点之间有且只有一条线段

引理3：△ABC中 ∠B＞∠C 求证AC＞AB（大角对大边）
证明：在AC上取一点D 使得∠DBC=∠C
由引理1可知DB=DC
∴AC=AD+DC=AD+DB＞AB
这里用到了两点之间线段最短
跟第五公设没关系
这个两点之间线段最短的结论如果非要证需要路径积分 不是容易的事 就不写了

下面开始证明原命题：
已知△ABC与△DEF中 AB=DE，AC=DF，∠A＞∠D 求证BC＞EF
证明：不妨设AB=DE≤AC=DF（这一步设定很重要，否则后面会出现很麻烦无法解决的问题）
让A与D重合 B与E重合 即AB与DE重合 后面证明只保留A和B 删掉D和E的标识
且DF位于∠BAC内部（之所以用较小的边重合也是避免出现后面无法解决的问题，这个后面详细说）

以A为圆心AC为半径作圆 延长AB与此圆交于G点（若AB=AC 则B与G重合，不影响结论）
易知弧CG（不包含端点）与A点分别位于BC的两侧 F在此圆弧上
∴A和F分别位于BC两侧
∵AC=AF
由引理2 ∠AFC=∠ACF

∴∠BFC＞∠AFC=∠ACF＞∠BCF
在△BCF中 由引理3
BC＞BF
∵B和E已经重合
即BC＞EF
Q.E.D

btw：如果用AC和DF（较长边）重合 讨论E点的位置 则有可能会出现E点在△ABC内部的情况
这种情况没办法处理（因为会用到外角大于不相临内角这结论，这结论依赖三角形内角和180°，这就没办法处理了）

【 在 knup 的大作中提到: 】
: 就是附件里那句话“有两组对应边分别相等的两个三角形，夹角大的第三边大”这句话
: 谁知道 不需要第五公设（平行公理）以及等价命题的情况下证明的方法？
: [upload=1][/upload][upload=2][/upload]
: ...................
--
修改:knup FROM 111.199.185.*
FROM 111.199.185.*