Metamath Proof Explorer

Theorem pell14qrdich

Description: A positive Pell solution is either in the first quadrant, or its reciprocal is. (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion pell14qrdich 
|- ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( A e. ( Pell1QR ` D ) \/ ( 1 / A ) e. ( Pell1QR ` D ) ) )

Proof

Step Hyp Ref Expression
1 elpell14qr 
 |-  ( D e. ( NN \ []NN ) -> ( A e. ( Pell14QR ` D ) <-> ( A e. RR /\ E. a e. NN0 E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) ) )
2 1 biimpa 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( A e. RR /\ E. a e. NN0 E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) )
3 simplrr 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> b e. ZZ )
4 elznn0 
 |-  ( b e. ZZ <-> ( b e. RR /\ ( b e. NN0 \/ -u b e. NN0 ) ) )
5 3 4 sylib 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( b e. RR /\ ( b e. NN0 \/ -u b e. NN0 ) ) )
6 5 simprd 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( b e. NN0 \/ -u b e. NN0 ) )
7 simplr 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) -> A e. RR )
8 7 ad2antrr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ b e. NN0 ) -> A e. RR )
9 simprl 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) -> a e. NN0 )
10 9 ad2antrr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ b e. NN0 ) -> a e. NN0 )
11 simpr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ b e. NN0 ) -> b e. NN0 )
12 simplr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ b e. NN0 ) -> ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) )
13 rsp2e 
 |-  ( ( a e. NN0 /\ b e. NN0 /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> E. a e. NN0 E. b e. NN0 ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) )
14 10 11 12 13 syl3anc 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ b e. NN0 ) -> E. a e. NN0 E. b e. NN0 ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) )
15 8 14 jca 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ b e. NN0 ) -> ( A e. RR /\ E. a e. NN0 E. b e. NN0 ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) )
16 15 ex 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( b e. NN0 -> ( A e. RR /\ E. a e. NN0 E. b e. NN0 ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) ) )
17 elpell1qr 
 |-  ( D e. ( NN \ []NN ) -> ( A e. ( Pell1QR ` D ) <-> ( A e. RR /\ E. a e. NN0 E. b e. NN0 ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) ) )
18 17 ad4antr 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( A e. ( Pell1QR ` D ) <-> ( A e. RR /\ E. a e. NN0 E. b e. NN0 ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) ) )
19 16 18 sylibrd 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( b e. NN0 -> A e. ( Pell1QR ` D ) ) )
20 7 ad2antrr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ -u b e. NN0 ) -> A e. RR )
21 pell14qrne0 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> A =/= 0 )
22 21 ad4antr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ -u b e. NN0 ) -> A =/= 0 )
23 20 22 rereccld 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ -u b e. NN0 ) -> ( 1 / A ) e. RR )
24 9 ad2antrr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ -u b e. NN0 ) -> a e. NN0 )
25 simpr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ -u b e. NN0 ) -> -u b e. NN0 )
26 pell14qrre 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> A e. RR )
27 26 recnd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> A e. CC )
28 27 21 reccld 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( 1 / A ) e. CC )
29 28 ad3antrrr 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( 1 / A ) e. CC )
30 nn0cn 
 |-  ( a e. NN0 -> a e. CC )
31 30 ad2antrl 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) -> a e. CC )
32 eldifi 
 |-  ( D e. ( NN \ []NN ) -> D e. NN )
33 32 nncnd 
 |-  ( D e. ( NN \ []NN ) -> D e. CC )
