Metamath Proof Explorer

Theorem pellqrex

Description: There is a nontrivial solution of a Pell equation in the first quadrant. (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion pellqrex ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ∃ 𝑥 ∈ ( Pell1QR ‘ 𝐷 ) 1 < 𝑥 )

Proof

Step Hyp Ref Expression
1 eldifi ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 𝐷 ∈ ℕ )
2 eldifn ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ¬ 𝐷 ∈ ◻NN )
3 1 anim1i ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( √ ‘ 𝐷 ) ∈ ℚ ) → ( 𝐷 ∈ ℕ ∧ ( √ ‘ 𝐷 ) ∈ ℚ ) )
4 fveq2 ⊢ ( 𝑎 = 𝐷 → ( √ ‘ 𝑎 ) = ( √ ‘ 𝐷 ) )
5 4 eleq1d ⊢ ( 𝑎 = 𝐷 → ( ( √ ‘ 𝑎 ) ∈ ℚ ↔ ( √ ‘ 𝐷 ) ∈ ℚ ) )
6 df-squarenn ⊢ ◻NN = { 𝑎 ∈ ℕ ∣ ( √ ‘ 𝑎 ) ∈ ℚ }
7 5 6 elrab2 ⊢ ( 𝐷 ∈ ◻NN ↔ ( 𝐷 ∈ ℕ ∧ ( √ ‘ 𝐷 ) ∈ ℚ ) )
8 3 7 sylibr ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( √ ‘ 𝐷 ) ∈ ℚ ) → 𝐷 ∈ ◻NN )
9 2 8 mtand ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ¬ ( √ ‘ 𝐷 ) ∈ ℚ )
10 pellex ⊢ ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ∃ 𝑐 ∈ ℕ ∃ 𝑑 ∈ ℕ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 )
11 1 9 10 syl2anc ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ∃ 𝑐 ∈ ℕ ∃ 𝑑 ∈ ℕ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 )
12 simpll ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) → 𝐷 ∈ ( ℕ ∖ ◻NN ) )
13 nnnn0 ⊢ ( 𝑐 ∈ ℕ → 𝑐 ∈ ℕ0 )
14 13 adantr ⊢ ( ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) → 𝑐 ∈ ℕ0 )
15 14 ad2antlr ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) → 𝑐 ∈ ℕ0 )
16 nnnn0 ⊢ ( 𝑑 ∈ ℕ → 𝑑 ∈ ℕ0 )
17 16 adantl ⊢ ( ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) → 𝑑 ∈ ℕ0 )
18 17 ad2antlr ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) → 𝑑 ∈ ℕ0 )
19 simpr ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) → ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 )
20 pellqrexplicit ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝑐 ∈ ℕ0 ∧ 𝑑 ∈ ℕ0 ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) → ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∈ ( Pell1QR ‘ 𝐷 ) )
21 12 15 18 19 20 syl31anc ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) → ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∈ ( Pell1QR ‘ 𝐷 ) )
22 1re ⊢ 1 ∈ ℝ
23 22 a1i ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → 1 ∈ ℝ )
24 22 22 readdcli ⊢ ( 1 + 1 ) ∈ ℝ
25 24 a1i ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → ( 1 + 1 ) ∈ ℝ )
26 nnre ⊢ ( 𝑐 ∈ ℕ → 𝑐 ∈ ℝ )
27 26 ad2antrl ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → 𝑐 ∈ ℝ )
28 1 adantr ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → 𝐷 ∈ ℕ )
29 28 nnrpd ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → 𝐷 ∈ ℝ+ )
30 29 rpsqrtcld ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → ( √ ‘ 𝐷 ) ∈ ℝ+ )
31 30 rpred ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → ( √ ‘ 𝐷 ) ∈ ℝ )
32 nnre ⊢ ( 𝑑 ∈ ℕ → 𝑑 ∈ ℝ )
33 32 ad2antll ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → 𝑑 ∈ ℝ )
34 31 33 remulcld ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → ( ( √ ‘ 𝐷 ) · 𝑑 ) ∈ ℝ )
35 27 34 readdcld ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∈ ℝ )
36 22 ltp1i ⊢ 1 < ( 1 + 1 )
37 36 a1i ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → 1 < ( 1 + 1 ) )
38 nnge1 ⊢ ( 𝑐 ∈ ℕ → 1 ≤ 𝑐 )
39 38 ad2antrl ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → 1 ≤ 𝑐 )
40 1t1e1 ⊢ ( 1 · 1 ) = 1
41 nnge1 ⊢ ( 𝐷 ∈ ℕ → 1 ≤ 𝐷 )
42 sq1 ⊢ ( 1 ↑ 2 ) = 1
43 42 a1i ⊢ ( 𝐷 ∈ ℕ → ( 1 ↑ 2 ) = 1 )
44 nncn ⊢ ( 𝐷 ∈ ℕ → 𝐷 ∈ ℂ )
45 44 sqsqrtd ⊢ ( 𝐷 ∈ ℕ → ( ( √ ‘ 𝐷 ) ↑ 2 ) = 𝐷 )
46 41 43 45 3brtr4d ⊢ ( 𝐷 ∈ ℕ → ( 1 ↑ 2 ) ≤ ( ( √ ‘ 𝐷 ) ↑ 2 ) )
47 22 a1i ⊢ ( 𝐷 ∈ ℕ → 1 ∈ ℝ )
48 nnrp ⊢ ( 𝐷 ∈ ℕ → 𝐷 ∈ ℝ+ )
49 48 rpsqrtcld ⊢ ( 𝐷 ∈ ℕ → ( √ ‘ 𝐷 ) ∈ ℝ+ )
50 49 rpred ⊢ ( 𝐷 ∈ ℕ → ( √ ‘ 𝐷 ) ∈ ℝ )
51 0le1 ⊢ 0 ≤ 1
52 51 a1i ⊢ ( 𝐷 ∈ ℕ → 0 ≤ 1 )
53 49 rpge0d ⊢ ( 𝐷 ∈ ℕ → 0 ≤ ( √ ‘ 𝐷 ) )
54 47 50 52 53 le2sqd ⊢ ( 𝐷 ∈ ℕ → ( 1 ≤ ( √ ‘ 𝐷 ) ↔ ( 1 ↑ 2 ) ≤ ( ( √ ‘ 𝐷 ) ↑ 2 ) ) )
55 46 54 mpbird ⊢ ( 𝐷 ∈ ℕ → 1 ≤ ( √ ‘ 𝐷 ) )
56 28 55 syl ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → 1 ≤ ( √ ‘ 𝐷 ) )
57 nnge1 ⊢ ( 𝑑 ∈ ℕ → 1 ≤ 𝑑 )
58 57 ad2antll ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → 1 ≤ 𝑑 )
59 23 51 jctir ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → ( 1 ∈ ℝ ∧ 0 ≤ 1 ) )
60 lemul12a ⊢ ( ( ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ ( √ ‘ 𝐷 ) ∈ ℝ ) ∧ ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ 𝑑 ∈ ℝ ) ) → ( ( 1 ≤ ( √ ‘ 𝐷 ) ∧ 1 ≤ 𝑑 ) → ( 1 · 1 ) ≤ ( ( √ ‘ 𝐷 ) · 𝑑 ) ) )
61 59 31 59 33 60 syl22anc ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → ( ( 1 ≤ ( √ ‘ 𝐷 ) ∧ 1 ≤ 𝑑 ) → ( 1 · 1 ) ≤ ( ( √ ‘ 𝐷 ) · 𝑑 ) ) )
62 56 58 61 mp2and ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → ( 1 · 1 ) ≤ ( ( √ ‘ 𝐷 ) · 𝑑 ) )
63 40 62 eqbrtrrid ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → 1 ≤ ( ( √ ‘ 𝐷 ) · 𝑑 ) )
64 23 23 27 34 39 63 le2addd ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → ( 1 + 1 ) ≤ ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) )
65 23 25 35 37 64 ltletrd ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → 1 < ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) )
66 65 adantr ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) → 1 < ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) )
67 breq2 ⊢ ( 𝑥 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) → ( 1 < 𝑥 ↔ 1 < ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ) )
68 67 rspcev ⊢ ( ( ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∈ ( Pell1QR ‘ 𝐷 ) ∧ 1 < ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ) → ∃ 𝑥 ∈ ( Pell1QR ‘ 𝐷 ) 1 < 𝑥 )
69 21 66 68 syl2anc ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) → ∃ 𝑥 ∈ ( Pell1QR ‘ 𝐷 ) 1 < 𝑥 )
70 69 ex ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝑐 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → ( ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 → ∃ 𝑥 ∈ ( Pell1QR ‘ 𝐷 ) 1 < 𝑥 ) )
71 70 rexlimdvva ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ∃ 𝑐 ∈ ℕ ∃ 𝑑 ∈ ℕ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 → ∃ 𝑥 ∈ ( Pell1QR ‘ 𝐷 ) 1 < 𝑥 ) )
72 11 71 mpd ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ∃ 𝑥 ∈ ( Pell1QR ‘ 𝐷 ) 1 < 𝑥 )