T1 triangle milieu 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é. -- T2 triangle milieu RESUME Dans un triangle, un segment qui joint les milieux de deux côtés mesure la moitié du 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 egal pr(2;QR) PN | le segment qui joint ces milieux mesure la moitié du troisième côté -- T3 triangle milieu RESUME Dans un triangle, si une droite passe par le milieu d'un côté et est parallèle à un deuxième côté, alors cette droite passe par le milieu du 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é appartient Q d1 | une droite passe par ce milieu para d1 (PN) | cette droite est parallèle au deuxième côté inter R d1 (PM) | cette droite coupe le troisième côté en un certain point ALORS milieu R M P | ce point est le milieu du troisième côté. -- TR1 triangle_rectangle RESUME Un triangle rectangle a deux côtés perpendiculaires. CONTEXTE SI tri_rect M N P ALORS perp (MN) (MP) -- TR2 triangle_rectangle RESUME Théorème de Pythagore SI tri_rect M N P ALORS egal ca(NP) so(ca(MN);ca(MP)) -- TR4 triangle_rectangle RESUME Dans un triangle rectangle, l'hypothénuse est deux fois plus longue que la médiane issue de l'angle droit SI tri_rect M N P milieu O N P ALORS egal NP pr(2;MO) -- TR4r triangle_rectangle RESUME Réciproque du T4 CONTEXTE Dans le triangle {M}{N}{P} SI milieu O N P egal NP pr(2;MO) ALORS tri_rect M N P -- TR5 triangle_rectangle cercle RESUME Dans un triangle rectangle, le milieu de l'hypothénuse est le centre du cercle circonscrit. SI tri_rect M N P milieu O N P cercle_circ c1 M N P ALORS centre O c1 -- TR6 triangle_rectangle cercle RESUME Dans un cercle, un triangle dont un des côtés est un diamètre et dont le troisième sommet appartient au cercle, est rectangle. SI cercle_diam c1 P Q appartient_cercle M c1 ALORS tri_rect M P Q perp (MP) (MQ) -- TR6r triangle_rectangle cercle RESUME Si un triangle est rectangle, alors le sommet de l'angle droit appartient au cercle de diamètre l'hypoténuse SI cercle_diam c1 P Q tri_rect M P Q ALORS appartient_cercle M c1 -- CC1 cercle RESUME Deux points d'un cercle sont équidistants du centre SI centre O c1 appartient_cercle M c1 appartient_cercle N c1 ALORS egal OM ON -- CC2 cercle RESUME Définition de la tangente à un cercle SI centre O c1 appartient_cercle M c1 appartient M d perp d OM ALORS tangente d c1 M -- CC3 cercle RESUME diamètre d'un cercle CONTEXTE {M} et {N} sont des points distincts SI centre O c1 appartient_cercle M c1 appartient_cercle N c1 aligne O M N ALORS cercle_diam c1 M N milieu O M N -- MDN1 médiane RESUME Caractérisation de la médiane CONTEXTE Dans le triangle {M}{N}{P} SI milieu O N P ALORS mediane (MO) M N P -- MDN2 médiane RESUME Le centre de gravité est situé au 2/3 d'une médiane CONTEXTE Dans le triangle {M}{N}{P} SI milieu O N P appartient Q (MO) egal MQ pr(qo(2;3);MO) ALORS gravite Q M N P -- MDN3 médiane RESUME Une médiane passe par le centre de gravité CONTEXTE Dans le triangle {M}{N}{P} SI gravite Q M N P ALORS mediane (MQ) M N P -- MDN4 médiane RESUME Les médianes sont concourantes en le centre de gravité. CONTEXTE Dans le triangle {M}{N}{P} SI mediane (MQ) M N P mediane (NR) M N P inter S (MQ) (NR) ALORS gravite S M N P -- MDT1 médiatrice RESUME La droite qui est perpendiculaire à un segment en son milieu est la médiatrice SI milieu O M N perp (OP) (MN) ALORS mediatrice (OP) M N -- MDT1r médiatrice RESUME la médiatrice est perpendiculaire à au segment en son milieu SI mediatrice d1 M N ALORS perp d1 (MN) passemilieu d1 M N -- MDT2 médiatrice RESUME Un point de la médiatrice est équidistant des extrémités du segment SI mediatrice d M N appartient P d ALORS egal PM PN -- MDT2r médiatrice RESUME Un point équidistant des extrémités du segment est sur la médiatrice SI egal PM PN ALORS appartient_mediatrice P M N -- MDT3 médiatrice RESUME la médiatrice est définie par deux points distincts CONTEXTE {P} et {Q} sont des points distincts SI appartient_mediatrice P M N appartient_mediatrice Q M N ALORS mediatrice (PQ) M N -- P1 parallélogramme RESUME Dans un parallélogramme, les diagonales se coupent en leur milieu. SI parallelogramme M N P Q | un parallélogramme, inter O (MP) (NQ) | ses diagonales sont sécantes en un point ALORS milieu O M P | ce point est le milieu d'une diagonale milieu O N Q | ce point est le milieu de l'autre diagonale. -- P1b parallélogramme RESUME Dans un parallélogramme, si un point est le milieu d'une diagonale, alors c'est aussi le milieu de l'autre diagonale. SI parallelogramme M N P Q | un parallélogramme, milieu O M P | un point milieu d'une diagonale ALORS milieu O N Q | ce point est le milieu de l'autre diagonale. -- P1r parallélogramme RESUME Un quadrilatère dont les diagonales se coupent en leur milieu est un parallèlogramme. CONTEXTE Dans le quadrilatère {M}{N}{P}{Q} | Dans un quadrilatère, SI milieu O M P | un point milieu d'une diagonale milieu O N Q | ce même point milieu d'une autre diagonale ALORS parallelogramme M N P Q | c'est un parallélogramme, -- P2 parallélogramme RESUME Dans un parallélogramme, les côtés opposés sont parallèles. SI parallelogramme M N P Q | un parallélogramme, ALORS para (MN) (PQ)| deux côtés opposés sont parallèles para (NP) (MQ) | les deux autres côtés opposés sont parallèles -- P2r parallélogramme RESUME Un quadrilatère dont les côtés opposés sont parallèles est un parallélogramme. CONTEXTE Dans le quadrilatère {M}{N}{P}{Q}| Dans un quadrilatère SI para (MN) (PQ)| deux côtés opposés parallèles para (NP) (MQ) | les deux autres côtés opposés parallèles ALORS parallelogramme M N P Q | c'est un parallélogramme, -- P3 parallélogramme RESUME Dans un parallélogramme, les côtés opposés sont de même longueur. SI parallelogramme M N P Q | un parallélogramme, ALORS egal MN PQ | deux côtés opposés sont de même longueur egal NP MQ | les deux autres côtés opposés sont de même longueur -- P3r parallélogramme RESUME Un quadrilatère non croisé dont les côtés opposés sont de même longueur est un parallélogramme. CONTEXTE Dans le quadrilatère non croisé {M}{N}{P}{Q}| Dans un quadrilatère non croisé SI egal MN PQ | deux côtés opposés de même longueur egal NP MQ | les deux autres côtés opposés de même longueur ALORS parallelogramme M N P Q | c'est un parallélogramme, -- 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. -- D2 droite RESUME Si deux droites sont perpendiculaires, toute droite perpendiculaire à l'une est parallèle à l'autre. SI perp d1 d2 | deux droites perpendiculaires perp d3 d1 | une droite perpendiculaire à l'une ALORS para d3 d2 | cette droite est parallèle à l'autre. -- D3 droite RESUME Si deux droites sont parallèles, toute droite parallèle à l'une est parallèle à l'autre. SI para d1 d2 | deux droites parallèles, para d3 d1 | une droite parallèle à l'une ALORS para d3 d2 | cette droite est parallèle à l'autre. -- D4 droite RESUME Deux droites perpendiculaires à une même troisème en un même point sont confondues. CONTEXTE Soient {O},{M},{N} et {P} des points distincts SI perp (OM) (OP) perp (ON) (OP) ALORS aligne O M N -- D5 droite RESUME Si MN+NP=MP alors M,N et P sont alignés dans cet ordre. CONTEXTE SI egal so(MN;NP) MP ALORS aligne_ordre M N P -- D6 droite RESUME Deux droites parallèles ayant un point commun sont confondues. SI para (MN) (MP) ALORS aligne M N P -- M1 milieu RESUME Le milieu partage le segment en deux parties de même longueur SI milieu O M N ALORS egal OM ON -- CA1 calcul_remplacement RESUME Deux quantités égales à une même troisième sont égales entre elles. SI egal X Y egal Z Y ALORS egal X Z -- SYM1 symétrie_centrale RESUME symétrique d'une droite, d'un segment SI sym_centrale P M O sym_centrale Q N O ALORS sym_centrale_drt (PQ) (MN) O sym_centrale_sgm P Q M N O -- SYM2 symétrie_centrale RESUME deux droites symétriques par rapport à un point sont parallèles SI sym_centrale_drt d1 d2 O ALORS para d1 d2 -- SYM3 symétrie_centrale RESUME deux segments symétriques par rapport à un point sont de même longueur SI sym_centrale_sgm P Q M N O ALORS egal PQ MN -- SYM4 symétrie_centrale angle RESUME symétrique d'un angle SI sym_centrale P X O sym_centrale Q Y O ALORS sym_centrale_agl O P Q O X Y O sym_centrale_agl O Q P O Y X O -- SYM5 symétrie_centrale angle RESUME deux angles symétriques par rapport à un point sont de même mesure SI sym_centrale_agl P Q R X Y Z O ALORS egal an(PQR) an(XYZ) -- SYM6 symétrie_centrale RESUME La symétrie centrale conserve l'alignement SI sym_centrale P X O sym_centrale Q Y O sym_centrale R Z O aligne X Y Z ALORS aligne P Q R -- SYM7 symétrie_centrale milieu RESUME milieu et symétrie centrale SI milieu O M N ALORS sym_centrale M N O -- ANG1 angle RESUME angles opposés par le sommet SI aligne_ordre M O N aligne_ordre Q O P ALORS egal an(MOP) an(QON) egal an(MOQ) an(NOP) -- ANG2 angle RESUME angles alternes-internes SI para_meme_sens M N P Q ALORS egal an(MNP) an(NPQ) egal an(MQP) an(NMQ) -- TI1 triangle_isocèle RESUME Un triangle qui a deux côtés de même longueur est isocèle SI egal MN MP ALORS tri_isoc M N P -- TI2 triangle_isocèle RESUME Un triangle isocèle à deux côtés de même longueur SI tri_isoc M N P ALORS egal MN NP -- TI3 triangle_isocèle RESUME Un triangle qui a deux angles de même mesure est isocèle SI egal an(MNP) an(MPN) ALORS tri_isoc M N P -- TI4 triangle_isocèle RESUME Un triangle isocèle à deux angles de même mesure SI tri_isoc M N P ALORS egal an(MNP) an(MPN) -- R1 rectangle RESUME un parallélogramme avec un angle droit est un rectangle SI parallelogramme M N P Q perp (MN) (MQ) ALORS rectangle M N P Q -- R2 rectangle RESUME un parallélogramme dont les diagonales ont même longueur est un rectangle SI parallelogramme M N P Q egal MP NQ ALORS rectangle M N P Q -- L1 losange RESUME un parallélogramme avec deux côtés consécutifs de même longueur est un losange SI parallelogramme M N P Q egal MN MQ ALORS losange M N P Q -- L2 losange RESUME un parallélogramme dont les diagonales sont perpendiculaires est un losange SI parallelogramme M N P Q perp (MP) (NQ) ALORS losange M N P Q -- CA1 carré RESUME Un quadrilatère à la fois losange et rectangle est un carré SI losange M N P Q rectangle M N P Q ALORS losange M N P Q