Metamath Proof Explorer

Theorem pell1234qrdich

Description: A general Pell solution is either a positive solution, or its negation is. (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion pell1234qrdich 
|- ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) -> ( A e. ( Pell14QR ` D ) \/ -u A e. ( Pell14QR ` D ) ) )

Proof

Step Hyp Ref Expression
1 elpell1234qr 
 |-  ( D e. ( NN \ []NN ) -> ( A e. ( Pell1234QR ` D ) <-> ( A e. RR /\ E. a e. ZZ E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) ) )
2 simp-4r 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ a e. NN0 ) /\ E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> A e. RR )
3 oveq1 
 |-  ( c = a -> ( c + ( ( sqrt ` D ) x. b ) ) = ( a + ( ( sqrt ` D ) x. b ) ) )
4 3 eqeq2d 
 |-  ( c = a -> ( A = ( c + ( ( sqrt ` D ) x. b ) ) <-> A = ( a + ( ( sqrt ` D ) x. b ) ) ) )
5 oveq1 
 |-  ( c = a -> ( c ^ 2 ) = ( a ^ 2 ) )
6 5 oveq1d 
 |-  ( c = a -> ( ( c ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) )
7 6 eqeq1d 
 |-  ( c = a -> ( ( ( c ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 <-> ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) )
8 4 7 anbi12d 
 |-  ( c = a -> ( ( A = ( c + ( ( sqrt ` D ) x. b ) ) /\ ( ( c ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) <-> ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) )
9 8 rexbidv 
 |-  ( c = a -> ( E. b e. ZZ ( A = ( c + ( ( sqrt ` D ) x. b ) ) /\ ( ( c ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) <-> E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) )
10 9 rspcev 
 |-  ( ( a e. NN0 /\ E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> E. c e. NN0 E. b e. ZZ ( A = ( c + ( ( sqrt ` D ) x. b ) ) /\ ( ( c ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) )
11 10 adantll 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ a e. NN0 ) /\ E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> E. c e. NN0 E. b e. ZZ ( A = ( c + ( ( sqrt ` D ) x. b ) ) /\ ( ( c ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) )
12 elpell14qr 
 |-  ( D e. ( NN \ []NN ) -> ( A e. ( Pell14QR ` D ) <-> ( A e. RR /\ E. c e. NN0 E. b e. ZZ ( A = ( c + ( ( sqrt ` D ) x. b ) ) /\ ( ( c ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) ) )
13 12 ad4antr 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ a e. NN0 ) /\ E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( A e. ( Pell14QR ` D ) <-> ( A e. RR /\ E. c e. NN0 E. b e. ZZ ( A = ( c + ( ( sqrt ` D ) x. b ) ) /\ ( ( c ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) ) )
14 2 11 13 mpbir2and 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ a e. NN0 ) /\ E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> A e. ( Pell14QR ` D ) )
15 14 orcd 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ a e. NN0 ) /\ E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( A e. ( Pell14QR ` D ) \/ -u A e. ( Pell14QR ` D ) ) )
16 15 exp31 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) -> ( a e. NN0 -> ( E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( A e. ( Pell14QR ` D ) \/ -u A e. ( Pell14QR ` D ) ) ) ) )
17 simp-5r 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ -u a e. NN0 ) /\ b e. ZZ ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> A e. RR )
18 17 renegcld 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ -u a e. NN0 ) /\ b e. ZZ ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> -u A e. RR )
19 simpllr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ -u a e. NN0 ) /\ b e. ZZ ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> -u a e. NN0 )
20 znegcl 
 |-  ( b e. ZZ -> -u b e. ZZ )
21 20 ad2antlr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ -u a e. NN0 ) /\ b e. ZZ ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> -u b e. ZZ )
22 simprl 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ -u a e. NN0 ) /\ b e. ZZ ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> A = ( a + ( ( sqrt ` D ) x. b ) ) )
23 22 negeqd 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ -u a e. NN0 ) /\ b e. ZZ ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> -u A = -u ( a + ( ( sqrt ` D ) x. b ) ) )
24 zcn 
 |-  ( a e. ZZ -> a e. CC )
25 24 ad4antlr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ -u a e. NN0 ) /\ b e. ZZ ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> a e. CC )
26 eldifi 
 |-  ( D e. ( NN \ []NN ) -> D e. NN )
27 26 nncnd 
 |-  ( D e. ( NN \ []NN ) -> D e. CC )
