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 43112

Description: Lemma for pellex 43114. Invoking fiphp3d 43098, 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 43111	. . 3 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ≈ ℕ)
2		fzfi 13897	. . . 4 ⊢ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∈ Fin
3		diffi 9101	. . . 4 ⊢ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∈ Fin → ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}) ∈ Fin)
4	2, 3	mp1i 13	. . 3 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}) ∈ Fin)
5		elopab 5474	. . . . 5 ⊢ (𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ↔ ∃𝑦∃𝑧(𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))))
6		fveq2 6833	. . . . . . . . . . . 12 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → (1^st ‘𝑎) = (1^st ‘⟨𝑦, 𝑧⟩))
7	6	oveq1d 7373	. . . . . . . . . . 11 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → ((1^st ‘𝑎)↑2) = ((1^st ‘⟨𝑦, 𝑧⟩)↑2))
8		fveq2 6833	. . . . . . . . . . . . 13 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → (2^nd ‘𝑎) = (2^nd ‘⟨𝑦, 𝑧⟩))
9	8	oveq1d 7373	. . . . . . . . . . . 12 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → ((2^nd ‘𝑎)↑2) = ((2^nd ‘⟨𝑦, 𝑧⟩)↑2))
10	9	oveq2d 7374	. . . . . . . . . . 11 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → (𝐷 · ((2^nd ‘𝑎)↑2)) = (𝐷 · ((2^nd ‘⟨𝑦, 𝑧⟩)↑2)))
11	7, 10	oveq12d 7376	. . . . . . . . . 10 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = (((1^st ‘⟨𝑦, 𝑧⟩)↑2) − (𝐷 · ((2^nd ‘⟨𝑦, 𝑧⟩)↑2))))
12		vex 3443	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
13		vex 3443	. . . . . . . . . . . . 13 ⊢ 𝑧 ∈ V
14	12, 13	op1st 7941	. . . . . . . . . . . 12 ⊢ (1^st ‘⟨𝑦, 𝑧⟩) = 𝑦
15	14	oveq1i 7368	. . . . . . . . . . 11 ⊢ ((1^st ‘⟨𝑦, 𝑧⟩)↑2) = (𝑦↑2)
16	12, 13	op2nd 7942	. . . . . . . . . . . . 13 ⊢ (2^nd ‘⟨𝑦, 𝑧⟩) = 𝑧
17	16	oveq1i 7368	. . . . . . . . . . . 12 ⊢ ((2^nd ‘⟨𝑦, 𝑧⟩)↑2) = (𝑧↑2)
18	17	oveq2i 7369	. . . . . . . . . . 11 ⊢ (𝐷 · ((2^nd ‘⟨𝑦, 𝑧⟩)↑2)) = (𝐷 · (𝑧↑2))
19	15, 18	oveq12i 7370	. . . . . . . . . 10 ⊢ (((1^st ‘⟨𝑦, 𝑧⟩)↑2) − (𝐷 · ((2^nd ‘⟨𝑦, 𝑧⟩)↑2))) = ((𝑦↑2) − (𝐷 · (𝑧↑2)))
20	11, 19	eqtrdi 2786	. . . . . . . . 9 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = ((𝑦↑2) − (𝐷 · (𝑧↑2))))
21	20	ad2antrl 729	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = ((𝑦↑2) − (𝐷 · (𝑧↑2))))
22		simprrl 781	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ ℕ ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ))
23		simpl 482	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ ℕ ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → 𝐷 ∈ ℕ)
24		simprr 773	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))
25	24	ad2antll 730	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ ℕ ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))
26		nnz 12511	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
27	26	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝑦 ∈ ℤ)
28		zsqcl 14054	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℤ → (𝑦↑2) ∈ ℤ)
29	27, 28	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (𝑦↑2) ∈ ℤ)
30		nnz 12511	. . . . . . . . . . . . . . 15 ⊢ (𝐷 ∈ ℕ → 𝐷 ∈ ℤ)
31	30	ad2antrl 729	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝐷 ∈ ℤ)
32		simplr 769	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝑧 ∈ ℕ)
33	32	nnzd 12516	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝑧 ∈ ℤ)
34		zsqcl 14054	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ℤ → (𝑧↑2) ∈ ℤ)
35	33, 34	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (𝑧↑2) ∈ ℤ)
36	31, 35	zmulcld 12604	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (𝐷 · (𝑧↑2)) ∈ ℤ)
37	29, 36	zsubcld 12603	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℤ)
38		1re 11134	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
39		2re 12221	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ
40		nnre 12154	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐷 ∈ ℕ → 𝐷 ∈ ℝ)
41	40	ad2antrl 729	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝐷 ∈ ℝ)
42		nnnn0 12410	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷 ∈ ℕ → 𝐷 ∈ ℕ₀)
43	42	ad2antrl 729	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝐷 ∈ ℕ₀)
44	43	nn0ge0d 12467	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 0 ≤ 𝐷)
45	41, 44	resqrtcld 15343	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (√‘𝐷) ∈ ℝ)
46		remulcl 11113	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℝ ∧ (√‘𝐷) ∈ ℝ) → (2 · (√‘𝐷)) ∈ ℝ)
47	39, 45, 46	sylancr 588	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (2 · (√‘𝐷)) ∈ ℝ)
48		readdcl 11111	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℝ ∧ (2 · (√‘𝐷)) ∈ ℝ) → (1 + (2 · (√‘𝐷))) ∈ ℝ)
49	38, 47, 48	sylancr 588	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (1 + (2 · (√‘𝐷))) ∈ ℝ)
50	49	flcld 13720	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℤ)
51	50	znegcld 12600	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → -(⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℤ)
52	37	zred 12598	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℝ)
53	50	zred 12598	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℝ)
54		nn0abscl 15237	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℤ → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ∈ ℕ₀)
55	37, 54	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ∈ ℕ₀)
56	55	nn0zd 12515	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ∈ ℤ)
57	56	zred 12598	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ∈ ℝ)
58		peano2re 11308	. . . . . . . . . . . . . . . 16 ⊢ ((⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℝ → ((⌊‘(1 + (2 · (√‘𝐷)))) + 1) ∈ ℝ)
59	53, 58	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → ((⌊‘(1 + (2 · (√‘𝐷)))) + 1) ∈ ℝ)
60		simprr 773	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))
61		flltp1 13722	. . . . . . . . . . . . . . . 16 ⊢ ((1 + (2 · (√‘𝐷))) ∈ ℝ → (1 + (2 · (√‘𝐷))) < ((⌊‘(1 + (2 · (√‘𝐷)))) + 1))
62	49, 61	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (1 + (2 · (√‘𝐷))) < ((⌊‘(1 + (2 · (√‘𝐷)))) + 1))
63	57, 49, 59, 60, 62	lttrd 11296	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < ((⌊‘(1 + (2 · (√‘𝐷)))) + 1))
64		zleltp1 12544	. . . . . . . . . . . . . . 15 ⊢ (((abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ∈ ℤ ∧ (⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℤ) → ((abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ≤ (⌊‘(1 + (2 · (√‘𝐷)))) ↔ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < ((⌊‘(1 + (2 · (√‘𝐷)))) + 1)))
65	56, 50, 64	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → ((abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ≤ (⌊‘(1 + (2 · (√‘𝐷)))) ↔ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < ((⌊‘(1 + (2 · (√‘𝐷)))) + 1)))
66	63, 65	mpbird 257	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ≤ (⌊‘(1 + (2 · (√‘𝐷)))))
67		absle 15241	. . . . . . . . . . . . . 14 ⊢ ((((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℝ ∧ (⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℝ) → ((abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ≤ (⌊‘(1 + (2 · (√‘𝐷)))) ↔ (-(⌊‘(1 + (2 · (√‘𝐷)))) ≤ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≤ (⌊‘(1 + (2 · (√‘𝐷)))))))
68	67	biimpa 476	. . . . . . . . . . . . 13 ⊢ (((((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℝ ∧ (⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℝ) ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ≤ (⌊‘(1 + (2 · (√‘𝐷))))) → (-(⌊‘(1 + (2 · (√‘𝐷)))) ≤ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≤ (⌊‘(1 + (2 · (√‘𝐷))))))
69	52, 53, 66, 68	syl21anc 838	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (-(⌊‘(1 + (2 · (√‘𝐷)))) ≤ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≤ (⌊‘(1 + (2 · (√‘𝐷))))))
70		elfz 13431	. . . . . . . . . . . . 13 ⊢ ((((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℤ ∧ -(⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℤ ∧ (⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℤ) → (((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ↔ (-(⌊‘(1 + (2 · (√‘𝐷)))) ≤ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≤ (⌊‘(1 + (2 · (√‘𝐷)))))))
71	70	biimpar 477	. . . . . . . . . . . 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 1376	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))))
73	22, 23, 25, 72	syl12anc 837	. . . . . . . . . 10 ⊢ ((𝐷 ∈ ℕ ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))))
74	73	adantlr 716	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))))
75		simprl 771	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0)
76	75	ad2antll 730	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0)
77		eldifsn 4741	. . . . . . . . 9 ⊢ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}) ↔ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0))
78	74, 76, 77	sylanbrc 584	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}))
79	21, 78	eqeltrd 2835	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}))
80	79	ex 412	. . . . . 6 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ((𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))) → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0})))
81	80	exlimdvv 1936	. . . . 5 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → (∃𝑦∃𝑧(𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))) → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0})))
82	5, 81	biimtrid 242	. . . 4 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → (𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0})))
83	82	imp 406	. . 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 43098	. 2 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ∃𝑥 ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}){𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ)
85		eldif 3910	. . . . . 6 ⊢ (𝑥 ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}) ↔ (𝑥 ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∧ ¬ 𝑥 ∈ {0}))
86		elfzelz 13442	. . . . . . . 8 ⊢ (𝑥 ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) → 𝑥 ∈ ℤ)
87		simp2 1138	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑥 ∈ ℤ ∧ ¬ 𝑥 ∈ {0}) → 𝑥 ∈ ℤ)
88		velsn 4595	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {0} ↔ 𝑥 = 0)
89	88	biimpri 228	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → 𝑥 ∈ {0})
90	89	necon3bi 2957	. . . . . . . . . . 11 ⊢ (¬ 𝑥 ∈ {0} → 𝑥 ≠ 0)
91	90	3ad2ant3 1136	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑥 ∈ ℤ ∧ ¬ 𝑥 ∈ {0}) → 𝑥 ≠ 0)
92	87, 91	jca 511	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑥 ∈ ℤ ∧ ¬ 𝑥 ∈ {0}) → (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0))
93	92	3exp 1120	. . . . . . . 8 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → (𝑥 ∈ ℤ → (¬ 𝑥 ∈ {0} → (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0))))
94	86, 93	syl5 34	. . . . . . 7 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → (𝑥 ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) → (¬ 𝑥 ∈ {0} → (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0))))
95	94	impd 410	. . . . . 6 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ((𝑥 ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∧ ¬ 𝑥 ∈ {0}) → (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)))
96	85, 95	biimtrid 242	. . . . 5 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → (𝑥 ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}) → (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)))
97		simp2l 1201	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → 𝑥 ∈ ℤ)
98		simp2r 1202	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → 𝑥 ≠ 0)
99		nnex 12153	. . . . . . . . . . 11 ⊢ ℕ ∈ V
100	99, 99	xpex 7698	. . . . . . . . . 10 ⊢ (ℕ × ℕ) ∈ V
101		opabssxp 5715	. . . . . . . . . 10 ⊢ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ⊆ (ℕ × ℕ)
102		ssdomg 8939	. . . . . . . . . 10 ⊢ ((ℕ × ℕ) ∈ V → ({⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ⊆ (ℕ × ℕ) → {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ (ℕ × ℕ)))
103	100, 101, 102	mp2 9	. . . . . . . . 9 ⊢ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ (ℕ × ℕ)
104		xpnnen 16138	. . . . . . . . 9 ⊢ (ℕ × ℕ) ≈ ℕ
105		domentr 8952	. . . . . . . . 9 ⊢ (({⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ (ℕ × ℕ) ∧ (ℕ × ℕ) ≈ ℕ) → {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ ℕ)
106	103, 104, 105	mp2an 693	. . . . . . . 8 ⊢ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ ℕ
107		ensym 8942	. . . . . . . . . 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 1136	. . . . . . . . 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 5266	. . . . . . . . . 10 ⊢ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ∈ V
110		fveq2 6833	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑏 → (1^st ‘𝑎) = (1^st ‘𝑏))
111	110	oveq1d 7373	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑏 → ((1^st ‘𝑎)↑2) = ((1^st ‘𝑏)↑2))
112		fveq2 6833	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑏 → (2^nd ‘𝑎) = (2^nd ‘𝑏))
113	112	oveq1d 7373	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑏 → ((2^nd ‘𝑎)↑2) = ((2^nd ‘𝑏)↑2))
114	113	oveq2d 7374	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑏 → (𝐷 · ((2^nd ‘𝑎)↑2)) = (𝐷 · ((2^nd ‘𝑏)↑2)))
115	111, 114	oveq12d 7376	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑏 → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))))
116	115	eqeq1d 2737	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑏 → ((((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥 ↔ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥))
117	116	elrab 3645	. . . . . . . . . . . . 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 771	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) ∧ (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → 𝑏 = ⟨𝑦, 𝑧⟩)
119		simprrl 781	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) ∧ (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ))
120		fveq2 6833	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → (1^st ‘𝑏) = (1^st ‘⟨𝑦, 𝑧⟩))
121	120	oveq1d 7373	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → ((1^st ‘𝑏)↑2) = ((1^st ‘⟨𝑦, 𝑧⟩)↑2))
122		fveq2 6833	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → (2^nd ‘𝑏) = (2^nd ‘⟨𝑦, 𝑧⟩))
123	122	oveq1d 7373	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → ((2^nd ‘𝑏)↑2) = ((2^nd ‘⟨𝑦, 𝑧⟩)↑2))
124	123	oveq2d 7374	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → (𝐷 · ((2^nd ‘𝑏)↑2)) = (𝐷 · ((2^nd ‘⟨𝑦, 𝑧⟩)↑2)))
125	121, 124	oveq12d 7376	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = (((1^st ‘⟨𝑦, 𝑧⟩)↑2) − (𝐷 · ((2^nd ‘⟨𝑦, 𝑧⟩)↑2))))
126	125, 19	eqtr2di 2787	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → ((𝑦↑2) − (𝐷 · (𝑧↑2))) = (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))))
127	126	ad2antrl 729	. . . . . . . . . . . . . . . . . . . 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 769	. . . . . . . . . . . . . . . . . . . 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 2770	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) ∧ (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)
130	118, 119, 129	jca32 515	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) ∧ (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)))
131	130	ex 412	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) → ((𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))) → (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥))))
132	131	2eximdv 1921	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) → (∃𝑦∃𝑧(𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))) → ∃𝑦∃𝑧(𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥))))
133		elopab 5474	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ↔ ∃𝑦∃𝑧(𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))))
134		elopab 5474	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ↔ ∃𝑦∃𝑧(𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)))
135	132, 133, 134	3imtr4g 296	. . . . . . . . . . . . . . 15 ⊢ ((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) → (𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} → 𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}))
136	135	expimpd 453	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → (((((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥 ∧ 𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))}) → 𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}))
137	136	ancomsd 465	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → ((𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) → 𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}))
138	117, 137	biimtrid 242	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → (𝑏 ∈ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} → 𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}))
139	138	ssrdv 3938	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ⊆ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)})
140	139	3adant3 1133	. . . . . . . . . 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 8939	. . . . . . . . . 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 68	. . . . . . . . 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 8951	. . . . . . . . 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 585	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → ℕ ≼ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)})
145		sbth 9027	. . . . . . . 8 ⊢ (({⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ ℕ ∧ ℕ ≼ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}) → {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ)
146	106, 144, 145	sylancr 588	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ)
147	97, 98, 146	jca32 515	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → (𝑥 ∈ ℤ ∧ (𝑥 ≠ 0 ∧ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ)))
148	147	3exp 1120	. . . . 5 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ((𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) → ({𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ → (𝑥 ∈ ℤ ∧ (𝑥 ≠ 0 ∧ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ)))))
149	96, 148	syld 47	. . . 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 410	. . 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 3145	. 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 15	1 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ∃𝑥 ∈ ℤ (𝑥 ≠ 0 ∧ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∃wex 1781 ∈ wcel 2114 ≠ wne 2931 ∃wrex 3059 {crab 3398 Vcvv 3439 ∖ cdif 3897 ⊆ wss 3900 {csn 4579 ⟨cop 4585 class class class wbr 5097 {copab 5159 × cxp 5621 ‘cfv 6491 (class class class)co 7358 1^st c1st 7931 2^nd c2nd 7932 ≈ cen 8882 ≼ cdom 8883 Fincfn 8885 ℝcr 11027 0cc0 11028 1c1 11029 + caddc 11031 · cmul 11033 < clt 11168 ≤ cle 11169 − cmin 11366 -cneg 11367 ℕcn 12147 2c2 12202 ℕ₀cn0 12403 ℤcz 12490 ℚcq 12863 ...cfz 13425 ⌊cfl 13712 ↑cexp 13986 √csqrt 15158 abscabs 15159

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2183 ax-ext 2707 ax-rep 5223 ax-sep 5240 ax-nul 5250 ax-pow 5309 ax-pr 5376 ax-un 7680 ax-inf2 9552 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105 ax-pre-sup 11106

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2538 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2810 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3349 df-reu 3350 df-rab 3399 df-v 3441 df-sbc 3740 df-csb 3849 df-dif 3903 df-un 3905 df-in 3907 df-ss 3917 df-pss 3920 df-nul 4285 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-int 4902 df-iun 4947 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-se 5577 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-pred 6258 df-ord 6319 df-on 6320 df-lim 6321 df-suc 6322 df-iota 6447 df-fun 6493 df-fn 6494 df-f 6495 df-f1 6496 df-fo 6497 df-f1o 6498 df-fv 6499 df-isom 6500 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7809 df-1st 7933 df-2nd 7934 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-1o 8397 df-oadd 8401 df-omul 8402 df-er 8635 df-map 8767 df-en 8886 df-dom 8887 df-sdom 8888 df-fin 8889 df-sup 9347 df-inf 9348 df-oi 9417 df-card 9853 df-acn 9856 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11368 df-neg 11369 df-div 11797 df-nn 12148 df-2 12210 df-3 12211 df-n0 12404 df-xnn0 12477 df-z 12491 df-uz 12754 df-q 12864 df-rp 12908 df-ico 13269 df-fz 13426 df-fl 13714 df-mod 13792 df-seq 13927 df-exp 13987 df-hash 14256 df-cj 15024 df-re 15025 df-im 15026 df-sqrt 15160 df-abs 15161 df-dvds 16182 df-gcd 16424 df-numer 16664 df-denom 16665

This theorem is referenced by: pellex 43114

W3C validator