Metamath Proof Explorer

Theorem pellexlem5

Description: Lemma for pellex . Invoking fiphp3d , we have infinitely many near-solutions for some specific norm. (Contributed by Stefan O'Rear, 19-Oct-2014)

Ref Expression
Assertion pellexlem5 ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ∃ 𝑥 ∈ ℤ ( 𝑥 ≠ 0 ∧ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } ≈ ℕ ) )

Proof

Step Hyp Ref Expression
1 pellexlem4 ⊢ ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ≈ ℕ )
2 fzfi ⊢ ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ... ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ∈ Fin
3 diffi ⊢ ( ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ... ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ∈ Fin → ( ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ... ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ∖ { 0 } ) ∈ Fin )
4 2 3 mp1i ⊢ ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ( ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ... ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ∖ { 0 } ) ∈ Fin )
5 elopab ⊢ ( 𝑎 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑎 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ) )
6 fveq2 ⊢ ( 𝑎 = ⟨ 𝑦 , 𝑧 ⟩ → ( 1st ‘ 𝑎 ) = ( 1st ‘ ⟨ 𝑦 , 𝑧 ⟩ ) )
7 6 oveq1d ⊢ ( 𝑎 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( 1st ‘ 𝑎 ) ↑ 2 ) = ( ( 1st ‘ ⟨ 𝑦 , 𝑧 ⟩ ) ↑ 2 ) )
8 fveq2 ⊢ ( 𝑎 = ⟨ 𝑦 , 𝑧 ⟩ → ( 2nd ‘ 𝑎 ) = ( 2nd ‘ ⟨ 𝑦 , 𝑧 ⟩ ) )
9 8 oveq1d ⊢ ( 𝑎 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( 2nd ‘ 𝑎 ) ↑ 2 ) = ( ( 2nd ‘ ⟨ 𝑦 , 𝑧 ⟩ ) ↑ 2 ) )
10 9 oveq2d ⊢ ( 𝑎 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) = ( 𝐷 · ( ( 2nd ‘ ⟨ 𝑦 , 𝑧 ⟩ ) ↑ 2 ) ) )
11 7 10 oveq12d ⊢ ( 𝑎 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = ( ( ( 1st ‘ ⟨ 𝑦 , 𝑧 ⟩ ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ ⟨ 𝑦 , 𝑧 ⟩ ) ↑ 2 ) ) ) )
12 vex ⊢ 𝑦 ∈ V
13 vex ⊢ 𝑧 ∈ V
14 12 13 op1st ⊢ ( 1st ‘ ⟨ 𝑦 , 𝑧 ⟩ ) = 𝑦
15 14 oveq1i ⊢ ( ( 1st ‘ ⟨ 𝑦 , 𝑧 ⟩ ) ↑ 2 ) = ( 𝑦 ↑ 2 )
16 12 13 op2nd ⊢ ( 2nd ‘ ⟨ 𝑦 , 𝑧 ⟩ ) = 𝑧
17 16 oveq1i ⊢ ( ( 2nd ‘ ⟨ 𝑦 , 𝑧 ⟩ ) ↑ 2 ) = ( 𝑧 ↑ 2 )
18 17 oveq2i ⊢ ( 𝐷 · ( ( 2nd ‘ ⟨ 𝑦 , 𝑧 ⟩ ) ↑ 2 ) ) = ( 𝐷 · ( 𝑧 ↑ 2 ) )
19 15 18 oveq12i ⊢ ( ( ( 1st ‘ ⟨ 𝑦 , 𝑧 ⟩ ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ ⟨ 𝑦 , 𝑧 ⟩ ) ↑ 2 ) ) ) = ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) )
20 11 19 eqtrdi ⊢ ( 𝑎 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) )
21 20 ad2antrl ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑎 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ) ) → ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) )
22 simprrl ⊢ ( ( 𝐷 ∈ ℕ ∧ ( 𝑎 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ) ) → ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) )
23 simpl ⊢ ( ( 𝐷 ∈ ℕ ∧ ( 𝑎 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ) ) → 𝐷 ∈ ℕ )
24 simprr ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) )
25 24 ad2antll ⊢ ( ( 𝐷 ∈ ℕ ∧ ( 𝑎 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ) ) → ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) )
26 nnz ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℤ )
27 26 ad2antrr ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝐷 ∈ ℕ ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → 𝑦 ∈ ℤ )
28 zsqcl ⊢ ( 𝑦 ∈ ℤ → ( 𝑦 ↑ 2 ) ∈ ℤ )
29 27 28 syl ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝐷 ∈ ℕ ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → ( 𝑦 ↑ 2 ) ∈ ℤ )
30 nnz ⊢ ( 𝐷 ∈ ℕ → 𝐷 ∈ ℤ )
31 30 ad2antrl ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝐷 ∈ ℕ ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → 𝐷 ∈ ℤ )
32 simplr ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝐷 ∈ ℕ ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → 𝑧 ∈ ℕ )
33 32 nnzd ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝐷 ∈ ℕ ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → 𝑧 ∈ ℤ )
34 zsqcl ⊢ ( 𝑧 ∈ ℤ → ( 𝑧 ↑ 2 ) ∈ ℤ )
35 33 34 syl ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝐷 ∈ ℕ ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → ( 𝑧 ↑ 2 ) ∈ ℤ )
36 31 35 zmulcld ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝐷 ∈ ℕ ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → ( 𝐷 · ( 𝑧 ↑ 2 ) ) ∈ ℤ )
37 29 36 zsubcld ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝐷 ∈ ℕ ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ∈ ℤ )
38 1re ⊢ 1 ∈ ℝ
39 2re ⊢ 2 ∈ ℝ
40 nnre ⊢ ( 𝐷 ∈ ℕ → 𝐷 ∈ ℝ )
41 40 ad2antrl ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝐷 ∈ ℕ ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → 𝐷 ∈ ℝ )
42 nnnn0 ⊢ ( 𝐷 ∈ ℕ → 𝐷 ∈ ℕ0 )
43 42 ad2antrl ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝐷 ∈ ℕ ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → 𝐷 ∈ ℕ0 )
44 43 nn0ge0d ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝐷 ∈ ℕ ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → 0 ≤ 𝐷 )
45 41 44 resqrtcld ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝐷 ∈ ℕ ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → ( √ ‘ 𝐷 ) ∈ ℝ )
46 remulcl ⊢ ( ( 2 ∈ ℝ ∧ ( √ ‘ 𝐷 ) ∈ ℝ ) → ( 2 · ( √ ‘ 𝐷 ) ) ∈ ℝ )
47 39 45 46 sylancr ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝐷 ∈ ℕ ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → ( 2 · ( √ ‘ 𝐷 ) ) ∈ ℝ )
48 readdcl ⊢ ( ( 1 ∈ ℝ ∧ ( 2 · ( √ ‘ 𝐷 ) ) ∈ ℝ ) → ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ∈ ℝ )
49 38 47 48 sylancr ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝐷 ∈ ℕ ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ∈ ℝ )
50 49 flcld ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝐷 ∈ ℕ ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ∈ ℤ )
51 50 znegcld ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝐷 ∈ ℕ ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ∈ ℤ )
52 37 zred ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝐷 ∈ ℕ ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ∈ ℝ )
53 50 zred ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝐷 ∈ ℕ ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ∈ ℝ )
54 nn0abscl ⊢ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ∈ ℤ → ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) ∈ ℕ0 )
55 37 54 syl ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝐷 ∈ ℕ ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) ∈ ℕ0 )
56 55 nn0zd ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝐷 ∈ ℕ ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) ∈ ℤ )
57 56 zred ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝐷 ∈ ℕ ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) ∈ ℝ )
58 peano2re ⊢ ( ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ∈ ℝ → ( ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) + 1 ) ∈ ℝ )
59 53 58 syl ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝐷 ∈ ℕ ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → ( ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) + 1 ) ∈ ℝ )
60 simprr ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝐷 ∈ ℕ ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) )
61 flltp1 ⊢ ( ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ∈ ℝ → ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) < ( ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) + 1 ) )
62 49 61 syl ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝐷 ∈ ℕ ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) < ( ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) + 1 ) )
63 57 49 59 60 62 lttrd ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝐷 ∈ ℕ ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) + 1 ) )
64 zleltp1 ⊢ ( ( ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) ∈ ℤ ∧ ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ∈ ℤ ) → ( ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) ≤ ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ↔ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) + 1 ) ) )
65 56 50 64 syl2anc ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝐷 ∈ ℕ ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → ( ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) ≤ ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ↔ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) + 1 ) ) )
66 63 65 mpbird ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝐷 ∈ ℕ ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) ≤ ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) )
67 absle ⊢ ( ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ∈ ℝ ∧ ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ∈ ℝ ) → ( ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) ≤ ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ↔ ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ≤ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≤ ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ) )
68 67 biimpa ⊢ ( ( ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ∈ ℝ ∧ ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ∈ ℝ ) ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) ≤ ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ≤ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≤ ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) )
69 52 53 66 68 syl21anc ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝐷 ∈ ℕ ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ≤ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≤ ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) )
70 elfz ⊢ ( ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ∈ ℤ ∧ - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ∈ ℤ ∧ ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ∈ ℤ ) → ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ∈ ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ... ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ↔ ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ≤ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≤ ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ) )
71 70 biimpar ⊢ ( ( ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ∈ ℤ ∧ - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ∈ ℤ ∧ ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ∈ ℤ ) ∧ ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ≤ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≤ ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ) → ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ∈ ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ... ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) )
72 37 51 50 69 71 syl31anc ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝐷 ∈ ℕ ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ∈ ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ... ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) )
73 22 23 25 72 syl12anc ⊢ ( ( 𝐷 ∈ ℕ ∧ ( 𝑎 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ) ) → ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ∈ ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ... ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) )
74 73 adantlr ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑎 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ) ) → ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ∈ ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ... ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) )
75 simprl ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 )
76 75 ad2antll ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑎 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ) ) → ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 )
77 eldifsn ⊢ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ∈ ( ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ... ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ∖ { 0 } ) ↔ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ∈ ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ... ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ) )
78 74 76 77 sylanbrc ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑎 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ) ) → ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ∈ ( ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ... ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ∖ { 0 } ) )
79 21 78 eqeltrd ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑎 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ) ) → ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) ∈ ( ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ... ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ∖ { 0 } ) )
80 79 ex ⊢ ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ( ( 𝑎 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ) → ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) ∈ ( ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ... ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ∖ { 0 } ) ) )
81 80 exlimdvv ⊢ ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ( ∃ 𝑦 ∃ 𝑧 ( 𝑎 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ) → ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) ∈ ( ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ... ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ∖ { 0 } ) ) )
82 5 81 biimtrid ⊢ ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ( 𝑎 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } → ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) ∈ ( ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ... ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ∖ { 0 } ) ) )
83 82 imp ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ) → ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) ∈ ( ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ... ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ∖ { 0 } ) )
84 1 4 83 fiphp3d ⊢ ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ∃ 𝑥 ∈ ( ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ... ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ∖ { 0 } ) { 𝑎 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ∣ ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = 𝑥 } ≈ ℕ )
85 eldif ⊢ ( 𝑥 ∈ ( ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ... ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ∖ { 0 } ) ↔ ( 𝑥 ∈ ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ... ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ∧ ¬ 𝑥 ∈ { 0 } ) )
86 elfzelz ⊢ ( 𝑥 ∈ ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ... ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → 𝑥 ∈ ℤ )
87 simp2 ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑥 ∈ ℤ ∧ ¬ 𝑥 ∈ { 0 } ) → 𝑥 ∈ ℤ )
88 velsn ⊢ ( 𝑥 ∈ { 0 } ↔ 𝑥 = 0 )
89 88 biimpri ⊢ ( 𝑥 = 0 → 𝑥 ∈ { 0 } )
90 89 necon3bi ⊢ ( ¬ 𝑥 ∈ { 0 } → 𝑥 ≠ 0 )
91 90 3ad2ant3 ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑥 ∈ ℤ ∧ ¬ 𝑥 ∈ { 0 } ) → 𝑥 ≠ 0 )
92 87 91 jca ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑥 ∈ ℤ ∧ ¬ 𝑥 ∈ { 0 } ) → ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) )
93 92 3exp ⊢ ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ( 𝑥 ∈ ℤ → ( ¬ 𝑥 ∈ { 0 } → ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) ) )
94 86 93 syl5 ⊢ ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ( 𝑥 ∈ ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ... ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) → ( ¬ 𝑥 ∈ { 0 } → ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) ) )
95 94 impd ⊢ ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ( ( 𝑥 ∈ ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ... ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ∧ ¬ 𝑥 ∈ { 0 } ) → ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) )
96 85 95 biimtrid ⊢ ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ( 𝑥 ∈ ( ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ... ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ∖ { 0 } ) → ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) )
97 simp2l ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ∧ { 𝑎 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ∣ ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = 𝑥 } ≈ ℕ ) → 𝑥 ∈ ℤ )
98 simp2r ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ∧ { 𝑎 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ∣ ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = 𝑥 } ≈ ℕ ) → 𝑥 ≠ 0 )
99 nnex ⊢ ℕ ∈ V
100 99 99 xpex ⊢ ( ℕ × ℕ ) ∈ V
101 opabssxp ⊢ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } ⊆ ( ℕ × ℕ )
102 ssdomg ⊢ ( ( ℕ × ℕ ) ∈ V → ( { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } ⊆ ( ℕ × ℕ ) → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } ≼ ( ℕ × ℕ ) ) )
103 100 101 102 mp2 ⊢ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } ≼ ( ℕ × ℕ )
104 xpnnen ⊢ ( ℕ × ℕ ) ≈ ℕ
105 domentr ⊢ ( ( { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } ≼ ( ℕ × ℕ ) ∧ ( ℕ × ℕ ) ≈ ℕ ) → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } ≼ ℕ )
106 103 104 105 mp2an ⊢ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } ≼ ℕ
107 ensym ⊢ ( { 𝑎 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ∣ ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = 𝑥 } ≈ ℕ → ℕ ≈ { 𝑎 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ∣ ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = 𝑥 } )
108 107 3ad2ant3 ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ∧ { 𝑎 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ∣ ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = 𝑥 } ≈ ℕ ) → ℕ ≈ { 𝑎 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ∣ ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = 𝑥 } )
109 100 101 ssexi ⊢ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } ∈ V
110 fveq2 ⊢ ( 𝑎 = 𝑏 → ( 1st ‘ 𝑎 ) = ( 1st ‘ 𝑏 ) )
111 110 oveq1d ⊢ ( 𝑎 = 𝑏 → ( ( 1st ‘ 𝑎 ) ↑ 2 ) = ( ( 1st ‘ 𝑏 ) ↑ 2 ) )
112 fveq2 ⊢ ( 𝑎 = 𝑏 → ( 2nd ‘ 𝑎 ) = ( 2nd ‘ 𝑏 ) )
113 112 oveq1d ⊢ ( 𝑎 = 𝑏 → ( ( 2nd ‘ 𝑎 ) ↑ 2 ) = ( ( 2nd ‘ 𝑏 ) ↑ 2 ) )
114 113 oveq2d ⊢ ( 𝑎 = 𝑏 → ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) = ( 𝐷 · ( ( 2nd ‘ 𝑏 ) ↑ 2 ) ) )
115 111 114 oveq12d ⊢ ( 𝑎 = 𝑏 → ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = ( ( ( 1st ‘ 𝑏 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑏 ) ↑ 2 ) ) ) )
116 115 eqeq1d ⊢ ( 𝑎 = 𝑏 → ( ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = 𝑥 ↔ ( ( ( 1st ‘ 𝑏 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑏 ) ↑ 2 ) ) ) = 𝑥 ) )
117 116 elrab ⊢ ( 𝑏 ∈ { 𝑎 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ∣ ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = 𝑥 } ↔ ( 𝑏 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ∧ ( ( ( 1st ‘ 𝑏 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑏 ) ↑ 2 ) ) ) = 𝑥 ) )
118 simprl ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) ∧ ( ( ( 1st ‘ 𝑏 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑏 ) ↑ 2 ) ) ) = 𝑥 ) ∧ ( 𝑏 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ) ) → 𝑏 = ⟨ 𝑦 , 𝑧 ⟩ )
119 simprrl ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) ∧ ( ( ( 1st ‘ 𝑏 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑏 ) ↑ 2 ) ) ) = 𝑥 ) ∧ ( 𝑏 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ) ) → ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) )
120 fveq2 ⊢ ( 𝑏 = ⟨ 𝑦 , 𝑧 ⟩ → ( 1st ‘ 𝑏 ) = ( 1st ‘ ⟨ 𝑦 , 𝑧 ⟩ ) )
121 120 oveq1d ⊢ ( 𝑏 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( 1st ‘ 𝑏 ) ↑ 2 ) = ( ( 1st ‘ ⟨ 𝑦 , 𝑧 ⟩ ) ↑ 2 ) )
122 fveq2 ⊢ ( 𝑏 = ⟨ 𝑦 , 𝑧 ⟩ → ( 2nd ‘ 𝑏 ) = ( 2nd ‘ ⟨ 𝑦 , 𝑧 ⟩ ) )
123 122 oveq1d ⊢ ( 𝑏 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( 2nd ‘ 𝑏 ) ↑ 2 ) = ( ( 2nd ‘ ⟨ 𝑦 , 𝑧 ⟩ ) ↑ 2 ) )
124 123 oveq2d ⊢ ( 𝑏 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝐷 · ( ( 2nd ‘ 𝑏 ) ↑ 2 ) ) = ( 𝐷 · ( ( 2nd ‘ ⟨ 𝑦 , 𝑧 ⟩ ) ↑ 2 ) ) )
125 121 124 oveq12d ⊢ ( 𝑏 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( ( 1st ‘ 𝑏 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑏 ) ↑ 2 ) ) ) = ( ( ( 1st ‘ ⟨ 𝑦 , 𝑧 ⟩ ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ ⟨ 𝑦 , 𝑧 ⟩ ) ↑ 2 ) ) ) )
126 125 19 eqtr2di ⊢ ( 𝑏 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = ( ( ( 1st ‘ 𝑏 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑏 ) ↑ 2 ) ) ) )
127 126 ad2antrl ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) ∧ ( ( ( 1st ‘ 𝑏 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑏 ) ↑ 2 ) ) ) = 𝑥 ) ∧ ( 𝑏 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ) ) → ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = ( ( ( 1st ‘ 𝑏 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑏 ) ↑ 2 ) ) ) )
128 simplr ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) ∧ ( ( ( 1st ‘ 𝑏 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑏 ) ↑ 2 ) ) ) = 𝑥 ) ∧ ( 𝑏 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ) ) → ( ( ( 1st ‘ 𝑏 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑏 ) ↑ 2 ) ) ) = 𝑥 )
129 127 128 eqtrd ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) ∧ ( ( ( 1st ‘ 𝑏 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑏 ) ↑ 2 ) ) ) = 𝑥 ) ∧ ( 𝑏 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ) ) → ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 )
130 118 119 129 jca32 ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) ∧ ( ( ( 1st ‘ 𝑏 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑏 ) ↑ 2 ) ) ) = 𝑥 ) ∧ ( 𝑏 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ) ) → ( 𝑏 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) ) )
131 130 ex ⊢ ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) ∧ ( ( ( 1st ‘ 𝑏 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑏 ) ↑ 2 ) ) ) = 𝑥 ) → ( ( 𝑏 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ) → ( 𝑏 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) ) ) )
132 131 2eximdv ⊢ ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) ∧ ( ( ( 1st ‘ 𝑏 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑏 ) ↑ 2 ) ) ) = 𝑥 ) → ( ∃ 𝑦 ∃ 𝑧 ( 𝑏 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ) → ∃ 𝑦 ∃ 𝑧 ( 𝑏 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) ) ) )
133 elopab ⊢ ( 𝑏 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑏 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ) )
134 elopab ⊢ ( 𝑏 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑏 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) ) )
135 132 133 134 3imtr4g ⊢ ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) ∧ ( ( ( 1st ‘ 𝑏 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑏 ) ↑ 2 ) ) ) = 𝑥 ) → ( 𝑏 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } → 𝑏 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } ) )
136 135 expimpd ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) → ( ( ( ( ( 1st ‘ 𝑏 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑏 ) ↑ 2 ) ) ) = 𝑥 ∧ 𝑏 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ) → 𝑏 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } ) )
137 136 ancomsd ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) → ( ( 𝑏 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ∧ ( ( ( 1st ‘ 𝑏 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑏 ) ↑ 2 ) ) ) = 𝑥 ) → 𝑏 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } ) )
138 117 137 biimtrid ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) → ( 𝑏 ∈ { 𝑎 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ∣ ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = 𝑥 } → 𝑏 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } ) )
139 138 ssrdv ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ) → { 𝑎 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ∣ ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = 𝑥 } ⊆ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } )
140 139 3adant3 ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ∧ { 𝑎 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ∣ ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = 𝑥 } ≈ ℕ ) → { 𝑎 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ∣ ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = 𝑥 } ⊆ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } )
141 ssdomg ⊢ ( { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } ∈ V → ( { 𝑎 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ∣ ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = 𝑥 } ⊆ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } → { 𝑎 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ∣ ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = 𝑥 } ≼ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } ) )
142 109 140 141 mpsyl ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ∧ { 𝑎 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ∣ ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = 𝑥 } ≈ ℕ ) → { 𝑎 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ∣ ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = 𝑥 } ≼ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } )
143 endomtr ⊢ ( ( ℕ ≈ { 𝑎 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ∣ ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = 𝑥 } ∧ { 𝑎 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ∣ ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = 𝑥 } ≼ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } ) → ℕ ≼ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } )
144 108 142 143 syl2anc ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ∧ { 𝑎 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ∣ ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = 𝑥 } ≈ ℕ ) → ℕ ≼ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } )
145 sbth ⊢ ( ( { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } ≼ ℕ ∧ ℕ ≼ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } ) → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } ≈ ℕ )
146 106 144 145 sylancr ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ∧ { 𝑎 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ∣ ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = 𝑥 } ≈ ℕ ) → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } ≈ ℕ )
147 97 98 146 jca32 ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) ∧ { 𝑎 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ∣ ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = 𝑥 } ≈ ℕ ) → ( 𝑥 ∈ ℤ ∧ ( 𝑥 ≠ 0 ∧ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } ≈ ℕ ) ) )
148 147 3exp ⊢ ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ( ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) → ( { 𝑎 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ∣ ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = 𝑥 } ≈ ℕ → ( 𝑥 ∈ ℤ ∧ ( 𝑥 ≠ 0 ∧ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } ≈ ℕ ) ) ) ) )
149 96 148 syld ⊢ ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ( 𝑥 ∈ ( ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ... ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ∖ { 0 } ) → ( { 𝑎 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ∣ ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = 𝑥 } ≈ ℕ → ( 𝑥 ∈ ℤ ∧ ( 𝑥 ≠ 0 ∧ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } ≈ ℕ ) ) ) ) )
150 149 impd ⊢ ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ( ( 𝑥 ∈ ( ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ... ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ∖ { 0 } ) ∧ { 𝑎 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ∣ ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = 𝑥 } ≈ ℕ ) → ( 𝑥 ∈ ℤ ∧ ( 𝑥 ≠ 0 ∧ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } ≈ ℕ ) ) ) )
151 150 reximdv2 ⊢ ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ( ∃ 𝑥 ∈ ( ( - ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ... ( ⌊ ‘ ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ∖ { 0 } ) { 𝑎 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ∣ ( ( ( 1st ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( 2nd ‘ 𝑎 ) ↑ 2 ) ) ) = 𝑥 } ≈ ℕ → ∃ 𝑥 ∈ ℤ ( 𝑥 ≠ 0 ∧ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } ≈ ℕ ) ) )
152 84 151 mpd ⊢ ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ∃ 𝑥 ∈ ℤ ( 𝑥 ≠ 0 ∧ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = 𝑥 ) } ≈ ℕ ) )