Metamath Proof Explorer

Theorem pell1234qrreccl

Description: General solutions of the Pell equation are closed under reciprocals. (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion pell1234qrreccl 
|- ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) -> ( 1 / A ) e. ( Pell1234QR ` 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 1 biimpa 
 |-  ( ( 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 ) ) )
3 pell1234qrre 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) -> A e. RR )
4 pell1234qrne0 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) -> A =/= 0 )
5 3 4 rereccld 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) -> ( 1 / A ) e. RR )
6 5 ad2antrr 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( 1 / A ) e. RR )
7 simplrl 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> a e. ZZ )
8 simplrr 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> b e. ZZ )
9 8 znegcld 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> -u b e. ZZ )
10 5 recnd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) -> ( 1 / A ) e. CC )
11 10 ad2antrr 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( 1 / A ) e. CC )
12 zcn 
 |-  ( a e. ZZ -> a e. CC )
13 12 adantr 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> a e. CC )
14 13 ad2antlr 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> a e. CC )
15 eldifi 
 |-  ( D e. ( NN \ []NN ) -> D e. NN )
16 15 nncnd 
 |-  ( D e. ( NN \ []NN ) -> D e. CC )
17 16 ad3antrrr 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> D e. CC )
18 17 sqrtcld 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( sqrt ` D ) e. CC )
19 8 zcnd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> b e. CC )
20 19 negcld 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> -u b e. CC )
21 18 20 mulcld 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( ( sqrt ` D ) x. -u b ) e. CC )
22 14 21 addcld 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( a + ( ( sqrt ` D ) x. -u b ) ) e. CC )
23 3 recnd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) -> A e. CC )
24 23 ad2antrr 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> A e. CC )
25 4 ad2antrr 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> A =/= 0 )
26 18 19 sqmuld 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( ( ( sqrt ` D ) x. b ) ^ 2 ) = ( ( ( sqrt ` D ) ^ 2 ) x. ( b ^ 2 ) ) )
27 17 sqsqrtd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( ( sqrt ` D ) ^ 2 ) = D )
28 27 oveq1d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( ( ( sqrt ` D ) ^ 2 ) x. ( b ^ 2 ) ) = ( D x. ( b ^ 2 ) ) )
29 26 28 eqtr2d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( D x. ( b ^ 2 ) ) = ( ( ( sqrt ` D ) x. b ) ^ 2 ) )
30 29 oveq2d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = ( ( a ^ 2 ) - ( ( ( sqrt ` D ) x. b ) ^ 2 ) ) )
31 simprr 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 )
32 18 19 mulcld 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( ( sqrt ` D ) x. b ) e. CC )
33 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 ) ) ) )
34 14 32 33 syl2anc 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( ( a ^ 2 ) - ( ( ( sqrt ` D ) x. b ) ^ 2 ) ) = ( ( a + ( ( sqrt ` D ) x. b ) ) x. ( a - ( ( sqrt ` D ) x. b ) ) ) )
35 30 31 34 3eqtr3d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> 1 = ( ( a + ( ( sqrt ` D ) x. b ) ) x. ( a - ( ( sqrt ` D ) x. b ) ) ) )
36 24 25 recidd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( A x. ( 1 / A ) ) = 1 )
37 simprl 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> A = ( a + ( ( sqrt ` D ) x. b ) ) )
38 18 19 mulneg2d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( ( sqrt ` D ) x. -u b ) = -u ( ( sqrt ` D ) x. b ) )
39 38 oveq2d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( a + ( ( sqrt ` D ) x. -u b ) ) = ( a + -u ( ( sqrt ` D ) x. b ) ) )
40 14 32 negsubd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( a + -u ( ( sqrt ` D ) x. b ) ) = ( a - ( ( sqrt ` D ) x. b ) ) )
41 39 40 eqtrd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( a + ( ( sqrt ` D ) x. -u b ) ) = ( a - ( ( sqrt ` D ) x. b ) ) )
42 37 41 oveq12d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( A x. ( a + ( ( sqrt ` D ) x. -u b ) ) ) = ( ( a + ( ( sqrt ` D ) x. b ) ) x. ( a - ( ( sqrt ` D ) x. b ) ) ) )
43 35 36 42 3eqtr4d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ 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 ) ) ) )
44 11 22 24 25 43 mulcanad 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( 1 / A ) = ( a + ( ( sqrt ` D ) x. -u b ) ) )
45 sqneg 
 |-  ( b e. CC -> ( -u b ^ 2 ) = ( b ^ 2 ) )
46 19 45 syl 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( -u b ^ 2 ) = ( b ^ 2 ) )
47 46 oveq2d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ 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 ) ) )
48 47 oveq2d 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( ( a ^ 2 ) - ( D x. ( -u b ^ 2 ) ) ) = ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) )
49 48 31 eqtrd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( ( a ^ 2 ) - ( D x. ( -u b ^ 2 ) ) ) = 1 )
50 oveq1 
 |-  ( c = a -> ( c + ( ( sqrt ` D ) x. d ) ) = ( a + ( ( sqrt ` D ) x. d ) ) )
51 50 eqeq2d 
 |-  ( c = a -> ( ( 1 / A ) = ( c + ( ( sqrt ` D ) x. d ) ) <-> ( 1 / A ) = ( a + ( ( sqrt ` D ) x. d ) ) ) )
52 oveq1 
 |-  ( c = a -> ( c ^ 2 ) = ( a ^ 2 ) )
53 52 oveq1d 
 |-  ( c = a -> ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = ( ( a ^ 2 ) - ( D x. ( d ^ 2 ) ) ) )
54 53 eqeq1d 
 |-  ( c = a -> ( ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 <-> ( ( a ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) )
55 51 54 anbi12d 
 |-  ( c = a -> ( ( ( 1 / A ) = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) <-> ( ( 1 / A ) = ( a + ( ( sqrt ` D ) x. d ) ) /\ ( ( a ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) )
