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

Theorem pellfundex 29152
 Description: The fundamental solution as an infimum is itself a solution, showing that the solution set is discrete. Since the fundamental solution is an infimum, there must be an element ge to Fund and lt 2*Fund. If this element is equal to the fundamental solution we're done, otherwise use the infimum again to find another element which must be ge Fund and lt the first element; their ratio is a group element in (1,2), contradicting pell14qrgapw 29142. (Contributed by Stefan O'Rear, 18-Sep-2014.)
Assertion
Ref Expression
pellfundex NN PellFund Pell1QR

Proof of Theorem pellfundex
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 2re 10387 . . . 4
2 pellfundre 29147 . . . 4 NN PellFund
3 remulcl 9363 . . . 4 PellFund PellFund
41, 2, 3sylancr 658 . . 3 NN PellFund
5 0re 9382 . . . . . . . 8
65a1i 11 . . . . . . 7 NN
7 1re 9381 . . . . . . . 8
87a1i 11 . . . . . . 7 NN
9 0lt1 9858 . . . . . . . 8
109a1i 11 . . . . . . 7 NN
11 pellfundgt1 29149 . . . . . . 7 NN PellFund
126, 8, 2, 10, 11lttrd 9528 . . . . . 6 NN PellFund
132, 12elrpd 11021 . . . . 5 NN PellFund
142, 13ltaddrpd 11052 . . . 4 NN PellFund PellFund PellFund
152recnd 9408 . . . . 5 NN PellFund
16152timesd 10563 . . . 4 NN PellFund PellFund PellFund
1714, 16breqtrrd 4315 . . 3 NN PellFund PellFund
18 pellfundglb 29151 . . 3 NN PellFund PellFund PellFund Pell1QRPellFund PellFund
194, 17, 18mpd3an23 1311 . 2 NN Pell1QRPellFund PellFund
202adantr 462 . . . . . 6 NN Pell1QR PellFund
21 pell1qrss14 29134 . . . . . . . 8 NN Pell1QR Pell14QR
2221sselda 3353 . . . . . . 7 NN Pell1QR Pell14QR
23 pell14qrre 29123 . . . . . . 7 NN Pell14QR
2422, 23syldan 467 . . . . . 6 NN Pell1QR
2520, 24leloed 9513 . . . . 5 NN Pell1QR PellFund PellFund PellFund
26 simpll 748 . . . . . . . . 9 NN Pell1QR PellFund PellFund NN
2724adantr 462 . . . . . . . . 9 NN Pell1QR PellFund PellFund
28 simprl 750 . . . . . . . . 9 NN Pell1QR PellFund PellFund PellFund
29 pellfundglb 29151 . . . . . . . . 9 NN PellFund Pell1QRPellFund
3026, 27, 28, 29syl3anc 1213 . . . . . . . 8 NN Pell1QR PellFund PellFund Pell1QRPellFund
31 simp-4l 760 . . . . . . . . . . 11 NN Pell1QR PellFund PellFund Pell1QR PellFund NN
32 simp-4r 761 . . . . . . . . . . 11 NN Pell1QR PellFund PellFund Pell1QR PellFund Pell1QR
33 simplr 749 . . . . . . . . . . 11 NN Pell1QR PellFund PellFund Pell1QR PellFund Pell1QR
34 simprr 751 . . . . . . . . . . 11 NN Pell1QR PellFund PellFund Pell1QR PellFund
3524ad3antrrr 724 . . . . . . . . . . . 12 NN Pell1QR PellFund PellFund Pell1QR PellFund
364adantr 462 . . . . . . . . . . . . 13 NN Pell1QR PellFund
3736ad3antrrr 724 . . . . . . . . . . . 12 NN Pell1QR PellFund PellFund Pell1QR PellFund PellFund
3821adantr 462 . . . . . . . . . . . . . . . 16 NN Pell1QR Pell1QR Pell14QR
3938ad3antrrr 724 . . . . . . . . . . . . . . 15 NN Pell1QR PellFund PellFund Pell1QR PellFund Pell1QR Pell14QR
4039, 33sseldd 3354 . . . . . . . . . . . . . 14 NN Pell1QR PellFund PellFund Pell1QR PellFund Pell14QR
41 pell14qrre 29123 . . . . . . . . . . . . . 14 NN Pell14QR
4231, 40, 41syl2anc 656 . . . . . . . . . . . . 13 NN Pell1QR PellFund PellFund Pell1QR PellFund
43 remulcl 9363 . . . . . . . . . . . . 13
441, 42, 43sylancr 658 . . . . . . . . . . . 12 NN Pell1QR PellFund PellFund Pell1QR PellFund
45 simprr 751 . . . . . . . . . . . . 13 NN Pell1QR PellFund PellFund PellFund
4645ad2antrr 720 . . . . . . . . . . . 12 NN Pell1QR PellFund PellFund Pell1QR PellFund PellFund
47 simprl 750 . . . . . . . . . . . . 13 NN Pell1QR PellFund PellFund Pell1QR PellFund PellFund
4820ad3antrrr 724 . . . . . . . . . . . . . 14 NN Pell1QR PellFund PellFund Pell1QR PellFund PellFund
491a1i 11 . . . . . . . . . . . . . 14 NN Pell1QR PellFund PellFund Pell1QR PellFund
50 2pos 10409 . . . . . . . . . . . . . . 15
5150a1i 11 . . . . . . . . . . . . . 14 NN Pell1QR PellFund PellFund Pell1QR PellFund
52 lemul2 10178 . . . . . . . . . . . . . 14 PellFund PellFund PellFund
5348, 42, 49, 51, 52syl112anc 1217 . . . . . . . . . . . . 13 NN Pell1QR PellFund PellFund Pell1QR PellFund PellFund PellFund
5447, 53mpbid 210 . . . . . . . . . . . 12 NN Pell1QR PellFund PellFund Pell1QR PellFund PellFund
5535, 37, 44, 46, 54ltletrd 9527 . . . . . . . . . . 11 NN Pell1QR PellFund PellFund Pell1QR PellFund
56 simp1 983 . . . . . . . . . . . 12 NN Pell1QR Pell1QR NN
57213ad2ant1 1004 . . . . . . . . . . . . . 14 NN Pell1QR Pell1QR Pell1QR Pell14QR
58 simp2l 1009 . . . . . . . . . . . . . 14 NN Pell1QR Pell1QR Pell1QR
5957, 58sseldd 3354 . . . . . . . . . . . . 13 NN Pell1QR Pell1QR Pell14QR
60 simp2r 1010 . . . . . . . . . . . . . 14 NN Pell1QR Pell1QR Pell1QR
6157, 60sseldd 3354 . . . . . . . . . . . . 13 NN Pell1QR Pell1QR Pell14QR
62 pell14qrdivcl 29131 . . . . . . . . . . . . 13 NN Pell14QR Pell14QR Pell14QR
6356, 59, 61, 62syl3anc 1213 . . . . . . . . . . . 12 NN Pell1QR Pell1QR Pell14QR
6456, 61, 41syl2anc 656 . . . . . . . . . . . . . . . 16 NN Pell1QR Pell1QR
6564recnd 9408 . . . . . . . . . . . . . . 15 NN Pell1QR Pell1QR
6665mulid2d 9400 . . . . . . . . . . . . . 14 NN Pell1QR Pell1QR
67 simp3l 1011 . . . . . . . . . . . . . 14 NN Pell1QR Pell1QR
6866, 67eqbrtrd 4309 . . . . . . . . . . . . 13 NN Pell1QR Pell1QR
697a1i 11 . . . . . . . . . . . . . 14 NN Pell1QR Pell1QR
7056, 59, 23syl2anc 656 . . . . . . . . . . . . . 14 NN Pell1QR Pell1QR
71 pell14qrgt0 29125 . . . . . . . . . . . . . . 15 NN Pell14QR
7256, 61, 71syl2anc 656 . . . . . . . . . . . . . 14 NN Pell1QR Pell1QR
73 ltmuldiv 10198 . . . . . . . . . . . . . 14
7469, 70, 64, 72, 73syl112anc 1217 . . . . . . . . . . . . 13 NN Pell1QR Pell1QR
7568, 74mpbid 210 . . . . . . . . . . . 12 NN Pell1QR Pell1QR
76 simp3r 1012 . . . . . . . . . . . . 13 NN Pell1QR Pell1QR
771a1i 11 . . . . . . . . . . . . . 14 NN Pell1QR Pell1QR
78 ltdivmul2 10203 . . . . . . . . . . . . . 14
7970, 77, 64, 72, 78syl112anc 1217 . . . . . . . . . . . . 13 NN Pell1QR Pell1QR
8076, 79mpbird 232 . . . . . . . . . . . 12 NN Pell1QR Pell1QR
81 simprr 751 . . . . . . . . . . . . 13 NN Pell14QR
82 simpll 748 . . . . . . . . . . . . . . 15 NN Pell14QR NN
83 simplr 749 . . . . . . . . . . . . . . 15 NN Pell14QR Pell14QR
84 simprl 750 . . . . . . . . . . . . . . 15 NN Pell14QR
85 pell14qrgapw 29142 . . . . . . . . . . . . . . 15 NN Pell14QR
8682, 83, 84, 85syl3anc 1213 . . . . . . . . . . . . . 14 NN Pell14QR
87 pell14qrre 29123 . . . . . . . . . . . . . . . 16 NN Pell14QR
8887adantr 462 . . . . . . . . . . . . . . 15 NN Pell14QR
89 ltnsym 9469 . . . . . . . . . . . . . . 15
901, 88, 89sylancr 658 . . . . . . . . . . . . . 14 NN Pell14QR
9186, 90mpd 15 . . . . . . . . . . . . 13 NN Pell14QR
9281, 91pm2.21dd 174 . . . . . . . . . . . 12 NN Pell14QR PellFund Pell1QR
9356, 63, 75, 80, 92syl22anc 1214 . . . . . . . . . . 11 NN Pell1QR Pell1QR PellFund Pell1QR
9431, 32, 33, 34, 55, 93syl122anc 1222 . . . . . . . . . 10 NN Pell1QR PellFund PellFund Pell1QR PellFund PellFund Pell1QR
9594ex 434 . . . . . . . . 9 NN Pell1QR PellFund PellFund Pell1QR PellFund PellFund Pell1QR
9695rexlimdva 2839 . . . . . . . 8 NN Pell1QR PellFund PellFund Pell1QRPellFund PellFund Pell1QR
9730, 96mpd 15 . . . . . . 7 NN Pell1QR PellFund PellFund PellFund Pell1QR
9897exp32 602 . . . . . 6 NN Pell1QR PellFund PellFund PellFund Pell1QR
99 simp2 984 . . . . . . . 8 NN Pell1QR PellFund PellFund PellFund
100 simp1r 1008 . . . . . . . 8 NN Pell1QR PellFund PellFund Pell1QR
10199, 100eqeltrd 2515 . . . . . . 7 NN Pell1QR PellFund PellFund PellFund Pell1QR
1021013exp 1181 . . . . . 6 NN Pell1QR PellFund PellFund PellFund Pell1QR
10398, 102jaod 380 . . . . 5 NN Pell1QR PellFund PellFund PellFund PellFund Pell1QR
10425, 103sylbid 215 . . . 4 NN Pell1QR PellFund PellFund PellFund Pell1QR
105104imp3a 431 . . 3 NN Pell1QR PellFund PellFund PellFund Pell1QR
106105rexlimdva 2839 . 2 NN Pell1QRPellFund PellFund PellFund Pell1QR
10719, 106mpd 15 1 NN PellFund Pell1QR
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 184   wo 368   wa 369   w3a 960   wceq 1364   wcel 1761  wrex 2714   cdif 3322   wss 3325   class class class wbr 4289  cfv 5415  (class class class)co 6090  cr 9277  cc0 9278  c1 9279   caddc 9281   cmul 9283   clt 9414   cle 9415   cdiv 9989  cn 10318  c2 10367  ◻NNcsquarenn 29102  Pell1QRcpell1qr 29103  Pell14QRcpell14qr 29105  PellFundcpellfund 29106 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-inf2 7843  ax-cnex 9334  ax-resscn 9335  ax-1cn 9336  ax-icn 9337  ax-addcl 9338  ax-addrcl 9339  ax-mulcl 9340  ax-mulrcl 9341  ax-mulcom 9342  ax-addass 9343  ax-mulass 9344  ax-distr 9345  ax-i2m1 9346  ax-1ne0 9347  ax-1rid 9348  ax-rnegex 9349  ax-rrecex 9350  ax-cnre 9351  ax-pre-lttri 9352  ax-pre-lttrn 9353  ax-pre-ltadd 9354  ax-pre-mulgt0 9355  ax-pre-sup 9356 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-nel 2607  df-ral 2718  df-rex 2719  df-reu 2720  df-rmo 2721  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-int 4126  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-tr 4383  df-eprel 4628  df-id 4632  df-po 4637  df-so 4638  df-fr 4675  df-se 4676  df-we 4677  df-ord 4718  df-on 4719  df-lim 4720  df-suc 4721  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-isom 5424  df-riota 6049  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-om 6476  df-1st 6576  df-2nd 6577  df-recs 6828  df-rdg 6862  df-1o 6916  df-oadd 6920  df-omul 6921  df-er 7097  df-map 7212  df-en 7307  df-dom 7308  df-sdom 7309  df-fin 7310  df-sup 7687  df-oi 7720  df-card 8105  df-acn 8108  df-pnf 9416  df-mnf 9417  df-xr 9418  df-ltxr 9419  df-le 9420  df-sub 9593  df-neg 9594  df-div 9990  df-nn 10319  df-2 10376  df-3 10377  df-n0 10576  df-z 10643  df-uz 10858  df-q 10950  df-rp 10988  df-ico 11302  df-fz 11434  df-fl 11638  df-mod 11705  df-seq 11803  df-exp 11862  df-hash 12100  df-cj 12584  df-re 12585  df-im 12586  df-sqr 12720  df-abs 12721  df-dvds 13532  df-gcd 13687  df-numer 13809  df-denom 13810  df-squarenn 29107  df-pell1qr 29108  df-pell14qr 29109  df-pell1234qr 29110  df-pellfund 29111 This theorem is referenced by:  pellfund14  29164  pellfund14b  29165
 Copyright terms: Public domain W3C validator