Metamath Proof Explorer

Theorem ioomidp

Description: The midpoint is an element of the open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion ioomidp 
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( ( A + B ) / 2 ) e. ( A (,) B ) )

Proof

Step Hyp Ref Expression
1 rexr 
 |-  ( A e. RR -> A e. RR* )
2 1 3ad2ant1 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> A e. RR* )
3 rexr 
 |-  ( B e. RR -> B e. RR* )
4 3 3ad2ant2 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> B e. RR* )
5 readdcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
6 5 rehalfcld 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A + B ) / 2 ) e. RR )
7 6 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( ( A + B ) / 2 ) e. RR )
8 avglt1 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> A < ( ( A + B ) / 2 ) ) )
9 8 biimp3a 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> A < ( ( A + B ) / 2 ) )
10 avglt2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( ( A + B ) / 2 ) < B ) )
11 10 biimp3a 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( ( A + B ) / 2 ) < B )
12 2 4 7 9 11 eliood 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( ( A + B ) / 2 ) e. ( A (,) B ) )