Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  chordthmlem Structured version   Visualization version   Unicode version

Theorem chordthmlem 23837
 Description: If M is the midpoint of AB and AQ = BQ, then QMB is a right angle. The proof uses ssscongptld 23830 to observe that, since AMQ and BMQ have equal sides, the angles QMB and QMA must be equal. Since they are supplementary, both must be right. (Contributed by David Moews, 28-Feb-2017.)
Hypotheses
Ref Expression
chordthmlem.angdef
chordthmlem.A
chordthmlem.B
chordthmlem.Q
chordthmlem.M
chordthmlem.ABequidistQ
chordthmlem.AneB
chordthmlem.QneM
Assertion
Ref Expression
chordthmlem
Distinct variable groups:   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)   (,)

Proof of Theorem chordthmlem
StepHypRef Expression
1 negpitopissre 23568 . . . . . 6
2 chordthmlem.angdef . . . . . . 7
3 chordthmlem.Q . . . . . . . 8
4 chordthmlem.M . . . . . . . . 9
5 chordthmlem.A . . . . . . . . . . 11
6 chordthmlem.B . . . . . . . . . . 11
75, 6addcld 9680 . . . . . . . . . 10
87halfcld 10880 . . . . . . . . 9
94, 8eqeltrd 2549 . . . . . . . 8
103, 9subcld 10005 . . . . . . 7
11 chordthmlem.QneM . . . . . . . 8
123, 9, 11subne0d 10014 . . . . . . 7
136, 9subcld 10005 . . . . . . 7
144oveq1d 6323 . . . . . . . . . . . . . 14
159times2d 10879 . . . . . . . . . . . . . 14
16 2cnd 10704 . . . . . . . . . . . . . . 15
17 2ne0 10724 . . . . . . . . . . . . . . . 16
1817a1i 11 . . . . . . . . . . . . . . 15
197, 16, 18divcan1d 10406 . . . . . . . . . . . . . 14
2014, 15, 193eqtr3d 2513 . . . . . . . . . . . . 13
21 chordthmlem.AneB . . . . . . . . . . . . . 14
225, 6, 6, 21addneintr2d 9859 . . . . . . . . . . . . 13
2320, 22eqnetrd 2710 . . . . . . . . . . . 12
2423neneqd 2648 . . . . . . . . . . 11
25 oveq12 6317 . . . . . . . . . . . 12
2625anidms 657 . . . . . . . . . . 11
2724, 26nsyl 125 . . . . . . . . . 10
2827neqned 2650 . . . . . . . . 9
2928necomd 2698 . . . . . . . 8
306, 9, 29subne0d 10014 . . . . . . 7
312, 10, 12, 13, 30angcld 23813 . . . . . 6
321, 31sseldi 3416 . . . . 5
3332recnd 9687 . . . 4
3433coscld 14262 . . 3
356, 9negsubdi2d 10021 . . . . . . 7
369, 9, 5, 6addsubeq4d 10056 . . . . . . . 8
3720, 36mpbid 215 . . . . . . 7
3835, 37eqtr4d 2508 . . . . . 6
3938oveq2d 6324 . . . . 5
4039fveq2d 5883 . . . 4
412, 10, 12, 13, 30cosangneg2d 23815 . . . 4
425, 5, 6, 21addneintrd 9858 . . . . . . . . . 10
4342, 20neeqtrrd 2717 . . . . . . . . 9
4443necomd 2698 . . . . . . . 8
4544neneqd 2648 . . . . . . 7
46 oveq12 6317 . . . . . . . 8
4746anidms 657 . . . . . . 7
4845, 47nsyl 125 . . . . . 6
4948neqned 2650 . . . . 5
50 eqidd 2472 . . . . 5
515, 9subcld 10005 . . . . . . 7
5251absnegd 13588 . . . . . 6
535, 9negsubdi2d 10021 . . . . . . 7
5453fveq2d 5883 . . . . . 6
5537fveq2d 5883 . . . . . 6
5652, 54, 553eqtr3d 2513 . . . . 5
57 chordthmlem.ABequidistQ . . . . 5
582, 3, 9, 5, 3, 9, 6, 11, 49, 11, 28, 50, 56, 57ssscongptld 23830 . . . 4
5940, 41, 583eqtr3rd 2514 . . 3