34 33 ad3antrrr 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) -> D e. CC )
35 34 sqrtcld 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) -> ( sqrt ` D ) e. CC )
36 zcn 
 |-  ( b e. ZZ -> b e. CC )
37 36 ad2antll 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) -> b e. CC )
38 37 negcld 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) -> -u b e. CC )
39 35 38 mulcld 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) -> ( ( sqrt ` D ) x. -u b ) e. CC )
40 31 39 addcld 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) -> ( a + ( ( sqrt ` D ) x. -u b ) ) e. CC )
41 40 adantr 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( a + ( ( sqrt ` D ) x. -u b ) ) e. CC )
42 27 ad3antrrr 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> A e. CC )
43 21 ad3antrrr 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> A =/= 0 )
44 27 21 recidd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( A x. ( 1 / A ) ) = 1 )
45 44 ad3antrrr 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( A x. ( 1 / A ) ) = 1 )
46 simprr 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( 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 )
47 45 46 eqtr4d 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( A x. ( 1 / A ) ) = ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) )
48 31 adantr 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ A = ( a + ( ( sqrt ` D ) x. b ) ) ) -> a e. CC )
49 35 37 mulcld 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) -> ( ( sqrt ` D ) x. b ) e. CC )
50 49 adantr 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ A = ( a + ( ( sqrt ` D ) x. b ) ) ) -> ( ( sqrt ` D ) x. b ) e. CC )
51 subsq 
 |-  ( ( a e. CC /\ ( ( sqrt ` D ) x. b ) e. CC ) -> ( ( a ^ 2 ) - ( ( ( sqrt ` D ) x. b ) ^ 2 ) ) = ( ( a + ( ( sqrt ` D ) x. b ) ) x. ( a - ( ( sqrt ` D ) x. b ) ) ) )
52 48 50 51 syl2anc 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ A = ( a + ( ( sqrt ` D ) x. b ) ) ) -> ( ( a ^ 2 ) - ( ( ( sqrt ` D ) x. b ) ^ 2 ) ) = ( ( a + ( ( sqrt ` D ) x. b ) ) x. ( a - ( ( sqrt ` D ) x. b ) ) ) )
53 35 37 sqmuld 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) -> ( ( ( sqrt ` D ) x. b ) ^ 2 ) = ( ( ( sqrt ` D ) ^ 2 ) x. ( b ^ 2 ) ) )
54 34 sqsqrtd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) -> ( ( sqrt ` D ) ^ 2 ) = D )
55 54 oveq1d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) -> ( ( ( sqrt ` D ) ^ 2 ) x. ( b ^ 2 ) ) = ( D x. ( b ^ 2 ) ) )
56 53 55 eqtr2d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) -> ( D x. ( b ^ 2 ) ) = ( ( ( sqrt ` D ) x. b ) ^ 2 ) )
57 56 oveq2d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) -> ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = ( ( a ^ 2 ) - ( ( ( sqrt ` D ) x. b ) ^ 2 ) ) )
58 57 adantr 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ A = ( a + ( ( sqrt ` D ) x. b ) ) ) -> ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = ( ( a ^ 2 ) - ( ( ( sqrt ` D ) x. b ) ^ 2 ) ) )
59 simpr 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ A = ( a + ( ( sqrt ` D ) x. b ) ) ) -> A = ( a + ( ( sqrt ` D ) x. b ) ) )
60 35 37 mulneg2d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) -> ( ( sqrt ` D ) x. -u b ) = -u ( ( sqrt ` D ) x. b ) )
61 60 oveq2d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) -> ( a + ( ( sqrt ` D ) x. -u b ) ) = ( a + -u ( ( sqrt ` D ) x. b ) ) )
62 negsub 
 |-  ( ( a e. CC /\ ( ( sqrt ` D ) x. b ) e. CC ) -> ( a + -u ( ( sqrt ` D ) x. b ) ) = ( a - ( ( sqrt ` D ) x. b ) ) )
63 62 eqcomd 
 |-  ( ( a e. CC /\ ( ( sqrt ` D ) x. b ) e. CC ) -> ( a - ( ( sqrt ` D ) x. b ) ) = ( a + -u ( ( sqrt ` D ) x. b ) ) )
