Metamath Proof Explorer

Theorem iimulcl

Description: The unit interval is closed under multiplication. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion iimulcl 
|- ( ( A e. ( 0 [,] 1 ) /\ B e. ( 0 [,] 1 ) ) -> ( A x. B ) e. ( 0 [,] 1 ) )

Proof

Step Hyp Ref Expression
1 remulcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
2 1 3ad2antr1 
 |-  ( ( A e. RR /\ ( B e. RR /\ 0 <_ B /\ B <_ 1 ) ) -> ( A x. B ) e. RR )
3 2 3ad2antl1 
 |-  ( ( ( A e. RR /\ 0 <_ A /\ A <_ 1 ) /\ ( B e. RR /\ 0 <_ B /\ B <_ 1 ) ) -> ( A x. B ) e. RR )
4 mulge0 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> 0 <_ ( A x. B ) )
5 4 3adantr3 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B /\ B <_ 1 ) ) -> 0 <_ ( A x. B ) )
6 5 3adantl3 
 |-  ( ( ( A e. RR /\ 0 <_ A /\ A <_ 1 ) /\ ( B e. RR /\ 0 <_ B /\ B <_ 1 ) ) -> 0 <_ ( A x. B ) )
7 an6 
 |-  ( ( ( A e. RR /\ 0 <_ A /\ A <_ 1 ) /\ ( B e. RR /\ 0 <_ B /\ B <_ 1 ) ) <-> ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 0 <_ B ) /\ ( A <_ 1 /\ B <_ 1 ) ) )
8 1re 
 |-  1 e. RR
9 lemul12a 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ 1 e. RR ) /\ ( ( B e. RR /\ 0 <_ B ) /\ 1 e. RR ) ) -> ( ( A <_ 1 /\ B <_ 1 ) -> ( A x. B ) <_ ( 1 x. 1 ) ) )
10 8 9 mpanr2 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ 1 e. RR ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A <_ 1 /\ B <_ 1 ) -> ( A x. B ) <_ ( 1 x. 1 ) ) )
11 8 10 mpanl2 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A <_ 1 /\ B <_ 1 ) -> ( A x. B ) <_ ( 1 x. 1 ) ) )
12 11 an4s 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 0 <_ B ) ) -> ( ( A <_ 1 /\ B <_ 1 ) -> ( A x. B ) <_ ( 1 x. 1 ) ) )
13 12 3impia 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 0 <_ B ) /\ ( A <_ 1 /\ B <_ 1 ) ) -> ( A x. B ) <_ ( 1 x. 1 ) )
14 7 13 sylbi 
 |-  ( ( ( A e. RR /\ 0 <_ A /\ A <_ 1 ) /\ ( B e. RR /\ 0 <_ B /\ B <_ 1 ) ) -> ( A x. B ) <_ ( 1 x. 1 ) )
15 1t1e1 
 |-  ( 1 x. 1 ) = 1
16 14 15 breqtrdi 
 |-  ( ( ( A e. RR /\ 0 <_ A /\ A <_ 1 ) /\ ( B e. RR /\ 0 <_ B /\ B <_ 1 ) ) -> ( A x. B ) <_ 1 )
17 3 6 16 3jca 
 |-  ( ( ( A e. RR /\ 0 <_ A /\ A <_ 1 ) /\ ( B e. RR /\ 0 <_ B /\ B <_ 1 ) ) -> ( ( A x. B ) e. RR /\ 0 <_ ( A x. B ) /\ ( A x. B ) <_ 1 ) )
18 elicc01 
 |-  ( A e. ( 0 [,] 1 ) <-> ( A e. RR /\ 0 <_ A /\ A <_ 1 ) )
19 elicc01 
 |-  ( B e. ( 0 [,] 1 ) <-> ( B e. RR /\ 0 <_ B /\ B <_ 1 ) )
20 18 19 anbi12i 
 |-  ( ( A e. ( 0 [,] 1 ) /\ B e. ( 0 [,] 1 ) ) <-> ( ( A e. RR /\ 0 <_ A /\ A <_ 1 ) /\ ( B e. RR /\ 0 <_ B /\ B <_ 1 ) ) )
21 elicc01 
 |-  ( ( A x. B ) e. ( 0 [,] 1 ) <-> ( ( A x. B ) e. RR /\ 0 <_ ( A x. B ) /\ ( A x. B ) <_ 1 ) )
22 17 20 21 3imtr4i 
 |-  ( ( A e. ( 0 [,] 1 ) /\ B e. ( 0 [,] 1 ) ) -> ( A x. B ) e. ( 0 [,] 1 ) )