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 . (Contributed by Stefan O'Rear, 18-Sep-2014)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | pellfundex | ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( PellFund ‘ 𝐷 ) ∈ ( Pell1QR ‘ 𝐷 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 2re | ⊢ 2 ∈ ℝ | |
| 2 | pellfundre | ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( PellFund ‘ 𝐷 ) ∈ ℝ ) | |
| 3 | remulcl | ⊢ ( ( 2 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) ∈ ℝ ) → ( 2 · ( PellFund ‘ 𝐷 ) ) ∈ ℝ ) | |
| 4 | 1 2 3 | sylancr | ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 2 · ( PellFund ‘ 𝐷 ) ) ∈ ℝ ) |
| 5 | 0red | ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 0 ∈ ℝ ) | |
| 6 | 1red | ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 1 ∈ ℝ ) | |
| 7 | 0lt1 | ⊢ 0 < 1 | |
| 8 | 7 | a1i | ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 0 < 1 ) |
| 9 | pellfundgt1 | ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 1 < ( PellFund ‘ 𝐷 ) ) | |
| 10 | 5 6 2 8 9 | lttrd | ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 0 < ( PellFund ‘ 𝐷 ) ) |
| 11 | 2 10 | elrpd | ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( PellFund ‘ 𝐷 ) ∈ ℝ+ ) |
| 12 | 2 11 | ltaddrpd | ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( PellFund ‘ 𝐷 ) < ( ( PellFund ‘ 𝐷 ) + ( PellFund ‘ 𝐷 ) ) ) |
| 13 | 2 | recnd | ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( PellFund ‘ 𝐷 ) ∈ ℂ ) |
| 14 | 13 | 2timesd | ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 2 · ( PellFund ‘ 𝐷 ) ) = ( ( PellFund ‘ 𝐷 ) + ( PellFund ‘ 𝐷 ) ) ) |
| 15 | 12 14 | breqtrrd | ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( PellFund ‘ 𝐷 ) < ( 2 · ( PellFund ‘ 𝐷 ) ) ) |
| 16 | pellfundglb | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 2 · ( PellFund ‘ 𝐷 ) ) ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < ( 2 · ( PellFund ‘ 𝐷 ) ) ) → ∃ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ( ( PellFund ‘ 𝐷 ) ≤ 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) ) | |
| 17 | 4 15 16 | mpd3an23 | ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ∃ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ( ( PellFund ‘ 𝐷 ) ≤ 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) ) |
| 18 | 2 | adantr | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) → ( PellFund ‘ 𝐷 ) ∈ ℝ ) |
| 19 | pell1qrss14 | ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( Pell1QR ‘ 𝐷 ) ⊆ ( Pell14QR ‘ 𝐷 ) ) | |
| 20 | 19 | sselda | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) → 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ) |
| 21 | pell14qrre | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝑎 ∈ ℝ ) | |
| 22 | 20 21 | syldan | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) → 𝑎 ∈ ℝ ) |
| 23 | 18 22 | leloed | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) → ( ( PellFund ‘ 𝐷 ) ≤ 𝑎 ↔ ( ( PellFund ‘ 𝐷 ) < 𝑎 ∨ ( PellFund ‘ 𝐷 ) = 𝑎 ) ) ) |
| 24 | simp-4l | ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) < 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) ≤ 𝑏 ∧ 𝑏 < 𝑎 ) ) → 𝐷 ∈ ( ℕ ∖ ◻NN ) ) | |
| 25 | simp-4r | ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) < 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) ≤ 𝑏 ∧ 𝑏 < 𝑎 ) ) → 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) | |
| 26 | simplr | ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) < 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) ≤ 𝑏 ∧ 𝑏 < 𝑎 ) ) → 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) | |
| 27 | simprr | ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) < 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) ≤ 𝑏 ∧ 𝑏 < 𝑎 ) ) → 𝑏 < 𝑎 ) | |
| 28 | 22 | ad3antrrr | ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) < 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) ≤ 𝑏 ∧ 𝑏 < 𝑎 ) ) → 𝑎 ∈ ℝ ) |
| 29 | 4 | ad4antr | ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) < 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) ≤ 𝑏 ∧ 𝑏 < 𝑎 ) ) → ( 2 · ( PellFund ‘ 𝐷 ) ) ∈ ℝ ) |
| 30 | 19 | ad4antr | ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) < 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) ≤ 𝑏 ∧ 𝑏 < 𝑎 ) ) → ( Pell1QR ‘ 𝐷 ) ⊆ ( Pell14QR ‘ 𝐷 ) ) |
| 31 | 30 26 | sseldd | ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) < 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) ≤ 𝑏 ∧ 𝑏 < 𝑎 ) ) → 𝑏 ∈ ( Pell14QR ‘ 𝐷 ) ) |
| 32 | pell14qrre | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑏 ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝑏 ∈ ℝ ) | |
| 33 | 24 31 32 | syl2anc | ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) < 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) ≤ 𝑏 ∧ 𝑏 < 𝑎 ) ) → 𝑏 ∈ ℝ ) |
| 34 | remulcl | ⊢ ( ( 2 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( 2 · 𝑏 ) ∈ ℝ ) | |
| 35 | 1 33 34 | sylancr | ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) < 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) ≤ 𝑏 ∧ 𝑏 < 𝑎 ) ) → ( 2 · 𝑏 ) ∈ ℝ ) |
| 36 | simprr | ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) < 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) ) → 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) | |
| 37 | 36 | ad2antrr | ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) < 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) ≤ 𝑏 ∧ 𝑏 < 𝑎 ) ) → 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) |
| 38 | simprl | ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) < 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) ≤ 𝑏 ∧ 𝑏 < 𝑎 ) ) → ( PellFund ‘ 𝐷 ) ≤ 𝑏 ) | |
| 39 | 2 | ad4antr | ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) < 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) ≤ 𝑏 ∧ 𝑏 < 𝑎 ) ) → ( PellFund ‘ 𝐷 ) ∈ ℝ ) |
| 40 | 1 | a1i | ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) < 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) ≤ 𝑏 ∧ 𝑏 < 𝑎 ) ) → 2 ∈ ℝ ) |
| 41 | 2pos | ⊢ 0 < 2 | |
| 42 | 41 | a1i | ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) < 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) ≤ 𝑏 ∧ 𝑏 < 𝑎 ) ) → 0 < 2 ) |
| 43 | lemul2 | ⊢ ( ( ( PellFund ‘ 𝐷 ) ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( PellFund ‘ 𝐷 ) ≤ 𝑏 ↔ ( 2 · ( PellFund ‘ 𝐷 ) ) ≤ ( 2 · 𝑏 ) ) ) | |
| 44 | 39 33 40 42 43 | syl112anc | ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) < 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) ≤ 𝑏 ∧ 𝑏 < 𝑎 ) ) → ( ( PellFund ‘ 𝐷 ) ≤ 𝑏 ↔ ( 2 · ( PellFund ‘ 𝐷 ) ) ≤ ( 2 · 𝑏 ) ) ) |
| 45 | 38 44 | mpbid | ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) < 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) ≤ 𝑏 ∧ 𝑏 < 𝑎 ) ) → ( 2 · ( PellFund ‘ 𝐷 ) ) ≤ ( 2 · 𝑏 ) ) |
| 46 | 28 29 35 37 45 | ltletrd | ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) < 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) ≤ 𝑏 ∧ 𝑏 < 𝑎 ) ) → 𝑎 < ( 2 · 𝑏 ) ) |
| 47 | simp1 | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( 𝑏 < 𝑎 ∧ 𝑎 < ( 2 · 𝑏 ) ) ) → 𝐷 ∈ ( ℕ ∖ ◻NN ) ) | |
| 48 | 19 | 3ad2ant1 | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( 𝑏 < 𝑎 ∧ 𝑎 < ( 2 · 𝑏 ) ) ) → ( Pell1QR ‘ 𝐷 ) ⊆ ( Pell14QR ‘ 𝐷 ) ) |
| 49 | simp2l | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( 𝑏 < 𝑎 ∧ 𝑎 < ( 2 · 𝑏 ) ) ) → 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) | |
| 50 | 48 49 | sseldd | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( 𝑏 < 𝑎 ∧ 𝑎 < ( 2 · 𝑏 ) ) ) → 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ) |
| 51 | simp2r | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( 𝑏 < 𝑎 ∧ 𝑎 < ( 2 · 𝑏 ) ) ) → 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) | |
| 52 | 48 51 | sseldd | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( 𝑏 < 𝑎 ∧ 𝑎 < ( 2 · 𝑏 ) ) ) → 𝑏 ∈ ( Pell14QR ‘ 𝐷 ) ) |
| 53 | pell14qrdivcl | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 𝑏 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝑎 / 𝑏 ) ∈ ( Pell14QR ‘ 𝐷 ) ) | |
| 54 | 47 50 52 53 | syl3anc | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( 𝑏 < 𝑎 ∧ 𝑎 < ( 2 · 𝑏 ) ) ) → ( 𝑎 / 𝑏 ) ∈ ( Pell14QR ‘ 𝐷 ) ) |
| 55 | 47 52 32 | syl2anc | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( 𝑏 < 𝑎 ∧ 𝑎 < ( 2 · 𝑏 ) ) ) → 𝑏 ∈ ℝ ) |
| 56 | 55 | recnd | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( 𝑏 < 𝑎 ∧ 𝑎 < ( 2 · 𝑏 ) ) ) → 𝑏 ∈ ℂ ) |
| 57 | 56 | mulid2d | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( 𝑏 < 𝑎 ∧ 𝑎 < ( 2 · 𝑏 ) ) ) → ( 1 · 𝑏 ) = 𝑏 ) |
| 58 | simp3l | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( 𝑏 < 𝑎 ∧ 𝑎 < ( 2 · 𝑏 ) ) ) → 𝑏 < 𝑎 ) | |
| 59 | 57 58 | eqbrtrd | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( 𝑏 < 𝑎 ∧ 𝑎 < ( 2 · 𝑏 ) ) ) → ( 1 · 𝑏 ) < 𝑎 ) |
| 60 | 1red | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( 𝑏 < 𝑎 ∧ 𝑎 < ( 2 · 𝑏 ) ) ) → 1 ∈ ℝ ) | |
| 61 | 47 50 21 | syl2anc | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( 𝑏 < 𝑎 ∧ 𝑎 < ( 2 · 𝑏 ) ) ) → 𝑎 ∈ ℝ ) |
| 62 | pell14qrgt0 | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑏 ∈ ( Pell14QR ‘ 𝐷 ) ) → 0 < 𝑏 ) | |
| 63 | 47 52 62 | syl2anc | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( 𝑏 < 𝑎 ∧ 𝑎 < ( 2 · 𝑏 ) ) ) → 0 < 𝑏 ) |
| 64 | ltmuldiv | ⊢ ( ( 1 ∈ ℝ ∧ 𝑎 ∈ ℝ ∧ ( 𝑏 ∈ ℝ ∧ 0 < 𝑏 ) ) → ( ( 1 · 𝑏 ) < 𝑎 ↔ 1 < ( 𝑎 / 𝑏 ) ) ) | |
| 65 | 60 61 55 63 64 | syl112anc | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( 𝑏 < 𝑎 ∧ 𝑎 < ( 2 · 𝑏 ) ) ) → ( ( 1 · 𝑏 ) < 𝑎 ↔ 1 < ( 𝑎 / 𝑏 ) ) ) |
| 66 | 59 65 | mpbid | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( 𝑏 < 𝑎 ∧ 𝑎 < ( 2 · 𝑏 ) ) ) → 1 < ( 𝑎 / 𝑏 ) ) |
| 67 | simp3r | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( 𝑏 < 𝑎 ∧ 𝑎 < ( 2 · 𝑏 ) ) ) → 𝑎 < ( 2 · 𝑏 ) ) | |
| 68 | 1 | a1i | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( 𝑏 < 𝑎 ∧ 𝑎 < ( 2 · 𝑏 ) ) ) → 2 ∈ ℝ ) |
| 69 | ltdivmul2 | ⊢ ( ( 𝑎 ∈ ℝ ∧ 2 ∈ ℝ ∧ ( 𝑏 ∈ ℝ ∧ 0 < 𝑏 ) ) → ( ( 𝑎 / 𝑏 ) < 2 ↔ 𝑎 < ( 2 · 𝑏 ) ) ) | |
| 70 | 61 68 55 63 69 | syl112anc | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( 𝑏 < 𝑎 ∧ 𝑎 < ( 2 · 𝑏 ) ) ) → ( ( 𝑎 / 𝑏 ) < 2 ↔ 𝑎 < ( 2 · 𝑏 ) ) ) |
| 71 | 67 70 | mpbird | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( 𝑏 < 𝑎 ∧ 𝑎 < ( 2 · 𝑏 ) ) ) → ( 𝑎 / 𝑏 ) < 2 ) |
| 72 | simprr | ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 / 𝑏 ) ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ ( 1 < ( 𝑎 / 𝑏 ) ∧ ( 𝑎 / 𝑏 ) < 2 ) ) → ( 𝑎 / 𝑏 ) < 2 ) | |
| 73 | simpll | ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 / 𝑏 ) ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ ( 1 < ( 𝑎 / 𝑏 ) ∧ ( 𝑎 / 𝑏 ) < 2 ) ) → 𝐷 ∈ ( ℕ ∖ ◻NN ) ) | |
| 74 | simplr | ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 / 𝑏 ) ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ ( 1 < ( 𝑎 / 𝑏 ) ∧ ( 𝑎 / 𝑏 ) < 2 ) ) → ( 𝑎 / 𝑏 ) ∈ ( Pell14QR ‘ 𝐷 ) ) | |
| 75 | simprl | ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 / 𝑏 ) ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ ( 1 < ( 𝑎 / 𝑏 ) ∧ ( 𝑎 / 𝑏 ) < 2 ) ) → 1 < ( 𝑎 / 𝑏 ) ) | |
| 76 | pell14qrgapw | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 / 𝑏 ) ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < ( 𝑎 / 𝑏 ) ) → 2 < ( 𝑎 / 𝑏 ) ) | |
| 77 | 73 74 75 76 | syl3anc | ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 / 𝑏 ) ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ ( 1 < ( 𝑎 / 𝑏 ) ∧ ( 𝑎 / 𝑏 ) < 2 ) ) → 2 < ( 𝑎 / 𝑏 ) ) |
| 78 | pell14qrre | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 / 𝑏 ) ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝑎 / 𝑏 ) ∈ ℝ ) | |
| 79 | 78 | adantr | ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 / 𝑏 ) ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ ( 1 < ( 𝑎 / 𝑏 ) ∧ ( 𝑎 / 𝑏 ) < 2 ) ) → ( 𝑎 / 𝑏 ) ∈ ℝ ) |
| 80 | ltnsym | ⊢ ( ( 2 ∈ ℝ ∧ ( 𝑎 / 𝑏 ) ∈ ℝ ) → ( 2 < ( 𝑎 / 𝑏 ) → ¬ ( 𝑎 / 𝑏 ) < 2 ) ) | |
| 81 | 1 79 80 | sylancr | ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 / 𝑏 ) ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ ( 1 < ( 𝑎 / 𝑏 ) ∧ ( 𝑎 / 𝑏 ) < 2 ) ) → ( 2 < ( 𝑎 / 𝑏 ) → ¬ ( 𝑎 / 𝑏 ) < 2 ) ) |
| 82 | 77 81 | mpd | ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 / 𝑏 ) ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ ( 1 < ( 𝑎 / 𝑏 ) ∧ ( 𝑎 / 𝑏 ) < 2 ) ) → ¬ ( 𝑎 / 𝑏 ) < 2 ) |
| 83 | 72 82 | pm2.21dd | ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 / 𝑏 ) ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ ( 1 < ( 𝑎 / 𝑏 ) ∧ ( 𝑎 / 𝑏 ) < 2 ) ) → ( PellFund ‘ 𝐷 ) ∈ ( Pell1QR ‘ 𝐷 ) ) |
| 84 | 47 54 66 71 83 | syl22anc | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( 𝑏 < 𝑎 ∧ 𝑎 < ( 2 · 𝑏 ) ) ) → ( PellFund ‘ 𝐷 ) ∈ ( Pell1QR ‘ 𝐷 ) ) |
| 85 | 24 25 26 27 46 84 | syl122anc | ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) < 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) ) ∧ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) ≤ 𝑏 ∧ 𝑏 < 𝑎 ) ) → ( PellFund ‘ 𝐷 ) ∈ ( Pell1QR ‘ 𝐷 ) ) |
| 86 | simpll | ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) < 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) ) → 𝐷 ∈ ( ℕ ∖ ◻NN ) ) | |
| 87 | 22 | adantr | ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) < 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) ) → 𝑎 ∈ ℝ ) |
| 88 | simprl | ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) < 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) ) → ( PellFund ‘ 𝐷 ) < 𝑎 ) | |
| 89 | pellfundglb | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝑎 ) → ∃ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ( ( PellFund ‘ 𝐷 ) ≤ 𝑏 ∧ 𝑏 < 𝑎 ) ) | |
| 90 | 86 87 88 89 | syl3anc | ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) < 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) ) → ∃ 𝑏 ∈ ( Pell1QR ‘ 𝐷 ) ( ( PellFund ‘ 𝐷 ) ≤ 𝑏 ∧ 𝑏 < 𝑎 ) ) |
| 91 | 85 90 | r19.29a | ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( ( PellFund ‘ 𝐷 ) < 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) ) → ( PellFund ‘ 𝐷 ) ∈ ( Pell1QR ‘ 𝐷 ) ) |
| 92 | 91 | exp32 | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) → ( ( PellFund ‘ 𝐷 ) < 𝑎 → ( 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) → ( PellFund ‘ 𝐷 ) ∈ ( Pell1QR ‘ 𝐷 ) ) ) ) |
| 93 | simp2 | ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( PellFund ‘ 𝐷 ) = 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) → ( PellFund ‘ 𝐷 ) = 𝑎 ) | |
| 94 | simp1r | ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( PellFund ‘ 𝐷 ) = 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) → 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) | |
| 95 | 93 94 | eqeltrd | ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) ∧ ( PellFund ‘ 𝐷 ) = 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) → ( PellFund ‘ 𝐷 ) ∈ ( Pell1QR ‘ 𝐷 ) ) |
| 96 | 95 | 3exp | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) → ( ( PellFund ‘ 𝐷 ) = 𝑎 → ( 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) → ( PellFund ‘ 𝐷 ) ∈ ( Pell1QR ‘ 𝐷 ) ) ) ) |
| 97 | 92 96 | jaod | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) → ( ( ( PellFund ‘ 𝐷 ) < 𝑎 ∨ ( PellFund ‘ 𝐷 ) = 𝑎 ) → ( 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) → ( PellFund ‘ 𝐷 ) ∈ ( Pell1QR ‘ 𝐷 ) ) ) ) |
| 98 | 23 97 | sylbid | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) → ( ( PellFund ‘ 𝐷 ) ≤ 𝑎 → ( 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) → ( PellFund ‘ 𝐷 ) ∈ ( Pell1QR ‘ 𝐷 ) ) ) ) |
| 99 | 98 | impd | ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ) → ( ( ( PellFund ‘ 𝐷 ) ≤ 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) → ( PellFund ‘ 𝐷 ) ∈ ( Pell1QR ‘ 𝐷 ) ) ) |
| 100 | 99 | rexlimdva | ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ∃ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) ( ( PellFund ‘ 𝐷 ) ≤ 𝑎 ∧ 𝑎 < ( 2 · ( PellFund ‘ 𝐷 ) ) ) → ( PellFund ‘ 𝐷 ) ∈ ( Pell1QR ‘ 𝐷 ) ) ) |
| 101 | 17 100 | mpd | ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( PellFund ‘ 𝐷 ) ∈ ( Pell1QR ‘ 𝐷 ) ) |