pellexlem5 - Mathbox for Stefan O'Rear

	Mathbox for Stefan O'Rear		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > pellexlem5		Structured version Visualization version GIF version

Theorem pellexlem5 43487

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

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

Distinct variable group: 𝑥,𝐷,𝑦,𝑧

Proof of Theorem pellexlem5 Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		pellexlem4 43486	. . 3 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ≈ ℕ)
2		fzfi 14008	. . . 4 ⊢ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∈ Fin
3		diffi 9159	. . . 4 ⊢ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∈ Fin → ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}) ∈ Fin)
4	2, 3	mp1i 14	. . 3 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}) ∈ Fin)
5		elopab 5512	. . . . 5 ⊢ (𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ↔ ∃𝑦∃𝑧(𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))))
6		fveq2 6882	. . . . . . . . . . . 12 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → (1^st ‘𝑎) = (1^st ‘⟨𝑦, 𝑧⟩))
7	6	oveq1d 7426	. . . . . . . . . . 11 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → ((1^st ‘𝑎)↑2) = ((1^st ‘⟨𝑦, 𝑧⟩)↑2))
8		fveq2 6882	. . . . . . . . . . . . 13 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → (2^nd ‘𝑎) = (2^nd ‘⟨𝑦, 𝑧⟩))
9	8	oveq1d 7426	. . . . . . . . . . . 12 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → ((2^nd ‘𝑎)↑2) = ((2^nd ‘⟨𝑦, 𝑧⟩)↑2))
10	9	oveq2d 7427	. . . . . . . . . . 11 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → (𝐷 · ((2^nd ‘𝑎)↑2)) = (𝐷 · ((2^nd ‘⟨𝑦, 𝑧⟩)↑2)))
11	7, 10	oveq12d 7429	. . . . . . . . . 10 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = (((1^st ‘⟨𝑦, 𝑧⟩)↑2) − (𝐷 · ((2^nd ‘⟨𝑦, 𝑧⟩)↑2))))
12		vex 3465	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
13		vex 3465	. . . . . . . . . . . . 13 ⊢ 𝑧 ∈ V
14	12, 13	op1st 7994	. . . . . . . . . . . 12 ⊢ (1^st ‘⟨𝑦, 𝑧⟩) = 𝑦
15	14	oveq1i 7421	. . . . . . . . . . 11 ⊢ ((1^st ‘⟨𝑦, 𝑧⟩)↑2) = (𝑦↑2)
16	12, 13	op2nd 7995	. . . . . . . . . . . . 13 ⊢ (2^nd ‘⟨𝑦, 𝑧⟩) = 𝑧
17	16	oveq1i 7421	. . . . . . . . . . . 12 ⊢ ((2^nd ‘⟨𝑦, 𝑧⟩)↑2) = (𝑧↑2)
18	17	oveq2i 7422	. . . . . . . . . . 11 ⊢ (𝐷 · ((2^nd ‘⟨𝑦, 𝑧⟩)↑2)) = (𝐷 · (𝑧↑2))
19	15, 18	oveq12i 7423	. . . . . . . . . 10 ⊢ (((1^st ‘⟨𝑦, 𝑧⟩)↑2) − (𝐷 · ((2^nd ‘⟨𝑦, 𝑧⟩)↑2))) = ((𝑦↑2) − (𝐷 · (𝑧↑2)))
20	11, 19	eqtrdi 2820	. . . . . . . . 9 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = ((𝑦↑2) − (𝐷 · (𝑧↑2))))
21	20	ad2antrl 740	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = ((𝑦↑2) − (𝐷 · (𝑧↑2))))
22		simprrl 792	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ ℕ ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ))
23		simpl 487	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ ℕ ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → 𝐷 ∈ ℕ)
24		simprr 784	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))
25	24	ad2antll 741	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ ℕ ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))
26		nnz 12612	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
27	26	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝑦 ∈ ℤ)
28		zsqcl 14165	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℤ → (𝑦↑2) ∈ ℤ)
29	27, 28	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (𝑦↑2) ∈ ℤ)
30		nnz 12612	. . . . . . . . . . . . . . 15 ⊢ (𝐷 ∈ ℕ → 𝐷 ∈ ℤ)
31	30	ad2antrl 740	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝐷 ∈ ℤ)
32		simplr 780	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝑧 ∈ ℕ)
33	32	nnzd 12617	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝑧 ∈ ℤ)
34		zsqcl 14165	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ℤ → (𝑧↑2) ∈ ℤ)
35	33, 34	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (𝑧↑2) ∈ ℤ)
36	31, 35	zmulcld 12706	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (𝐷 · (𝑧↑2)) ∈ ℤ)
37	29, 36	zsubcld 12705	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℤ)
38		1re 11208	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
39		2re 12315	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ
40		nnre 12240	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐷 ∈ ℕ → 𝐷 ∈ ℝ)
41	40	ad2antrl 740	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝐷 ∈ ℝ)
42		nnnn0 12511	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷 ∈ ℕ → 𝐷 ∈ ℕ₀)
43	42	ad2antrl 740	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝐷 ∈ ℕ₀)
44	43	nn0ge0d 12568	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 0 ≤ 𝐷)
45	41, 44	resqrtcld 15469	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (√‘𝐷) ∈ ℝ)
46		remulcl 11185	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℝ ∧ (√‘𝐷) ∈ ℝ) → (2 · (√‘𝐷)) ∈ ℝ)
47	39, 45, 46	sylancr 598	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (2 · (√‘𝐷)) ∈ ℝ)
48		readdcl 11183	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℝ ∧ (2 · (√‘𝐷)) ∈ ℝ) → (1 + (2 · (√‘𝐷))) ∈ ℝ)
49	38, 47, 48	sylancr 598	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (1 + (2 · (√‘𝐷))) ∈ ℝ)
50	49	flcld 13831	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℤ)
51	50	znegcld 12702	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → -(⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℤ)
52	37	zred 12700	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℝ)
53	50	zred 12700	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℝ)
54		nn0abscl 15363	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℤ → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ∈ ℕ₀)
55	37, 54	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ∈ ℕ₀)
56	55	nn0zd 12616	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ∈ ℤ)
57	56	zred 12700	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ∈ ℝ)
58		peano2re 11383	. . . . . . . . . . . . . . . 16 ⊢ ((⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℝ → ((⌊‘(1 + (2 · (√‘𝐷)))) + 1) ∈ ℝ)
59	53, 58	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → ((⌊‘(1 + (2 · (√‘𝐷)))) + 1) ∈ ℝ)
60		simprr 784	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))
61		flltp1 13833	. . . . . . . . . . . . . . . 16 ⊢ ((1 + (2 · (√‘𝐷))) ∈ ℝ → (1 + (2 · (√‘𝐷))) < ((⌊‘(1 + (2 · (√‘𝐷)))) + 1))
62	49, 61	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (1 + (2 · (√‘𝐷))) < ((⌊‘(1 + (2 · (√‘𝐷)))) + 1))
63	57, 49, 59, 60, 62	lttrd 11371	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < ((⌊‘(1 + (2 · (√‘𝐷)))) + 1))
64		zleltp1 12645	. . . . . . . . . . . . . . 15 ⊢ (((abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ∈ ℤ ∧ (⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℤ) → ((abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ≤ (⌊‘(1 + (2 · (√‘𝐷)))) ↔ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < ((⌊‘(1 + (2 · (√‘𝐷)))) + 1)))
65	56, 50, 64	syl2anc 595	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → ((abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ≤ (⌊‘(1 + (2 · (√‘𝐷)))) ↔ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < ((⌊‘(1 + (2 · (√‘𝐷)))) + 1)))
66	63, 65	mpbird 260	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ≤ (⌊‘(1 + (2 · (√‘𝐷)))))
67		absle 15367	. . . . . . . . . . . . . 14 ⊢ ((((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℝ ∧ (⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℝ) → ((abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ≤ (⌊‘(1 + (2 · (√‘𝐷)))) ↔ (-(⌊‘(1 + (2 · (√‘𝐷)))) ≤ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≤ (⌊‘(1 + (2 · (√‘𝐷)))))))
68	67	biimpa 481	. . . . . . . . . . . . 13 ⊢ (((((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℝ ∧ (⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℝ) ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ≤ (⌊‘(1 + (2 · (√‘𝐷))))) → (-(⌊‘(1 + (2 · (√‘𝐷)))) ≤ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≤ (⌊‘(1 + (2 · (√‘𝐷))))))
69	52, 53, 66, 68	syl21anc 850	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (-(⌊‘(1 + (2 · (√‘𝐷)))) ≤ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≤ (⌊‘(1 + (2 · (√‘𝐷))))))
70		elfz 13541	. . . . . . . . . . . . 13 ⊢ ((((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℤ ∧ -(⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℤ ∧ (⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℤ) → (((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ↔ (-(⌊‘(1 + (2 · (√‘𝐷)))) ≤ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≤ (⌊‘(1 + (2 · (√‘𝐷)))))))
71	70	biimpar 482	. . . . . . . . . . . 12 ⊢ (((((𝑦↑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 1398	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))))
73	22, 23, 25, 72	syl12anc 849	. . . . . . . . . 10 ⊢ ((𝐷 ∈ ℕ ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))))
74	73	adantlr 727	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))))
75		simprl 782	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0)
76	75	ad2antll 741	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0)
77		eldifsn 4756	. . . . . . . . 9 ⊢ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}) ↔ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0))
78	74, 76, 77	sylanbrc 594	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}))
79	21, 78	eqeltrd 2869	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}))
80	79	ex 417	. . . . . 6 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ((𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))) → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0})))
81	80	exlimdvv 1961	. . . . 5 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → (∃𝑦∃𝑧(𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))) → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0})))
82	5, 81	biimtrid 245	. . . 4 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → (𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0})))
83	82	imp 411	. . 3 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))}) → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}))
84	1, 4, 83	fiphp3d 43473	. 2 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ∃𝑥 ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}){𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ)
85		eldif 3921	. . . . . 6 ⊢ (𝑥 ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}) ↔ (𝑥 ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∧ ¬ 𝑥 ∈ {0}))
86		elfzelz 13552	. . . . . . . 8 ⊢ (𝑥 ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) → 𝑥 ∈ ℤ)
87		simp2 1153	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑥 ∈ ℤ ∧ ¬ 𝑥 ∈ {0}) → 𝑥 ∈ ℤ)
88		velsn 4608	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {0} ↔ 𝑥 = 0)
89	88	biimpri 231	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → 𝑥 ∈ {0})
90	89	necon3bi 2990	. . . . . . . . . . 11 ⊢ (¬ 𝑥 ∈ {0} → 𝑥 ≠ 0)
91	90	3ad2ant3 1151	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑥 ∈ ℤ ∧ ¬ 𝑥 ∈ {0}) → 𝑥 ≠ 0)
92	87, 91	jca 520	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑥 ∈ ℤ ∧ ¬ 𝑥 ∈ {0}) → (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0))
93	92	3exp 1135	. . . . . . . 8 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → (𝑥 ∈ ℤ → (¬ 𝑥 ∈ {0} → (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0))))
94	86, 93	syl5 35	. . . . . . 7 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → (𝑥 ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) → (¬ 𝑥 ∈ {0} → (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0))))
95	94	impd 415	. . . . . 6 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ((𝑥 ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∧ ¬ 𝑥 ∈ {0}) → (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)))
96	85, 95	biimtrid 245	. . . . 5 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → (𝑥 ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}) → (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)))
97		simp2l 1216	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → 𝑥 ∈ ℤ)
98		simp2r 1217	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → 𝑥 ≠ 0)
99		nnex 12239	. . . . . . . . . . 11 ⊢ ℕ ∈ V
100	99, 99	xpex 7752	. . . . . . . . . 10 ⊢ (ℕ × ℕ) ∈ V
101		opabssxp 5754	. . . . . . . . . 10 ⊢ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ⊆ (ℕ × ℕ)
102		ssdomg 8997	. . . . . . . . . 10 ⊢ ((ℕ × ℕ) ∈ V → ({⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ⊆ (ℕ × ℕ) → {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ (ℕ × ℕ)))
103	100, 101, 102	mp2 9	. . . . . . . . 9 ⊢ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ (ℕ × ℕ)
104		xpnnen 16267	. . . . . . . . 9 ⊢ (ℕ × ℕ) ≈ ℕ
105		domentr 9010	. . . . . . . . 9 ⊢ (({⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ (ℕ × ℕ) ∧ (ℕ × ℕ) ≈ ℕ) → {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ ℕ)
106	103, 104, 105	mp2an 704	. . . . . . . 8 ⊢ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ ℕ
107		ensym 9000	. . . . . . . . . 10 ⊢ ({𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ → ℕ ≈ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥})
108	107	3ad2ant3 1151	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → ℕ ≈ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥})
109	100, 101	ssexi 5293	. . . . . . . . . 10 ⊢ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ∈ V
110		fveq2 6882	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑏 → (1^st ‘𝑎) = (1^st ‘𝑏))
111	110	oveq1d 7426	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑏 → ((1^st ‘𝑎)↑2) = ((1^st ‘𝑏)↑2))
112		fveq2 6882	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑏 → (2^nd ‘𝑎) = (2^nd ‘𝑏))
113	112	oveq1d 7426	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑏 → ((2^nd ‘𝑎)↑2) = ((2^nd ‘𝑏)↑2))
114	113	oveq2d 7427	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑏 → (𝐷 · ((2^nd ‘𝑎)↑2)) = (𝐷 · ((2^nd ‘𝑏)↑2)))
115	111, 114	oveq12d 7429	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑏 → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))))
116	115	eqeq1d 2771	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑏 → ((((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥 ↔ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥))
117	116	elrab 3657	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ↔ (𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥))
118		simprl 782	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) ∧ (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → 𝑏 = ⟨𝑦, 𝑧⟩)
119		simprrl 792	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) ∧ (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ))
120		fveq2 6882	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → (1^st ‘𝑏) = (1^st ‘⟨𝑦, 𝑧⟩))
121	120	oveq1d 7426	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → ((1^st ‘𝑏)↑2) = ((1^st ‘⟨𝑦, 𝑧⟩)↑2))
122		fveq2 6882	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → (2^nd ‘𝑏) = (2^nd ‘⟨𝑦, 𝑧⟩))
123	122	oveq1d 7426	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → ((2^nd ‘𝑏)↑2) = ((2^nd ‘⟨𝑦, 𝑧⟩)↑2))
124	123	oveq2d 7427	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → (𝐷 · ((2^nd ‘𝑏)↑2)) = (𝐷 · ((2^nd ‘⟨𝑦, 𝑧⟩)↑2)))
125	121, 124	oveq12d 7429	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = (((1^st ‘⟨𝑦, 𝑧⟩)↑2) − (𝐷 · ((2^nd ‘⟨𝑦, 𝑧⟩)↑2))))
126	125, 19	eqtr2di 2821	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → ((𝑦↑2) − (𝐷 · (𝑧↑2))) = (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))))
127	126	ad2antrl 740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) ∧ (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) = (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))))
128		simplr 780	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) ∧ (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥)
129	127, 128	eqtrd 2804	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) ∧ (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)
130	118, 119, 129	jca32 524	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) ∧ (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)))
131	130	ex 417	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) → ((𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))) → (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥))))
132	131	2eximdv 1946	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) → (∃𝑦∃𝑧(𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))) → ∃𝑦∃𝑧(𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥))))
133		elopab 5512	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ↔ ∃𝑦∃𝑧(𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))))
134		elopab 5512	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ↔ ∃𝑦∃𝑧(𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)))
135	132, 133, 134	3imtr4g 299	. . . . . . . . . . . . . . 15 ⊢ ((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) → (𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} → 𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}))
136	135	expimpd 458	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → (((((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥 ∧ 𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))}) → 𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}))
137	136	ancomsd 470	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → ((𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) → 𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}))
138	117, 137	biimtrid 245	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → (𝑏 ∈ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} → 𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}))
139	138	ssrdv 3949	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ⊆ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)})
140	139	3adant3 1148	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ⊆ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)})
141		ssdomg 8997	. . . . . . . . . 10 ⊢ ({⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ∈ V → ({𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ⊆ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} → {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≼ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}))
142	109, 140, 141	mpsyl 69	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≼ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)})
143		endomtr 9009	. . . . . . . . 9 ⊢ ((ℕ ≈ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≼ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}) → ℕ ≼ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)})
144	108, 142, 143	syl2anc 595	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → ℕ ≼ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)})
145		sbth 9085	. . . . . . . 8 ⊢ (({⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ ℕ ∧ ℕ ≼ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}) → {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ)
146	106, 144, 145	sylancr 598	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ)
147	97, 98, 146	jca32 524	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → (𝑥 ∈ ℤ ∧ (𝑥 ≠ 0 ∧ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ)))
148	147	3exp 1135	. . . . 5 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ((𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) → ({𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ → (𝑥 ∈ ℤ ∧ (𝑥 ≠ 0 ∧ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ)))))
149	96, 148	syld 48	. . . 4 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → (𝑥 ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}) → ({𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ → (𝑥 ∈ ℤ ∧ (𝑥 ≠ 0 ∧ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ)))))
150	149	impd 415	. . 3 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ((𝑥 ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}) ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → (𝑥 ∈ ℤ ∧ (𝑥 ≠ 0 ∧ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ))))
151	150	reximdv2 3181	. 2 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → (∃𝑥 ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}){𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ → ∃𝑥 ∈ ℤ (𝑥 ≠ 0 ∧ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ)))
152	84, 151	mpd 16	1 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ∃𝑥 ∈ ℤ (𝑥 ≠ 0 ∧ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 = wceq 1567 ∃wex 1806 ∈ wcel 2149 ≠ wne 2964 ∃wrex 3095 {crab 3422 Vcvv 3461 ∖ cdif 3908 ⊆ wss 3911 {csn 4592 ⟨cop 4598 class class class wbr 5111 {copab 5175 × cxp 5660 ‘cfv 6537 (class class class)co 7411 1^st c1st 7984 2^nd c2nd 7985 ≈ cen 8940 ≼ cdom 8941 Fincfn 8943 ℝcr 11099 0cc0 11100 1c1 11101 + caddc 11103 · cmul 11105 < clt 11243 ≤ cle 11244 − cmin 11441 -cneg 11442 ℕcn 12233 2c2 12295 ℕ₀cn0 12504 ℤcz 12591 ℚcq 12972 ...cfz 13535 ⌊cfl 13823 ↑cexp 14097 √csqrt 15284 abscabs 15285

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-inf2 9610 ax-cnex 11156 ax-resscn 11157 ax-1cn 11158 ax-icn 11159 ax-addcl 11160 ax-addrcl 11161 ax-mulcl 11162 ax-mulrcl 11163 ax-mulcom 11164 ax-addass 11165 ax-mulass 11166 ax-distr 11167 ax-i2m1 11168 ax-1ne0 11169 ax-1rid 11170 ax-rnegex 11171 ax-rrecex 11172 ax-cnre 11173 ax-pre-lttri 11174 ax-pre-lttrn 11175 ax-pre-ltadd 11176 ax-pre-mulgt0 11177 ax-pre-sup 11178

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3375 df-reu 3376 df-rab 3423 df-v 3463 df-sbc 3752 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4491 df-pw 4567 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-int 4915 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-se 5616 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7863 df-1st 7986 df-2nd 7987 df-frecs 8278 df-wrecs 8309 df-recs 8358 df-rdg 8397 df-1o 8453 df-oadd 8457 df-omul 8458 df-er 8694 df-map 8826 df-en 8944 df-dom 8945 df-sdom 8946 df-fin 8947 df-sup 9402 df-inf 9403 df-oi 9472 df-card 9925 df-acn 9928 df-pnf 11245 df-mnf 11246 df-xr 11247 df-ltxr 11248 df-le 11249 df-sub 11443 df-neg 11444 df-div 11872 df-nn 12234 df-2 12303 df-3 12304 df-n0 12505 df-xnn0 12578 df-z 12592 df-uz 12863 df-q 12973 df-rp 13017 df-ico 13378 df-fz 13536 df-fl 13825 df-mod 13903 df-seq 14038 df-exp 14098 df-hash 14367 df-cj 15150 df-re 15151 df-im 15152 df-sqrt 15286 df-abs 15287 df-dvds 16311 df-gcd 16553 df-numer 16794 df-denom 16795

This theorem is referenced by: pellex 43489

W3C validator