AVL-tree insertion complexity proof

I tried to figure out the proof of insertion operation in AVL-tree is O(log n), but I do not know how. I also tried to find it somewhere on the Internet, but I could not find any good results. Do you guys have any ideas how do we proof that?

• Take a look at Section 6.2.3 (Balanced Trees) in Volume III (Sorting and Searching) of "The Art of Computer Programming" by Donald Knuth. – Steven Feb 9 at 17:48
• We start by proving that if an AVL tree has a path of length $h$ then the tree has at least $2^{h/2}$ nodes, see this site AVL tree height log n proof. – Hendrik Jan Feb 9 at 22:55

As an immediate consequence of this lemma, we can implement the dynamic-set operations SEARCH , MINIMUM , MAXIMUM , SUCCESSOR , and PREDECESSOR in $$O(\log n)$$ time on red-black trees, since each can run in $$O(h)$$ time on a binary search tree of height $$h$$ (as shown in Chapter 12) and any red-black tree on n nodes is a binary search tree with height $$O(\log n)$$.
Regarding a pure understanding of why the INSERTION is $$O(\log n)$$, check this implementation example. There you can clearly see that what makes an AVL differ from a standard BST are the rotations, that can be performed in constant time. With those you get a balanced tree, and with a balanced tree you get $$O(\log n)$$ INSERTION.