Definition df-pell1qr

Description: Define the solutions of a Pell equation in the first quadrant. To avoid pair pain, we represent this via the canonical embedding into the reals. (Contributed by Stefan O'Rear, 17-Sep-2014)

	Ref	Expression
Assertion	df-pell1qr	⊢ Pell1QR = ( 𝑥 ∈ ( ℕ ∖ ◻NN ) ↦ { 𝑦 ∈ ℝ ∣ ∃ 𝑧 ∈ ℕ0 ∃ 𝑤 ∈ ℕ0 ( 𝑦 = ( 𝑧 + ( ( √ ‘ 𝑥 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝑥 · ( 𝑤 ↑ 2 ) ) ) = 1 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpell1qr	⊢ Pell1QR
1		vx	⊢ 𝑥
2		cn	⊢ ℕ
3		csquarenn	⊢ ◻NN
4	2 3	cdif	⊢ ( ℕ ∖ ◻NN )
5		vy	⊢ 𝑦
6		cr	⊢ ℝ
7		vz	⊢ 𝑧
8		cn0	⊢ ℕ0
9		vw	⊢ 𝑤
10	5	cv	⊢ 𝑦
11	7	cv	⊢ 𝑧
12		caddc	⊢ +
13		csqrt	⊢ √
14	1	cv	⊢ 𝑥
15	14 13	cfv	⊢ ( √ ‘ 𝑥 )
16		cmul	⊢ ·
17	9	cv	⊢ 𝑤
18	15 17 16	co	⊢ ( ( √ ‘ 𝑥 ) · 𝑤 )
19	11 18 12	co	⊢ ( 𝑧 + ( ( √ ‘ 𝑥 ) · 𝑤 ) )
20	10 19	wceq	⊢ 𝑦 = ( 𝑧 + ( ( √ ‘ 𝑥 ) · 𝑤 ) )
21		cexp	⊢ ↑
22		c2	⊢ 2
23	11 22 21	co	⊢ ( 𝑧 ↑ 2 )
24		cmin	⊢ −
25	17 22 21	co	⊢ ( 𝑤 ↑ 2 )
26	14 25 16	co	⊢ ( 𝑥 · ( 𝑤 ↑ 2 ) )
27	23 26 24	co	⊢ ( ( 𝑧 ↑ 2 ) − ( 𝑥 · ( 𝑤 ↑ 2 ) ) )
28		c1	⊢ 1
29	27 28	wceq	⊢ ( ( 𝑧 ↑ 2 ) − ( 𝑥 · ( 𝑤 ↑ 2 ) ) ) = 1
30	20 29	wa	⊢ ( 𝑦 = ( 𝑧 + ( ( √ ‘ 𝑥 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝑥 · ( 𝑤 ↑ 2 ) ) ) = 1 )
31	30 9 8	wrex	⊢ ∃ 𝑤 ∈ ℕ0 ( 𝑦 = ( 𝑧 + ( ( √ ‘ 𝑥 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝑥 · ( 𝑤 ↑ 2 ) ) ) = 1 )
32	31 7 8	wrex	⊢ ∃ 𝑧 ∈ ℕ0 ∃ 𝑤 ∈ ℕ0 ( 𝑦 = ( 𝑧 + ( ( √ ‘ 𝑥 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝑥 · ( 𝑤 ↑ 2 ) ) ) = 1 )
33	32 5 6	crab	⊢ { 𝑦 ∈ ℝ ∣ ∃ 𝑧 ∈ ℕ0 ∃ 𝑤 ∈ ℕ0 ( 𝑦 = ( 𝑧 + ( ( √ ‘ 𝑥 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝑥 · ( 𝑤 ↑ 2 ) ) ) = 1 ) }
34	1 4 33	cmpt	⊢ ( 𝑥 ∈ ( ℕ ∖ ◻NN ) ↦ { 𝑦 ∈ ℝ ∣ ∃ 𝑧 ∈ ℕ0 ∃ 𝑤 ∈ ℕ0 ( 𝑦 = ( 𝑧 + ( ( √ ‘ 𝑥 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝑥 · ( 𝑤 ↑ 2 ) ) ) = 1 ) } )
35	0 34	wceq	⊢ Pell1QR = ( 𝑥 ∈ ( ℕ ∖ ◻NN ) ↦ { 𝑦 ∈ ℝ ∣ ∃ 𝑧 ∈ ℕ0 ∃ 𝑤 ∈ ℕ0 ( 𝑦 = ( 𝑧 + ( ( √ ‘ 𝑥 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝑥 · ( 𝑤 ↑ 2 ) ) ) = 1 ) } )