Metamath Proof Explorer


Theorem le2sqi

Description: The square function on nonnegative reals is monotonic. (Contributed by NM, 12-Sep-1999)

Ref Expression
Hypotheses resqcl.1 โŠข ๐ด โˆˆ โ„
lt2sq.2 โŠข ๐ต โˆˆ โ„
Assertion le2sqi ( ( 0 โ‰ค ๐ด โˆง 0 โ‰ค ๐ต ) โ†’ ( ๐ด โ‰ค ๐ต โ†” ( ๐ด โ†‘ 2 ) โ‰ค ( ๐ต โ†‘ 2 ) ) )

Proof

Step Hyp Ref Expression
1 resqcl.1 โŠข ๐ด โˆˆ โ„
2 lt2sq.2 โŠข ๐ต โˆˆ โ„
3 1 2 le2msqi โŠข ( ( 0 โ‰ค ๐ด โˆง 0 โ‰ค ๐ต ) โ†’ ( ๐ด โ‰ค ๐ต โ†” ( ๐ด ยท ๐ด ) โ‰ค ( ๐ต ยท ๐ต ) ) )
4 1 recni โŠข ๐ด โˆˆ โ„‚
5 4 sqvali โŠข ( ๐ด โ†‘ 2 ) = ( ๐ด ยท ๐ด )
6 2 recni โŠข ๐ต โˆˆ โ„‚
7 6 sqvali โŠข ( ๐ต โ†‘ 2 ) = ( ๐ต ยท ๐ต )
8 5 7 breq12i โŠข ( ( ๐ด โ†‘ 2 ) โ‰ค ( ๐ต โ†‘ 2 ) โ†” ( ๐ด ยท ๐ด ) โ‰ค ( ๐ต ยท ๐ต ) )
9 3 8 bitr4di โŠข ( ( 0 โ‰ค ๐ด โˆง 0 โ‰ค ๐ต ) โ†’ ( ๐ด โ‰ค ๐ต โ†” ( ๐ด โ†‘ 2 ) โ‰ค ( ๐ต โ†‘ 2 ) ) )