HT2a hauteur
RESUME
Dans un triangle, l'intersection de deux hauteurs est l'orthocentre.
CONTEXTE
Dans le triangle {M}{N}{P}
SI
hauteur (MO) M N P
hauteur (NO) N M P
ALORS
ortho O M N P
--
HT1a hauteur
RESUME
Caractérisation de la hauteur
SI
triangle M N P | un triangle
perp (MQ) (NP) | une droite issue d'un sommet et perpendiculaire au côté opposé
ALORS
hauteur (MQ) M N P | cette droite est la hauteur issue de ce sommet
--
HT1b hauteur
RESUME
Caractérisation de la hauteur
SI
triangle M N P | un triangle
perp (MQ) (NP) | une droite issue d'un sommet et perpendiculaire au côté opposé
ALORS
hauteur (MQ) M N P | cette droite est la hauteur issue de ce sommet
--
TR1 triangle_rectangle
RESUME
Un triangle rectangle a deux côtés perpendiculaires.
CONTEXTE
SI
tri_rect M N P
ALORS
perp (MN) (MP)
--
T1 triangle
RESUME
Dans un triangle, une droite qui passe par les milieux de deux côtés est parallèle au troisième côté.
CONTEXTE
Dans le triangle {M}{N}{P} |  Dans un triangle,
SI
milieu Q M N | le milieu d'un côté
milieu R M P | le milieu d'un autre côté
ALORS
para (QR) (PN) | la droite qui passe par ces milieux est parallèle au troisième côté.
--
D1 droite
RESUME
Si deux droites sont parallèles, toute droite perpendiculaire à l'une est perpendiculaire à l'autre.
SI
para d1 d2 | deux droites parallèles
perp d3 d1 | une droite perpendiculaire à l'une
ALORS
perp d3 d2 | cette droite est perpendiculaire à l'autre.
--
HT4 hauteur
RESUME
Dans un triangle, une droite passant par l'orthocentre et un sommet est perpendiculaire au côté opposé.
SI
ortho O M N P
ALORS
perp (OM) (NP)
perp (ON) (NP)
perp (OP) (MN)
@options;
@figure;
  A = point( -5.86 , -1.86 );
  B = point( 4.05 , -2.64 );
  sAB = segment( A , B );
  dAC = perpendiculaire( A , sAB )  { i };
  C = pointsur( dAC , 6.48 );
  sBC = segment( B , C );
  dAH = perpendiculaire( A , sBC ) { i };
  H = intersection( sBC , dAH );
  sAH= segment (A,H);
  I = milieu( H , B );
  J = milieu( A , H );
  dCJ = droite( C , J );
  dAI = droite( A , I );
  sAC = segment( A , C );
MODE
SI
tri_rect A B C
appartient_segment H B C
milieu J A H
milieu I B H
perp (AJ) (CI)
triangle A H C
triangle A I C
triangle A H B
ALORS
perp (AI) (CJ)