56 oveq2 
 |-  ( d = -u b -> ( ( sqrt ` D ) x. d ) = ( ( sqrt ` D ) x. -u b ) )
57 56 oveq2d 
 |-  ( d = -u b -> ( a + ( ( sqrt ` D ) x. d ) ) = ( a + ( ( sqrt ` D ) x. -u b ) ) )
58 57 eqeq2d 
 |-  ( d = -u b -> ( ( 1 / A ) = ( a + ( ( sqrt ` D ) x. d ) ) <-> ( 1 / A ) = ( a + ( ( sqrt ` D ) x. -u b ) ) ) )
59 oveq1 
 |-  ( d = -u b -> ( d ^ 2 ) = ( -u b ^ 2 ) )
60 59 oveq2d 
 |-  ( d = -u b -> ( D x. ( d ^ 2 ) ) = ( D x. ( -u b ^ 2 ) ) )
61 60 oveq2d 
 |-  ( d = -u b -> ( ( a ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = ( ( a ^ 2 ) - ( D x. ( -u b ^ 2 ) ) ) )
62 61 eqeq1d 
 |-  ( d = -u b -> ( ( ( a ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 <-> ( ( a ^ 2 ) - ( D x. ( -u b ^ 2 ) ) ) = 1 ) )
63 58 62 anbi12d 
 |-  ( d = -u b -> ( ( ( 1 / A ) = ( a + ( ( sqrt ` D ) x. d ) ) /\ ( ( a ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) <-> ( ( 1 / A ) = ( a + ( ( sqrt ` D ) x. -u b ) ) /\ ( ( a ^ 2 ) - ( D x. ( -u b ^ 2 ) ) ) = 1 ) ) )
64 55 63 rspc2ev 
 |-  ( ( a e. ZZ /\ -u b e. ZZ /\ ( ( 1 / A ) = ( a + ( ( sqrt ` D ) x. -u b ) ) /\ ( ( a ^ 2 ) - ( D x. ( -u b ^ 2 ) ) ) = 1 ) ) -> E. c e. ZZ E. d e. ZZ ( ( 1 / A ) = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) )
65 7 9 44 49 64 syl112anc 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> E. c e. ZZ E. d e. ZZ ( ( 1 / A ) = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) )
66 6 65 jca 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) -> ( ( 1 / A ) e. RR /\ E. c e. ZZ E. d e. ZZ ( ( 1 / A ) = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) )
67 66 ex 
 |-  ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( ( 1 / A ) e. RR /\ E. c e. ZZ E. d e. ZZ ( ( 1 / A ) = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) ) )
68 67 rexlimdvva 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) -> ( E. a e. ZZ E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) -> ( ( 1 / A ) e. RR /\ E. c e. ZZ E. d e. ZZ ( ( 1 / A ) = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) ) )
69 68 adantld 
 |-  ( ( 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 ) ) -> ( ( 1 / A ) e. RR /\ E. c e. ZZ E. d e. ZZ ( ( 1 / A ) = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) ) )
70 2 69 mpd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) -> ( ( 1 / A ) e. RR /\ E. c e. ZZ E. d e. ZZ ( ( 1 / A ) = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) )
71 elpell1234qr 
 |-  ( D e. ( NN \ []NN ) -> ( ( 1 / A ) e. ( Pell1234QR ` D ) <-> ( ( 1 / A ) e. RR /\ E. c e. ZZ E. d e. ZZ ( ( 1 / A ) = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) ) )
72 71 adantr 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) -> ( ( 1 / A ) e. ( Pell1234QR ` D ) <-> ( ( 1 / A ) e. RR /\ E. c e. ZZ E. d e. ZZ ( ( 1 / A ) = ( c + ( ( sqrt ` D ) x. d ) ) /\ ( ( c ^ 2 ) - ( D x. ( d ^ 2 ) ) ) = 1 ) ) ) )
73 70 72 mpbird 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) -> ( 1 / A ) e. ( Pell1234QR ` D ) )