Step | Hyp | Ref
| Expression |
1 | | pellexlem4 40651 |
. . 3
⊢ ((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) → {〈𝑦,
𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
≈ ℕ) |
2 | | fzfi 13690 |
. . . 4
⊢
(-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 ·
(√‘𝐷)))))
∈ Fin |
3 | | diffi 8944 |
. . . 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 5443 |
. . . . 5
⊢ (𝑎 ∈ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
↔ ∃𝑦∃𝑧(𝑎 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷))))))) |
6 | | fveq2 6771 |
. . . . . . . . . . . 12
⊢ (𝑎 = 〈𝑦, 𝑧〉 → (1st ‘𝑎) = (1st
‘〈𝑦, 𝑧〉)) |
7 | 6 | oveq1d 7286 |
. . . . . . . . . . 11
⊢ (𝑎 = 〈𝑦, 𝑧〉 → ((1st ‘𝑎)↑2) = ((1st
‘〈𝑦, 𝑧〉)↑2)) |
8 | | fveq2 6771 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 〈𝑦, 𝑧〉 → (2nd ‘𝑎) = (2nd
‘〈𝑦, 𝑧〉)) |
9 | 8 | oveq1d 7286 |
. . . . . . . . . . . 12
⊢ (𝑎 = 〈𝑦, 𝑧〉 → ((2nd ‘𝑎)↑2) = ((2nd
‘〈𝑦, 𝑧〉)↑2)) |
10 | 9 | oveq2d 7287 |
. . . . . . . . . . 11
⊢ (𝑎 = 〈𝑦, 𝑧〉 → (𝐷 · ((2nd ‘𝑎)↑2)) = (𝐷 · ((2nd
‘〈𝑦, 𝑧〉)↑2))) |
11 | 7, 10 | oveq12d 7289 |
. . . . . . . . . 10
⊢ (𝑎 = 〈𝑦, 𝑧〉 → (((1st ‘𝑎)↑2) − (𝐷 · ((2nd
‘𝑎)↑2))) =
(((1st ‘〈𝑦, 𝑧〉)↑2) − (𝐷 · ((2nd
‘〈𝑦, 𝑧〉)↑2)))) |
12 | | vex 3435 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
13 | | vex 3435 |
. . . . . . . . . . . . 13
⊢ 𝑧 ∈ V |
14 | 12, 13 | op1st 7832 |
. . . . . . . . . . . 12
⊢
(1st ‘〈𝑦, 𝑧〉) = 𝑦 |
15 | 14 | oveq1i 7281 |
. . . . . . . . . . 11
⊢
((1st ‘〈𝑦, 𝑧〉)↑2) = (𝑦↑2) |
16 | 12, 13 | op2nd 7833 |
. . . . . . . . . . . . 13
⊢
(2nd ‘〈𝑦, 𝑧〉) = 𝑧 |
17 | 16 | oveq1i 7281 |
. . . . . . . . . . . 12
⊢
((2nd ‘〈𝑦, 𝑧〉)↑2) = (𝑧↑2) |
18 | 17 | oveq2i 7282 |
. . . . . . . . . . 11
⊢ (𝐷 · ((2nd
‘〈𝑦, 𝑧〉)↑2)) = (𝐷 · (𝑧↑2)) |
19 | 15, 18 | oveq12i 7283 |
. . . . . . . . . 10
⊢
(((1st ‘〈𝑦, 𝑧〉)↑2) − (𝐷 · ((2nd
‘〈𝑦, 𝑧〉)↑2))) = ((𝑦↑2) − (𝐷 · (𝑧↑2))) |
20 | 11, 19 | eqtrdi 2796 |
. . . . . . . . 9
⊢ (𝑎 = 〈𝑦, 𝑧〉 → (((1st ‘𝑎)↑2) − (𝐷 · ((2nd
‘𝑎)↑2))) =
((𝑦↑2) − (𝐷 · (𝑧↑2)))) |
21 | 20 | ad2antrl 725 |
. . . . . . . 8
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 =
〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))))
→ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) = ((𝑦↑2) − (𝐷 · (𝑧↑2)))) |
22 | | simprrl 778 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ ℕ ∧ (𝑎 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))))
→ (𝑦 ∈ ℕ
∧ 𝑧 ∈
ℕ)) |
23 | | simpl 483 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ ℕ ∧ (𝑎 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))))
→ 𝐷 ∈
ℕ) |
24 | | simprr 770 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))
→ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))) |
25 | 24 | ad2antll 726 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ ℕ ∧ (𝑎 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))))
→ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))) |
26 | | nnz 12342 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
27 | 26 | ad2antrr 723 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧
(abs‘((𝑦↑2)
− (𝐷 · (𝑧↑2)))) < (1 + (2
· (√‘𝐷))))) → 𝑦 ∈ ℤ) |
28 | | zsqcl 13846 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℤ → (𝑦↑2) ∈
ℤ) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧
(abs‘((𝑦↑2)
− (𝐷 · (𝑧↑2)))) < (1 + (2
· (√‘𝐷))))) → (𝑦↑2) ∈ ℤ) |
30 | | nnz 12342 |
. . . . . . . . . . . . . . 15
⊢ (𝐷 ∈ ℕ → 𝐷 ∈
ℤ) |
31 | 30 | ad2antrl 725 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧
(abs‘((𝑦↑2)
− (𝐷 · (𝑧↑2)))) < (1 + (2
· (√‘𝐷))))) → 𝐷 ∈ ℤ) |
32 | | simplr 766 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧
(abs‘((𝑦↑2)
− (𝐷 · (𝑧↑2)))) < (1 + (2
· (√‘𝐷))))) → 𝑧 ∈ ℕ) |
33 | 32 | nnzd 12424 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧
(abs‘((𝑦↑2)
− (𝐷 · (𝑧↑2)))) < (1 + (2
· (√‘𝐷))))) → 𝑧 ∈ ℤ) |
34 | | zsqcl 13846 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℤ → (𝑧↑2) ∈
ℤ) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧
(abs‘((𝑦↑2)
− (𝐷 · (𝑧↑2)))) < (1 + (2
· (√‘𝐷))))) → (𝑧↑2) ∈ ℤ) |
36 | 31, 35 | zmulcld 12431 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧
(abs‘((𝑦↑2)
− (𝐷 · (𝑧↑2)))) < (1 + (2
· (√‘𝐷))))) → (𝐷 · (𝑧↑2)) ∈ ℤ) |
37 | 29, 36 | zsubcld 12430 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧
(abs‘((𝑦↑2)
− (𝐷 · (𝑧↑2)))) < (1 + (2
· (√‘𝐷))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℤ) |
38 | | 1re 10976 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ |
39 | | 2re 12047 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ |
40 | | nnre 11980 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐷 ∈ ℕ → 𝐷 ∈
ℝ) |
41 | 40 | ad2antrl 725 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧
(abs‘((𝑦↑2)
− (𝐷 · (𝑧↑2)))) < (1 + (2
· (√‘𝐷))))) → 𝐷 ∈ ℝ) |
42 | | nnnn0 12240 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐷 ∈ ℕ → 𝐷 ∈
ℕ0) |
43 | 42 | ad2antrl 725 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧
(abs‘((𝑦↑2)
− (𝐷 · (𝑧↑2)))) < (1 + (2
· (√‘𝐷))))) → 𝐷 ∈
ℕ0) |
44 | 43 | nn0ge0d 12296 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧
(abs‘((𝑦↑2)
− (𝐷 · (𝑧↑2)))) < (1 + (2
· (√‘𝐷))))) → 0 ≤ 𝐷) |
45 | 41, 44 | resqrtcld 15127 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧
(abs‘((𝑦↑2)
− (𝐷 · (𝑧↑2)))) < (1 + (2
· (√‘𝐷))))) → (√‘𝐷) ∈
ℝ) |
46 | | remulcl 10957 |
. . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℝ ∧ (√‘𝐷) ∈ ℝ) → (2 ·
(√‘𝐷)) ∈
ℝ) |
47 | 39, 45, 46 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧
(abs‘((𝑦↑2)
− (𝐷 · (𝑧↑2)))) < (1 + (2
· (√‘𝐷))))) → (2 ·
(√‘𝐷)) ∈
ℝ) |
48 | | readdcl 10955 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℝ ∧ (2 · (√‘𝐷)) ∈ ℝ) → (1 + (2 ·
(√‘𝐷))) ∈
ℝ) |
49 | 38, 47, 48 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧
(abs‘((𝑦↑2)
− (𝐷 · (𝑧↑2)))) < (1 + (2
· (√‘𝐷))))) → (1 + (2 ·
(√‘𝐷))) ∈
ℝ) |
50 | 49 | flcld 13516 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧
(abs‘((𝑦↑2)
− (𝐷 · (𝑧↑2)))) < (1 + (2
· (√‘𝐷))))) → (⌊‘(1 + (2 ·
(√‘𝐷)))) ∈
ℤ) |
51 | 50 | znegcld 12427 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧
(abs‘((𝑦↑2)
− (𝐷 · (𝑧↑2)))) < (1 + (2
· (√‘𝐷))))) → -(⌊‘(1 + (2
· (√‘𝐷)))) ∈ ℤ) |
52 | 37 | zred 12425 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧
(abs‘((𝑦↑2)
− (𝐷 · (𝑧↑2)))) < (1 + (2
· (√‘𝐷))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℝ) |
53 | 50 | zred 12425 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧
(abs‘((𝑦↑2)
− (𝐷 · (𝑧↑2)))) < (1 + (2
· (√‘𝐷))))) → (⌊‘(1 + (2 ·
(√‘𝐷)))) ∈
ℝ) |
54 | | nn0abscl 15022 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℤ →
(abs‘((𝑦↑2)
− (𝐷 · (𝑧↑2)))) ∈
ℕ0) |
55 | 37, 54 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧
(abs‘((𝑦↑2)
− (𝐷 · (𝑧↑2)))) < (1 + (2
· (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ∈
ℕ0) |
56 | 55 | nn0zd 12423 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧
(abs‘((𝑦↑2)
− (𝐷 · (𝑧↑2)))) < (1 + (2
· (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ∈ ℤ) |
57 | 56 | zred 12425 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧
(abs‘((𝑦↑2)
− (𝐷 · (𝑧↑2)))) < (1 + (2
· (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ∈ ℝ) |
58 | | peano2re 11148 |
. . . . . . . . . . . . . . . 16
⊢
((⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℝ →
((⌊‘(1 + (2 · (√‘𝐷)))) + 1) ∈ ℝ) |
59 | 53, 58 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧
(abs‘((𝑦↑2)
− (𝐷 · (𝑧↑2)))) < (1 + (2
· (√‘𝐷))))) → ((⌊‘(1 + (2
· (√‘𝐷)))) + 1) ∈ ℝ) |
60 | | simprr 770 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧
(abs‘((𝑦↑2)
− (𝐷 · (𝑧↑2)))) < (1 + (2
· (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))) |
61 | | flltp1 13518 |
. . . . . . . . . . . . . . . 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 11136 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧
(abs‘((𝑦↑2)
− (𝐷 · (𝑧↑2)))) < (1 + (2
· (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < ((⌊‘(1 + (2
· (√‘𝐷)))) + 1)) |
64 | | zleltp1 12371 |
. . . . . . . . . . . . . . 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 256 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧
(abs‘((𝑦↑2)
− (𝐷 · (𝑧↑2)))) < (1 + (2
· (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ≤ (⌊‘(1 + (2
· (√‘𝐷))))) |
67 | | absle 15025 |
. . . . . . . . . . . . . 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 835 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧
(abs‘((𝑦↑2)
− (𝐷 · (𝑧↑2)))) < (1 + (2
· (√‘𝐷))))) → (-(⌊‘(1 + (2
· (√‘𝐷)))) ≤ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≤ (⌊‘(1 + (2
· (√‘𝐷)))))) |
70 | | elfz 13244 |
. . . . . . . . . . . . 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 1372 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧
(abs‘((𝑦↑2)
− (𝐷 · (𝑧↑2)))) < (1 + (2
· (√‘𝐷))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ (-(⌊‘(1 + (2
· (√‘𝐷))))...(⌊‘(1 + (2 ·
(√‘𝐷)))))) |
73 | 22, 23, 25, 72 | syl12anc 834 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ ℕ ∧ (𝑎 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))))
→ ((𝑦↑2) −
(𝐷 · (𝑧↑2))) ∈
(-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 ·
(√‘𝐷)))))) |
74 | 73 | adantlr 712 |
. . . . . . . . 9
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 =
〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))))
→ ((𝑦↑2) −
(𝐷 · (𝑧↑2))) ∈
(-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 ·
(√‘𝐷)))))) |
75 | | simprl 768 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))
→ ((𝑦↑2) −
(𝐷 · (𝑧↑2))) ≠
0) |
76 | 75 | ad2antll 726 |
. . . . . . . . 9
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 =
〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))))
→ ((𝑦↑2) −
(𝐷 · (𝑧↑2))) ≠
0) |
77 | | eldifsn 4726 |
. . . . . . . . 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 2841 |
. . . . . . 7
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑎 =
〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))))
→ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) ∈
((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 ·
(√‘𝐷)))))
∖ {0})) |
80 | 79 | ex 413 |
. . . . . 6
⊢ ((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) → ((𝑎 =
〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷))))))
→ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) ∈
((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 ·
(√‘𝐷)))))
∖ {0}))) |
81 | 80 | exlimdvv 1941 |
. . . . 5
⊢ ((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) → (∃𝑦∃𝑧(𝑎 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷))))))
→ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) ∈
((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 ·
(√‘𝐷)))))
∖ {0}))) |
82 | 5, 81 | syl5bi 241 |
. . . 4
⊢ ((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) → (𝑎 ∈
{〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
→ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) ∈
((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 ·
(√‘𝐷)))))
∖ {0}))) |
83 | 82 | imp 407 |
. . 3
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ 𝑎 ∈
{〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))})
→ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) ∈
((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 ·
(√‘𝐷)))))
∖ {0})) |
84 | 1, 4, 83 | fiphp3d 40638 |
. 2
⊢ ((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) → ∃𝑥
∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 ·
(√‘𝐷)))))
∖ {0}){𝑎 ∈
{〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∣ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) |
85 | | eldif 3902 |
. . . . . 6
⊢ (𝑥 ∈ ((-(⌊‘(1 +
(2 · (√‘𝐷))))...(⌊‘(1 + (2 ·
(√‘𝐷)))))
∖ {0}) ↔ (𝑥
∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 ·
(√‘𝐷))))) ∧
¬ 𝑥 ∈
{0})) |
86 | | elfzelz 13255 |
. . . . . . . 8
⊢ (𝑥 ∈ (-(⌊‘(1 + (2
· (√‘𝐷))))...(⌊‘(1 + (2 ·
(√‘𝐷)))))
→ 𝑥 ∈
ℤ) |
87 | | simp2 1136 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ 𝑥 ∈
ℤ ∧ ¬ 𝑥
∈ {0}) → 𝑥 ∈
ℤ) |
88 | | velsn 4583 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ {0} ↔ 𝑥 = 0) |
89 | 88 | biimpri 227 |
. . . . . . . . . . . 12
⊢ (𝑥 = 0 → 𝑥 ∈ {0}) |
90 | 89 | necon3bi 2972 |
. . . . . . . . . . 11
⊢ (¬
𝑥 ∈ {0} → 𝑥 ≠ 0) |
91 | 90 | 3ad2ant3 1134 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ 𝑥 ∈
ℤ ∧ ¬ 𝑥
∈ {0}) → 𝑥 ≠
0) |
92 | 87, 91 | jca 512 |
. . . . . . . . 9
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ 𝑥 ∈
ℤ ∧ ¬ 𝑥
∈ {0}) → (𝑥
∈ ℤ ∧ 𝑥 ≠
0)) |
93 | 92 | 3exp 1118 |
. . . . . . . 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 241 |
. . . . 5
⊢ ((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) → (𝑥 ∈
((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 ·
(√‘𝐷)))))
∖ {0}) → (𝑥
∈ ℤ ∧ 𝑥 ≠
0))) |
97 | | simp2l 1198 |
. . . . . . 7
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑥 ∈
ℤ ∧ 𝑥 ≠ 0)
∧ {𝑎 ∈
{〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∣ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → 𝑥 ∈ ℤ) |
98 | | simp2r 1199 |
. . . . . . 7
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑥 ∈
ℤ ∧ 𝑥 ≠ 0)
∧ {𝑎 ∈
{〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∣ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → 𝑥 ≠ 0) |
99 | | nnex 11979 |
. . . . . . . . . . 11
⊢ ℕ
∈ V |
100 | 99, 99 | xpex 7597 |
. . . . . . . . . 10
⊢ (ℕ
× ℕ) ∈ V |
101 | | opabssxp 5679 |
. . . . . . . . . 10
⊢
{〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ⊆ (ℕ ×
ℕ) |
102 | | ssdomg 8769 |
. . . . . . . . . 10
⊢ ((ℕ
× ℕ) ∈ V → ({〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ⊆ (ℕ × ℕ) →
{〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ (ℕ ×
ℕ))) |
103 | 100, 101,
102 | mp2 9 |
. . . . . . . . 9
⊢
{〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ (ℕ ×
ℕ) |
104 | | xpnnen 15918 |
. . . . . . . . 9
⊢ (ℕ
× ℕ) ≈ ℕ |
105 | | domentr 8782 |
. . . . . . . . 9
⊢
(({〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ (ℕ × ℕ) ∧
(ℕ × ℕ) ≈ ℕ) → {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ ℕ) |
106 | 103, 104,
105 | mp2an 689 |
. . . . . . . 8
⊢
{〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ ℕ |
107 | | ensym 8772 |
. . . . . . . . . 10
⊢ ({𝑎 ∈ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∣ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ → ℕ ≈
{𝑎 ∈ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∣ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) = 𝑥}) |
108 | 107 | 3ad2ant3 1134 |
. . . . . . . . 9
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑥 ∈
ℤ ∧ 𝑥 ≠ 0)
∧ {𝑎 ∈
{〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∣ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → ℕ ≈
{𝑎 ∈ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∣ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) = 𝑥}) |
109 | 100, 101 | ssexi 5250 |
. . . . . . . . . 10
⊢
{〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ∈ V |
110 | | fveq2 6771 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑏 → (1st ‘𝑎) = (1st ‘𝑏)) |
111 | 110 | oveq1d 7286 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑏 → ((1st ‘𝑎)↑2) = ((1st
‘𝑏)↑2)) |
112 | | fveq2 6771 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑏 → (2nd ‘𝑎) = (2nd ‘𝑏)) |
113 | 112 | oveq1d 7286 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑏 → ((2nd ‘𝑎)↑2) = ((2nd
‘𝑏)↑2)) |
114 | 113 | oveq2d 7287 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑏 → (𝐷 · ((2nd ‘𝑎)↑2)) = (𝐷 · ((2nd ‘𝑏)↑2))) |
115 | 111, 114 | oveq12d 7289 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑏 → (((1st ‘𝑎)↑2) − (𝐷 · ((2nd
‘𝑎)↑2))) =
(((1st ‘𝑏)↑2) − (𝐷 · ((2nd ‘𝑏)↑2)))) |
116 | 115 | eqeq1d 2742 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑏 → ((((1st ‘𝑎)↑2) − (𝐷 · ((2nd
‘𝑎)↑2))) = 𝑥 ↔ (((1st
‘𝑏)↑2) −
(𝐷 ·
((2nd ‘𝑏)↑2))) = 𝑥)) |
117 | 116 | elrab 3626 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ {𝑎 ∈ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∣ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) = 𝑥} ↔ (𝑏 ∈ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∧ (((1st ‘𝑏)↑2) − (𝐷 · ((2nd ‘𝑏)↑2))) = 𝑥)) |
118 | | simprl 768 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1st
‘𝑏)↑2) −
(𝐷 ·
((2nd ‘𝑏)↑2))) = 𝑥) ∧ (𝑏 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))))
→ 𝑏 = 〈𝑦, 𝑧〉) |
119 | | simprrl 778 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1st
‘𝑏)↑2) −
(𝐷 ·
((2nd ‘𝑏)↑2))) = 𝑥) ∧ (𝑏 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))))
→ (𝑦 ∈ ℕ
∧ 𝑧 ∈
ℕ)) |
120 | | fveq2 6771 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑏 = 〈𝑦, 𝑧〉 → (1st ‘𝑏) = (1st
‘〈𝑦, 𝑧〉)) |
121 | 120 | oveq1d 7286 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑏 = 〈𝑦, 𝑧〉 → ((1st ‘𝑏)↑2) = ((1st
‘〈𝑦, 𝑧〉)↑2)) |
122 | | fveq2 6771 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑏 = 〈𝑦, 𝑧〉 → (2nd ‘𝑏) = (2nd
‘〈𝑦, 𝑧〉)) |
123 | 122 | oveq1d 7286 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑏 = 〈𝑦, 𝑧〉 → ((2nd ‘𝑏)↑2) = ((2nd
‘〈𝑦, 𝑧〉)↑2)) |
124 | 123 | oveq2d 7287 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑏 = 〈𝑦, 𝑧〉 → (𝐷 · ((2nd ‘𝑏)↑2)) = (𝐷 · ((2nd
‘〈𝑦, 𝑧〉)↑2))) |
125 | 121, 124 | oveq12d 7289 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 = 〈𝑦, 𝑧〉 → (((1st ‘𝑏)↑2) − (𝐷 · ((2nd
‘𝑏)↑2))) =
(((1st ‘〈𝑦, 𝑧〉)↑2) − (𝐷 · ((2nd
‘〈𝑦, 𝑧〉)↑2)))) |
126 | 125, 19 | eqtr2di 2797 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 = 〈𝑦, 𝑧〉 → ((𝑦↑2) − (𝐷 · (𝑧↑2))) = (((1st ‘𝑏)↑2) − (𝐷 · ((2nd
‘𝑏)↑2)))) |
127 | 126 | ad2antrl 725 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1st
‘𝑏)↑2) −
(𝐷 ·
((2nd ‘𝑏)↑2))) = 𝑥) ∧ (𝑏 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))))
→ ((𝑦↑2) −
(𝐷 · (𝑧↑2))) = (((1st
‘𝑏)↑2) −
(𝐷 ·
((2nd ‘𝑏)↑2)))) |
128 | | simplr 766 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1st
‘𝑏)↑2) −
(𝐷 ·
((2nd ‘𝑏)↑2))) = 𝑥) ∧ (𝑏 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))))
→ (((1st ‘𝑏)↑2) − (𝐷 · ((2nd ‘𝑏)↑2))) = 𝑥) |
129 | 127, 128 | eqtrd 2780 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1st
‘𝑏)↑2) −
(𝐷 ·
((2nd ‘𝑏)↑2))) = 𝑥) ∧ (𝑏 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))))
→ ((𝑦↑2) −
(𝐷 · (𝑧↑2))) = 𝑥) |
130 | 118, 119,
129 | jca32 516 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1st
‘𝑏)↑2) −
(𝐷 ·
((2nd ‘𝑏)↑2))) = 𝑥) ∧ (𝑏 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))))
→ (𝑏 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥))) |
131 | 130 | ex 413 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑥 ∈
ℤ ∧ 𝑥 ≠ 0))
∧ (((1st ‘𝑏)↑2) − (𝐷 · ((2nd ‘𝑏)↑2))) = 𝑥) → ((𝑏 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷))))))
→ (𝑏 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)))) |
132 | 131 | 2eximdv 1926 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑥 ∈
ℤ ∧ 𝑥 ≠ 0))
∧ (((1st ‘𝑏)↑2) − (𝐷 · ((2nd ‘𝑏)↑2))) = 𝑥) → (∃𝑦∃𝑧(𝑏 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷))))))
→ ∃𝑦∃𝑧(𝑏 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)))) |
133 | | elopab 5443 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ∈ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
↔ ∃𝑦∃𝑧(𝑏 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷))))))) |
134 | | elopab 5443 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ∈ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ↔ ∃𝑦∃𝑧(𝑏 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥))) |
135 | 132, 133,
134 | 3imtr4g 296 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑥 ∈
ℤ ∧ 𝑥 ≠ 0))
∧ (((1st ‘𝑏)↑2) − (𝐷 · ((2nd ‘𝑏)↑2))) = 𝑥) → (𝑏 ∈ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
→ 𝑏 ∈
{〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)})) |
136 | 135 | expimpd 454 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑥 ∈
ℤ ∧ 𝑥 ≠ 0))
→ (((((1st ‘𝑏)↑2) − (𝐷 · ((2nd ‘𝑏)↑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 ·
(√‘𝐷)))))}
∧ (((1st ‘𝑏)↑2) − (𝐷 · ((2nd ‘𝑏)↑2))) = 𝑥) → 𝑏 ∈ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)})) |
138 | 117, 137 | syl5bi 241 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑥 ∈
ℤ ∧ 𝑥 ≠ 0))
→ (𝑏 ∈ {𝑎 ∈ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∣ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) = 𝑥} → 𝑏 ∈ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)})) |
139 | 138 | ssrdv 3932 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑥 ∈
ℤ ∧ 𝑥 ≠ 0))
→ {𝑎 ∈
{〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∣ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) = 𝑥} ⊆ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}) |
140 | 139 | 3adant3 1131 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑥 ∈
ℤ ∧ 𝑥 ≠ 0)
∧ {𝑎 ∈
{〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∣ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → {𝑎 ∈ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∣ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) = 𝑥} ⊆ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}) |
141 | | ssdomg 8769 |
. . . . . . . . . 10
⊢
({〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ∈ V → ({𝑎 ∈ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∣ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) = 𝑥} ⊆ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} → {𝑎 ∈ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∣ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) = 𝑥} ≼ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)})) |
142 | 109, 140,
141 | mpsyl 68 |
. . . . . . . . 9
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑥 ∈
ℤ ∧ 𝑥 ≠ 0)
∧ {𝑎 ∈
{〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∣ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → {𝑎 ∈ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∣ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) = 𝑥} ≼ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}) |
143 | | endomtr 8781 |
. . . . . . . . 9
⊢ ((ℕ
≈ {𝑎 ∈
{〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∣ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) = 𝑥} ∧ {𝑎 ∈ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∣ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) = 𝑥} ≼ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}) → ℕ ≼ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}) |
144 | 108, 142,
143 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑥 ∈
ℤ ∧ 𝑥 ≠ 0)
∧ {𝑎 ∈
{〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∣ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → ℕ ≼
{〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}) |
145 | | sbth 8862 |
. . . . . . . 8
⊢
(({〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ ℕ ∧ ℕ ≼
{〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}) → {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ) |
146 | 106, 144,
145 | sylancr 587 |
. . . . . . 7
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑥 ∈
ℤ ∧ 𝑥 ≠ 0)
∧ {𝑎 ∈
{〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∣ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ) |
147 | 97, 98, 146 | jca32 516 |
. . . . . 6
⊢ (((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ (𝑥 ∈
ℤ ∧ 𝑥 ≠ 0)
∧ {𝑎 ∈
{〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∣ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → (𝑥 ∈ ℤ ∧ (𝑥 ≠ 0 ∧ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ))) |
148 | 147 | 3exp 1118 |
. . . . 5
⊢ ((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) → ((𝑥 ∈
ℤ ∧ 𝑥 ≠ 0)
→ ({𝑎 ∈
{〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∣ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ → (𝑥 ∈ ℤ ∧ (𝑥 ≠ 0 ∧ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ))))) |
149 | 96, 148 | syld 47 |
. . . 4
⊢ ((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) → (𝑥 ∈
((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 ·
(√‘𝐷)))))
∖ {0}) → ({𝑎
∈ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∣ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ → (𝑥 ∈ ℤ ∧ (𝑥 ≠ 0 ∧ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ))))) |
150 | 149 | impd 411 |
. . 3
⊢ ((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) → ((𝑥 ∈
((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 ·
(√‘𝐷)))))
∖ {0}) ∧ {𝑎
∈ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∣ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → (𝑥 ∈ ℤ ∧ (𝑥 ≠ 0 ∧ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ)))) |
151 | 150 | reximdv2 3201 |
. 2
⊢ ((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) → (∃𝑥
∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 ·
(√‘𝐷)))))
∖ {0}){𝑎 ∈
{〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 ·
(√‘𝐷)))))}
∣ (((1st ‘𝑎)↑2) − (𝐷 · ((2nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ → ∃𝑥 ∈ ℤ (𝑥 ≠ 0 ∧ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ))) |
152 | 84, 151 | mpd 15 |
1
⊢ ((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) → ∃𝑥
∈ ℤ (𝑥 ≠ 0
∧ {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ)) |