begin
theorem Th1:
:: deftheorem defines `1 EUCLID_5:def 1 :
:: deftheorem defines `2 EUCLID_5:def 2 :
:: deftheorem defines `3 EUCLID_5:def 3 :
theorem
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
for
x1,
y1,
z1,
x2,
y2,
z2 being
Real holds
|[x1,y1,z1]| + |[x2,y2,z2]| = |[(x1 + x2),(y1 + y2),(z1 + z2)]|
theorem Th7:
theorem Th8:
theorem
theorem Th10:
theorem
theorem Th12:
theorem Th13:
for
x1,
y1,
z1,
x2,
y2,
z2 being
Real holds
|[x1,y1,z1]| - |[x2,y2,z2]| = |[(x1 - x2),(y1 - y2),(z1 - z2)]|
:: deftheorem EUCLID_5:def 4 :
canceled;
:: deftheorem defines <X> EUCLID_5:def 5 :
theorem
theorem Th15:
for
x1,
y1,
z1,
x2,
y2,
z2 being
Real holds
|[x1,y1,z1]| <X> |[x2,y2,z2]| = |[((y1 * z2) - (z1 * y2)),((z1 * x2) - (x1 * z2)),((x1 * y2) - (y1 * x2))]|
theorem
theorem Th17:
theorem
theorem
theorem
theorem
theorem
theorem Th23:
theorem Th24:
theorem
theorem
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
:: deftheorem defines |{ EUCLID_5:def 6 :
theorem
theorem
theorem Th33:
theorem
theorem