Metamath Proof Explorer


Theorem 2sqreunnlem2

Description: Lemma 2 for 2sqreunn . (Contributed by AV, 25-Jun-2023)

Ref Expression
Hypothesis 2sqreulem4.1 φψa2+b2=P
Assertion 2sqreunnlem2 a*bφ

Proof

Step Hyp Ref Expression
1 2sqreulem4.1 φψa2+b2=P
2 nnssnn0 0
3 1 2sqreulem4 a0*b0φ
4 nfcv _b
5 nfcv _b0
6 4 5 ssrmof 0*b0φ*bφ
7 6 ralimdv 0a0*b0φa0*bφ
8 2 3 7 mp2 a0*bφ
9 ssralv 0a0*bφa*bφ
10 2 8 9 mp2 a*bφ