Metamath Proof Explorer

Theorem ge0xmulcl

Description: The nonnegative extended reals are closed under multiplication. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion ge0xmulcl ( ( ๐ด โˆˆ ( 0 [,] +โˆž ) โˆง ๐ต โˆˆ ( 0 [,] +โˆž ) ) โ†’ ( ๐ด ยทe ๐ต ) โˆˆ ( 0 [,] +โˆž ) )

Proof

Step Hyp Ref Expression
1 elxrge0 โŠข ( ๐ด โˆˆ ( 0 [,] +โˆž ) โ†” ( ๐ด โˆˆ โ„* โˆง 0 โ‰ค ๐ด ) )
2 elxrge0 โŠข ( ๐ต โˆˆ ( 0 [,] +โˆž ) โ†” ( ๐ต โˆˆ โ„* โˆง 0 โ‰ค ๐ต ) )
3 xmulcl โŠข ( ( ๐ด โˆˆ โ„* โˆง ๐ต โˆˆ โ„* ) โ†’ ( ๐ด ยทe ๐ต ) โˆˆ โ„* )
4 3 ad2ant2r โŠข ( ( ( ๐ด โˆˆ โ„* โˆง 0 โ‰ค ๐ด ) โˆง ( ๐ต โˆˆ โ„* โˆง 0 โ‰ค ๐ต ) ) โ†’ ( ๐ด ยทe ๐ต ) โˆˆ โ„* )
5 xmulge0 โŠข ( ( ( ๐ด โˆˆ โ„* โˆง 0 โ‰ค ๐ด ) โˆง ( ๐ต โˆˆ โ„* โˆง 0 โ‰ค ๐ต ) ) โ†’ 0 โ‰ค ( ๐ด ยทe ๐ต ) )
6 elxrge0 โŠข ( ( ๐ด ยทe ๐ต ) โˆˆ ( 0 [,] +โˆž ) โ†” ( ( ๐ด ยทe ๐ต ) โˆˆ โ„* โˆง 0 โ‰ค ( ๐ด ยทe ๐ต ) ) )
7 4 5 6 sylanbrc โŠข ( ( ( ๐ด โˆˆ โ„* โˆง 0 โ‰ค ๐ด ) โˆง ( ๐ต โˆˆ โ„* โˆง 0 โ‰ค ๐ต ) ) โ†’ ( ๐ด ยทe ๐ต ) โˆˆ ( 0 [,] +โˆž ) )
8 1 2 7 syl2anb โŠข ( ( ๐ด โˆˆ ( 0 [,] +โˆž ) โˆง ๐ต โˆˆ ( 0 [,] +โˆž ) ) โ†’ ( ๐ด ยทe ๐ต ) โˆˆ ( 0 [,] +โˆž ) )