28 27 ad5antr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ -u a e. NN0 ) /\ b e. ZZ ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> D e. CC )
29 28 sqrtcld 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ -u a e. NN0 ) /\ b e. ZZ ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( sqrt ` D ) e. CC )
30 zcn 
 |-  ( b e. ZZ -> b e. CC )
31 30 ad2antlr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ -u a e. NN0 ) /\ b e. ZZ ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> b e. CC )
32 29 31 mulcld 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ -u a e. NN0 ) /\ b e. ZZ ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( ( sqrt ` D ) x. b ) e. CC )
33 25 32 negdid 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ -u a e. NN0 ) /\ b e. ZZ ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> -u ( a + ( ( sqrt ` D ) x. b ) ) = ( -u a + -u ( ( sqrt ` D ) x. b ) ) )
34 mulneg2 
 |-  ( ( ( sqrt ` D ) e. CC /\ b e. CC ) -> ( ( sqrt ` D ) x. -u b ) = -u ( ( sqrt ` D ) x. b ) )
35 34 eqcomd 
 |-  ( ( ( sqrt ` D ) e. CC /\ b e. CC ) -> -u ( ( sqrt ` D ) x. b ) = ( ( sqrt ` D ) x. -u b ) )
36 29 31 35 syl2anc 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ -u a e. NN0 ) /\ b e. ZZ ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> -u ( ( sqrt ` D ) x. b ) = ( ( sqrt ` D ) x. -u b ) )
37 36 oveq2d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ -u a e. NN0 ) /\ b e. ZZ ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( -u a + -u ( ( sqrt ` D ) x. b ) ) = ( -u a + ( ( sqrt ` D ) x. -u b ) ) )
38 23 33 37 3eqtrd 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ -u a e. NN0 ) /\ b e. ZZ ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> -u A = ( -u a + ( ( sqrt ` D ) x. -u b ) ) )
39 sqneg 
 |-  ( a e. CC -> ( -u a ^ 2 ) = ( a ^ 2 ) )
40 25 39 syl 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ -u a e. NN0 ) /\ b e. ZZ ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( -u a ^ 2 ) = ( a ^ 2 ) )
41 sqneg 
 |-  ( b e. CC -> ( -u b ^ 2 ) = ( b ^ 2 ) )
42 31 41 syl 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ -u a e. NN0 ) /\ b e. ZZ ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( -u b ^ 2 ) = ( b ^ 2 ) )
43 42 oveq2d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ -u a e. NN0 ) /\ b e. ZZ ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( D x. ( -u b ^ 2 ) ) = ( D x. ( b ^ 2 ) ) )
44 40 43 oveq12d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ -u a e. NN0 ) /\ b e. ZZ ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( ( -u a ^ 2 ) - ( D x. ( -u b ^ 2 ) ) ) = ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) )
45 simprr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ -u a e. NN0 ) /\ b e. ZZ ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 )
46 44 45 eqtrd 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ -u a e. NN0 ) /\ b e. ZZ ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( ( -u a ^ 2 ) - ( D x. ( -u b ^ 2 ) ) ) = 1 )
47 oveq1 
 |-  ( c = -u a -> ( c + ( ( sqrt ` D ) x. d ) ) = ( -u a + ( ( sqrt ` D ) x. d ) ) )
48 47 eqeq2d 
 |-  ( c = -u a -> ( -u A = ( c + ( ( sqrt ` D ) x. d ) ) <-> -u A = ( -u a + ( ( sqrt ` D ) x. d ) ) ) )
49 oveq1 
 |-  ( c = -u a -> ( c ^ 2 ) = ( -u a ^ 2 ) )
50 49 oveq1d 
 |-  ( c = -u a -> ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = ( ( -u a ^ 2 ) - ( D x. ( d ^ 2 ) ) ) )
51 50 eqeq1d 
 |-  ( c = -u a -> ( ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 <-> ( ( -u a ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) )
52 48 51 anbi12d 
 |-  ( c = -u a -> ( ( -u A = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) <-> ( -u A = ( -u a + ( ( sqrt ` D ) x. d ) ) /\ ( ( -u a ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) )
53 oveq2 
 |-  ( d = -u b -> ( ( sqrt ` D ) x. d ) = ( ( sqrt ` D ) x. -u b ) )
54 53 oveq2d 
 |-  ( d = -u b -> ( -u a + ( ( sqrt ` D ) x. d ) ) = ( -u a + ( ( sqrt ` D ) x. -u b ) ) )
55 54 eqeq2d 
 |-  ( d = -u b -> ( -u A = ( -u a + ( ( sqrt ` D ) x. d ) ) <-> -u A = ( -u a + ( ( sqrt ` D ) x. -u b ) ) ) )
