Metamath Proof Explorer


Definition df-pell1234qr

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

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpell1234qr Pell1234QR
1 vx 𝑥
2 cn
3 csquarenn NN
4 2 3 cdif ( ℕ ∖ ◻NN )
5 vy 𝑦
6 cr
7 vz 𝑧
8 cz
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 𝑤 ∈ ℤ ( 𝑦 = ( 𝑧 + ( ( √ ‘ 𝑥 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝑥 · ( 𝑤 ↑ 2 ) ) ) = 1 )
32 31 7 8 wrex 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ ( 𝑦 = ( 𝑧 + ( ( √ ‘ 𝑥 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝑥 · ( 𝑤 ↑ 2 ) ) ) = 1 )
33 32 5 6 crab { 𝑦 ∈ ℝ ∣ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ ( 𝑦 = ( 𝑧 + ( ( √ ‘ 𝑥 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝑥 · ( 𝑤 ↑ 2 ) ) ) = 1 ) }
34 1 4 33 cmpt ( 𝑥 ∈ ( ℕ ∖ ◻NN ) ↦ { 𝑦 ∈ ℝ ∣ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ ( 𝑦 = ( 𝑧 + ( ( √ ‘ 𝑥 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝑥 · ( 𝑤 ↑ 2 ) ) ) = 1 ) } )
35 0 34 wceq Pell1234QR = ( 𝑥 ∈ ( ℕ ∖ ◻NN ) ↦ { 𝑦 ∈ ℝ ∣ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ ( 𝑦 = ( 𝑧 + ( ( √ ‘ 𝑥 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝑥 · ( 𝑤 ↑ 2 ) ) ) = 1 ) } )