Theorem 2sqreunnlem2

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

	Ref	Expression
Hypothesis	2sqreulem4.1	|- ( ph <-> ( ps /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )
Assertion	2sqreunnlem2	|- A. a e. NN E* b e. NN ph

Proof

Step	Hyp	Ref	Expression
1		2sqreulem4.1	|- ( ph <-> ( ps /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )
2		nnssnn0	|- NN C_ NN0
3	1	2sqreulem4	|- A. a e. NN0 E* b e. NN0 ph
4		nfcv	|- F/_ b NN
5		nfcv	|- F/_ b NN0
6	4 5	ssrmof	|- ( NN C_ NN0 -> ( E* b e. NN0 ph -> E* b e. NN ph ) )
7	6	ralimdv	|- ( NN C_ NN0 -> ( A. a e. NN0 E* b e. NN0 ph -> A. a e. NN0 E* b e. NN ph ) )
8	2 3 7	mp2	|- A. a e. NN0 E* b e. NN ph
9		ssralv	|- ( NN C_ NN0 -> ( A. a e. NN0 E* b e. NN ph -> A. a e. NN E* b e. NN ph ) )
10	2 8 9	mp2	|- A. a e. NN E* b e. NN ph