64 31 49 63 syl2anc 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) -> ( a - ( ( sqrt ` D ) x. b ) ) = ( a + -u ( ( sqrt ` D ) x. b ) ) )
65 61 64 eqtr4d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) -> ( a + ( ( sqrt ` D ) x. -u b ) ) = ( a - ( ( sqrt ` D ) x. b ) ) )
66 65 adantr 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ A = ( a + ( ( sqrt ` D ) x. b ) ) ) -> ( a + ( ( sqrt ` D ) x. -u b ) ) = ( a - ( ( sqrt ` D ) x. b ) ) )
67 59 66 oveq12d 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ A = ( a + ( ( sqrt ` D ) x. b ) ) ) -> ( A x. ( a + ( ( sqrt ` D ) x. -u b ) ) ) = ( ( a + ( ( sqrt ` D ) x. b ) ) x. ( a - ( ( sqrt ` D ) x. b ) ) ) )
68 52 58 67 3eqtr4d 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ A = ( a + ( ( sqrt ` D ) x. b ) ) ) -> ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = ( A x. ( a + ( ( sqrt ` D ) x. -u b ) ) ) )
69 68 adantrr 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( 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 ) ) ) = ( A x. ( a + ( ( sqrt ` D ) x. -u b ) ) ) )
70 47 69 eqtrd 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( A x. ( 1 / A ) ) = ( A x. ( a + ( ( sqrt ` D ) x. -u b ) ) ) )
71 29 41 42 43 70 mulcanad 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( 1 / A ) = ( a + ( ( sqrt ` D ) x. -u b ) ) )
72 71 adantr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ -u b e. NN0 ) -> ( 1 / A ) = ( a + ( ( sqrt ` D ) x. -u b ) ) )
73 37 ad2antrr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ -u b e. NN0 ) -> b e. CC )
74 sqneg 
 |-  ( b e. CC -> ( -u b ^ 2 ) = ( b ^ 2 ) )
75 73 74 syl 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ -u b e. NN0 ) -> ( -u b ^ 2 ) = ( b ^ 2 ) )
76 75 oveq2d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ -u b e. NN0 ) -> ( D x. ( -u b ^ 2 ) ) = ( D x. ( b ^ 2 ) ) )
77 76 oveq2d 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ -u b e. NN0 ) -> ( ( a ^ 2 ) - ( D x. ( -u b ^ 2 ) ) ) = ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) )
78 simplrr 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ -u b e. NN0 ) -> ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 )
79 77 78 eqtrd 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ -u b e. NN0 ) -> ( ( a ^ 2 ) - ( D x. ( -u b ^ 2 ) ) ) = 1 )
80 72 79 jca 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ -u b e. NN0 ) -> ( ( 1 / A ) = ( a + ( ( sqrt ` D ) x. -u b ) ) /\ ( ( a ^ 2 ) - ( D x. ( -u b ^ 2 ) ) ) = 1 ) )
81 oveq2 
 |-  ( c = -u b -> ( ( sqrt ` D ) x. c ) = ( ( sqrt ` D ) x. -u b ) )
82 81 oveq2d 
 |-  ( c = -u b -> ( a + ( ( sqrt ` D ) x. c ) ) = ( a + ( ( sqrt ` D ) x. -u b ) ) )
83 82 eqeq2d 
 |-  ( c = -u b -> ( ( 1 / A ) = ( a + ( ( sqrt ` D ) x. c ) ) <-> ( 1 / A ) = ( a + ( ( sqrt ` D ) x. -u b ) ) ) )
84 oveq1 
 |-  ( c = -u b -> ( c ^ 2 ) = ( -u b ^ 2 ) )
85 84 oveq2d 
 |-  ( c = -u b -> ( D x. ( c ^ 2 ) ) = ( D x. ( -u b ^ 2 ) ) )
