Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pell14qrre Structured version   Visualization version   GIF version

Theorem pell14qrre 40410
Description: A positive Pell solution is a real number. (Contributed by Stefan O'Rear, 18-Sep-2014.)
Assertion
Ref Expression
pell14qrre ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 𝐴 ∈ ℝ)

Proof of Theorem pell14qrre
StepHypRef Expression
1 pell14qrss1234 40409 . . 3 (𝐷 ∈ (ℕ ∖ ◻NN) → (Pell14QR‘𝐷) ⊆ (Pell1234QR‘𝐷))
21sselda 3915 . 2 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 𝐴 ∈ (Pell1234QR‘𝐷))
3 pell1234qrre 40405 . 2 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷)) → 𝐴 ∈ ℝ)
42, 3syldan 594 1 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2111  cdif 3877  cfv 6397  cr 10752  cn 11854  NNcsquarenn 40389  Pell1234QRcpell1234qr 40391  Pell14QRcpell14qr 40392
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-sep 5206  ax-nul 5213  ax-pr 5336  ax-un 7541  ax-cnex 10809  ax-resscn 10810  ax-1cn 10811  ax-icn 10812  ax-addcl 10813  ax-addrcl 10814  ax-mulcl 10815  ax-mulrcl 10816  ax-i2m1 10821  ax-1ne0 10822  ax-rnegex 10824  ax-rrecex 10825  ax-cnre 10826
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-ral 3067  df-rex 3068  df-reu 3069  df-rab 3071  df-v 3422  df-sbc 3709  df-csb 3826  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-pss 3899  df-nul 4252  df-if 4454  df-pw 4529  df-sn 4556  df-pr 4558  df-tp 4560  df-op 4562  df-uni 4834  df-iun 4920  df-br 5068  df-opab 5130  df-mpt 5150  df-tr 5176  df-id 5469  df-eprel 5474  df-po 5482  df-so 5483  df-fr 5523  df-we 5525  df-xp 5571  df-rel 5572  df-cnv 5573  df-co 5574  df-dm 5575  df-rn 5576  df-res 5577  df-ima 5578  df-pred 6175  df-ord 6233  df-on 6234  df-lim 6235  df-suc 6236  df-iota 6355  df-fun 6399  df-fn 6400  df-f 6401  df-f1 6402  df-fo 6403  df-f1o 6404  df-fv 6405  df-ov 7234  df-om 7663  df-wrecs 8067  df-recs 8128  df-rdg 8166  df-neg 11089  df-nn 11855  df-n0 12115  df-z 12201  df-pell14qr 40396  df-pell1234qr 40397
This theorem is referenced by:  pell14qrrp  40413  pell14qrdivcl  40418  pell14qrexpclnn0  40419  pell14qrexpcl  40420  pell14qrdich  40422  elpell1qr2  40425  pell14qrgap  40428  pell14qrgapw  40429  pellfundre  40434  pellfundge  40435  pellfundlb  40437  pellfundglb  40438  pellfundex  40439  pellfund14gap  40440  pellfund14  40451
  Copyright terms: Public domain W3C validator