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 ) )