Metamath Proof Explorer

Theorem pellfundglb

Description: If a real is larger than the fundamental solution, there is a nontrivial solution less than it. (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion pellfundglb ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) → ∃ 𝑥 ∈ ( Pell1QR ‘ 𝐷 ) ( ( PellFund ‘ 𝐷 ) ≤ 𝑥 ∧ 𝑥 < 𝐴 ) )

Proof

Step Hyp Ref Expression
1 pellfundval ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( PellFund ‘ 𝐷 ) = inf ( { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } , ℝ , < ) )
2 1 3ad2ant1 ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) → ( PellFund ‘ 𝐷 ) = inf ( { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } , ℝ , < ) )
3 simp3 ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) → ( PellFund ‘ 𝐷 ) < 𝐴 )
4 2 3 eqbrtrrd ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) → inf ( { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } , ℝ , < ) < 𝐴 )
5 pellfundre ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( PellFund ‘ 𝐷 ) ∈ ℝ )
6 5 3ad2ant1 ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) → ( PellFund ‘ 𝐷 ) ∈ ℝ )
7 2 6 eqeltrrd ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) → inf ( { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } , ℝ , < ) ∈ ℝ )
8 simp2 ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) → 𝐴 ∈ ℝ )
9 7 8 ltnled ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) → ( inf ( { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } , ℝ , < ) < 𝐴 ↔ ¬ 𝐴 ≤ inf ( { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } , ℝ , < ) ) )
10 4 9 mpbid ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) → ¬ 𝐴 ≤ inf ( { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } , ℝ , < ) )
11 ssrab2 ⊢ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ⊆ ( Pell14QR ‘ 𝐷 )
12 pell14qrre ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝑎 ∈ ℝ )
13 12 ex ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) → 𝑎 ∈ ℝ ) )
14 13 ssrdv ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( Pell14QR ‘ 𝐷 ) ⊆ ℝ )
15 14 3ad2ant1 ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) → ( Pell14QR ‘ 𝐷 ) ⊆ ℝ )
16 11 15 sstrid ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) → { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ⊆ ℝ )
17 pell1qrss14 ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( Pell1QR ‘ 𝐷 ) ⊆ ( Pell14QR ‘ 𝐷 ) )
18 17 3ad2ant1 ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) → ( Pell1QR ‘ 𝐷 ) ⊆ ( Pell14QR ‘ 𝐷 ) )
19 pellqrex ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ∃ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) 1 < 𝑎 )
20 19 3ad2ant1 ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) → ∃ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) 1 < 𝑎 )
21 ssrexv ⊢ ( ( Pell1QR ‘ 𝐷 ) ⊆ ( Pell14QR ‘ 𝐷 ) → ( ∃ 𝑎 ∈ ( Pell1QR ‘ 𝐷 ) 1 < 𝑎 → ∃ 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) 1 < 𝑎 ) )
22 18 20 21 sylc ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) → ∃ 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) 1 < 𝑎 )
23 rabn0 ⊢ ( { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ≠ ∅ ↔ ∃ 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) 1 < 𝑎 )
24 22 23 sylibr ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) → { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ≠ ∅ )
25 infmrgelbi ⊢ ( ( ( { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ⊆ ℝ ∧ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ≠ ∅ ∧ 𝐴 ∈ ℝ ) ∧ ∀ 𝑥 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } 𝐴 ≤ 𝑥 ) → 𝐴 ≤ inf ( { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } , ℝ , < ) )
26 25 ex ⊢ ( ( { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ⊆ ℝ ∧ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ≠ ∅ ∧ 𝐴 ∈ ℝ ) → ( ∀ 𝑥 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } 𝐴 ≤ 𝑥 → 𝐴 ≤ inf ( { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } , ℝ , < ) ) )
27 16 24 8 26 syl3anc ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) → ( ∀ 𝑥 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } 𝐴 ≤ 𝑥 → 𝐴 ≤ inf ( { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } , ℝ , < ) ) )
28 10 27 mtod ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) → ¬ ∀ 𝑥 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } 𝐴 ≤ 𝑥 )
29 rexnal ⊢ ( ∃ 𝑥 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ¬ 𝐴 ≤ 𝑥 ↔ ¬ ∀ 𝑥 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } 𝐴 ≤ 𝑥 )
30 28 29 sylibr ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) → ∃ 𝑥 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ¬ 𝐴 ≤ 𝑥 )
31 breq2 ⊢ ( 𝑎 = 𝑥 → ( 1 < 𝑎 ↔ 1 < 𝑥 ) )
32 31 elrab ⊢ ( 𝑥 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ↔ ( 𝑥 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝑥 ) )
33 simprl ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) ∧ ( 𝑥 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝑥 ) ) → 𝑥 ∈ ( Pell14QR ‘ 𝐷 ) )
34 1red ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) ∧ ( 𝑥 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝑥 ) ) → 1 ∈ ℝ )
35 simpl1 ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) ∧ ( 𝑥 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝑥 ) ) → 𝐷 ∈ ( ℕ ∖ ◻NN ) )
36 pell14qrre ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑥 ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝑥 ∈ ℝ )
37 35 33 36 syl2anc ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) ∧ ( 𝑥 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝑥 ) ) → 𝑥 ∈ ℝ )
38 simprr ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) ∧ ( 𝑥 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝑥 ) ) → 1 < 𝑥 )
39 34 37 38 ltled ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) ∧ ( 𝑥 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝑥 ) ) → 1 ≤ 𝑥 )
40 33 39 jca ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) ∧ ( 𝑥 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝑥 ) ) → ( 𝑥 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 ≤ 𝑥 ) )
41 elpell1qr2 ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝑥 ∈ ( Pell1QR ‘ 𝐷 ) ↔ ( 𝑥 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 ≤ 𝑥 ) ) )
42 35 41 syl ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) ∧ ( 𝑥 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝑥 ) ) → ( 𝑥 ∈ ( Pell1QR ‘ 𝐷 ) ↔ ( 𝑥 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 ≤ 𝑥 ) ) )
43 40 42 mpbird ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) ∧ ( 𝑥 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝑥 ) ) → 𝑥 ∈ ( Pell1QR ‘ 𝐷 ) )
44 32 43 sylan2b ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) ∧ 𝑥 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ) → 𝑥 ∈ ( Pell1QR ‘ 𝐷 ) )
45 44 adantrr ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) ∧ ( 𝑥 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ∧ ¬ 𝐴 ≤ 𝑥 ) ) → 𝑥 ∈ ( Pell1QR ‘ 𝐷 ) )
46 simpl1 ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) ∧ ( 𝑥 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ∧ ¬ 𝐴 ≤ 𝑥 ) ) → 𝐷 ∈ ( ℕ ∖ ◻NN ) )
47 simprl ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) ∧ ( 𝑥 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ∧ ¬ 𝐴 ≤ 𝑥 ) ) → 𝑥 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } )
48 11 47 sselid ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) ∧ ( 𝑥 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ∧ ¬ 𝐴 ≤ 𝑥 ) ) → 𝑥 ∈ ( Pell14QR ‘ 𝐷 ) )
49 simpr ⊢ ( ( 𝑥 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝑥 ) → 1 < 𝑥 )
50 49 a1i ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) → ( ( 𝑥 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝑥 ) → 1 < 𝑥 ) )
51 32 50 syl5bi ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) → ( 𝑥 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } → 1 < 𝑥 ) )
52 51 imp ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) ∧ 𝑥 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ) → 1 < 𝑥 )
53 52 adantrr ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) ∧ ( 𝑥 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ∧ ¬ 𝐴 ≤ 𝑥 ) ) → 1 < 𝑥 )
54 pellfundlb ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑥 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 1 < 𝑥 ) → ( PellFund ‘ 𝐷 ) ≤ 𝑥 )
55 46 48 53 54 syl3anc ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) ∧ ( 𝑥 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ∧ ¬ 𝐴 ≤ 𝑥 ) ) → ( PellFund ‘ 𝐷 ) ≤ 𝑥 )
56 simprr ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) ∧ ( 𝑥 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ∧ ¬ 𝐴 ≤ 𝑥 ) ) → ¬ 𝐴 ≤ 𝑥 )
57 15 adantr ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) ∧ ( 𝑥 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ∧ ¬ 𝐴 ≤ 𝑥 ) ) → ( Pell14QR ‘ 𝐷 ) ⊆ ℝ )
58 57 48 sseldd ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) ∧ ( 𝑥 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ∧ ¬ 𝐴 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ )
59 simpl2 ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) ∧ ( 𝑥 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ∧ ¬ 𝐴 ≤ 𝑥 ) ) → 𝐴 ∈ ℝ )
60 58 59 ltnled ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) ∧ ( 𝑥 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ∧ ¬ 𝐴 ≤ 𝑥 ) ) → ( 𝑥 < 𝐴 ↔ ¬ 𝐴 ≤ 𝑥 ) )
61 56 60 mpbird ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) ∧ ( 𝑥 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ∧ ¬ 𝐴 ≤ 𝑥 ) ) → 𝑥 < 𝐴 )
62 55 61 jca ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) ∧ ( 𝑥 ∈ { 𝑎 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑎 } ∧ ¬ 𝐴 ≤ 𝑥 ) ) → ( ( PellFund ‘ 𝐷 ) ≤ 𝑥 ∧ 𝑥 < 𝐴 ) )
63 30 45 62 reximssdv ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ∧ ( PellFund ‘ 𝐷 ) < 𝐴 ) → ∃ 𝑥 ∈ ( Pell1QR ‘ 𝐷 ) ( ( PellFund ‘ 𝐷 ) ≤ 𝑥 ∧ 𝑥 < 𝐴 ) )