56 oveq1 
 |-  ( d = -u b -> ( d ^ 2 ) = ( -u b ^ 2 ) )
57 56 oveq2d 
 |-  ( d = -u b -> ( D x. ( d ^ 2 ) ) = ( D x. ( -u b ^ 2 ) ) )
58 57 oveq2d 
 |-  ( d = -u b -> ( ( -u a ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = ( ( -u a ^ 2 ) - ( D x. ( -u b ^ 2 ) ) ) )
59 58 eqeq1d 
 |-  ( d = -u b -> ( ( ( -u a ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 <-> ( ( -u a ^ 2 ) - ( D x. ( -u b ^ 2 ) ) ) = 1 ) )
60 55 59 anbi12d 
 |-  ( d = -u b -> ( ( -u A = ( -u a + ( ( sqrt ` D ) x. d ) ) /\ ( ( -u a ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) <-> ( -u A = ( -u a + ( ( sqrt ` D ) x. -u b ) ) /\ ( ( -u a ^ 2 ) - ( D x. ( -u b ^ 2 ) ) ) = 1 ) ) )
61 52 60 rspc2ev 
 |-  ( ( -u a e. NN0 /\ -u b e. ZZ /\ ( -u A = ( -u a + ( ( sqrt ` D ) x. -u b ) ) /\ ( ( -u a ^ 2 ) - ( D x. ( -u b ^ 2 ) ) ) = 1 ) ) -> E. c e. NN0 E. d e. ZZ ( -u A = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) )
62 19 21 38 46 61 syl112anc 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ -u a e. NN0 ) /\ b e. ZZ ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> E. c e. NN0 E. d e. ZZ ( -u A = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) )
63 elpell14qr 
 |-  ( D e. ( NN \ []NN ) -> ( -u A e. ( Pell14QR ` D ) <-> ( -u A e. RR /\ E. c e. NN0 E. d e. ZZ ( -u A = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) ) )
64 63 ad5antr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ -u a e. NN0 ) /\ b e. ZZ ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( -u A e. ( Pell14QR ` D ) <-> ( -u A e. RR /\ E. c e. NN0 E. d e. ZZ ( -u A = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) ) )
65 18 62 64 mpbir2and 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ -u a e. NN0 ) /\ b e. ZZ ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> -u A e. ( Pell14QR ` D ) )
66 65 olcd 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ -u a e. NN0 ) /\ b e. ZZ ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( A e. ( Pell14QR ` D ) \/ -u A e. ( Pell14QR ` D ) ) )
67 66 ex 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ -u a e. NN0 ) /\ b e. ZZ ) -> ( ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( A e. ( Pell14QR ` D ) \/ -u A e. ( Pell14QR ` D ) ) ) )
68 67 rexlimdva 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) /\ -u a e. NN0 ) -> ( E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( A e. ( Pell14QR ` D ) \/ -u A e. ( Pell14QR ` D ) ) ) )
69 68 ex 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) -> ( -u a e. NN0 -> ( E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( A e. ( Pell14QR ` D ) \/ -u A e. ( Pell14QR ` D ) ) ) ) )
70 elznn0 
 |-  ( a e. ZZ <-> ( a e. RR /\ ( a e. NN0 \/ -u a e. NN0 ) ) )
71 70 simprbi 
 |-  ( a e. ZZ -> ( a e. NN0 \/ -u a e. NN0 ) )
72 71 adantl 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) -> ( a e. NN0 \/ -u a e. NN0 ) )
73 16 69 72 mpjaod 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. RR ) /\ a e. ZZ ) -> ( E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( A e. ( Pell14QR ` D ) \/ -u A e. ( Pell14QR ` D ) ) ) )
74 73 rexlimdva 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. RR ) -> ( E. a e. ZZ E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( A e. ( Pell14QR ` D ) \/ -u A e. ( Pell14QR ` D ) ) ) )
75 74 expimpd 
 |-  ( D e. ( NN \ []NN ) -> ( ( A e. RR /\ E. a e. ZZ E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( A e. ( Pell14QR ` D ) \/ -u A e. ( Pell14QR ` D ) ) ) )
76 1 75 sylbid 
 |-  ( D e. ( NN \ []NN ) -> ( A e. ( Pell1234QR ` D ) -> ( A e. ( Pell14QR ` D ) \/ -u A e. ( Pell14QR ` D ) ) ) )
77 76 imp 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) -> ( A e. ( Pell14QR ` D ) \/ -u A e. ( Pell14QR ` D ) ) )