Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pell14qrdich Structured version   Unicode version

Theorem pell14qrdich 35641
 Description: A positive Pell solution is either in the first quadrant, or its reciprocal is. (Contributed by Stefan O'Rear, 18-Sep-2014.)
Assertion
Ref Expression
pell14qrdich NN Pell14QR Pell1QR Pell1QR

Proof of Theorem pell14qrdich
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elpell14qr 35621 . . 3 NN Pell14QR
21biimpa 487 . 2 NN Pell14QR
3 simplrr 770 . . . . . . . 8 NN Pell14QR
4 elznn0 10954 . . . . . . . 8
53, 4sylib 200 . . . . . . 7 NN Pell14QR
65simprd 465 . . . . . 6 NN Pell14QR
7 simplr 761 . . . . . . . . . . 11 NN Pell14QR
87ad2antrr 731 . . . . . . . . . 10 NN Pell14QR
9 simprl 763 . . . . . . . . . . . 12 NN Pell14QR
109ad2antrr 731 . . . . . . . . . . 11 NN Pell14QR
11 simpr 463 . . . . . . . . . . 11 NN Pell14QR
12 simplr 761 . . . . . . . . . . 11 NN Pell14QR
13 rsp2e 2885 . . . . . . . . . . 11
1410, 11, 12, 13syl3anc 1265 . . . . . . . . . 10 NN Pell14QR
158, 14jca 535 . . . . . . . . 9 NN Pell14QR
1615ex 436 . . . . . . . 8 NN Pell14QR
17 elpell1qr 35619 . . . . . . . . 9 NN Pell1QR
1817ad4antr 737 . . . . . . . 8 NN Pell14QR Pell1QR
1916, 18sylibrd 238 . . . . . . 7 NN Pell14QR Pell1QR
207ad2antrr 731 . . . . . . . . . . 11 NN Pell14QR
21 pell14qrne0 35630 . . . . . . . . . . . 12 NN Pell14QR
2221ad4antr 737 . . . . . . . . . . 11 NN Pell14QR
2320, 22rereccld 10436 . . . . . . . . . 10 NN Pell14QR
249ad2antrr 731 . . . . . . . . . . 11 NN Pell14QR
25 simpr 463 . . . . . . . . . . . 12 NN Pell14QR
26 pell14qrre 35629 . . . . . . . . . . . . . . . . . 18 NN Pell14QR
2726recnd 9671 . . . . . . . . . . . . . . . . 17 NN Pell14QR
2827, 21reccld 10378 . . . . . . . . . . . . . . . 16 NN Pell14QR
2928ad3antrrr 735 . . . . . . . . . . . . . . 15 NN Pell14QR
30 nn0cn 10881 . . . . . . . . . . . . . . . . . 18
3130ad2antrl 733 . . . . . . . . . . . . . . . . 17 NN Pell14QR
32 eldifi 3588 . . . . . . . . . . . . . . . . . . . . 21 NN
3332nncnd 10627 . . . . . . . . . . . . . . . . . . . 20 NN
3433ad3antrrr 735 . . . . . . . . . . . . . . . . . . 19 NN Pell14QR
3534sqrtcld 13492 . . . . . . . . . . . . . . . . . 18 NN Pell14QR
36 zcn 10944 . . . . . . . . . . . . . . . . . . . 20
3736ad2antll 734 . . . . . . . . . . . . . . . . . . 19 NN Pell14QR
3837negcld 9975 . . . . . . . . . . . . . . . . . 18 NN Pell14QR
3935, 38mulcld 9665 . . . . . . . . . . . . . . . . 17 NN Pell14QR
4031, 39addcld 9664 . . . . . . . . . . . . . . . 16 NN Pell14QR
4140adantr 467 . . . . . . . . . . . . . . 15 NN Pell14QR
4227ad3antrrr 735 . . . . . . . . . . . . . . 15 NN Pell14QR
4321ad3antrrr 735 . . . . . . . . . . . . . . 15 NN Pell14QR
4427, 21recidd 10380 . . . . . . . . . . . . . . . . . 18 NN Pell14QR
4544ad3antrrr 735 . . . . . . . . . . . . . . . . 17 NN Pell14QR
46 simprr 765 . . . . . . . . . . . . . . . . 17 NN Pell14QR
4745, 46eqtr4d 2467 . . . . . . . . . . . . . . . 16 NN Pell14QR
4831adantr 467 . . . . . . . . . . . . . . . . . . 19 NN Pell14QR
4935, 37mulcld 9665 . . . . . . . . . . . . . . . . . . . 20 NN Pell14QR
5049adantr 467 . . . . . . . . . . . . . . . . . . 19 NN Pell14QR
51 subsq 12383 . . . . . . . . . . . . . . . . . . 19
5248, 50, 51syl2anc 666 . . . . . . . . . . . . . . . . . 18 NN Pell14QR
5335, 37sqmuld 12429 . . . . . . . . . . . . . . . . . . . . 21 NN Pell14QR
5434sqsqrtd 13494 . . . . . . . . . . . . . . . . . . . . . 22 NN Pell14QR
5554oveq1d 6318 . . . . . . . . . . . . . . . . . . . . 21 NN Pell14QR
5653, 55eqtr2d 2465 . . . . . . . . . . . . . . . . . . . 20 NN Pell14QR
5756oveq2d 6319 . . . . . . . . . . . . . . . . . . 19 NN Pell14QR
5857adantr 467 . . . . . . . . . . . . . . . . . 18 NN Pell14QR
59 simpr 463 . . . . . . . . . . . . . . . . . . 19 NN Pell14QR
6035, 37mulneg2d 10074 . . . . . . . . . . . . . . . . . . . . . 22 NN Pell14QR
6160oveq2d 6319 . . . . . . . . . . . . . . . . . . . . 21 NN Pell14QR
62 negsub 9924 . . . . . . . . . . . . . . . . . . . . . . 23
6362eqcomd 2431 . . . . . . . . . . . . . . . . . . . . . 22
6431, 49, 63syl2anc 666 . . . . . . . . . . . . . . . . . . . . 21 NN Pell14QR
6561, 64eqtr4d 2467 . . . . . . . . . . . . . . . . . . . 20 NN Pell14QR
6665adantr 467 . . . . . . . . . . . . . . . . . . 19 NN Pell14QR
6759, 66oveq12d 6321 . . . . . . . . . . . . . . . . . 18 NN Pell14QR
6852, 58, 673eqtr4d 2474 . . . . . . . . . . . . . . . . 17 NN Pell14QR
6968adantrr 722 . . . . . . . . . . . . . . . 16 NN Pell14QR
7047, 69eqtrd 2464 . . . . . . . . . . . . . . 15 NN Pell14QR
7129, 41, 42, 43, 70mulcanad 10249 . . . . . . . . . . . . . 14 NN Pell14QR
7271adantr 467 . . . . . . . . . . . . 13 NN Pell14QR
7337ad2antrr 731 . . . . . . . . . . . . . . . . 17 NN Pell14QR
74 sqneg 12336 . . . . . . . . . . . . . . . . 17
7573, 74syl 17 . . . . . . . . . . . . . . . 16 NN Pell14QR
7675oveq2d 6319 . . . . . . . . . . . . . . 15 NN Pell14QR
7776oveq2d 6319 . . . . . . . . . . . . . 14 NN Pell14QR
78 simplrr 770 . . . . . . . . . . . . . 14 NN Pell14QR
7977, 78eqtrd 2464 . . . . . . . . . . . . 13 NN Pell14QR
8072, 79jca 535 . . . . . . . . . . . 12 NN Pell14QR
81 oveq2 6311 . . . . . . . . . . . . . . . 16
8281oveq2d 6319 . . . . . . . . . . . . . . 15
8382eqeq2d 2437 . . . . . . . . . . . . . 14
84 oveq1 6310 . . . . . . . . . . . . . . . . 17
8584oveq2d 6319 . . . . . . . . . . . . . . . 16
8685oveq2d 6319 . . . . . . . . . . . . . . 15
8786eqeq1d 2425 . . . . . . . . . . . . . 14
8883, 87anbi12d 716 . . . . . . . . . . . . 13
8988rspcev 3183 . . . . . . . . . . . 12
9025, 80, 89syl2anc 666 . . . . . . . . . . 11 NN Pell14QR
91 rspe 2884 . . . . . . . . . . 11
9224, 90, 91syl2anc 666 . . . . . . . . . 10 NN Pell14QR
9323, 92jca 535 . . . . . . . . 9 NN Pell14QR
9493ex 436 . . . . . . . 8 NN Pell14QR
95 elpell1qr 35619 . . . . . . . . 9 NN Pell1QR
9695ad4antr 737 . . . . . . . 8 NN Pell14QR Pell1QR
9794, 96sylibrd 238 . . . . . . 7 NN Pell14QR Pell1QR
9819, 97orim12d 847 . . . . . 6 NN Pell14QR Pell1QR Pell1QR
996, 98mpd 15 . . . . 5 NN Pell14QR Pell1QR Pell1QR
10099ex 436 . . . 4 NN Pell14QR Pell1QR Pell1QR
101100rexlimdvva 2925 . . 3 NN Pell14QR Pell1QR Pell1QR
102101expimpd 607 . 2 NN Pell14QR Pell1QR Pell1QR
1032, 102mpd 15 1 NN Pell14QR Pell1QR Pell1QR
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wo 370   wa 371   wceq 1438   wcel 1869   wne 2619  wrex 2777   cdif 3434  cfv 5599  (class class class)co 6303  cc 9539  cr 9540  cc0 9541  c1 9542   caddc 9544   cmul 9546   cmin 9862  cneg 9863   cdiv 10271  cn 10611  c2 10661  cn0 10871  cz 10939  cexp 12273  csqrt 13290  ◻NNcsquarenn 35606  Pell1QRcpell1qr 35607  Pell14QRcpell14qr 35609 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658  ax-un 6595  ax-cnex 9597  ax-resscn 9598  ax-1cn 9599  ax-icn 9600  ax-addcl 9601  ax-addrcl 9602  ax-mulcl 9603  ax-mulrcl 9604  ax-mulcom 9605  ax-addass 9606  ax-mulass 9607  ax-distr 9608  ax-i2m1 9609  ax-1ne0 9610  ax-1rid 9611  ax-rnegex 9612  ax-rrecex 9613  ax-cnre 9614  ax-pre-lttri 9615  ax-pre-lttrn 9616  ax-pre-ltadd 9617  ax-pre-mulgt0 9618  ax-pre-sup 9619 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-nel 2622  df-ral 2781  df-rex 2782  df-reu 2783  df-rmo 2784  df-rab 2785  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3763  df-if 3911  df-pw 3982  df-sn 3998  df-pr 4000  df-tp 4002  df-op 4004  df-uni 4218  df-iun 4299  df-br 4422  df-opab 4481  df-mpt 4482  df-tr 4517  df-eprel 4762  df-id 4766  df-po 4772  df-so 4773  df-fr 4810  df-we 4812  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-pred 5397  df-ord 5443  df-on 5444  df-lim 5445  df-suc 5446  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-f1 5604  df-fo 5605  df-f1o 5606  df-fv 5607  df-riota 6265  df-ov 6306  df-oprab 6307  df-mpt2 6308  df-om 6705  df-2nd 6806  df-wrecs 7034  df-recs 7096  df-rdg 7134  df-er 7369  df-en 7576  df-dom 7577  df-sdom 7578  df-sup 7960  df-pnf 9679  df-mnf 9680  df-xr 9681  df-ltxr 9682  df-le 9683  df-sub 9864  df-neg 9865  df-div 10272  df-nn 10612  df-2 10670  df-3 10671  df-n0 10872  df-z 10940  df-uz 11162  df-rp 11305  df-seq 12215  df-exp 12274  df-cj 13156  df-re 13157  df-im 13158  df-sqrt 13292  df-abs 13293  df-pell1qr 35613  df-pell14qr 35614  df-pell1234qr 35615 This theorem is referenced by:  elpell1qr2  35644
 Copyright terms: Public domain W3C validator