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 ) ) )