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 42202
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 42192. (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 12290 . . . 4 2 ∈ ℝ
2 pellfundre 42197 . . . 4 (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ ℝ)
3 remulcl 11197 . . . 4 ((2 ∈ ℝ ∧ (PellFund‘𝐷) ∈ ℝ) → (2 · (PellFund‘𝐷)) ∈ ℝ)
41, 2, 3sylancr 586 . . 3 (𝐷 ∈ (ℕ ∖ ◻NN) → (2 · (PellFund‘𝐷)) ∈ ℝ)
5 0red 11221 . . . . . . 7 (𝐷 ∈ (ℕ ∖ ◻NN) → 0 ∈ ℝ)
6 1red 11219 . . . . . . 7 (𝐷 ∈ (ℕ ∖ ◻NN) → 1 ∈ ℝ)
7 0lt1 11740 . . . . . . . 8 0 < 1
87a1i 11 . . . . . . 7 (𝐷 ∈ (ℕ ∖ ◻NN) → 0 < 1)
9 pellfundgt1 42199 . . . . . . 7 (𝐷 ∈ (ℕ ∖ ◻NN) → 1 < (PellFund‘𝐷))
105, 6, 2, 8, 9lttrd 11379 . . . . . 6 (𝐷 ∈ (ℕ ∖ ◻NN) → 0 < (PellFund‘𝐷))
112, 10elrpd 13019 . . . . 5 (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ ℝ+)
122, 11ltaddrpd 13055 . . . 4 (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) < ((PellFund‘𝐷) + (PellFund‘𝐷)))
132recnd 11246 . . . . 5 (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ ℂ)
14132timesd 12459 . . . 4 (𝐷 ∈ (ℕ ∖ ◻NN) → (2 · (PellFund‘𝐷)) = ((PellFund‘𝐷) + (PellFund‘𝐷)))
1512, 14breqtrrd 5169 . . 3 (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) < (2 · (PellFund‘𝐷)))
16 pellfundglb 42201 . . 3 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (2 · (PellFund‘𝐷)) ∈ ℝ ∧ (PellFund‘𝐷) < (2 · (PellFund‘𝐷))) → ∃𝑎 ∈ (Pell1QR‘𝐷)((PellFund‘𝐷) ≤ 𝑎𝑎 < (2 · (PellFund‘𝐷))))
174, 15, 16mpd3an23 1459 . 2 (𝐷 ∈ (ℕ ∖ ◻NN) → ∃𝑎 ∈ (Pell1QR‘𝐷)((PellFund‘𝐷) ≤ 𝑎𝑎 < (2 · (PellFund‘𝐷))))
182adantr 480 . . . . . 6 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → (PellFund‘𝐷) ∈ ℝ)
19 pell1qrss14 42184 . . . . . . . 8 (𝐷 ∈ (ℕ ∖ ◻NN) → (Pell1QR‘𝐷) ⊆ (Pell14QR‘𝐷))
2019sselda 3977 . . . . . . 7 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → 𝑎 ∈ (Pell14QR‘𝐷))
21 pell14qrre 42173 . . . . . . 7 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell14QR‘𝐷)) → 𝑎 ∈ ℝ)
2220, 21syldan 590 . . . . . 6 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → 𝑎 ∈ ℝ)
2318, 22leloed 11361 . . . . 5 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → ((PellFund‘𝐷) ≤ 𝑎 ↔ ((PellFund‘𝐷) < 𝑎 ∨ (PellFund‘𝐷) = 𝑎)))
24 simp-4l 780 . . . . . . . . 9 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → 𝐷 ∈ (ℕ ∖ ◻NN))
25 simp-4r 781 . . . . . . . . 9 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → 𝑎 ∈ (Pell1QR‘𝐷))
26 simplr 766 . . . . . . . . 9 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → 𝑏 ∈ (Pell1QR‘𝐷))
27 simprr 770 . . . . . . . . 9 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → 𝑏 < 𝑎)
2822ad3antrrr 727 . . . . . . . . . 10 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → 𝑎 ∈ ℝ)
294ad4antr 729 . . . . . . . . . 10 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → (2 · (PellFund‘𝐷)) ∈ ℝ)
3019ad4antr 729 . . . . . . . . . . . . 13 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → (Pell1QR‘𝐷) ⊆ (Pell14QR‘𝐷))
3130, 26sseldd 3978 . . . . . . . . . . . 12 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → 𝑏 ∈ (Pell14QR‘𝐷))
32 pell14qrre 42173 . . . . . . . . . . . 12 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑏 ∈ (Pell14QR‘𝐷)) → 𝑏 ∈ ℝ)
3324, 31, 32syl2anc 583 . . . . . . . . . . 11 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → 𝑏 ∈ ℝ)
34 remulcl 11197 . . . . . . . . . . 11 ((2 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (2 · 𝑏) ∈ ℝ)
351, 33, 34sylancr 586 . . . . . . . . . 10 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → (2 · 𝑏) ∈ ℝ)
36 simprr 770 . . . . . . . . . . 11 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) → 𝑎 < (2 · (PellFund‘𝐷)))
3736ad2antrr 723 . . . . . . . . . 10 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → 𝑎 < (2 · (PellFund‘𝐷)))
38 simprl 768 . . . . . . . . . . 11 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → (PellFund‘𝐷) ≤ 𝑏)
392ad4antr 729 . . . . . . . . . . . 12 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → (PellFund‘𝐷) ∈ ℝ)
401a1i 11 . . . . . . . . . . . 12 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → 2 ∈ ℝ)
41 2pos 12319 . . . . . . . . . . . . 13 0 < 2
4241a1i 11 . . . . . . . . . . . 12 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → 0 < 2)
43 lemul2 12071 . . . . . . . . . . . 12 (((PellFund‘𝐷) ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((PellFund‘𝐷) ≤ 𝑏 ↔ (2 · (PellFund‘𝐷)) ≤ (2 · 𝑏)))
4439, 33, 40, 42, 43syl112anc 1371 . . . . . . . . . . 11 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → ((PellFund‘𝐷) ≤ 𝑏 ↔ (2 · (PellFund‘𝐷)) ≤ (2 · 𝑏)))
4538, 44mpbid 231 . . . . . . . . . 10 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → (2 · (PellFund‘𝐷)) ≤ (2 · 𝑏))
4628, 29, 35, 37, 45ltletrd 11378 . . . . . . . . 9 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → 𝑎 < (2 · 𝑏))
47 simp1 1133 . . . . . . . . . 10 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → 𝐷 ∈ (ℕ ∖ ◻NN))
48193ad2ant1 1130 . . . . . . . . . . . 12 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → (Pell1QR‘𝐷) ⊆ (Pell14QR‘𝐷))
49 simp2l 1196 . . . . . . . . . . . 12 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → 𝑎 ∈ (Pell1QR‘𝐷))
5048, 49sseldd 3978 . . . . . . . . . . 11 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → 𝑎 ∈ (Pell14QR‘𝐷))
51 simp2r 1197 . . . . . . . . . . . 12 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → 𝑏 ∈ (Pell1QR‘𝐷))
5248, 51sseldd 3978 . . . . . . . . . . 11 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → 𝑏 ∈ (Pell14QR‘𝐷))
53 pell14qrdivcl 42181 . . . . . . . . . . 11 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell14QR‘𝐷) ∧ 𝑏 ∈ (Pell14QR‘𝐷)) → (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷))
5447, 50, 52, 53syl3anc 1368 . . . . . . . . . 10 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷))
5547, 52, 32syl2anc 583 . . . . . . . . . . . . . 14 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → 𝑏 ∈ ℝ)
5655recnd 11246 . . . . . . . . . . . . 13 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → 𝑏 ∈ ℂ)
5756mullidd 11236 . . . . . . . . . . . 12 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → (1 · 𝑏) = 𝑏)
58 simp3l 1198 . . . . . . . . . . . 12 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → 𝑏 < 𝑎)
5957, 58eqbrtrd 5163 . . . . . . . . . . 11 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → (1 · 𝑏) < 𝑎)
60 1red 11219 . . . . . . . . . . . 12 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → 1 ∈ ℝ)
6147, 50, 21syl2anc 583 . . . . . . . . . . . 12 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → 𝑎 ∈ ℝ)
62 pell14qrgt0 42175 . . . . . . . . . . . . 13 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑏 ∈ (Pell14QR‘𝐷)) → 0 < 𝑏)
6347, 52, 62syl2anc 583 . . . . . . . . . . . 12 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → 0 < 𝑏)
64 ltmuldiv 12091 . . . . . . . . . . . 12 ((1 ∈ ℝ ∧ 𝑎 ∈ ℝ ∧ (𝑏 ∈ ℝ ∧ 0 < 𝑏)) → ((1 · 𝑏) < 𝑎 ↔ 1 < (𝑎 / 𝑏)))
6560, 61, 55, 63, 64syl112anc 1371 . . . . . . . . . . 11 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → ((1 · 𝑏) < 𝑎 ↔ 1 < (𝑎 / 𝑏)))
6659, 65mpbid 231 . . . . . . . . . 10 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → 1 < (𝑎 / 𝑏))
67 simp3r 1199 . . . . . . . . . . 11 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → 𝑎 < (2 · 𝑏))
681a1i 11 . . . . . . . . . . . 12 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → 2 ∈ ℝ)
69 ltdivmul2 12095 . . . . . . . . . . . 12 ((𝑎 ∈ ℝ ∧ 2 ∈ ℝ ∧ (𝑏 ∈ ℝ ∧ 0 < 𝑏)) → ((𝑎 / 𝑏) < 2 ↔ 𝑎 < (2 · 𝑏)))
7061, 68, 55, 63, 69syl112anc 1371 . . . . . . . . . . 11 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → ((𝑎 / 𝑏) < 2 ↔ 𝑎 < (2 · 𝑏)))
7167, 70mpbird 257 . . . . . . . . . 10 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → (𝑎 / 𝑏) < 2)
72 simprr 770 . . . . . . . . . . 11 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → (𝑎 / 𝑏) < 2)
73 simpll 764 . . . . . . . . . . . . 13 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → 𝐷 ∈ (ℕ ∖ ◻NN))
74 simplr 766 . . . . . . . . . . . . 13 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷))
75 simprl 768 . . . . . . . . . . . . 13 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → 1 < (𝑎 / 𝑏))
76 pell14qrgapw 42192 . . . . . . . . . . . . 13 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷) ∧ 1 < (𝑎 / 𝑏)) → 2 < (𝑎 / 𝑏))
7773, 74, 75, 76syl3anc 1368 . . . . . . . . . . . 12 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → 2 < (𝑎 / 𝑏))
78 pell14qrre 42173 . . . . . . . . . . . . . 14 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) → (𝑎 / 𝑏) ∈ ℝ)
7978adantr 480 . . . . . . . . . . . . 13 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → (𝑎 / 𝑏) ∈ ℝ)
80 ltnsym 11316 . . . . . . . . . . . . 13 ((2 ∈ ℝ ∧ (𝑎 / 𝑏) ∈ ℝ) → (2 < (𝑎 / 𝑏) → ¬ (𝑎 / 𝑏) < 2))
811, 79, 80sylancr 586 . . . . . . . . . . . 12 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → (2 < (𝑎 / 𝑏) → ¬ (𝑎 / 𝑏) < 2))
8277, 81mpd 15 . . . . . . . . . . 11 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → ¬ (𝑎 / 𝑏) < 2)
8372, 82pm2.21dd 194 . . . . . . . . . 10 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷))
8447, 54, 66, 71, 83syl22anc 836 . . . . . . . . 9 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎𝑎 < (2 · 𝑏))) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷))
8524, 25, 26, 27, 46, 84syl122anc 1376 . . . . . . . 8 (((((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎)) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷))
86 simpll 764 . . . . . . . . 9 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) → 𝐷 ∈ (ℕ ∖ ◻NN))
8722adantr 480 . . . . . . . . 9 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) → 𝑎 ∈ ℝ)
88 simprl 768 . . . . . . . . 9 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) → (PellFund‘𝐷) < 𝑎)
89 pellfundglb 42201 . . . . . . . . 9 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ ℝ ∧ (PellFund‘𝐷) < 𝑎) → ∃𝑏 ∈ (Pell1QR‘𝐷)((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎))
9086, 87, 88, 89syl3anc 1368 . . . . . . . 8 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) → ∃𝑏 ∈ (Pell1QR‘𝐷)((PellFund‘𝐷) ≤ 𝑏𝑏 < 𝑎))
9185, 90r19.29a 3156 . . . . . . 7 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎𝑎 < (2 · (PellFund‘𝐷)))) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷))
9291exp32 420 . . . . . 6 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → ((PellFund‘𝐷) < 𝑎 → (𝑎 < (2 · (PellFund‘𝐷)) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷))))
93 simp2 1134 . . . . . . . 8 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ (PellFund‘𝐷) = 𝑎𝑎 < (2 · (PellFund‘𝐷))) → (PellFund‘𝐷) = 𝑎)
94 simp1r 1195 . . . . . . . 8 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ (PellFund‘𝐷) = 𝑎𝑎 < (2 · (PellFund‘𝐷))) → 𝑎 ∈ (Pell1QR‘𝐷))
9593, 94eqeltrd 2827 . . . . . . 7 (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ (PellFund‘𝐷) = 𝑎𝑎 < (2 · (PellFund‘𝐷))) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷))
96953exp 1116 . . . . . 6 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → ((PellFund‘𝐷) = 𝑎 → (𝑎 < (2 · (PellFund‘𝐷)) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷))))
9792, 96jaod 856 . . . . 5 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → (((PellFund‘𝐷) < 𝑎 ∨ (PellFund‘𝐷) = 𝑎) → (𝑎 < (2 · (PellFund‘𝐷)) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷))))
9823, 97sylbid 239 . . . 4 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → ((PellFund‘𝐷) ≤ 𝑎 → (𝑎 < (2 · (PellFund‘𝐷)) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷))))
9998impd 410 . . 3 ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → (((PellFund‘𝐷) ≤ 𝑎𝑎 < (2 · (PellFund‘𝐷))) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷)))
10099rexlimdva 3149 . 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 205  wa 395  wo 844  w3a 1084   = wceq 1533  wcel 2098  wrex 3064  cdif 3940  wss 3943   class class class wbr 5141  cfv 6537  (class class class)co 7405  cr 11111  0cc0 11112  1c1 11113   + caddc 11115   · cmul 11117   < clt 11252  cle 11253   / cdiv 11875  cn 12216  2c2 12271  NNcsquarenn 42152  Pell1QRcpell1qr 42153  Pell14QRcpell14qr 42155  PellFundcpellfund 42156
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7853  df-1st 7974  df-2nd 7975  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-1o 8467  df-oadd 8471  df-omul 8472  df-er 8705  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-sup 9439  df-inf 9440  df-oi 9507  df-card 9936  df-acn 9939  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-n0 12477  df-xnn0 12549  df-z 12563  df-uz 12827  df-q 12937  df-rp 12981  df-ico 13336  df-fz 13491  df-fl 13763  df-mod 13841  df-seq 13973  df-exp 14033  df-hash 14296  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-dvds 16205  df-gcd 16443  df-numer 16680  df-denom 16681  df-squarenn 42157  df-pell1qr 42158  df-pell14qr 42159  df-pell1234qr 42160  df-pellfund 42161
This theorem is referenced by:  pellfund14  42214  pellfund14b  42215
  Copyright terms: Public domain W3C validator