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 < 𝑥 )