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 42925

Description: Lemma for pellex 42927. Invoking fiphp3d 42911, 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 42924	. . 3 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ≈ ℕ)
2		fzfi 13879	. . . 4 ⊢ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∈ Fin
3		diffi 9084	. . . 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 5465	. . . . 5 ⊢ (𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ↔ ∃𝑦∃𝑧(𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))))
6		fveq2 6822	. . . . . . . . . . . 12 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → (1^st ‘𝑎) = (1^st ‘⟨𝑦, 𝑧⟩))
7	6	oveq1d 7361	. . . . . . . . . . 11 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → ((1^st ‘𝑎)↑2) = ((1^st ‘⟨𝑦, 𝑧⟩)↑2))
8		fveq2 6822	. . . . . . . . . . . . 13 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → (2^nd ‘𝑎) = (2^nd ‘⟨𝑦, 𝑧⟩))
9	8	oveq1d 7361	. . . . . . . . . . . 12 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → ((2^nd ‘𝑎)↑2) = ((2^nd ‘⟨𝑦, 𝑧⟩)↑2))
10	9	oveq2d 7362	. . . . . . . . . . 11 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → (𝐷 · ((2^nd ‘𝑎)↑2)) = (𝐷 · ((2^nd ‘⟨𝑦, 𝑧⟩)↑2)))
11	7, 10	oveq12d 7364	. . . . . . . . . 10 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = (((1^st ‘⟨𝑦, 𝑧⟩)↑2) − (𝐷 · ((2^nd ‘⟨𝑦, 𝑧⟩)↑2))))
12		vex 3440	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
13		vex 3440	. . . . . . . . . . . . 13 ⊢ 𝑧 ∈ V
14	12, 13	op1st 7929	. . . . . . . . . . . 12 ⊢ (1^st ‘⟨𝑦, 𝑧⟩) = 𝑦
15	14	oveq1i 7356	. . . . . . . . . . 11 ⊢ ((1^st ‘⟨𝑦, 𝑧⟩)↑2) = (𝑦↑2)
16	12, 13	op2nd 7930	. . . . . . . . . . . . 13 ⊢ (2^nd ‘⟨𝑦, 𝑧⟩) = 𝑧
17	16	oveq1i 7356	. . . . . . . . . . . 12 ⊢ ((2^nd ‘⟨𝑦, 𝑧⟩)↑2) = (𝑧↑2)
18	17	oveq2i 7357	. . . . . . . . . . 11 ⊢ (𝐷 · ((2^nd ‘⟨𝑦, 𝑧⟩)↑2)) = (𝐷 · (𝑧↑2))
19	15, 18	oveq12i 7358	. . . . . . . . . 10 ⊢ (((1^st ‘⟨𝑦, 𝑧⟩)↑2) − (𝐷 · ((2^nd ‘⟨𝑦, 𝑧⟩)↑2))) = ((𝑦↑2) − (𝐷 · (𝑧↑2)))
20	11, 19	eqtrdi 2782	. . . . . . . . 9 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = ((𝑦↑2) − (𝐷 · (𝑧↑2))))
21	20	ad2antrl 728	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = ((𝑦↑2) − (𝐷 · (𝑧↑2))))
22		simprrl 780	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ ℕ ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ))
23		simpl 482	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ ℕ ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → 𝐷 ∈ ℕ)
24		simprr 772	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))
25	24	ad2antll 729	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ ℕ ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))
26		nnz 12489	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
27	26	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝑦 ∈ ℤ)
28		zsqcl 14036	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℤ → (𝑦↑2) ∈ ℤ)
29	27, 28	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (𝑦↑2) ∈ ℤ)
30		nnz 12489	. . . . . . . . . . . . . . 15 ⊢ (𝐷 ∈ ℕ → 𝐷 ∈ ℤ)
31	30	ad2antrl 728	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝐷 ∈ ℤ)
32		simplr 768	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝑧 ∈ ℕ)
33	32	nnzd 12495	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝑧 ∈ ℤ)
34		zsqcl 14036	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ℤ → (𝑧↑2) ∈ ℤ)
35	33, 34	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (𝑧↑2) ∈ ℤ)
36	31, 35	zmulcld 12583	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (𝐷 · (𝑧↑2)) ∈ ℤ)
37	29, 36	zsubcld 12582	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℤ)
38		1re 11112	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
39		2re 12199	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ
40		nnre 12132	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐷 ∈ ℕ → 𝐷 ∈ ℝ)
41	40	ad2antrl 728	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝐷 ∈ ℝ)
42		nnnn0 12388	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷 ∈ ℕ → 𝐷 ∈ ℕ₀)
43	42	ad2antrl 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝐷 ∈ ℕ₀)
44	43	nn0ge0d 12445	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 0 ≤ 𝐷)
45	41, 44	resqrtcld 15325	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (√‘𝐷) ∈ ℝ)
46		remulcl 11091	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℝ ∧ (√‘𝐷) ∈ ℝ) → (2 · (√‘𝐷)) ∈ ℝ)
47	39, 45, 46	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (2 · (√‘𝐷)) ∈ ℝ)
48		readdcl 11089	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℝ ∧ (2 · (√‘𝐷)) ∈ ℝ) → (1 + (2 · (√‘𝐷))) ∈ ℝ)
49	38, 47, 48	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (1 + (2 · (√‘𝐷))) ∈ ℝ)
50	49	flcld 13702	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℤ)
51	50	znegcld 12579	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → -(⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℤ)
52	37	zred 12577	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℝ)
53	50	zred 12577	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℝ)
54		nn0abscl 15219	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℤ → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ∈ ℕ₀)
55	37, 54	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ∈ ℕ₀)
56	55	nn0zd 12494	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ∈ ℤ)
57	56	zred 12577	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ∈ ℝ)
58		peano2re 11286	. . . . . . . . . . . . . . . 16 ⊢ ((⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℝ → ((⌊‘(1 + (2 · (√‘𝐷)))) + 1) ∈ ℝ)
59	53, 58	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → ((⌊‘(1 + (2 · (√‘𝐷)))) + 1) ∈ ℝ)
60		simprr 772	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))
61		flltp1 13704	. . . . . . . . . . . . . . . 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 11274	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < ((⌊‘(1 + (2 · (√‘𝐷)))) + 1))
64		zleltp1 12523	. . . . . . . . . . . . . . 15 ⊢ (((abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ∈ ℤ ∧ (⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℤ) → ((abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ≤ (⌊‘(1 + (2 · (√‘𝐷)))) ↔ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < ((⌊‘(1 + (2 · (√‘𝐷)))) + 1)))
65	56, 50, 64	syl2anc 584	. . . . . . . . . . . . . 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 15223	. . . . . . . . . . . . . 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 837	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (-(⌊‘(1 + (2 · (√‘𝐷)))) ≤ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≤ (⌊‘(1 + (2 · (√‘𝐷))))))
70		elfz 13413	. . . . . . . . . . . . 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 1375	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))))
73	22, 23, 25, 72	syl12anc 836	. . . . . . . . . 10 ⊢ ((𝐷 ∈ ℕ ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))))
74	73	adantlr 715	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))))
75		simprl 770	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0)
76	75	ad2antll 729	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0)
77		eldifsn 4735	. . . . . . . . 9 ⊢ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}) ↔ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0))
78	74, 76, 77	sylanbrc 583	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}))
79	21, 78	eqeltrd 2831	. . . . . . 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 1935	. . . . 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 42911	. 2 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ∃𝑥 ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}){𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ)
85		eldif 3907	. . . . . 6 ⊢ (𝑥 ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}) ↔ (𝑥 ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∧ ¬ 𝑥 ∈ {0}))
86		elfzelz 13424	. . . . . . . 8 ⊢ (𝑥 ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) → 𝑥 ∈ ℤ)
87		simp2 1137	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑥 ∈ ℤ ∧ ¬ 𝑥 ∈ {0}) → 𝑥 ∈ ℤ)
88		velsn 4589	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {0} ↔ 𝑥 = 0)
89	88	biimpri 228	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → 𝑥 ∈ {0})
90	89	necon3bi 2954	. . . . . . . . . . 11 ⊢ (¬ 𝑥 ∈ {0} → 𝑥 ≠ 0)
91	90	3ad2ant3 1135	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑥 ∈ ℤ ∧ ¬ 𝑥 ∈ {0}) → 𝑥 ≠ 0)
92	87, 91	jca 511	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑥 ∈ ℤ ∧ ¬ 𝑥 ∈ {0}) → (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0))
93	92	3exp 1119	. . . . . . . 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 1200	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → 𝑥 ∈ ℤ)
98		simp2r 1201	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → 𝑥 ≠ 0)
99		nnex 12131	. . . . . . . . . . 11 ⊢ ℕ ∈ V
100	99, 99	xpex 7686	. . . . . . . . . 10 ⊢ (ℕ × ℕ) ∈ V
101		opabssxp 5706	. . . . . . . . . 10 ⊢ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ⊆ (ℕ × ℕ)
102		ssdomg 8922	. . . . . . . . . 10 ⊢ ((ℕ × ℕ) ∈ V → ({⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ⊆ (ℕ × ℕ) → {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ (ℕ × ℕ)))
103	100, 101, 102	mp2 9	. . . . . . . . 9 ⊢ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ (ℕ × ℕ)
104		xpnnen 16120	. . . . . . . . 9 ⊢ (ℕ × ℕ) ≈ ℕ
105		domentr 8935	. . . . . . . . 9 ⊢ (({⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ (ℕ × ℕ) ∧ (ℕ × ℕ) ≈ ℕ) → {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ ℕ)
106	103, 104, 105	mp2an 692	. . . . . . . 8 ⊢ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ ℕ
107		ensym 8925	. . . . . . . . . 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 1135	. . . . . . . . 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 5258	. . . . . . . . . 10 ⊢ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ∈ V
110		fveq2 6822	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑏 → (1^st ‘𝑎) = (1^st ‘𝑏))
111	110	oveq1d 7361	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑏 → ((1^st ‘𝑎)↑2) = ((1^st ‘𝑏)↑2))
112		fveq2 6822	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑏 → (2^nd ‘𝑎) = (2^nd ‘𝑏))
113	112	oveq1d 7361	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑏 → ((2^nd ‘𝑎)↑2) = ((2^nd ‘𝑏)↑2))
114	113	oveq2d 7362	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑏 → (𝐷 · ((2^nd ‘𝑎)↑2)) = (𝐷 · ((2^nd ‘𝑏)↑2)))
115	111, 114	oveq12d 7364	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑏 → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))))
116	115	eqeq1d 2733	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑏 → ((((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥 ↔ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥))
117	116	elrab 3642	. . . . . . . . . . . . 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 770	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) ∧ (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → 𝑏 = ⟨𝑦, 𝑧⟩)
119		simprrl 780	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) ∧ (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ))
120		fveq2 6822	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → (1^st ‘𝑏) = (1^st ‘⟨𝑦, 𝑧⟩))
121	120	oveq1d 7361	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → ((1^st ‘𝑏)↑2) = ((1^st ‘⟨𝑦, 𝑧⟩)↑2))
122		fveq2 6822	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → (2^nd ‘𝑏) = (2^nd ‘⟨𝑦, 𝑧⟩))
123	122	oveq1d 7361	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → ((2^nd ‘𝑏)↑2) = ((2^nd ‘⟨𝑦, 𝑧⟩)↑2))
124	123	oveq2d 7362	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → (𝐷 · ((2^nd ‘𝑏)↑2)) = (𝐷 · ((2^nd ‘⟨𝑦, 𝑧⟩)↑2)))
125	121, 124	oveq12d 7364	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = (((1^st ‘⟨𝑦, 𝑧⟩)↑2) − (𝐷 · ((2^nd ‘⟨𝑦, 𝑧⟩)↑2))))
126	125, 19	eqtr2di 2783	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → ((𝑦↑2) − (𝐷 · (𝑧↑2))) = (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))))
127	126	ad2antrl 728	. . . . . . . . . . . . . . . . . . . 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 768	. . . . . . . . . . . . . . . . . . . 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 2766	. . . . . . . . . . . . . . . . . . 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 1920	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) → (∃𝑦∃𝑧(𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))) → ∃𝑦∃𝑧(𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥))))
133		elopab 5465	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ↔ ∃𝑦∃𝑧(𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))))
134		elopab 5465	. . . . . . . . . . . . . . . 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 3935	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ⊆ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)})
140	139	3adant3 1132	. . . . . . . . . 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 8922	. . . . . . . . . 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 8934	. . . . . . . . 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 584	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → ℕ ≼ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)})
145		sbth 9010	. . . . . . . 8 ⊢ (({⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ ℕ ∧ ℕ ≼ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}) → {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ)
146	106, 144, 145	sylancr 587	. . . . . . 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 1119	. . . . 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 3142	. 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 1086 = wceq 1541 ∃wex 1780 ∈ wcel 2111 ≠ wne 2928 ∃wrex 3056 {crab 3395 Vcvv 3436 ∖ cdif 3894 ⊆ wss 3897 {csn 4573 ⟨cop 4579 class class class wbr 5089 {copab 5151 × cxp 5612 ‘cfv 6481 (class class class)co 7346 1^st c1st 7919 2^nd c2nd 7920 ≈ cen 8866 ≼ cdom 8867 Fincfn 8869 ℝcr 11005 0cc0 11006 1c1 11007 + caddc 11009 · cmul 11011 < clt 11146 ≤ cle 11147 − cmin 11344 -cneg 11345 ℕcn 12125 2c2 12180 ℕ₀cn0 12381 ℤcz 12468 ℚcq 12846 ...cfz 13407 ⌊cfl 13694 ↑cexp 13968 √csqrt 15140 abscabs 15141

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668 ax-inf2 9531 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083 ax-pre-sup 11084

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-int 4896 df-iun 4941 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-se 5568 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-isom 6490 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-om 7797 df-1st 7921 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-oadd 8389 df-omul 8390 df-er 8622 df-map 8752 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-sup 9326 df-inf 9327 df-oi 9396 df-card 9832 df-acn 9835 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-div 11775 df-nn 12126 df-2 12188 df-3 12189 df-n0 12382 df-xnn0 12455 df-z 12469 df-uz 12733 df-q 12847 df-rp 12891 df-ico 13251 df-fz 13408 df-fl 13696 df-mod 13774 df-seq 13909 df-exp 13969 df-hash 14238 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-dvds 16164 df-gcd 16406 df-numer 16646 df-denom 16647

This theorem is referenced by: pellex 42927

W3C validator