### Abstract

This entry provides an analytic proof to Ptolemy's Theorem using polar form transformation and trigonometric identities. In this formalization, we use ideas from John Harrison's HOL Light formalization and the proof sketch on the Wikipedia entry of Ptolemy's Theorem. This theorem is the 95th theorem of the Top 100 Theorems list.

### License

BSD License

### Topics

- Mathematics/Geometry

### Session Ptolemys_Theorem

- Ptolemys_Theorem

## Cite

×

Ptolemys_Theorem-AFP

    @article{Ptolemys_Theorem-AFP,
      author  = {Lukas Bulwahn},
      title   = {Ptolemy's Theorem},
      journal = {Archive of Formal Proofs},
      month   = {August},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/Ptolemys_Theorem.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Aug 8, 2016 : Isabelle2016