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 DAPell1234QRD1APell1234QRD

Proof

Step Hyp Ref Expression
1 elpell1234qr DAPell1234QRDAabA=a+Dba2Db2=1
2 1 biimpa DAPell1234QRDAabA=a+Dba2Db2=1
3 pell1234qrre DAPell1234QRDA
4 pell1234qrne0 DAPell1234QRDA0
5 3 4 rereccld DAPell1234QRD1A
6 5 ad2antrr DAPell1234QRDabA=a+Dba2Db2=11A
7 simplrl DAPell1234QRDabA=a+Dba2Db2=1a
8 simplrr DAPell1234QRDabA=a+Dba2Db2=1b
9 8 znegcld DAPell1234QRDabA=a+Dba2Db2=1b
10 5 recnd DAPell1234QRD1A
11 10 ad2antrr DAPell1234QRDabA=a+Dba2Db2=11A
12 zcn aa
13 12 adantr aba
14 13 ad2antlr DAPell1234QRDabA=a+Dba2Db2=1a
15 eldifi DD
16 15 nncnd DD
17 16 ad3antrrr DAPell1234QRDabA=a+Dba2Db2=1D
18 17 sqrtcld DAPell1234QRDabA=a+Dba2Db2=1D
19 8 zcnd DAPell1234QRDabA=a+Dba2Db2=1b
20 19 negcld DAPell1234QRDabA=a+Dba2Db2=1b
21 18 20 mulcld DAPell1234QRDabA=a+Dba2Db2=1Db
22 14 21 addcld DAPell1234QRDabA=a+Dba2Db2=1a+Db
23 3 recnd DAPell1234QRDA
24 23 ad2antrr DAPell1234QRDabA=a+Dba2Db2=1A
25 4 ad2antrr DAPell1234QRDabA=a+Dba2Db2=1A0
26 18 19 sqmuld DAPell1234QRDabA=a+Dba2Db2=1Db2=D2b2
27 17 sqsqrtd DAPell1234QRDabA=a+Dba2Db2=1D2=D
28 27 oveq1d DAPell1234QRDabA=a+Dba2Db2=1D2b2=Db2
29 26 28 eqtr2d DAPell1234QRDabA=a+Dba2Db2=1Db2=Db2
30 29 oveq2d DAPell1234QRDabA=a+Dba2Db2=1a2Db2=a2Db2
31 simprr DAPell1234QRDabA=a+Dba2Db2=1a2Db2=1
32 18 19 mulcld DAPell1234QRDabA=a+Dba2Db2=1Db
33 subsq aDba2Db2=a+DbaDb
34 14 32 33 syl2anc DAPell1234QRDabA=a+Dba2Db2=1a2Db2=a+DbaDb
35 30 31 34 3eqtr3d DAPell1234QRDabA=a+Dba2Db2=11=a+DbaDb
36 24 25 recidd DAPell1234QRDabA=a+Dba2Db2=1A1A=1
37 simprl DAPell1234QRDabA=a+Dba2Db2=1A=a+Db
38 18 19 mulneg2d DAPell1234QRDabA=a+Dba2Db2=1Db=Db
39 38 oveq2d DAPell1234QRDabA=a+Dba2Db2=1a+Db=a+Db
40 14 32 negsubd DAPell1234QRDabA=a+Dba2Db2=1a+Db=aDb
41 39 40 eqtrd DAPell1234QRDabA=a+Dba2Db2=1a+Db=aDb
42 37 41 oveq12d DAPell1234QRDabA=a+Dba2Db2=1Aa+Db=a+DbaDb
43 35 36 42 3eqtr4d DAPell1234QRDabA=a+Dba2Db2=1A1A=Aa+Db
44 11 22 24 25 43 mulcanad DAPell1234QRDabA=a+Dba2Db2=11A=a+Db
45 sqneg bb2=b2
46 19 45 syl DAPell1234QRDabA=a+Dba2Db2=1b2=b2
47 46 oveq2d DAPell1234QRDabA=a+Dba2Db2=1Db2=Db2
48 47 oveq2d DAPell1234QRDabA=a+Dba2Db2=1a2Db2=a2Db2
49 48 31 eqtrd DAPell1234QRDabA=a+Dba2Db2=1a2Db2=1
50 oveq1 c=ac+Dd=a+Dd
51 50 eqeq2d c=a1A=c+Dd1A=a+Dd
52 oveq1 c=ac2=a2
53 52 oveq1d c=ac2Dd2=a2Dd2
54 53 eqeq1d c=ac2Dd2=1a2Dd2=1
55 51 54 anbi12d c=a1A=c+Ddc2Dd2=11A=a+Dda2Dd2=1
56 oveq2 d=bDd=Db
57 56 oveq2d d=ba+Dd=a+Db
58 57 eqeq2d d=b1A=a+Dd1A=a+Db
59 oveq1 d=bd2=b2
60 59 oveq2d d=bDd2=Db2
61 60 oveq2d d=ba2Dd2=a2Db2
62 61 eqeq1d d=ba2Dd2=1a2Db2=1
63 58 62 anbi12d d=b1A=a+Dda2Dd2=11A=a+Dba2Db2=1
64 55 63 rspc2ev ab1A=a+Dba2Db2=1cd1A=c+Ddc2Dd2=1
65 7 9 44 49 64 syl112anc DAPell1234QRDabA=a+Dba2Db2=1cd1A=c+Ddc2Dd2=1
66 6 65 jca DAPell1234QRDabA=a+Dba2Db2=11Acd1A=c+Ddc2Dd2=1
67 66 ex DAPell1234QRDabA=a+Dba2Db2=11Acd1A=c+Ddc2Dd2=1
68 67 rexlimdvva DAPell1234QRDabA=a+Dba2Db2=11Acd1A=c+Ddc2Dd2=1
69 68 adantld DAPell1234QRDAabA=a+Dba2Db2=11Acd1A=c+Ddc2Dd2=1
70 2 69 mpd DAPell1234QRD1Acd1A=c+Ddc2Dd2=1
71 elpell1234qr D1APell1234QRD1Acd1A=c+Ddc2Dd2=1
72 71 adantr DAPell1234QRD1APell1234QRD1Acd1A=c+Ddc2Dd2=1
73 70 72 mpbird DAPell1234QRD1APell1234QRD