Definition Per

Per := fun A B C => exists C', is_midpoint B C C' /\ Cong A C A C'

Sorry, the GeoGebra Applet could not be started. Please make sure that Java 1.4.2 (or later) is installed and active in your browser (Click here to install Java now)

l8_2 (Per symmetry)

forall A B C, Per A B C → Per C B A

l8_3

forall A B C A', Per A B C → A ≠ B → Col B A A' → Per A' B C

Sorry, the GeoGebra Applet could not be started. Please make sure that Java 1.4.2 (or later) is installed and active in your browser (Click here to install Java now)

l8_4

forall A B C C', Per A B C → is_midpoint B C C' → Per A B C'

Sorry, the GeoGebra Applet could not be started. Please make sure that Java 1.4.2 (or later) is installed and active in your browser (Click here to install Java now)

l8_5

forall A B, Per A B B

l8_6

forall A B C A', Per A B C → Per A' B C → Bet A C A' → B = C

Sorry, the GeoGebra Applet could not be started. Please make sure that Java 1.4.2 (or later) is installed and active in your browser (Click here to install Java now)

l8_7

forall A B C, Per A B C → Per A C B → B = C

l8_8

forall A B, Per A B A → A = B

l8_9

forall A B C, Per A B C → Col A B C → A = B \/ C = B

l8_10

forall A B C A' B' C', Per A B C → Cong_3 A B C A' B' C' → Per A' B' C'

Sorry, the GeoGebra Applet could not be started. Please make sure that Java 1.4.2 (or later) is installed and active in your browser (Click here to install Java now)

Definition Perp_in

Perp_in := fun X A B C D =>
A ≠ B /\ C ≠D /\ Col X A B /\ Col X C D /\ (forall U V, Col U A B → Col V C D → Per U X V)

Sorry, the GeoGebra Applet could not be started. Please make sure that Java 1.4.2 (or later) is installed and active in your browser (Click here to install Java now)

Definition Perp

Perp := fun A B C D => exists X, Perp_in X A B C D

Sorry, the GeoGebra Applet could not be started. Please make sure that Java 1.4.2 (or later) is installed and active in your browser (Click here to install Java now)

l8_12 (Perp_in symmetry)

forall A B C D X, Perp_in X A B C D → Perp_in X C D A B

l8_13_2

forall A B C D X,
A ≠ B → C ≠ D → Col X A B → Col X C D →
(exists U, exists V, Col U A B /\ Col V C D /\ U ≠ X /\ V ≠ X /\ Per U X V) → Perp_in X A B C D.

Sorry, the GeoGebra Applet could not be started. Please make sure that Java 1.4.2 (or later) is installed and active in your browser (Click here to install Java now)

l8_14_1 (Perp not reflexive)

forall A B, ~ Perp A B A B

l8_14_2_1a (Perp_in → Perp)

forall X A B C D, Perp_in X A B C D → Perp A B C D

l8_14_2_1b

forall X A B C D Y, Perp_in X A B C D → Col Y A B → Col Y C D → X=Y

Sorry, the GeoGebra Applet could not be started. Please make sure that Java 1.4.2 (or later) is installed and active in your browser (Click here to install Java now)

l8_14_2_1b_bis

forall A B C D X, Perp A B C D → Col X A B → Col X C D → Perp_in X A B C D

l8_14_2_2

forall X A B C D, Perp A B C D → (forall Y, Col Y A B → Col Y C D → X = Y) → Perp_in X A B C D

l8_14_3 : Perp_in unicity

forall A B C D X Y, Perp_in X A B C D → Perp_in Y A B C D → X = Y

l8_15_1 (Perp_in → Perp)

forall A B C X, A ≠ B → Col A B X → Perp A B C X → Perp_in X A B C X

l8_15_2 : Perp → Perp_in

forall A B C X, A<>B → Col A B X → Perp_in X A B C X → Perp A B C X

l8_16_1

forall A B C U X, A ≠ B → Col A B X → Col A B U → U<>X → Perp A B C X
→ ~ Col A B C /\ Per C X U

Sorry, the GeoGebra Applet could not be started. Please make sure that Java 1.4.2 (or later) is installed and active in your browser (Click here to install Java now)

l8_16_2

forall A B C U X,
A<>B → Col A B X → Col A B U → U<>X → ~ Col A B C → Per C X U → Perp A B C X

Sorry, the GeoGebra Applet could not be started. Please make sure that Java 1.4.2 (or later) is installed and active in your browser (Click here to install Java now)

l8_18_unicity

forall A B C X Y,
~ Col A B C → Col A B X → Perp A B C X → Col A B Y → Perp A B C Y → X = Y

Sorry, the GeoGebra Applet could not be started. Please make sure that Java 1.4.2 (or later) is installed and active in your browser (Click here to install Java now)

l8_18_existence

forall A B C, ~ Col A B C → exists X, Col A B X /\ Perp A B C X

Sorry, the GeoGebra Applet could not be started. Please make sure that Java 1.4.2 (or later) is installed and active in your browser (Click here to install Java now)

l8_20_1

forall A B C C' D P,
Per A B C → is_midpoint P C' D → is_midpoint A C' C → is_midpoint B D C → Per B A P

Sorry, the GeoGebra Applet could not be started. Please make sure that Java 1.4.2 (or later) is installed and active in your browser (Click here to install Java now)

l8_20_2

forall A B C C' D P,
Per A B C → is_midpoint P C' D → is_midpoint A C' C → is_midpoint B D C → B ≠ C → A ≠ P

l8_21

forall A B C, A ≠ B → exists P, exists T, Perp A B P A /\ Col A B T /\ Bet C T P

Sorry, the GeoGebra Applet could not be started. Please make sure that Java 1.4.2 (or later) is installed and active in your browser (Click here to install Java now)

perp_symmetry

forall A B C D, Perp A B C D → Perp C D A B

perp_commutativity

forall A B C D, Perp A B C D → Perp B A D C

perp_left_commutativity

forall A B C D, Perp A B C D → Perp B A C D

perp_right_commutativity

forall A B C D, Perp A B C D → Perp A B D C

perp_in_left_commutativity

forall A B C D X, Perp_in X A B C D → Perp_in X B A C D

perp_in_right_commutativity

forall A B C D X, Perp_in X A B C D → Perp_in X A B D C

perp_in_commutativity

forall A B C D X, Perp_in X A B C D → Perp_in X B A D C

perp_in_symmetry

forall A B C D X, Perp_in X A B C D → Perp_in X C D A B

perp_per_1

forall A B C, A<>B → Perp A B C A → Per B A C

perp_per_2

forall A B C, A<>B → Perp A B A C → Per B A C

perp_col

forall A B C D E, A ≠ E → Perp A B C D → Col A B E → Perp A E C D

perp_not_eq_1

forall A B C D, Perp A B C D → A ≠ B

perp_not_eq_2

forall A B C D, Perp A B C D → C ≠ D

perp_perp_in

forall A B C, Perp A B C A → Perp_in A A B C A

mid_point_existence

forall A B, exists X, is_midpoint X A B

l8_22

forall A B P R X ,
A ≠ B → A ≠ P → Per B A P → Per A B R → Cong A P B R → Bet A X B → Bet P X R →
Cong A R P B /\ is_midpoint X A B /\ is_midpoint X P R

Sorry, the GeoGebra Applet could not be started. Please make sure that Java 1.4.2 (or later) is installed and active in your browser (Click here to install Java now)