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 38936

Description: Lemma for pellex 38938. Invoking fiphp3d 38922, 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 38935	. . 3 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ≈ ℕ)
2		fzfi 13194	. . . 4 ⊢ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∈ Fin
3		diffi 8603	. . . 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 5311	. . . . 5 ⊢ (𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ↔ ∃𝑦∃𝑧(𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))))
6		fveq2 6545	. . . . . . . . . . . 12 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → (1^st ‘𝑎) = (1^st ‘⟨𝑦, 𝑧⟩))
7	6	oveq1d 7038	. . . . . . . . . . 11 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → ((1^st ‘𝑎)↑2) = ((1^st ‘⟨𝑦, 𝑧⟩)↑2))
8		fveq2 6545	. . . . . . . . . . . . 13 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → (2^nd ‘𝑎) = (2^nd ‘⟨𝑦, 𝑧⟩))
9	8	oveq1d 7038	. . . . . . . . . . . 12 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → ((2^nd ‘𝑎)↑2) = ((2^nd ‘⟨𝑦, 𝑧⟩)↑2))
10	9	oveq2d 7039	. . . . . . . . . . 11 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → (𝐷 · ((2^nd ‘𝑎)↑2)) = (𝐷 · ((2^nd ‘⟨𝑦, 𝑧⟩)↑2)))
11	7, 10	oveq12d 7041	. . . . . . . . . 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 7560	. . . . . . . . . . . 12 ⊢ (1^st ‘⟨𝑦, 𝑧⟩) = 𝑦
15	14	oveq1i 7033	. . . . . . . . . . 11 ⊢ ((1^st ‘⟨𝑦, 𝑧⟩)↑2) = (𝑦↑2)
16	12, 13	op2nd 7561	. . . . . . . . . . . . 13 ⊢ (2^nd ‘⟨𝑦, 𝑧⟩) = 𝑧
17	16	oveq1i 7033	. . . . . . . . . . . 12 ⊢ ((2^nd ‘⟨𝑦, 𝑧⟩)↑2) = (𝑧↑2)
18	17	oveq2i 7034	. . . . . . . . . . 11 ⊢ (𝐷 · ((2^nd ‘⟨𝑦, 𝑧⟩)↑2)) = (𝐷 · (𝑧↑2))
19	15, 18	oveq12i 7035	. . . . . . . . . 10 ⊢ (((1^st ‘⟨𝑦, 𝑧⟩)↑2) − (𝐷 · ((2^nd ‘⟨𝑦, 𝑧⟩)↑2))) = ((𝑦↑2) − (𝐷 · (𝑧↑2)))
20	11, 19	syl6eq 2849	. . . . . . . . 9 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = ((𝑦↑2) − (𝐷 · (𝑧↑2))))
21	20	ad2antrl 724	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = ((𝑦↑2) − (𝐷 · (𝑧↑2))))
22		simprrl 777	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ ℕ ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ))
23		simpl 483	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ ℕ ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → 𝐷 ∈ ℕ)
24		simprr 769	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))
25	24	ad2antll 725	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ ℕ ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))
26		nnz 11858	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
27	26	ad2antrr 722	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝑦 ∈ ℤ)
28		zsqcl 13348	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℤ → (𝑦↑2) ∈ ℤ)
29	27, 28	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (𝑦↑2) ∈ ℤ)
30		nnz 11858	. . . . . . . . . . . . . . 15 ⊢ (𝐷 ∈ ℕ → 𝐷 ∈ ℤ)
31	30	ad2antrl 724	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝐷 ∈ ℤ)
32		simplr 765	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝑧 ∈ ℕ)
33	32	nnzd 11940	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝑧 ∈ ℤ)
34		zsqcl 13348	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ℤ → (𝑧↑2) ∈ ℤ)
35	33, 34	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (𝑧↑2) ∈ ℤ)
36	31, 35	zmulcld 11947	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (𝐷 · (𝑧↑2)) ∈ ℤ)
37	29, 36	zsubcld 11946	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℤ)
38		1re 10494	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
39		2re 11565	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ
40		nnre 11499	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐷 ∈ ℕ → 𝐷 ∈ ℝ)
41	40	ad2antrl 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝐷 ∈ ℝ)
42		nnnn0 11758	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷 ∈ ℕ → 𝐷 ∈ ℕ₀)
43	42	ad2antrl 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝐷 ∈ ℕ₀)
44	43	nn0ge0d 11812	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 0 ≤ 𝐷)
45	41, 44	resqrtcld 14615	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (√‘𝐷) ∈ ℝ)
46		remulcl 10475	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℝ ∧ (√‘𝐷) ∈ ℝ) → (2 · (√‘𝐷)) ∈ ℝ)
47	39, 45, 46	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (2 · (√‘𝐷)) ∈ ℝ)
48		readdcl 10473	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℝ ∧ (2 · (√‘𝐷)) ∈ ℝ) → (1 + (2 · (√‘𝐷))) ∈ ℝ)
49	38, 47, 48	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (1 + (2 · (√‘𝐷))) ∈ ℝ)
50	49	flcld 13022	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℤ)
51	50	znegcld 11943	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → -(⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℤ)
52	37	zred 11941	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℝ)
53	50	zred 11941	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℝ)
54		nn0abscl 14510	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℤ → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ∈ ℕ₀)
55	37, 54	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ∈ ℕ₀)
56	55	nn0zd 11939	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ∈ ℤ)
57	56	zred 11941	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ∈ ℝ)
58		peano2re 10666	. . . . . . . . . . . . . . . 16 ⊢ ((⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℝ → ((⌊‘(1 + (2 · (√‘𝐷)))) + 1) ∈ ℝ)
59	53, 58	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → ((⌊‘(1 + (2 · (√‘𝐷)))) + 1) ∈ ℝ)
60		simprr 769	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))
61		flltp1 13024	. . . . . . . . . . . . . . . 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 10654	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < ((⌊‘(1 + (2 · (√‘𝐷)))) + 1))
64		zleltp1 11887	. . . . . . . . . . . . . . 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 258	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ≤ (⌊‘(1 + (2 · (√‘𝐷)))))
67		absle 14513	. . . . . . . . . . . . . 14 ⊢ ((((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℝ ∧ (⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℝ) → ((abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ≤ (⌊‘(1 + (2 · (√‘𝐷)))) ↔ (-(⌊‘(1 + (2 · (√‘𝐷)))) ≤ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≤ (⌊‘(1 + (2 · (√‘𝐷)))))))
68	67	biimpa 477	. . . . . . . . . . . . 13 ⊢ (((((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℝ ∧ (⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℝ) ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ≤ (⌊‘(1 + (2 · (√‘𝐷))))) → (-(⌊‘(1 + (2 · (√‘𝐷)))) ≤ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≤ (⌊‘(1 + (2 · (√‘𝐷))))))
69	52, 53, 66, 68	syl21anc 834	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (-(⌊‘(1 + (2 · (√‘𝐷)))) ≤ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≤ (⌊‘(1 + (2 · (√‘𝐷))))))
70		elfz 12752	. . . . . . . . . . . . 13 ⊢ ((((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℤ ∧ -(⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℤ ∧ (⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℤ) → (((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ↔ (-(⌊‘(1 + (2 · (√‘𝐷)))) ≤ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≤ (⌊‘(1 + (2 · (√‘𝐷)))))))
71	70	biimpar 478	. . . . . . . . . . . 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 1366	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))))
73	22, 23, 25, 72	syl12anc 833	. . . . . . . . . 10 ⊢ ((𝐷 ∈ ℕ ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))))
74	73	adantlr 711	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))))
75		simprl 767	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0)
76	75	ad2antll 725	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0)
77		eldifsn 4632	. . . . . . . . 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 2885	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}))
80	79	ex 413	. . . . . 6 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ((𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))) → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0})))
81	80	exlimdvv 1916	. . . . 5 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → (∃𝑦∃𝑧(𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))) → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0})))
82	5, 81	syl5bi 243	. . . 4 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → (𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0})))
83	82	imp 407	. . 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 38922	. 2 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ∃𝑥 ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}){𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ)
85		eldif 3875	. . . . . 6 ⊢ (𝑥 ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}) ↔ (𝑥 ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∧ ¬ 𝑥 ∈ {0}))
86		elfzelz 12762	. . . . . . . 8 ⊢ (𝑥 ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) → 𝑥 ∈ ℤ)
87		simp2 1130	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑥 ∈ ℤ ∧ ¬ 𝑥 ∈ {0}) → 𝑥 ∈ ℤ)
88		velsn 4494	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {0} ↔ 𝑥 = 0)
89	88	biimpri 229	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → 𝑥 ∈ {0})
90	89	necon3bi 3012	. . . . . . . . . . 11 ⊢ (¬ 𝑥 ∈ {0} → 𝑥 ≠ 0)
91	90	3ad2ant3 1128	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑥 ∈ ℤ ∧ ¬ 𝑥 ∈ {0}) → 𝑥 ≠ 0)
92	87, 91	jca 512	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑥 ∈ ℤ ∧ ¬ 𝑥 ∈ {0}) → (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0))
93	92	3exp 1112	. . . . . . . 8 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → (𝑥 ∈ ℤ → (¬ 𝑥 ∈ {0} → (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0))))
94	86, 93	syl5 34	. . . . . . 7 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → (𝑥 ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) → (¬ 𝑥 ∈ {0} → (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0))))
95	94	impd 411	. . . . . 6 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ((𝑥 ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∧ ¬ 𝑥 ∈ {0}) → (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)))
96	85, 95	syl5bi 243	. . . . 5 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → (𝑥 ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}) → (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)))
97		simp2l 1192	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → 𝑥 ∈ ℤ)
98		simp2r 1193	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → 𝑥 ≠ 0)
99		nnex 11498	. . . . . . . . . . 11 ⊢ ℕ ∈ V
100	99, 99	xpex 7340	. . . . . . . . . 10 ⊢ (ℕ × ℕ) ∈ V
101		opabssxp 5536	. . . . . . . . . 10 ⊢ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ⊆ (ℕ × ℕ)
102		ssdomg 8410	. . . . . . . . . 10 ⊢ ((ℕ × ℕ) ∈ V → ({⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ⊆ (ℕ × ℕ) → {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ (ℕ × ℕ)))
103	100, 101, 102	mp2 9	. . . . . . . . 9 ⊢ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ (ℕ × ℕ)
104		xpnnen 15401	. . . . . . . . 9 ⊢ (ℕ × ℕ) ≈ ℕ
105		domentr 8423	. . . . . . . . 9 ⊢ (({⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ (ℕ × ℕ) ∧ (ℕ × ℕ) ≈ ℕ) → {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ ℕ)
106	103, 104, 105	mp2an 688	. . . . . . . 8 ⊢ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ ℕ
107		ensym 8413	. . . . . . . . . 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 1128	. . . . . . . . 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 5124	. . . . . . . . . 10 ⊢ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ∈ V
110		fveq2 6545	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑏 → (1^st ‘𝑎) = (1^st ‘𝑏))
111	110	oveq1d 7038	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑏 → ((1^st ‘𝑎)↑2) = ((1^st ‘𝑏)↑2))
112		fveq2 6545	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑏 → (2^nd ‘𝑎) = (2^nd ‘𝑏))
113	112	oveq1d 7038	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑏 → ((2^nd ‘𝑎)↑2) = ((2^nd ‘𝑏)↑2))
114	113	oveq2d 7039	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑏 → (𝐷 · ((2^nd ‘𝑎)↑2)) = (𝐷 · ((2^nd ‘𝑏)↑2)))
115	111, 114	oveq12d 7041	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑏 → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))))
116	115	eqeq1d 2799	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑏 → ((((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥 ↔ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥))
117	116	elrab 3621	. . . . . . . . . . . . 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 767	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) ∧ (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → 𝑏 = ⟨𝑦, 𝑧⟩)
119		simprrl 777	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) ∧ (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ))
120		fveq2 6545	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → (1^st ‘𝑏) = (1^st ‘⟨𝑦, 𝑧⟩))
121	120	oveq1d 7038	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → ((1^st ‘𝑏)↑2) = ((1^st ‘⟨𝑦, 𝑧⟩)↑2))
122		fveq2 6545	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → (2^nd ‘𝑏) = (2^nd ‘⟨𝑦, 𝑧⟩))
123	122	oveq1d 7038	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → ((2^nd ‘𝑏)↑2) = ((2^nd ‘⟨𝑦, 𝑧⟩)↑2))
124	123	oveq2d 7039	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → (𝐷 · ((2^nd ‘𝑏)↑2)) = (𝐷 · ((2^nd ‘⟨𝑦, 𝑧⟩)↑2)))
125	121, 124	oveq12d 7041	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = (((1^st ‘⟨𝑦, 𝑧⟩)↑2) − (𝐷 · ((2^nd ‘⟨𝑦, 𝑧⟩)↑2))))
126	125, 19	syl6req 2850	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → ((𝑦↑2) − (𝐷 · (𝑧↑2))) = (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))))
127	126	ad2antrl 724	. . . . . . . . . . . . . . . . . . . 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 765	. . . . . . . . . . . . . . . . . . . 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 2833	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) ∧ (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)
130	118, 119, 129	jca32 516	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) ∧ (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)))
131	130	ex 413	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) → ((𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))) → (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥))))
132	131	2eximdv 1901	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) → (∃𝑦∃𝑧(𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))) → ∃𝑦∃𝑧(𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥))))
133		elopab 5311	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ↔ ∃𝑦∃𝑧(𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))))
134		elopab 5311	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ↔ ∃𝑦∃𝑧(𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)))
135	132, 133, 134	3imtr4g 297	. . . . . . . . . . . . . . 15 ⊢ ((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) → (𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} → 𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}))
136	135	expimpd 454	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → (((((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥 ∧ 𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))}) → 𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}))
137	136	ancomsd 466	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → ((𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) → 𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}))
138	117, 137	syl5bi 243	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → (𝑏 ∈ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} → 𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}))
139	138	ssrdv 3901	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ⊆ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)})
140	139	3adant3 1125	. . . . . . . . . 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 8410	. . . . . . . . . 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 8422	. . . . . . . . 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 8491	. . . . . . . 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 516	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → (𝑥 ∈ ℤ ∧ (𝑥 ≠ 0 ∧ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ)))
148	147	3exp 1112	. . . . 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 411	. . 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 3236	. 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 207 ∧ wa 396 ∧ w3a 1080 = wceq 1525 ∃wex 1765 ∈ wcel 2083 ≠ wne 2986 ∃wrex 3108 {crab 3111 Vcvv 3440 ∖ cdif 3862 ⊆ wss 3865 {csn 4478 ⟨cop 4484 class class class wbr 4968 {copab 5030 × cxp 5448 ‘cfv 6232 (class class class)co 7023 1^st c1st 7550 2^nd c2nd 7551 ≈ cen 8361 ≼ cdom 8362 Fincfn 8364 ℝcr 10389 0cc0 10390 1c1 10391 + caddc 10393 · cmul 10395 < clt 10528 ≤ cle 10529 − cmin 10723 -cneg 10724 ℕcn 11492 2c2 11546 ℕ₀cn0 11751 ℤcz 11835 ℚcq 12201 ...cfz 12746 ⌊cfl 13014 ↑cexp 13283 √csqrt 14430 abscabs 14431

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-13 2346 ax-ext 2771 ax-rep 5088 ax-sep 5101 ax-nul 5108 ax-pow 5164 ax-pr 5228 ax-un 7326 ax-inf2 8957 ax-cnex 10446 ax-resscn 10447 ax-1cn 10448 ax-icn 10449 ax-addcl 10450 ax-addrcl 10451 ax-mulcl 10452 ax-mulrcl 10453 ax-mulcom 10454 ax-addass 10455 ax-mulass 10456 ax-distr 10457 ax-i2m1 10458 ax-1ne0 10459 ax-1rid 10460 ax-rnegex 10461 ax-rrecex 10462 ax-cnre 10463 ax-pre-lttri 10464 ax-pre-lttrn 10465 ax-pre-ltadd 10466 ax-pre-mulgt0 10467 ax-pre-sup 10468

This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-mo 2578 df-eu 2614 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ne 2987 df-nel 3093 df-ral 3112 df-rex 3113 df-reu 3114 df-rmo 3115 df-rab 3116 df-v 3442 df-sbc 3712 df-csb 3818 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-pss 3882 df-nul 4218 df-if 4388 df-pw 4461 df-sn 4479 df-pr 4481 df-tp 4483 df-op 4485 df-uni 4752 df-int 4789 df-iun 4833 df-br 4969 df-opab 5031 df-mpt 5048 df-tr 5071 df-id 5355 df-eprel 5360 df-po 5369 df-so 5370 df-fr 5409 df-se 5410 df-we 5411 df-xp 5456 df-rel 5457 df-cnv 5458 df-co 5459 df-dm 5460 df-rn 5461 df-res 5462 df-ima 5463 df-pred 6030 df-ord 6076 df-on 6077 df-lim 6078 df-suc 6079 df-iota 6196 df-fun 6234 df-fn 6235 df-f 6236 df-f1 6237 df-fo 6238 df-f1o 6239 df-fv 6240 df-isom 6241 df-riota 6984 df-ov 7026 df-oprab 7027 df-mpo 7028 df-om 7444 df-1st 7552 df-2nd 7553 df-wrecs 7805 df-recs 7867 df-rdg 7905 df-1o 7960 df-oadd 7964 df-omul 7965 df-er 8146 df-map 8265 df-en 8365 df-dom 8366 df-sdom 8367 df-fin 8368 df-sup 8759 df-inf 8760 df-oi 8827 df-card 9221 df-acn 9224 df-pnf 10530 df-mnf 10531 df-xr 10532 df-ltxr 10533 df-le 10534 df-sub 10725 df-neg 10726 df-div 11152 df-nn 11493 df-2 11554 df-3 11555 df-n0 11752 df-xnn0 11822 df-z 11836 df-uz 12098 df-q 12202 df-rp 12244 df-ico 12598 df-fz 12747 df-fl 13016 df-mod 13092 df-seq 13224 df-exp 13284 df-hash 13545 df-cj 14296 df-re 14297 df-im 14298 df-sqrt 14432 df-abs 14433 df-dvds 15445 df-gcd 15681 df-numer 15908 df-denom 15909

This theorem is referenced by: pellex 38938

W3C validator