Step |
Hyp |
Ref |
Expression |
1 |
|
pell1234qrval |
⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( Pell1234QR ‘ 𝐷 ) = { 𝑎 ∈ ℝ ∣ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ ( 𝑎 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝐷 · ( 𝑤 ↑ 2 ) ) ) = 1 ) } ) |
2 |
1
|
eleq2d |
⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ↔ 𝐴 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ ( 𝑎 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝐷 · ( 𝑤 ↑ 2 ) ) ) = 1 ) } ) ) |
3 |
|
eqeq1 |
⊢ ( 𝑎 = 𝐴 → ( 𝑎 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ↔ 𝐴 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ) ) |
4 |
3
|
anbi1d |
⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝐷 · ( 𝑤 ↑ 2 ) ) ) = 1 ) ↔ ( 𝐴 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝐷 · ( 𝑤 ↑ 2 ) ) ) = 1 ) ) ) |
5 |
4
|
2rexbidv |
⊢ ( 𝑎 = 𝐴 → ( ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ ( 𝑎 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝐷 · ( 𝑤 ↑ 2 ) ) ) = 1 ) ↔ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ ( 𝐴 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝐷 · ( 𝑤 ↑ 2 ) ) ) = 1 ) ) ) |
6 |
5
|
elrab |
⊢ ( 𝐴 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ ( 𝑎 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝐷 · ( 𝑤 ↑ 2 ) ) ) = 1 ) } ↔ ( 𝐴 ∈ ℝ ∧ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ ( 𝐴 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝐷 · ( 𝑤 ↑ 2 ) ) ) = 1 ) ) ) |
7 |
2 6
|
bitrdi |
⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ↔ ( 𝐴 ∈ ℝ ∧ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ ( 𝐴 = ( 𝑧 + ( ( √ ‘ 𝐷 ) · 𝑤 ) ) ∧ ( ( 𝑧 ↑ 2 ) − ( 𝐷 · ( 𝑤 ↑ 2 ) ) ) = 1 ) ) ) ) |