Metamath Proof Explorer

Theorem 2sqreulem4

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

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

Proof

Step Hyp Ref Expression
1 2sqreulem4.1 
 |-  ( ph <-> ( ps /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )
2 2sqreulem3 
 |-  ( ( a e. NN0 /\ ( b e. NN0 /\ c e. NN0 ) ) -> ( ( ( ps /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) /\ ( [. c / b ]. ps /\ ( ( a ^ 2 ) + ( c ^ 2 ) ) = P ) ) -> b = c ) )
3 2 ralrimivva 
 |-  ( a e. NN0 -> A. b e. NN0 A. c e. NN0 ( ( ( ps /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) /\ ( [. c / b ]. ps /\ ( ( a ^ 2 ) + ( c ^ 2 ) ) = P ) ) -> b = c ) )
4 1 rmobii 
 |-  ( E* b e. NN0 ph <-> E* b e. NN0 ( ps /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) )
5 nfcv 
 |-  F/_ b NN0
6 nfcv 
 |-  F/_ c NN0
7 nfsbc1v 
 |-  F/ b [. c / b ]. ps
8 nfv 
 |-  F/ b ( ( a ^ 2 ) + ( c ^ 2 ) ) = P
9 7 8 nfan 
 |-  F/ b ( [. c / b ]. ps /\ ( ( a ^ 2 ) + ( c ^ 2 ) ) = P )
10 sbceq1a 
 |-  ( b = c -> ( ps <-> [. c / b ]. ps ) )
11 oveq1 
 |-  ( b = c -> ( b ^ 2 ) = ( c ^ 2 ) )
12 11 oveq2d 
 |-  ( b = c -> ( ( a ^ 2 ) + ( b ^ 2 ) ) = ( ( a ^ 2 ) + ( c ^ 2 ) ) )
13 12 eqeq1d 
 |-  ( b = c -> ( ( ( a ^ 2 ) + ( b ^ 2 ) ) = P <-> ( ( a ^ 2 ) + ( c ^ 2 ) ) = P ) )
14 10 13 anbi12d 
 |-  ( b = c -> ( ( ps /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) <-> ( [. c / b ]. ps /\ ( ( a ^ 2 ) + ( c ^ 2 ) ) = P ) ) )
15 5 6 9 14 rmo4f 
 |-  ( E* b e. NN0 ( ps /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) <-> A. b e. NN0 A. c e. NN0 ( ( ( ps /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) /\ ( [. c / b ]. ps /\ ( ( a ^ 2 ) + ( c ^ 2 ) ) = P ) ) -> b = c ) )
16 4 15 bitri 
 |-  ( E* b e. NN0 ph <-> A. b e. NN0 A. c e. NN0 ( ( ( ps /\ ( ( a ^ 2 ) + ( b ^ 2 ) ) = P ) /\ ( [. c / b ]. ps /\ ( ( a ^ 2 ) + ( c ^ 2 ) ) = P ) ) -> b = c ) )
17 3 16 sylibr 
 |-  ( a e. NN0 -> E* b e. NN0 ph )
18 17 rgen 
 |-  A. a e. NN0 E* b e. NN0 ph