bb2

MODE
construction 1
implicite
bao
figure ggb cmd 0|1|5|2|4|6|40
ENONCE
(C) est un cercle de  centre I.
[AB] est un diamètre de (C).
Construire :
D est un point de (C).
E est un point du segment [AI].
(b) est la perpendiculaire à (AB) passant par E
F est l'intersection de (b) avec (AD)
G est l'intersection de (BD) et (EF)
Montrer que : 
(BF) et (AG) sont perpendiculaires
ALORS
perp (BF) (AG)

A =(-1.58, 3.82)
B =(1.18, 0.02)
I = MilieuCentre[ A , B ]
C = Cercle[ I , A ]

TR6
SI
cercle_diam c P Q
appartient_cercle M c
ALORS
perp (MP) (MQ)
--
HT1R hauteur
SI
hauteur d M N P
ALORS
perp d (NP)
--
HT1d hauteur
RESUME
Caractérisation de la hauteur
CONTEXTE
Dans le triangle {M}{N}{P}
SI
appartient Q (PN)
perp (MQ) (PQ)
ALORS
hauteur (MQ) M N P
--
HT1d hauteur
RESUME
Caractérisation de la hauteur
CONTEXTE
Dans le triangle {M}{N}{P}
SI
appartient Q (PN)
perp (MQ) (PQ)
ALORS
hauteur (MQ) M N P
--
HT2b hauteur
RESUME
Dans un triangle, l'intersection de deux hauteurs est l'orthocentre.
CONTEXTE
Dans le triangle {M}{N}{P}
SI
hauteur d1 M N P
hauteur d2 N P M
inter O d1 d2
ALORS
ortho O M N P
--
HT3 hauteur
RESUME
Dans un triangle, les trois hauteurs passent par l'orthocentre.
CONTEXTE
Dans le triangle {M}{N}{P}
SI
ortho O M N P
ALORS
hauteur (MO) M N P
hauteur (NO) N P M
hauteur (PO) P M N

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é.
--
T2 triangle
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
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
inter Q d (MN) | une droite coupe un côté du triangle
milieu Q M N | en un point qui est le milieu de ce côté
para d (PN) | cette droite est parallèle au deuxième côté
inter R d (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é.
--
T3bis triangle
EVIDENCE
EV1 EV2
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
passemilieu d M N | une droite qui passe par le milieu d'un côté
para d (PN) | et qui est parallèle à un deuxième côté
ALORS
passemilieu d M P | cette droite passe par le milieu du troisième côté.
--
T3ter triangle
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
para (QR) (PN) | une droite parallèle à un côté
milieu Q M N | qui passe par le milieu d'un deuxième côté.
inter S (QR) (PM) | cette droite coupe le troisième côté en un certain point
ALORS
milieu S 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))
--
TR2r triangle_rectangle
RESUME
Réciproque du théorème de Pythagore
CONTEXTE
Dans le triangle {M}{N}{P}
SI
egal ca(NP) so(ca(MN);ca(MP))
ALORS
tri_rect M N P
--
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
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 c M N P
ALORS
centre O c
--
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
--
HT1a hauteur
RESUME
Caractérisation de la hauteur
SI
triangle M N P | Dans un triangle
perp (MQ) (NP) | une droite issue d'un sommet et perpendiculaire au côté opposé
ALORS
hauteur (MQ) M N P | est la hauteur issue de ce sommet
--
HT1b hauteur
RESUME
Caractérisation de la hauteur
SI
triangle M N P | Dans un triangle
appartient M d | une droite passant par un sommet
perp d (NP) | tout en étant perpendiculaire au côté opposé
ALORS
hauteur d M N P | est la hauteur issue de ce sommet
--
HT1c hauteur
RESUME
Caractérisation de la hauteur
SI
triangle M N P | Dans un triangle
perp (MQ) (NP) | une droite issue d'un sommet et perpendiculaire au côté opposé
ALORS
hauteur (MQ) M N P | est la hauteur issue de ce sommet
--
HT2a hauteur
RESUME
Dans un triangle, l'intersection de deux hauteurs est l'orthocentre.
CONTEXTE
Dans le triangle {M}{N}{P} | Dans un triangle
SI
hauteur (MO) M N P
hauteur (NO) N M P
ALORS
ortho O M N P
--
HT2b hauteur
RESUME
Dans un triangle, l'intersection de deux hauteurs est l'orthocentre.
CONTEXTE
Dans le triangle {M}{N}{P} | Dans un triangle
SI
hauteur d1 M N P
hauteur d2 N P M
inter O d1 d2
ALORS
ortho O M N P
--
HT3 hauteur
RESUME
Dans un triangle, les trois hauteurs passent par l'orthocentre.
CONTEXTE
Dans le triangle {M}{N}{P} | Dans un triangle
SI
ortho O M N P
ALORS
hauteur (MO) M N P
hauteur (NO) N P M
hauteur (PO) P M N
--
MDT1 médiatrice
RESUME
Caractérisation de la médiatrice
SI
perp d (MN)
passemilieu d M N
ALORS
mediatrice d M N
--
MDT1r médiatrice
RESUME
Définition de la médiatrice
SI
mediatrice d M N
ALORS
perp d (MN)
passemilieu d M N
--
MDT2 médiatrice
RESUME
Un point de la médiatrice est équidistant des extrémités du segment.
SI
mediatrice (PQ) M N
ALORS
egal PM PN
egal QM QN
--
MDT2r médiatrice
RESUME
Une droite qui passe par deux points équidistants des extrémités d'un segment est la médiatrice de ce segment.
CONTEXTE
{P}, {Q}, {M} et {N} sont distincts
SI
egal PM PN
egal QM QN
ALORS
mediatrice (PQ) M N
--
MDT3 médiatrice
RESUME
Une droite qui passe par un point équidistant des extrémités d'un segment et est perpendiculaire  à ce segment est la médiatrice de ce segment.
CONTEXTE
{P}, {Q}, {M} et {N} sont distincts
SI
egal PM PN
perp (PQ) (MN)
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,
--
P4 parallélogramme
RESUME
lien entre l'aire d'un parallélogramme et l'aire d'un certain triangle.
CONTEXTE
SI
parallelogramme M N P Q
appartient R (PQ)
ALORS
egal ai(MNPQ) pr(2;ai(MNR))
--
L1 losagne
RESUME
Un losange a ses côtés de même longueur.
SI
losange M N P Q
ALORS
egal MN NP
egal NP PQ
egal PQ QM
egal QM MN
--
R1 rectangle
RESUME
Un rectangle a 4 angles droits.
SI
rectangle M N P Q
ALORS
perp (MQ) (MN)
perp (NM) (NP)
perp (PN) (PQ)
perp (QP) (QM)
--
R1bis rectangle
RESUME
Un rectangle a 4 angles qui mesurent 90°.
SI
rectangle M N P Q
ALORS
egal an(QMN) 90
egal an(MNP) 90
egal an(NPQ) 90
egal an(PQM) 90
--
A1 angle
RESUME
La mesure d'un angle formé par 2 angles adjacents est la somme de la mesure de ces 2 angles.
SI
angle_adj O M N P
ALORS
egal an(MOP) so(an(MON);an(NOP))
--
A2 angle
RESUME
Un angle droit mesure 90°.
SI
perp (OM) (ON)
ALORS
egal an(MON) 90
--
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 d1 d2
appartient M d1
appartient M d2
ALORS
confondu d1 d2
--
D6bis 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
--
S1 symétrie
RESUME
Dans une symétrie centrale, le centre de symétrie est le milieu du segment dont les extrémités sont un point et son image.
SI
sym_centrale N M O
ALORS
milieu O M N
--
TH1 Thalès
RESUME
théorème de Thalès
CONTEXTE
Dans le triangle {O}{M}{N}
SI
appartient Q (OM)
appartient R (ON)
para (QR) (MN)
ALORS
egal3 qo(OQ;OM) qo(OR;ON) qo(QR;MN) 
--
TH1bis Thalès
RESUME
théorème de Thalès à l'intérieur d'un triangle
CONTEXTE
Dans le triangle {O}{M}{N}
SI
appartient_segment Q O M
appartient_segment R O N
para (QR) (MN)
ALORS
egal3 qo(OQ;OM) qo(OR;ON) qo(QR;MN)
--
RP1 calcul_remplacement
RESUME
Remplacement dans une double égalité. La première égalité est l'expression principale. Les égalités suivantes servent à remplacer certains élèments de l'expression principale.
SI
egal3 X Y Z
egal m n
egal r s
egal p q
ALORS
egal3 U V W
--
RP2 calcul_remplacement
RESUME
Remplacement dans une égalité simple. La première égalité est l'expression principale. Les égalités suivantes servent à remplacer certains élèments de l'expression principale.
SI
egal X Y
egal m n
egal p q
egal r s
ALORS
egal U V
--
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

ression principale. Les égalités suivantes servent à remplacer certains élèments de l'expression principale. SI egal3 X Y Z egal m n egal r s egal p q ALORS egal3 U V W -- RP2 calcul_remplacement RESUME Remplacement dans une égalité simple. La première égalité est l'expression principale. Les égalités suivantes servent à remplacer certains élèments de l'expression principale. SI egal X Y egal m n egal p q egal r s ALORS egal U V -- 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