Metamath Proof Explorer


Theorem lt2sq

Description: The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 24-Feb-2006)

Ref Expression
Assertion lt2sq ( ( ( ๐ด โˆˆ โ„ โˆง 0 โ‰ค ๐ด ) โˆง ( ๐ต โˆˆ โ„ โˆง 0 โ‰ค ๐ต ) ) โ†’ ( ๐ด < ๐ต โ†” ( ๐ด โ†‘ 2 ) < ( ๐ต โ†‘ 2 ) ) )

Proof

Step Hyp Ref Expression
1 lt2msq โŠข ( ( ( ๐ด โˆˆ โ„ โˆง 0 โ‰ค ๐ด ) โˆง ( ๐ต โˆˆ โ„ โˆง 0 โ‰ค ๐ต ) ) โ†’ ( ๐ด < ๐ต โ†” ( ๐ด ยท ๐ด ) < ( ๐ต ยท ๐ต ) ) )
2 recn โŠข ( ๐ด โˆˆ โ„ โ†’ ๐ด โˆˆ โ„‚ )
3 recn โŠข ( ๐ต โˆˆ โ„ โ†’ ๐ต โˆˆ โ„‚ )
4 sqval โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ๐ด โ†‘ 2 ) = ( ๐ด ยท ๐ด ) )
5 sqval โŠข ( ๐ต โˆˆ โ„‚ โ†’ ( ๐ต โ†‘ 2 ) = ( ๐ต ยท ๐ต ) )
6 4 5 breqan12d โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โ†’ ( ( ๐ด โ†‘ 2 ) < ( ๐ต โ†‘ 2 ) โ†” ( ๐ด ยท ๐ด ) < ( ๐ต ยท ๐ต ) ) )
7 2 3 6 syl2an โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ ( ( ๐ด โ†‘ 2 ) < ( ๐ต โ†‘ 2 ) โ†” ( ๐ด ยท ๐ด ) < ( ๐ต ยท ๐ต ) ) )
8 7 ad2ant2r โŠข ( ( ( ๐ด โˆˆ โ„ โˆง 0 โ‰ค ๐ด ) โˆง ( ๐ต โˆˆ โ„ โˆง 0 โ‰ค ๐ต ) ) โ†’ ( ( ๐ด โ†‘ 2 ) < ( ๐ต โ†‘ 2 ) โ†” ( ๐ด ยท ๐ด ) < ( ๐ต ยท ๐ต ) ) )
9 1 8 bitr4d โŠข ( ( ( ๐ด โˆˆ โ„ โˆง 0 โ‰ค ๐ด ) โˆง ( ๐ต โˆˆ โ„ โˆง 0 โ‰ค ๐ต ) ) โ†’ ( ๐ด < ๐ต โ†” ( ๐ด โ†‘ 2 ) < ( ๐ต โ†‘ 2 ) ) )