Definition df-pell14qr

Description: Define the positive solutions of a Pell equation. (Contributed by Stefan O'Rear, 17-Sep-2014)

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

Detailed syntax breakdown

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