Metamath Proof Explorer

Theorem pellqrexplicit

Description: Condition for a calculated real to be a Pell solution. (Contributed by Stefan O'Rear, 19-Sep-2014)

Ref Expression
Assertion pellqrexplicit 
|- ( ( ( D e. ( NN \ []NN ) /\ A e. NN0 /\ B e. NN0 ) /\ ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) = 1 ) -> ( A + ( ( sqrt ` D ) x. B ) ) e. ( Pell1QR ` D ) )

Proof

Step Hyp Ref Expression
1 nn0re 
 |-  ( A e. NN0 -> A e. RR )
2 1 3ad2ant2 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. NN0 /\ B e. NN0 ) -> A e. RR )
3 eldifi 
 |-  ( D e. ( NN \ []NN ) -> D e. NN )
4 3 3ad2ant1 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. NN0 /\ B e. NN0 ) -> D e. NN )
5 4 nnrpd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. NN0 /\ B e. NN0 ) -> D e. RR+ )
6 5 rpsqrtcld 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. NN0 /\ B e. NN0 ) -> ( sqrt ` D ) e. RR+ )
7 6 rpred 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. NN0 /\ B e. NN0 ) -> ( sqrt ` D ) e. RR )
8 nn0re 
 |-  ( B e. NN0 -> B e. RR )
9 8 3ad2ant3 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. NN0 /\ B e. NN0 ) -> B e. RR )
10 7 9 remulcld 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. NN0 /\ B e. NN0 ) -> ( ( sqrt ` D ) x. B ) e. RR )
11 2 10 readdcld 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. NN0 /\ B e. NN0 ) -> ( A + ( ( sqrt ` D ) x. B ) ) e. RR )
12 11 adantr 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. NN0 /\ B e. NN0 ) /\ ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) = 1 ) -> ( A + ( ( sqrt ` D ) x. B ) ) e. RR )
13 simpl2 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. NN0 /\ B e. NN0 ) /\ ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) = 1 ) -> A e. NN0 )
14 simpl3 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. NN0 /\ B e. NN0 ) /\ ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) = 1 ) -> B e. NN0 )
15 eqidd 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. NN0 /\ B e. NN0 ) /\ ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) = 1 ) -> ( A + ( ( sqrt ` D ) x. B ) ) = ( A + ( ( sqrt ` D ) x. B ) ) )
16 simpr 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. NN0 /\ B e. NN0 ) /\ ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) = 1 ) -> ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) = 1 )
17 oveq1 
 |-  ( a = A -> ( a + ( ( sqrt ` D ) x. b ) ) = ( A + ( ( sqrt ` D ) x. b ) ) )
18 17 eqeq2d 
 |-  ( a = A -> ( ( A + ( ( sqrt ` D ) x. B ) ) = ( a + ( ( sqrt ` D ) x. b ) ) <-> ( A + ( ( sqrt ` D ) x. B ) ) = ( A + ( ( sqrt ` D ) x. b ) ) ) )
19 oveq1 
 |-  ( a = A -> ( a ^ 2 ) = ( A ^ 2 ) )
20 19 oveq1d 
 |-  ( a = A -> ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = ( ( A ^ 2 ) - ( D x. ( b ^ 2 ) ) ) )
21 20 eqeq1d 
 |-  ( a = A -> ( ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 <-> ( ( A ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) )
22 18 21 anbi12d 
 |-  ( a = A -> ( ( ( A + ( ( sqrt ` D ) x. B ) ) = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) <-> ( ( A + ( ( sqrt ` D ) x. B ) ) = ( A + ( ( sqrt ` D ) x. b ) ) /\ ( ( A ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) )
23 oveq2 
 |-  ( b = B -> ( ( sqrt ` D ) x. b ) = ( ( sqrt ` D ) x. B ) )
24 23 oveq2d 
 |-  ( b = B -> ( A + ( ( sqrt ` D ) x. b ) ) = ( A + ( ( sqrt ` D ) x. B ) ) )
25 24 eqeq2d 
 |-  ( b = B -> ( ( A + ( ( sqrt ` D ) x. B ) ) = ( A + ( ( sqrt ` D ) x. b ) ) <-> ( A + ( ( sqrt ` D ) x. B ) ) = ( A + ( ( sqrt ` D ) x. B ) ) ) )
26 oveq1 
 |-  ( b = B -> ( b ^ 2 ) = ( B ^ 2 ) )
27 26 oveq2d 
 |-  ( b = B -> ( D x. ( b ^ 2 ) ) = ( D x. ( B ^ 2 ) ) )
28 27 oveq2d 
 |-  ( b = B -> ( ( A ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) )
29 28 eqeq1d 
 |-  ( b = B -> ( ( ( A ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 <-> ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) = 1 ) )
30 25 29 anbi12d 
 |-  ( b = B -> ( ( ( A + ( ( sqrt ` D ) x. B ) ) = ( A + ( ( sqrt ` D ) x. b ) ) /\ ( ( A ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) <-> ( ( A + ( ( sqrt ` D ) x. B ) ) = ( A + ( ( sqrt ` D ) x. B ) ) /\ ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) = 1 ) ) )
31 22 30 rspc2ev 
 |-  ( ( A e. NN0 /\ B e. NN0 /\ ( ( A + ( ( sqrt ` D ) x. B ) ) = ( A + ( ( sqrt ` D ) x. B ) ) /\ ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) = 1 ) ) -> E. a e. NN0 E. b e. NN0 ( ( A + ( ( sqrt ` D ) x. B ) ) = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) )
32 13 14 15 16 31 syl112anc 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. NN0 /\ B e. NN0 ) /\ ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) = 1 ) -> E. a e. NN0 E. b e. NN0 ( ( A + ( ( sqrt ` D ) x. B ) ) = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) )
33 elpell1qr 
 |-  ( D e. ( NN \ []NN ) -> ( ( A + ( ( sqrt ` D ) x. B ) ) e. ( Pell1QR ` D ) <-> ( ( A + ( ( sqrt ` D ) x. B ) ) e. RR /\ E. a e. NN0 E. b e. NN0 ( ( A + ( ( sqrt ` D ) x. B ) ) = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) ) )
34 33 3ad2ant1 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. NN0 /\ B e. NN0 ) -> ( ( A + ( ( sqrt ` D ) x. B ) ) e. ( Pell1QR ` D ) <-> ( ( A + ( ( sqrt ` D ) x. B ) ) e. RR /\ E. a e. NN0 E. b e. NN0 ( ( A + ( ( sqrt ` D ) x. B ) ) = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) ) )
35 34 adantr 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. NN0 /\ B e. NN0 ) /\ ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) = 1 ) -> ( ( A + ( ( sqrt ` D ) x. B ) ) e. ( Pell1QR ` D ) <-> ( ( A + ( ( sqrt ` D ) x. B ) ) e. RR /\ E. a e. NN0 E. b e. NN0 ( ( A + ( ( sqrt ` D ) x. B ) ) = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) ) )
36 12 32 35 mpbir2and 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. NN0 /\ B e. NN0 ) /\ ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) = 1 ) -> ( A + ( ( sqrt ` D ) x. B ) ) e. ( Pell1QR ` D ) )