Metamath Proof Explorer


Theorem abs2sqlei

Description: The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007)

Ref Expression
Hypotheses abs2sqlei.1 A
abs2sqlei.2 B
Assertion abs2sqlei A B A 2 B 2

Proof

Step Hyp Ref Expression
1 abs2sqlei.1 A
2 abs2sqlei.2 B
3 1 absge0i 0 A
4 2 absge0i 0 B
5 1 abscli A
6 2 abscli B
7 5 6 le2sqi 0 A 0 B A B A 2 B 2
8 3 4 7 mp2an A B A 2 B 2