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

Theorem pellfundex 38993
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 38983. (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 11564 . . . 4 2 ∈ ℝ
2 pellfundre 38988 . . . 4 (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ ℝ)
3 remulcl 10473 . . . 4 ((2 ∈ ℝ ∧ (PellFund‘𝐷) ∈ ℝ) → (2 · (PellFund‘𝐷)) ∈ ℝ)
41, 2, 3sylancr 587 . . 3 (𝐷 ∈ (ℕ ∖ ◻NN) → (2 · (PellFund‘𝐷)) ∈ ℝ)
5 0red 10495 . . . . . . 7 (𝐷 ∈ (ℕ ∖ ◻NN) → 0 ∈ ℝ)
6 1red 10493 . . . . . . 7 (𝐷 ∈ (ℕ ∖ ◻NN) → 1 ∈ ℝ)
7 0lt1 11015 . . . . . . . 8 0 < 1
87a1i 11 . . . . . . 7 (𝐷 ∈ (ℕ ∖ ◻NN) → 0 < 1)
9 pellfundgt1 38990 . . . . . . 7 (𝐷 ∈ (ℕ ∖ ◻NN) → 1 < (PellFund‘𝐷))
105, 6, 2, 8, 9lttrd 10653 . . . . . 6 (𝐷 ∈ (ℕ ∖ ◻NN) → 0 < (PellFund‘𝐷))
112, 10elrpd 12283 . . . . 5 (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ ℝ+)
122, 11ltaddrpd 12319 . . . 4 (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) < ((PellFund‘𝐷) + (PellFund‘𝐷)))
132recnd 10520 . . . . 5 (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ ℂ)
14132timesd 11733 . . . 4 (𝐷 ∈ (ℕ ∖ ◻NN) → (2 · (PellFund‘𝐷)) = ((PellFund‘𝐷) + (PellFund‘𝐷)))
1512, 14breqtrrd 4994 . . 3 (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) < (2 · (PellFund‘𝐷)))
16 pellfundglb 38992 . . 3 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (2 · (PellFund‘𝐷)) ∈ ℝ ∧ (PellFund‘𝐷) < (2 · (PellFund‘𝐷))) → ∃𝑎 ∈ (Pell1QR‘𝐷)((PellFund‘𝐷) ≤ 𝑎𝑎 < (2 · (PellFund‘𝐷))))
174, 15, 16mpd3an23 1455 . 2 (𝐷 ∈ (ℕ ∖ ◻NN) → ∃𝑎 ∈ (Pell1QR‘𝐷)((PellFund‘𝐷) ≤ 𝑎𝑎 < (2 · (PellFund‘𝐷))))
182adantr 481 . . . . . 6 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → (PellFund‘𝐷) ∈ ℝ)
19 pell1qrss14 38975 . . . . . . . 8 (𝐷 ∈ (ℕ ∖ ◻NN) → (Pell1QR‘𝐷) ⊆ (Pell14QR‘𝐷))
2019sselda 3893 . . . . . . 7 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → 𝑎 ∈ (Pell14QR‘𝐷))
21 pell14qrre 38964 . . . . . . 7 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell14QR‘𝐷)) → 𝑎 ∈ ℝ)
2220, 21syldan 591 . . . . . 6 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → 𝑎 ∈ ℝ)
2318, 22leloed 10635 . . . . 5 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → ((PellFund‘𝐷) ≤ 𝑎 ↔ ((PellFund‘𝐷) < 𝑎 ∨ (PellFund‘𝐷) = 𝑎)))
24 simp-4l 779 . . . . . . . . 9 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → 𝐷 ∈ (ℕ ∖ ◻NN))
25 simp-4r 780 . . . . . . . . 9 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → 𝑎 ∈ (Pell1QR‘𝐷))
26 simplr 765 . . . . . . . . 9 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → 𝑏 ∈ (Pell1QR‘𝐷))
27 simprr 769 . . . . . . . . 9 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → 𝑏 < 𝑎)
2822ad3antrrr 726 . . . . . . . . . 10 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → 𝑎 ∈ ℝ)
294ad4antr 728 . . . . . . . . . 10 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → (2 · (PellFund‘𝐷)) ∈ ℝ)
3019ad4antr 728 . . . . . . . . . . . . 13 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → (Pell1QR‘𝐷) ⊆ (Pell14QR‘𝐷))
3130, 26sseldd 3894 . . . . . . . . . . . 12 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → 𝑏 ∈ (Pell14QR‘𝐷))
32 pell14qrre 38964 . . . . . . . . . . . 12 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑏 ∈ (Pell14QR‘𝐷)) → 𝑏 ∈ ℝ)
3324, 31, 32syl2anc 584 . . . . . . . . . . 11 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → 𝑏 ∈ ℝ)
34 remulcl 10473 . . . . . . . . . . 11 ((2 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (2 · 𝑏) ∈ ℝ)
351, 33, 34sylancr 587 . . . . . . . . . 10 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → (2 · 𝑏) ∈ ℝ)
36 simprr 769 . . . . . . . . . . 11 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) → 𝑎 < (2 · (PellFund‘𝐷)))
3736ad2antrr 722 . . . . . . . . . 10 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → 𝑎 < (2 · (PellFund‘𝐷)))
38 simprl 767 . . . . . . . . . . 11 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → (PellFund‘𝐷) ≤ 𝑏)
392ad4antr 728 . . . . . . . . . . . 12 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → (PellFund‘𝐷) ∈ ℝ)
401a1i 11 . . . . . . . . . . . 12 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → 2 ∈ ℝ)
41 2pos 11593 . . . . . . . . . . . . 13 0 < 2
4241a1i 11 . . . . . . . . . . . 12 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → 0 < 2)
43 lemul2 11346 . . . . . . . . . . . 12 (((PellFund‘𝐷) ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((PellFund‘𝐷) ≤ 𝑏 ↔ (2 · (PellFund‘𝐷)) ≤ (2 · 𝑏)))
4439, 33, 40, 42, 43syl112anc 1367 . . . . . . . . . . 11 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → ((PellFund‘𝐷) ≤ 𝑏 ↔ (2 · (PellFund‘𝐷)) ≤ (2 · 𝑏)))
4538, 44mpbid 233 . . . . . . . . . 10 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → (2 · (PellFund‘𝐷)) ≤ (2 · 𝑏))
4628, 29, 35, 37, 45ltletrd 10652 . . . . . . . . 9 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → 𝑎 < (2 · 𝑏))
47 simp1 1129 . . . . . . . . . 10 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → 𝐷 ∈ (ℕ ∖ ◻NN))
48193ad2ant1 1126 . . . . . . . . . . . 12 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → (Pell1QR‘𝐷) ⊆ (Pell14QR‘𝐷))
49 simp2l 1192 . . . . . . . . . . . 12 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → 𝑎 ∈ (Pell1QR‘𝐷))
5048, 49sseldd 3894 . . . . . . . . . . 11 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → 𝑎 ∈ (Pell14QR‘𝐷))
51 simp2r 1193 . . . . . . . . . . . 12 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → 𝑏 ∈ (Pell1QR‘𝐷))
5248, 51sseldd 3894 . . . . . . . . . . 11 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → 𝑏 ∈ (Pell14QR‘𝐷))
53 pell14qrdivcl 38972 . . . . . . . . . . 11 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell14QR‘𝐷) ∧ 𝑏 ∈ (Pell14QR‘𝐷)) → (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷))
5447, 50, 52, 53syl3anc 1364 . . . . . . . . . 10 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷))
5547, 52, 32syl2anc 584 . . . . . . . . . . . . . 14 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → 𝑏 ∈ ℝ)
5655recnd 10520 . . . . . . . . . . . . 13 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → 𝑏 ∈ ℂ)
5756mulid2d 10510 . . . . . . . . . . . 12 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → (1 · 𝑏) = 𝑏)
58 simp3l 1194 . . . . . . . . . . . 12 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → 𝑏 < 𝑎)
5957, 58eqbrtrd 4988 . . . . . . . . . . 11 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → (1 · 𝑏) < 𝑎)
60 1red 10493 . . . . . . . . . . . 12 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → 1 ∈ ℝ)
6147, 50, 21syl2anc 584 . . . . . . . . . . . 12 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → 𝑎 ∈ ℝ)
62 pell14qrgt0 38966 . . . . . . . . . . . . 13 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑏 ∈ (Pell14QR‘𝐷)) → 0 < 𝑏)
6347, 52, 62syl2anc 584 . . . . . . . . . . . 12 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → 0 < 𝑏)
64 ltmuldiv 11366 . . . . . . . . . . . 12 ((1 ∈ ℝ ∧ 𝑎 ∈ ℝ ∧ (𝑏 ∈ ℝ ∧ 0 < 𝑏)) → ((1 · 𝑏) < 𝑎 ↔ 1 < (𝑎 / 𝑏)))
6560, 61, 55, 63, 64syl112anc 1367 . . . . . . . . . . 11 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → ((1 · 𝑏) < 𝑎 ↔ 1 < (𝑎 / 𝑏)))
6659, 65mpbid 233 . . . . . . . . . 10 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → 1 < (𝑎 / 𝑏))
67 simp3r 1195 . . . . . . . . . . 11 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → 𝑎 < (2 · 𝑏))
681a1i 11 . . . . . . . . . . . 12 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → 2 ∈ ℝ)
69 ltdivmul2 11370 . . . . . . . . . . . 12 ((𝑎 ∈ ℝ ∧ 2 ∈ ℝ ∧ (𝑏 ∈ ℝ ∧ 0 < 𝑏)) → ((𝑎 / 𝑏) < 2 ↔ 𝑎 < (2 · 𝑏)))
7061, 68, 55, 63, 69syl112anc 1367 . . . . . . . . . . 11 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → ((𝑎 / 𝑏) < 2 ↔ 𝑎 < (2 · 𝑏)))
7167, 70mpbird 258 . . . . . . . . . 10 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → (𝑎 / 𝑏) < 2)
72 simprr 769 . . . . . . . . . . 11 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → (𝑎 / 𝑏) < 2)
73 simpll 763 . . . . . . . . . . . . 13 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → 𝐷 ∈ (ℕ ∖ ◻NN))
74 simplr 765 . . . . . . . . . . . . 13 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷))
75 simprl 767 . . . . . . . . . . . . 13 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → 1 < (𝑎 / 𝑏))
76 pell14qrgapw 38983 . . . . . . . . . . . . 13 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷) ∧ 1 < (𝑎 / 𝑏)) → 2 < (𝑎 / 𝑏))
7773, 74, 75, 76syl3anc 1364 . . . . . . . . . . . 12 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → 2 < (𝑎 / 𝑏))
78 pell14qrre 38964 . . . . . . . . . . . . . 14 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) → (𝑎 / 𝑏) ∈ ℝ)
7978adantr 481 . . . . . . . . . . . . 13 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → (𝑎 / 𝑏) ∈ ℝ)
80 ltnsym 10590 . . . . . . . . . . . . 13 ((2 ∈ ℝ ∧ (𝑎 / 𝑏) ∈ ℝ) → (2 < (𝑎 / 𝑏) → ¬ (𝑎 / 𝑏) < 2))
811, 79, 80sylancr 587 . . . . . . . . . . . 12 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → (2 < (𝑎 / 𝑏) → ¬ (𝑎 / 𝑏) < 2))
8277, 81mpd 15 . . . . . . . . . . 11 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → ¬ (𝑎 / 𝑏) < 2)
8372, 82pm2.21dd 196 . . . . . . . . . 10 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷))
8447, 54, 66, 71, 83syl22anc 835 . . . . . . . . 9 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷))
8524, 25, 26, 27, 46, 84syl122anc 1372 . . . . . . . 8 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷))
86 simpll 763 . . . . . . . . 9 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) → 𝐷 ∈ (ℕ ∖ ◻NN))
8722adantr 481 . . . . . . . . 9 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) → 𝑎 ∈ ℝ)
88 simprl 767 . . . . . . . . 9 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) → (PellFund‘𝐷) < 𝑎)
89 pellfundglb 38992 . . . . . . . . 9 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ ℝ ∧ (PellFund‘𝐷) < 𝑎) → ∃𝑏 ∈ (Pell1QR‘𝐷)((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎))
9086, 87, 88, 89syl3anc 1364 . . . . . . . 8 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) → ∃𝑏 ∈ (Pell1QR‘𝐷)((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎))
9185, 90r19.29a 3252 . . . . . . 7 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷))
9291exp32 421 . . . . . 6 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → ((PellFund‘𝐷) < 𝑎 → (𝑎 < (2 · (PellFund‘𝐷)) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷))))
93 simp2 1130 . . . . . . . 8 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ (PellFund‘𝐷) = 𝑎𝑎 < (2 · (PellFund‘𝐷))) → (PellFund‘𝐷) = 𝑎)
94 simp1r 1191 . . . . . . . 8 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ (PellFund‘𝐷) = 𝑎𝑎 < (2 · (PellFund‘𝐷))) → 𝑎 ∈ (Pell1QR‘𝐷))
9593, 94eqeltrd 2883 . . . . . . 7 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ (PellFund‘𝐷) = 𝑎𝑎 < (2 · (PellFund‘𝐷))) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷))
96953exp 1112 . . . . . 6 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → ((PellFund‘𝐷) = 𝑎 → (𝑎 < (2 · (PellFund‘𝐷)) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷))))
9792, 96jaod 854 . . . . 5 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → (((PellFund‘𝐷) < 𝑎 ∨ (PellFund‘𝐷) = 𝑎) → (𝑎 < (2 · (PellFund‘𝐷)) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷))))
9823, 97sylbid 241 . . . 4 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → ((PellFund‘𝐷) ≤ 𝑎 → (𝑎 < (2 · (PellFund‘𝐷)) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷))))
9998impd 411 . . 3 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → (((PellFund‘𝐷) ≤ 𝑎𝑎 < (2 · (PellFund‘𝐷))) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷)))
10099rexlimdva 3247 . 2 (𝐷 ∈ (ℕ ∖ ◻NN) → (∃𝑎 ∈ (Pell1QR‘𝐷)((PellFund‘𝐷) ≤ 𝑎𝑎 < (2 · (PellFund‘𝐷))) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷)))
10117, 100mpd 15 1 (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 842  w3a 1080   = wceq 1522  wcel 2081  wrex 3106  cdif 3860  wss 3863   class class class wbr 4966  cfv 6230  (class class class)co 7021  cr 10387  0cc0 10388  1c1 10389   + caddc 10391   · cmul 10393   < clt 10526  cle 10527   / cdiv 11150  cn 11491  2c2 11545  NNcsquarenn 38943  Pell1QRcpell1qr 38944  Pell14QRcpell14qr 38946  PellFundcpellfund 38947
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5086  ax-sep 5099  ax-nul 5106  ax-pow 5162  ax-pr 5226  ax-un 7324  ax-inf2 8955  ax-cnex 10444  ax-resscn 10445  ax-1cn 10446  ax-icn 10447  ax-addcl 10448  ax-addrcl 10449  ax-mulcl 10450  ax-mulrcl 10451  ax-mulcom 10452  ax-addass 10453  ax-mulass 10454  ax-distr 10455  ax-i2m1 10456  ax-1ne0 10457  ax-1rid 10458  ax-rnegex 10459  ax-rrecex 10460  ax-cnre 10461  ax-pre-lttri 10462  ax-pre-lttrn 10463  ax-pre-ltadd 10464  ax-pre-mulgt0 10465  ax-pre-sup 10466
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-reu 3112  df-rmo 3113  df-rab 3114  df-v 3439  df-sbc 3710  df-csb 3816  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-pss 3880  df-nul 4216  df-if 4386  df-pw 4459  df-sn 4477  df-pr 4479  df-tp 4481  df-op 4483  df-uni 4750  df-int 4787  df-iun 4831  df-br 4967  df-opab 5029  df-mpt 5046  df-tr 5069  df-id 5353  df-eprel 5358  df-po 5367  df-so 5368  df-fr 5407  df-se 5408  df-we 5409  df-xp 5454  df-rel 5455  df-cnv 5456  df-co 5457  df-dm 5458  df-rn 5459  df-res 5460  df-ima 5461  df-pred 6028  df-ord 6074  df-on 6075  df-lim 6076  df-suc 6077  df-iota 6194  df-fun 6232  df-fn 6233  df-f 6234  df-f1 6235  df-fo 6236  df-f1o 6237  df-fv 6238  df-isom 6239  df-riota 6982  df-ov 7024  df-oprab 7025  df-mpo 7026  df-om 7442  df-1st 7550  df-2nd 7551  df-wrecs 7803  df-recs 7865  df-rdg 7903  df-1o 7958  df-oadd 7962  df-omul 7963  df-er 8144  df-map 8263  df-en 8363  df-dom 8364  df-sdom 8365  df-fin 8366  df-sup 8757  df-inf 8758  df-oi 8825  df-card 9219  df-acn 9222  df-pnf 10528  df-mnf 10529  df-xr 10530  df-ltxr 10531  df-le 10532  df-sub 10724  df-neg 10725  df-div 11151  df-nn 11492  df-2 11553  df-3 11554  df-n0 11751  df-xnn0 11821  df-z 11835  df-uz 12099  df-q 12203  df-rp 12245  df-ico 12599  df-fz 12748  df-fl 13017  df-mod 13093  df-seq 13225  df-exp 13285  df-hash 13546  df-cj 14297  df-re 14298  df-im 14299  df-sqrt 14433  df-abs 14434  df-dvds 15446  df-gcd 15682  df-numer 15909  df-denom 15910  df-squarenn 38948  df-pell1qr 38949  df-pell14qr 38950  df-pell1234qr 38951  df-pellfund 38952
This theorem is referenced by:  pellfund14  39005  pellfund14b  39006
  Copyright terms: Public domain W3C validator