86 85 oveq2d 
 |-  ( c = -u b -> ( ( a ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = ( ( a ^ 2 ) - ( D x. ( -u b ^ 2 ) ) ) )
87 86 eqeq1d 
 |-  ( c = -u b -> ( ( ( a ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = 1 <-> ( ( a ^ 2 ) - ( D x. ( -u b ^ 2 ) ) ) = 1 ) )
88 83 87 anbi12d 
 |-  ( c = -u b -> ( ( ( 1 / A ) = ( a + ( ( sqrt ` D ) x. c ) ) /\ ( ( a ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = 1 ) <-> ( ( 1 / A ) = ( a + ( ( sqrt ` D ) x. -u b ) ) /\ ( ( a ^ 2 ) - ( D x. ( -u b ^ 2 ) ) ) = 1 ) ) )
89 88 rspcev 
 |-  ( ( -u b e. NN0 /\ ( ( 1 / A ) = ( a + ( ( sqrt ` D ) x. -u b ) ) /\ ( ( a ^ 2 ) - ( D x. ( -u b ^ 2 ) ) ) = 1 ) ) -> E. c e. NN0 ( ( 1 / A ) = ( a + ( ( sqrt ` D ) x. c ) ) /\ ( ( a ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = 1 ) )
90 25 80 89 syl2anc 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ -u b e. NN0 ) -> E. c e. NN0 ( ( 1 / A ) = ( a + ( ( sqrt ` D ) x. c ) ) /\ ( ( a ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = 1 ) )
91 rspe 
 |-  ( ( a e. NN0 /\ E. c e. NN0 ( ( 1 / A ) = ( a + ( ( sqrt ` D ) x. c ) ) /\ ( ( a ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = 1 ) ) -> E. a e. NN0 E. c e. NN0 ( ( 1 / A ) = ( a + ( ( sqrt ` D ) x. c ) ) /\ ( ( a ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = 1 ) )
92 24 90 91 syl2anc 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ -u b e. NN0 ) -> E. a e. NN0 E. c e. NN0 ( ( 1 / A ) = ( a + ( ( sqrt ` D ) x. c ) ) /\ ( ( a ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = 1 ) )
93 23 92 jca 
 |-  ( ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) /\ -u b e. NN0 ) -> ( ( 1 / A ) e. RR /\ E. a e. NN0 E. c e. NN0 ( ( 1 / A ) = ( a + ( ( sqrt ` D ) x. c ) ) /\ ( ( a ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = 1 ) ) )
94 93 ex 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( -u b e. NN0 -> ( ( 1 / A ) e. RR /\ E. a e. NN0 E. c e. NN0 ( ( 1 / A ) = ( a + ( ( sqrt ` D ) x. c ) ) /\ ( ( a ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = 1 ) ) ) )
95 elpell1qr 
 |-  ( D e. ( NN \ []NN ) -> ( ( 1 / A ) e. ( Pell1QR ` D ) <-> ( ( 1 / A ) e. RR /\ E. a e. NN0 E. c e. NN0 ( ( 1 / A ) = ( a + ( ( sqrt ` D ) x. c ) ) /\ ( ( a ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = 1 ) ) ) )
96 95 ad4antr 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( ( 1 / A ) e. ( Pell1QR ` D ) <-> ( ( 1 / A ) e. RR /\ E. a e. NN0 E. c e. NN0 ( ( 1 / A ) = ( a + ( ( sqrt ` D ) x. c ) ) /\ ( ( a ^ 2 ) - ( D x. ( c ^ 2 ) ) ) = 1 ) ) ) )
97 94 96 sylibrd 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( -u b e. NN0 -> ( 1 / A ) e. ( Pell1QR ` D ) ) )
98 19 97 orim12d 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( ( b e. NN0 \/ -u b e. NN0 ) -> ( A e. ( Pell1QR ` D ) \/ ( 1 / A ) e. ( Pell1QR ` D ) ) ) )
99 6 98 mpd 
 |-  ( ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( A e. ( Pell1QR ` D ) \/ ( 1 / A ) e. ( Pell1QR ` D ) ) )
100 99 ex 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) /\ ( a e. NN0 /\ b e. ZZ ) ) -> ( ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( A e. ( Pell1QR ` D ) \/ ( 1 / A ) e. ( Pell1QR ` D ) ) ) )
101 100 rexlimdvva 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ A e. RR ) -> ( E. a e. NN0 E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( A e. ( Pell1QR ` D ) \/ ( 1 / A ) e. ( Pell1QR ` D ) ) ) )
102 101 expimpd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( A e. RR /\ E. a e. NN0 E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( A e. ( Pell1QR ` D ) \/ ( 1 / A ) e. ( Pell1QR ` D ) ) ) )
103 2 102 mpd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( A e. ( Pell1QR ` D ) \/ ( 1 / A ) e. ( Pell1QR ` D ) ) )