| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fzfi 14014 | . . . . . . . 8
⊢
(0...((abs‘𝑎)
− 1)) ∈ Fin | 
| 2 |  | xpfi 9359 | . . . . . . . 8
⊢
(((0...((abs‘𝑎) − 1)) ∈ Fin ∧
(0...((abs‘𝑎) −
1)) ∈ Fin) → ((0...((abs‘𝑎) − 1)) × (0...((abs‘𝑎) − 1))) ∈
Fin) | 
| 3 | 1, 1, 2 | mp2an 692 | . . . . . . 7
⊢
((0...((abs‘𝑎)
− 1)) × (0...((abs‘𝑎) − 1))) ∈ Fin | 
| 4 |  | isfinite 9693 | . . . . . . 7
⊢
(((0...((abs‘𝑎) − 1)) × (0...((abs‘𝑎) − 1))) ∈ Fin ↔
((0...((abs‘𝑎)
− 1)) × (0...((abs‘𝑎) − 1))) ≺
ω) | 
| 5 | 3, 4 | mpbi 230 | . . . . . 6
⊢
((0...((abs‘𝑎)
− 1)) × (0...((abs‘𝑎) − 1))) ≺
ω | 
| 6 |  | nnenom 14022 | . . . . . . 7
⊢ ℕ
≈ ω | 
| 7 | 6 | ensymi 9045 | . . . . . 6
⊢ ω
≈ ℕ | 
| 8 |  | sdomentr 9152 | . . . . . 6
⊢
((((0...((abs‘𝑎) − 1)) × (0...((abs‘𝑎) − 1))) ≺ ω
∧ ω ≈ ℕ) → ((0...((abs‘𝑎) − 1)) × (0...((abs‘𝑎) − 1))) ≺
ℕ) | 
| 9 | 5, 7, 8 | mp2an 692 | . . . . 5
⊢
((0...((abs‘𝑎)
− 1)) × (0...((abs‘𝑎) − 1))) ≺
ℕ | 
| 10 |  | ensym 9044 | . . . . . 6
⊢
({〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)} ≈ ℕ → ℕ ≈
{〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)}) | 
| 11 | 10 | ad2antll 729 | . . . . 5
⊢ ((((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ 𝑎 ∈
ℤ) ∧ (𝑎 ≠ 0
∧ {〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)} ≈ ℕ)) → ℕ ≈
{〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)}) | 
| 12 |  | sdomentr 9152 | . . . . 5
⊢
((((0...((abs‘𝑎) − 1)) × (0...((abs‘𝑎) − 1))) ≺ ℕ
∧ ℕ ≈ {〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)}) → ((0...((abs‘𝑎) − 1)) ×
(0...((abs‘𝑎) −
1))) ≺ {〈𝑏,
𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)}) | 
| 13 | 9, 11, 12 | sylancr 587 | . . . 4
⊢ ((((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ 𝑎 ∈
ℤ) ∧ (𝑎 ≠ 0
∧ {〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)} ≈ ℕ)) →
((0...((abs‘𝑎)
− 1)) × (0...((abs‘𝑎) − 1))) ≺ {〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)}) | 
| 14 |  | opabssxp 5777 | . . . . . . . 8
⊢
{〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)} ⊆ (ℕ ×
ℕ) | 
| 15 | 14 | sseli 3978 | . . . . . . 7
⊢ (𝑑 ∈ {〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)} → 𝑑 ∈ (ℕ ×
ℕ)) | 
| 16 |  | simprrl 780 | . . . . . . . . . . . 12
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 ∈ (V × V) ∧ ((1st
‘𝑑) ∈ ℕ
∧ (2nd ‘𝑑) ∈ ℕ))) → (1st
‘𝑑) ∈
ℕ) | 
| 17 | 16 | nnzd 12642 | . . . . . . . . . . 11
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 ∈ (V × V) ∧ ((1st
‘𝑑) ∈ ℕ
∧ (2nd ‘𝑑) ∈ ℕ))) → (1st
‘𝑑) ∈
ℤ) | 
| 18 |  | simpllr 775 | . . . . . . . . . . . 12
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 ∈ (V × V) ∧ ((1st
‘𝑑) ∈ ℕ
∧ (2nd ‘𝑑) ∈ ℕ))) → 𝑎 ∈ ℤ) | 
| 19 |  | simplr 768 | . . . . . . . . . . . 12
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 ∈ (V × V) ∧ ((1st
‘𝑑) ∈ ℕ
∧ (2nd ‘𝑑) ∈ ℕ))) → 𝑎 ≠ 0) | 
| 20 |  | nnabscl 15365 | . . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℤ ∧ 𝑎 ≠ 0) → (abs‘𝑎) ∈
ℕ) | 
| 21 | 18, 19, 20 | syl2anc 584 | . . . . . . . . . . 11
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 ∈ (V × V) ∧ ((1st
‘𝑑) ∈ ℕ
∧ (2nd ‘𝑑) ∈ ℕ))) → (abs‘𝑎) ∈
ℕ) | 
| 22 |  | zmodfz 13934 | . . . . . . . . . . 11
⊢
(((1st ‘𝑑) ∈ ℤ ∧ (abs‘𝑎) ∈ ℕ) →
((1st ‘𝑑)
mod (abs‘𝑎)) ∈
(0...((abs‘𝑎) −
1))) | 
| 23 | 17, 21, 22 | syl2anc 584 | . . . . . . . . . 10
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 ∈ (V × V) ∧ ((1st
‘𝑑) ∈ ℕ
∧ (2nd ‘𝑑) ∈ ℕ))) → ((1st
‘𝑑) mod
(abs‘𝑎)) ∈
(0...((abs‘𝑎) −
1))) | 
| 24 |  | simprrr 781 | . . . . . . . . . . . 12
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 ∈ (V × V) ∧ ((1st
‘𝑑) ∈ ℕ
∧ (2nd ‘𝑑) ∈ ℕ))) → (2nd
‘𝑑) ∈
ℕ) | 
| 25 | 24 | nnzd 12642 | . . . . . . . . . . 11
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 ∈ (V × V) ∧ ((1st
‘𝑑) ∈ ℕ
∧ (2nd ‘𝑑) ∈ ℕ))) → (2nd
‘𝑑) ∈
ℤ) | 
| 26 |  | zmodfz 13934 | . . . . . . . . . . 11
⊢
(((2nd ‘𝑑) ∈ ℤ ∧ (abs‘𝑎) ∈ ℕ) →
((2nd ‘𝑑)
mod (abs‘𝑎)) ∈
(0...((abs‘𝑎) −
1))) | 
| 27 | 25, 21, 26 | syl2anc 584 | . . . . . . . . . 10
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 ∈ (V × V) ∧ ((1st
‘𝑑) ∈ ℕ
∧ (2nd ‘𝑑) ∈ ℕ))) → ((2nd
‘𝑑) mod
(abs‘𝑎)) ∈
(0...((abs‘𝑎) −
1))) | 
| 28 | 23, 27 | jca 511 | . . . . . . . . 9
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 ∈ (V × V) ∧ ((1st
‘𝑑) ∈ ℕ
∧ (2nd ‘𝑑) ∈ ℕ))) → (((1st
‘𝑑) mod
(abs‘𝑎)) ∈
(0...((abs‘𝑎) −
1)) ∧ ((2nd ‘𝑑) mod (abs‘𝑎)) ∈ (0...((abs‘𝑎) − 1)))) | 
| 29 | 28 | ex 412 | . . . . . . . 8
⊢ ((((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ 𝑎 ∈
ℤ) ∧ 𝑎 ≠ 0)
→ ((𝑑 ∈ (V
× V) ∧ ((1st ‘𝑑) ∈ ℕ ∧ (2nd
‘𝑑) ∈ ℕ))
→ (((1st ‘𝑑) mod (abs‘𝑎)) ∈ (0...((abs‘𝑎) − 1)) ∧ ((2nd
‘𝑑) mod
(abs‘𝑎)) ∈
(0...((abs‘𝑎) −
1))))) | 
| 30 |  | elxp7 8050 | . . . . . . . 8
⊢ (𝑑 ∈ (ℕ ×
ℕ) ↔ (𝑑 ∈
(V × V) ∧ ((1st ‘𝑑) ∈ ℕ ∧ (2nd
‘𝑑) ∈
ℕ))) | 
| 31 |  | opelxp 5720 | . . . . . . . 8
⊢
(〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd ‘𝑑) mod (abs‘𝑎))〉 ∈
((0...((abs‘𝑎)
− 1)) × (0...((abs‘𝑎) − 1))) ↔ (((1st
‘𝑑) mod
(abs‘𝑎)) ∈
(0...((abs‘𝑎) −
1)) ∧ ((2nd ‘𝑑) mod (abs‘𝑎)) ∈ (0...((abs‘𝑎) − 1)))) | 
| 32 | 29, 30, 31 | 3imtr4g 296 | . . . . . . 7
⊢ ((((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ 𝑎 ∈
ℤ) ∧ 𝑎 ≠ 0)
→ (𝑑 ∈ (ℕ
× ℕ) → 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd ‘𝑑) mod (abs‘𝑎))〉 ∈
((0...((abs‘𝑎)
− 1)) × (0...((abs‘𝑎) − 1))))) | 
| 33 | 15, 32 | syl5 34 | . . . . . 6
⊢ ((((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ 𝑎 ∈
ℤ) ∧ 𝑎 ≠ 0)
→ (𝑑 ∈
{〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)} → 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 ∈
((0...((abs‘𝑎)
− 1)) × (0...((abs‘𝑎) − 1))))) | 
| 34 | 33 | imp 406 | . . . . 5
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ 𝑑 ∈ {〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)}) → 〈((1st
‘𝑑) mod
(abs‘𝑎)),
((2nd ‘𝑑)
mod (abs‘𝑎))〉
∈ ((0...((abs‘𝑎)
− 1)) × (0...((abs‘𝑎) − 1)))) | 
| 35 | 34 | adantlrr 721 | . . . 4
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ (𝑎 ≠ 0 ∧ {〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)} ≈ ℕ)) ∧ 𝑑 ∈ {〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)}) → 〈((1st
‘𝑑) mod
(abs‘𝑎)),
((2nd ‘𝑑)
mod (abs‘𝑎))〉
∈ ((0...((abs‘𝑎)
− 1)) × (0...((abs‘𝑎) − 1)))) | 
| 36 |  | fveq2 6905 | . . . . . 6
⊢ (𝑑 = 𝑒 → (1st ‘𝑑) = (1st ‘𝑒)) | 
| 37 | 36 | oveq1d 7447 | . . . . 5
⊢ (𝑑 = 𝑒 → ((1st ‘𝑑) mod (abs‘𝑎)) = ((1st
‘𝑒) mod
(abs‘𝑎))) | 
| 38 |  | fveq2 6905 | . . . . . 6
⊢ (𝑑 = 𝑒 → (2nd ‘𝑑) = (2nd ‘𝑒)) | 
| 39 | 38 | oveq1d 7447 | . . . . 5
⊢ (𝑑 = 𝑒 → ((2nd ‘𝑑) mod (abs‘𝑎)) = ((2nd
‘𝑒) mod
(abs‘𝑎))) | 
| 40 | 37, 39 | opeq12d 4880 | . . . 4
⊢ (𝑑 = 𝑒 → 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉) | 
| 41 | 13, 35, 40 | fphpd 42832 | . . 3
⊢ ((((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ 𝑎 ∈
ℤ) ∧ (𝑎 ≠ 0
∧ {〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)} ≈ ℕ)) → ∃𝑑 ∈ {〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)}∃𝑒 ∈ {〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)} (𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉)) | 
| 42 |  | eleq1w 2823 | . . . . . . . . . . . 12
⊢ (𝑏 = 𝑓 → (𝑏 ∈ ℕ ↔ 𝑓 ∈ ℕ)) | 
| 43 |  | eleq1w 2823 | . . . . . . . . . . . 12
⊢ (𝑐 = 𝑔 → (𝑐 ∈ ℕ ↔ 𝑔 ∈ ℕ)) | 
| 44 | 42, 43 | bi2anan9 638 | . . . . . . . . . . 11
⊢ ((𝑏 = 𝑓 ∧ 𝑐 = 𝑔) → ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ↔ (𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ))) | 
| 45 |  | oveq1 7439 | . . . . . . . . . . . . 13
⊢ (𝑏 = 𝑓 → (𝑏↑2) = (𝑓↑2)) | 
| 46 |  | oveq1 7439 | . . . . . . . . . . . . . 14
⊢ (𝑐 = 𝑔 → (𝑐↑2) = (𝑔↑2)) | 
| 47 | 46 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (𝑐 = 𝑔 → (𝐷 · (𝑐↑2)) = (𝐷 · (𝑔↑2))) | 
| 48 | 45, 47 | oveqan12d 7451 | . . . . . . . . . . . 12
⊢ ((𝑏 = 𝑓 ∧ 𝑐 = 𝑔) → ((𝑏↑2) − (𝐷 · (𝑐↑2))) = ((𝑓↑2) − (𝐷 · (𝑔↑2)))) | 
| 49 | 48 | eqeq1d 2738 | . . . . . . . . . . 11
⊢ ((𝑏 = 𝑓 ∧ 𝑐 = 𝑔) → (((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎 ↔ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)) | 
| 50 | 44, 49 | anbi12d 632 | . . . . . . . . . 10
⊢ ((𝑏 = 𝑓 ∧ 𝑐 = 𝑔) → (((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎) ↔ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎))) | 
| 51 | 50 | cbvopabv 5215 | . . . . . . . . 9
⊢
{〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)} = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)} | 
| 52 | 51 | eleq2i 2832 | . . . . . . . 8
⊢ (𝑒 ∈ {〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)} ↔ 𝑒 ∈ {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)}) | 
| 53 | 52 | biimpi 216 | . . . . . . 7
⊢ (𝑒 ∈ {〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)} → 𝑒 ∈ {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)}) | 
| 54 |  | elopab 5531 | . . . . . . . . 9
⊢ (𝑑 ∈ {〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)} ↔ ∃𝑏∃𝑐(𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎))) | 
| 55 |  | elopab 5531 | . . . . . . . . . . . 12
⊢ (𝑒 ∈ {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)} ↔ ∃𝑓∃𝑔(𝑒 = 〈𝑓, 𝑔〉 ∧ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎))) | 
| 56 |  | simp3ll 1244 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ 𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)) → 𝑏 ∈ ℕ) | 
| 57 | 56 | 3expb 1120 | . . . . . . . . . . . . . . . 16
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎))) → 𝑏 ∈ ℕ) | 
| 58 | 57 | 3ad2ant1 1133 | . . . . . . . . . . . . . . 15
⊢
((((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎))) ∧ (𝑒 = 〈𝑓, 𝑔〉 ∧ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)) ∧ (𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉)) → 𝑏 ∈
ℕ) | 
| 59 |  | simp3lr 1245 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ 𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)) → 𝑐 ∈ ℕ) | 
| 60 | 59 | 3expb 1120 | . . . . . . . . . . . . . . . 16
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎))) → 𝑐 ∈ ℕ) | 
| 61 | 60 | 3ad2ant1 1133 | . . . . . . . . . . . . . . 15
⊢
((((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎))) ∧ (𝑒 = 〈𝑓, 𝑔〉 ∧ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)) ∧ (𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉)) → 𝑐 ∈
ℕ) | 
| 62 |  | simp1lr 1237 | . . . . . . . . . . . . . . . 16
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑒 = 〈𝑓, 𝑔〉 ∧ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)) ∧ (𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉)) → 𝑎 ∈
ℤ) | 
| 63 | 62 | 3adant1r 1177 | . . . . . . . . . . . . . . 15
⊢
((((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎))) ∧ (𝑒 = 〈𝑓, 𝑔〉 ∧ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)) ∧ (𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉)) → 𝑎 ∈
ℤ) | 
| 64 |  | simp-4l 782 | . . . . . . . . . . . . . . . 16
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎))) → 𝐷 ∈ ℕ) | 
| 65 | 64 | 3ad2ant1 1133 | . . . . . . . . . . . . . . 15
⊢
((((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎))) ∧ (𝑒 = 〈𝑓, 𝑔〉 ∧ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)) ∧ (𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉)) → 𝐷 ∈
ℕ) | 
| 66 |  | simp-4r 783 | . . . . . . . . . . . . . . . 16
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎))) → ¬ (√‘𝐷) ∈
ℚ) | 
| 67 | 66 | 3ad2ant1 1133 | . . . . . . . . . . . . . . 15
⊢
((((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎))) ∧ (𝑒 = 〈𝑓, 𝑔〉 ∧ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)) ∧ (𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉)) → ¬
(√‘𝐷) ∈
ℚ) | 
| 68 |  | simp2ll 1240 | . . . . . . . . . . . . . . . 16
⊢
((((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎))) ∧ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎) ∧ (𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉)) → 𝑓 ∈
ℕ) | 
| 69 | 68 | 3adant2l 1178 | . . . . . . . . . . . . . . 15
⊢
((((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎))) ∧ (𝑒 = 〈𝑓, 𝑔〉 ∧ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)) ∧ (𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉)) → 𝑓 ∈
ℕ) | 
| 70 |  | simp2lr 1241 | . . . . . . . . . . . . . . . 16
⊢
((((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎))) ∧ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎) ∧ (𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉)) → 𝑔 ∈
ℕ) | 
| 71 | 70 | 3adant2l 1178 | . . . . . . . . . . . . . . 15
⊢
((((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎))) ∧ (𝑒 = 〈𝑓, 𝑔〉 ∧ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)) ∧ (𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉)) → 𝑔 ∈
ℕ) | 
| 72 |  | simp2l 1199 | . . . . . . . . . . . . . . . 16
⊢
((((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎))) ∧ (𝑒 = 〈𝑓, 𝑔〉 ∧ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)) ∧ (𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉)) → 𝑒 = 〈𝑓, 𝑔〉) | 
| 73 |  | simp1rl 1238 | . . . . . . . . . . . . . . . 16
⊢
((((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎))) ∧ (𝑒 = 〈𝑓, 𝑔〉 ∧ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)) ∧ (𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉)) → 𝑑 = 〈𝑏, 𝑐〉) | 
| 74 |  | simp3l 1201 | . . . . . . . . . . . . . . . 16
⊢
((((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎))) ∧ (𝑒 = 〈𝑓, 𝑔〉 ∧ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)) ∧ (𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉)) → 𝑑 ≠ 𝑒) | 
| 75 |  | simp3 1138 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑒 = 〈𝑓, 𝑔〉 ∧ 𝑑 = 〈𝑏, 𝑐〉 ∧ 𝑑 ≠ 𝑒) → 𝑑 ≠ 𝑒) | 
| 76 |  | simp2 1137 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑒 = 〈𝑓, 𝑔〉 ∧ 𝑑 = 〈𝑏, 𝑐〉 ∧ 𝑑 ≠ 𝑒) → 𝑑 = 〈𝑏, 𝑐〉) | 
| 77 |  | simp1 1136 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑒 = 〈𝑓, 𝑔〉 ∧ 𝑑 = 〈𝑏, 𝑐〉 ∧ 𝑑 ≠ 𝑒) → 𝑒 = 〈𝑓, 𝑔〉) | 
| 78 | 75, 76, 77 | 3netr3d 3016 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑒 = 〈𝑓, 𝑔〉 ∧ 𝑑 = 〈𝑏, 𝑐〉 ∧ 𝑑 ≠ 𝑒) → 〈𝑏, 𝑐〉 ≠ 〈𝑓, 𝑔〉) | 
| 79 |  | vex 3483 | . . . . . . . . . . . . . . . . . . 19
⊢ 𝑏 ∈ V | 
| 80 |  | vex 3483 | . . . . . . . . . . . . . . . . . . 19
⊢ 𝑐 ∈ V | 
| 81 | 79, 80 | opth 5480 | . . . . . . . . . . . . . . . . . 18
⊢
(〈𝑏, 𝑐〉 = 〈𝑓, 𝑔〉 ↔ (𝑏 = 𝑓 ∧ 𝑐 = 𝑔)) | 
| 82 | 81 | necon3abii 2986 | . . . . . . . . . . . . . . . . 17
⊢
(〈𝑏, 𝑐〉 ≠ 〈𝑓, 𝑔〉 ↔ ¬ (𝑏 = 𝑓 ∧ 𝑐 = 𝑔)) | 
| 83 | 78, 82 | sylib 218 | . . . . . . . . . . . . . . . 16
⊢ ((𝑒 = 〈𝑓, 𝑔〉 ∧ 𝑑 = 〈𝑏, 𝑐〉 ∧ 𝑑 ≠ 𝑒) → ¬ (𝑏 = 𝑓 ∧ 𝑐 = 𝑔)) | 
| 84 | 72, 73, 74, 83 | syl3anc 1372 | . . . . . . . . . . . . . . 15
⊢
((((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎))) ∧ (𝑒 = 〈𝑓, 𝑔〉 ∧ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)) ∧ (𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉)) → ¬ (𝑏 = 𝑓 ∧ 𝑐 = 𝑔)) | 
| 85 |  | simp1lr 1237 | . . . . . . . . . . . . . . 15
⊢
((((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎))) ∧ (𝑒 = 〈𝑓, 𝑔〉 ∧ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)) ∧ (𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉)) → 𝑎 ≠ 0) | 
| 86 |  | simp1rr 1239 | . . . . . . . . . . . . . . . 16
⊢ (((𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)) ∧ (𝑒 = 〈𝑓, 𝑔〉 ∧ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)) ∧ (𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉)) → ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎) | 
| 87 | 86 | 3adant1l 1176 | . . . . . . . . . . . . . . 15
⊢
((((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎))) ∧ (𝑒 = 〈𝑓, 𝑔〉 ∧ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)) ∧ (𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉)) → ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎) | 
| 88 |  | simp2rr 1243 | . . . . . . . . . . . . . . 15
⊢
((((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎))) ∧ (𝑒 = 〈𝑓, 𝑔〉 ∧ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)) ∧ (𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉)) → ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎) | 
| 89 |  | simp3r 1202 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎))) ∧ (𝑒 = 〈𝑓, 𝑔〉 ∧ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)) ∧ (𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉)) →
〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd ‘𝑑) mod (abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉) | 
| 90 |  | simp3 1138 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑑 = 〈𝑏, 𝑐〉 ∧ 𝑒 = 〈𝑓, 𝑔〉 ∧ 〈((1st
‘𝑑) mod
(abs‘𝑎)),
((2nd ‘𝑑)
mod (abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉) →
〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd ‘𝑑) mod (abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉) | 
| 91 |  | ovex 7465 | . . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑑) mod (abs‘𝑎)) ∈ V | 
| 92 |  | ovex 7465 | . . . . . . . . . . . . . . . . . . . 20
⊢
((2nd ‘𝑑) mod (abs‘𝑎)) ∈ V | 
| 93 | 91, 92 | opth 5480 | . . . . . . . . . . . . . . . . . . 19
⊢
(〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd ‘𝑑) mod (abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉 ↔
(((1st ‘𝑑)
mod (abs‘𝑎)) =
((1st ‘𝑒)
mod (abs‘𝑎)) ∧
((2nd ‘𝑑)
mod (abs‘𝑎)) =
((2nd ‘𝑒)
mod (abs‘𝑎)))) | 
| 94 | 90, 93 | sylib 218 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑑 = 〈𝑏, 𝑐〉 ∧ 𝑒 = 〈𝑓, 𝑔〉 ∧ 〈((1st
‘𝑑) mod
(abs‘𝑎)),
((2nd ‘𝑑)
mod (abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉) →
(((1st ‘𝑑)
mod (abs‘𝑎)) =
((1st ‘𝑒)
mod (abs‘𝑎)) ∧
((2nd ‘𝑑)
mod (abs‘𝑎)) =
((2nd ‘𝑒)
mod (abs‘𝑎)))) | 
| 95 |  | simprl 770 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑑 = 〈𝑏, 𝑐〉 ∧ 𝑒 = 〈𝑓, 𝑔〉) ∧ (((1st ‘𝑑) mod (abs‘𝑎)) = ((1st
‘𝑒) mod
(abs‘𝑎)) ∧
((2nd ‘𝑑)
mod (abs‘𝑎)) =
((2nd ‘𝑒)
mod (abs‘𝑎)))) →
((1st ‘𝑑)
mod (abs‘𝑎)) =
((1st ‘𝑒)
mod (abs‘𝑎))) | 
| 96 |  | simpll 766 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑑 = 〈𝑏, 𝑐〉 ∧ 𝑒 = 〈𝑓, 𝑔〉) ∧ (((1st ‘𝑑) mod (abs‘𝑎)) = ((1st
‘𝑒) mod
(abs‘𝑎)) ∧
((2nd ‘𝑑)
mod (abs‘𝑎)) =
((2nd ‘𝑒)
mod (abs‘𝑎)))) →
𝑑 = 〈𝑏, 𝑐〉) | 
| 97 | 96 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑑 = 〈𝑏, 𝑐〉 ∧ 𝑒 = 〈𝑓, 𝑔〉) ∧ (((1st ‘𝑑) mod (abs‘𝑎)) = ((1st
‘𝑒) mod
(abs‘𝑎)) ∧
((2nd ‘𝑑)
mod (abs‘𝑎)) =
((2nd ‘𝑒)
mod (abs‘𝑎)))) →
(1st ‘𝑑) =
(1st ‘〈𝑏, 𝑐〉)) | 
| 98 | 79, 80 | op1st 8023 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(1st ‘〈𝑏, 𝑐〉) = 𝑏 | 
| 99 | 97, 98 | eqtrdi 2792 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑑 = 〈𝑏, 𝑐〉 ∧ 𝑒 = 〈𝑓, 𝑔〉) ∧ (((1st ‘𝑑) mod (abs‘𝑎)) = ((1st
‘𝑒) mod
(abs‘𝑎)) ∧
((2nd ‘𝑑)
mod (abs‘𝑎)) =
((2nd ‘𝑒)
mod (abs‘𝑎)))) →
(1st ‘𝑑) =
𝑏) | 
| 100 | 99 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑑 = 〈𝑏, 𝑐〉 ∧ 𝑒 = 〈𝑓, 𝑔〉) ∧ (((1st ‘𝑑) mod (abs‘𝑎)) = ((1st
‘𝑒) mod
(abs‘𝑎)) ∧
((2nd ‘𝑑)
mod (abs‘𝑎)) =
((2nd ‘𝑒)
mod (abs‘𝑎)))) →
((1st ‘𝑑)
mod (abs‘𝑎)) = (𝑏 mod (abs‘𝑎))) | 
| 101 |  | simplr 768 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑑 = 〈𝑏, 𝑐〉 ∧ 𝑒 = 〈𝑓, 𝑔〉) ∧ (((1st ‘𝑑) mod (abs‘𝑎)) = ((1st
‘𝑒) mod
(abs‘𝑎)) ∧
((2nd ‘𝑑)
mod (abs‘𝑎)) =
((2nd ‘𝑒)
mod (abs‘𝑎)))) →
𝑒 = 〈𝑓, 𝑔〉) | 
| 102 | 101 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑑 = 〈𝑏, 𝑐〉 ∧ 𝑒 = 〈𝑓, 𝑔〉) ∧ (((1st ‘𝑑) mod (abs‘𝑎)) = ((1st
‘𝑒) mod
(abs‘𝑎)) ∧
((2nd ‘𝑑)
mod (abs‘𝑎)) =
((2nd ‘𝑒)
mod (abs‘𝑎)))) →
(1st ‘𝑒) =
(1st ‘〈𝑓, 𝑔〉)) | 
| 103 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑓 ∈ V | 
| 104 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑔 ∈ V | 
| 105 | 103, 104 | op1st 8023 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(1st ‘〈𝑓, 𝑔〉) = 𝑓 | 
| 106 | 102, 105 | eqtrdi 2792 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑑 = 〈𝑏, 𝑐〉 ∧ 𝑒 = 〈𝑓, 𝑔〉) ∧ (((1st ‘𝑑) mod (abs‘𝑎)) = ((1st
‘𝑒) mod
(abs‘𝑎)) ∧
((2nd ‘𝑑)
mod (abs‘𝑎)) =
((2nd ‘𝑒)
mod (abs‘𝑎)))) →
(1st ‘𝑒) =
𝑓) | 
| 107 | 106 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑑 = 〈𝑏, 𝑐〉 ∧ 𝑒 = 〈𝑓, 𝑔〉) ∧ (((1st ‘𝑑) mod (abs‘𝑎)) = ((1st
‘𝑒) mod
(abs‘𝑎)) ∧
((2nd ‘𝑑)
mod (abs‘𝑎)) =
((2nd ‘𝑒)
mod (abs‘𝑎)))) →
((1st ‘𝑒)
mod (abs‘𝑎)) = (𝑓 mod (abs‘𝑎))) | 
| 108 | 95, 100, 107 | 3eqtr3d 2784 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑑 = 〈𝑏, 𝑐〉 ∧ 𝑒 = 〈𝑓, 𝑔〉) ∧ (((1st ‘𝑑) mod (abs‘𝑎)) = ((1st
‘𝑒) mod
(abs‘𝑎)) ∧
((2nd ‘𝑑)
mod (abs‘𝑎)) =
((2nd ‘𝑒)
mod (abs‘𝑎)))) →
(𝑏 mod (abs‘𝑎)) = (𝑓 mod (abs‘𝑎))) | 
| 109 |  | simprr 772 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑑 = 〈𝑏, 𝑐〉 ∧ 𝑒 = 〈𝑓, 𝑔〉) ∧ (((1st ‘𝑑) mod (abs‘𝑎)) = ((1st
‘𝑒) mod
(abs‘𝑎)) ∧
((2nd ‘𝑑)
mod (abs‘𝑎)) =
((2nd ‘𝑒)
mod (abs‘𝑎)))) →
((2nd ‘𝑑)
mod (abs‘𝑎)) =
((2nd ‘𝑒)
mod (abs‘𝑎))) | 
| 110 | 96 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑑 = 〈𝑏, 𝑐〉 ∧ 𝑒 = 〈𝑓, 𝑔〉) ∧ (((1st ‘𝑑) mod (abs‘𝑎)) = ((1st
‘𝑒) mod
(abs‘𝑎)) ∧
((2nd ‘𝑑)
mod (abs‘𝑎)) =
((2nd ‘𝑒)
mod (abs‘𝑎)))) →
(2nd ‘𝑑) =
(2nd ‘〈𝑏, 𝑐〉)) | 
| 111 | 79, 80 | op2nd 8024 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(2nd ‘〈𝑏, 𝑐〉) = 𝑐 | 
| 112 | 110, 111 | eqtrdi 2792 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑑 = 〈𝑏, 𝑐〉 ∧ 𝑒 = 〈𝑓, 𝑔〉) ∧ (((1st ‘𝑑) mod (abs‘𝑎)) = ((1st
‘𝑒) mod
(abs‘𝑎)) ∧
((2nd ‘𝑑)
mod (abs‘𝑎)) =
((2nd ‘𝑒)
mod (abs‘𝑎)))) →
(2nd ‘𝑑) =
𝑐) | 
| 113 | 112 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑑 = 〈𝑏, 𝑐〉 ∧ 𝑒 = 〈𝑓, 𝑔〉) ∧ (((1st ‘𝑑) mod (abs‘𝑎)) = ((1st
‘𝑒) mod
(abs‘𝑎)) ∧
((2nd ‘𝑑)
mod (abs‘𝑎)) =
((2nd ‘𝑒)
mod (abs‘𝑎)))) →
((2nd ‘𝑑)
mod (abs‘𝑎)) = (𝑐 mod (abs‘𝑎))) | 
| 114 | 101 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑑 = 〈𝑏, 𝑐〉 ∧ 𝑒 = 〈𝑓, 𝑔〉) ∧ (((1st ‘𝑑) mod (abs‘𝑎)) = ((1st
‘𝑒) mod
(abs‘𝑎)) ∧
((2nd ‘𝑑)
mod (abs‘𝑎)) =
((2nd ‘𝑒)
mod (abs‘𝑎)))) →
(2nd ‘𝑒) =
(2nd ‘〈𝑓, 𝑔〉)) | 
| 115 | 103, 104 | op2nd 8024 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(2nd ‘〈𝑓, 𝑔〉) = 𝑔 | 
| 116 | 114, 115 | eqtrdi 2792 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑑 = 〈𝑏, 𝑐〉 ∧ 𝑒 = 〈𝑓, 𝑔〉) ∧ (((1st ‘𝑑) mod (abs‘𝑎)) = ((1st
‘𝑒) mod
(abs‘𝑎)) ∧
((2nd ‘𝑑)
mod (abs‘𝑎)) =
((2nd ‘𝑒)
mod (abs‘𝑎)))) →
(2nd ‘𝑒) =
𝑔) | 
| 117 | 116 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑑 = 〈𝑏, 𝑐〉 ∧ 𝑒 = 〈𝑓, 𝑔〉) ∧ (((1st ‘𝑑) mod (abs‘𝑎)) = ((1st
‘𝑒) mod
(abs‘𝑎)) ∧
((2nd ‘𝑑)
mod (abs‘𝑎)) =
((2nd ‘𝑒)
mod (abs‘𝑎)))) →
((2nd ‘𝑒)
mod (abs‘𝑎)) = (𝑔 mod (abs‘𝑎))) | 
| 118 | 109, 113,
117 | 3eqtr3d 2784 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑑 = 〈𝑏, 𝑐〉 ∧ 𝑒 = 〈𝑓, 𝑔〉) ∧ (((1st ‘𝑑) mod (abs‘𝑎)) = ((1st
‘𝑒) mod
(abs‘𝑎)) ∧
((2nd ‘𝑑)
mod (abs‘𝑎)) =
((2nd ‘𝑒)
mod (abs‘𝑎)))) →
(𝑐 mod (abs‘𝑎)) = (𝑔 mod (abs‘𝑎))) | 
| 119 | 108, 118 | jca 511 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑑 = 〈𝑏, 𝑐〉 ∧ 𝑒 = 〈𝑓, 𝑔〉) ∧ (((1st ‘𝑑) mod (abs‘𝑎)) = ((1st
‘𝑒) mod
(abs‘𝑎)) ∧
((2nd ‘𝑑)
mod (abs‘𝑎)) =
((2nd ‘𝑒)
mod (abs‘𝑎)))) →
((𝑏 mod (abs‘𝑎)) = (𝑓 mod (abs‘𝑎)) ∧ (𝑐 mod (abs‘𝑎)) = (𝑔 mod (abs‘𝑎)))) | 
| 120 | 119 | ex 412 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑑 = 〈𝑏, 𝑐〉 ∧ 𝑒 = 〈𝑓, 𝑔〉) → ((((1st
‘𝑑) mod
(abs‘𝑎)) =
((1st ‘𝑒)
mod (abs‘𝑎)) ∧
((2nd ‘𝑑)
mod (abs‘𝑎)) =
((2nd ‘𝑒)
mod (abs‘𝑎))) →
((𝑏 mod (abs‘𝑎)) = (𝑓 mod (abs‘𝑎)) ∧ (𝑐 mod (abs‘𝑎)) = (𝑔 mod (abs‘𝑎))))) | 
| 121 | 120 | 3adant3 1132 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑑 = 〈𝑏, 𝑐〉 ∧ 𝑒 = 〈𝑓, 𝑔〉 ∧ 〈((1st
‘𝑑) mod
(abs‘𝑎)),
((2nd ‘𝑑)
mod (abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉) →
((((1st ‘𝑑) mod (abs‘𝑎)) = ((1st ‘𝑒) mod (abs‘𝑎)) ∧ ((2nd
‘𝑑) mod
(abs‘𝑎)) =
((2nd ‘𝑒)
mod (abs‘𝑎))) →
((𝑏 mod (abs‘𝑎)) = (𝑓 mod (abs‘𝑎)) ∧ (𝑐 mod (abs‘𝑎)) = (𝑔 mod (abs‘𝑎))))) | 
| 122 | 94, 121 | mpd 15 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑑 = 〈𝑏, 𝑐〉 ∧ 𝑒 = 〈𝑓, 𝑔〉 ∧ 〈((1st
‘𝑑) mod
(abs‘𝑎)),
((2nd ‘𝑑)
mod (abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉) → ((𝑏 mod (abs‘𝑎)) = (𝑓 mod (abs‘𝑎)) ∧ (𝑐 mod (abs‘𝑎)) = (𝑔 mod (abs‘𝑎)))) | 
| 123 | 73, 72, 89, 122 | syl3anc 1372 | . . . . . . . . . . . . . . . 16
⊢
((((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎))) ∧ (𝑒 = 〈𝑓, 𝑔〉 ∧ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)) ∧ (𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉)) → ((𝑏 mod (abs‘𝑎)) = (𝑓 mod (abs‘𝑎)) ∧ (𝑐 mod (abs‘𝑎)) = (𝑔 mod (abs‘𝑎)))) | 
| 124 | 123 | simpld 494 | . . . . . . . . . . . . . . 15
⊢
((((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎))) ∧ (𝑒 = 〈𝑓, 𝑔〉 ∧ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)) ∧ (𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉)) → (𝑏 mod (abs‘𝑎)) = (𝑓 mod (abs‘𝑎))) | 
| 125 | 123 | simprd 495 | . . . . . . . . . . . . . . 15
⊢
((((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎))) ∧ (𝑒 = 〈𝑓, 𝑔〉 ∧ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)) ∧ (𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉)) → (𝑐 mod (abs‘𝑎)) = (𝑔 mod (abs‘𝑎))) | 
| 126 | 58, 61, 63, 65, 67, 69, 71, 84, 85, 87, 88, 124, 125 | pellexlem6 42850 | . . . . . . . . . . . . . 14
⊢
((((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎))) ∧ (𝑒 = 〈𝑓, 𝑔〉 ∧ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)) ∧ (𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉)) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ ((𝑥↑2) − (𝐷 · (𝑦↑2))) = 1) | 
| 127 | 126 | 3exp 1119 | . . . . . . . . . . . . 13
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎))) → ((𝑒 = 〈𝑓, 𝑔〉 ∧ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)) → ((𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ ((𝑥↑2) − (𝐷 · (𝑦↑2))) = 1))) | 
| 128 | 127 | exlimdvv 1933 | . . . . . . . . . . . 12
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎))) → (∃𝑓∃𝑔(𝑒 = 〈𝑓, 𝑔〉 ∧ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)) → ((𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ ((𝑥↑2) − (𝐷 · (𝑦↑2))) = 1))) | 
| 129 | 55, 128 | biimtrid 242 | . . . . . . . . . . 11
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ (𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎))) → (𝑒 ∈ {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)} → ((𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ ((𝑥↑2) − (𝐷 · (𝑦↑2))) = 1))) | 
| 130 | 129 | ex 412 | . . . . . . . . . 10
⊢ ((((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ 𝑎 ∈
ℤ) ∧ 𝑎 ≠ 0)
→ ((𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)) → (𝑒 ∈ {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)} → ((𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ ((𝑥↑2) − (𝐷 · (𝑦↑2))) = 1)))) | 
| 131 | 130 | exlimdvv 1933 | . . . . . . . . 9
⊢ ((((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ 𝑎 ∈
ℤ) ∧ 𝑎 ≠ 0)
→ (∃𝑏∃𝑐(𝑑 = 〈𝑏, 𝑐〉 ∧ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)) → (𝑒 ∈ {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)} → ((𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ ((𝑥↑2) − (𝐷 · (𝑦↑2))) = 1)))) | 
| 132 | 54, 131 | biimtrid 242 | . . . . . . . 8
⊢ ((((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ 𝑎 ∈
ℤ) ∧ 𝑎 ≠ 0)
→ (𝑑 ∈
{〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)} → (𝑒 ∈ {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)} → ((𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ ((𝑥↑2) − (𝐷 · (𝑦↑2))) = 1)))) | 
| 133 | 132 | impd 410 | . . . . . . 7
⊢ ((((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ 𝑎 ∈
ℤ) ∧ 𝑎 ≠ 0)
→ ((𝑑 ∈
{〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)} ∧ 𝑒 ∈ {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ) ∧ ((𝑓↑2) − (𝐷 · (𝑔↑2))) = 𝑎)}) → ((𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ ((𝑥↑2) − (𝐷 · (𝑦↑2))) = 1))) | 
| 134 | 53, 133 | sylan2i 606 | . . . . . 6
⊢ ((((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ 𝑎 ∈
ℤ) ∧ 𝑎 ≠ 0)
→ ((𝑑 ∈
{〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)} ∧ 𝑒 ∈ {〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)}) → ((𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ ((𝑥↑2) − (𝐷 · (𝑦↑2))) = 1))) | 
| 135 | 134 | rexlimdvv 3211 | . . . . 5
⊢ ((((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ 𝑎 ∈
ℤ) ∧ 𝑎 ≠ 0)
→ (∃𝑑 ∈
{〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)}∃𝑒 ∈ {〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)} (𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ ((𝑥↑2) − (𝐷 · (𝑦↑2))) = 1)) | 
| 136 | 135 | imp 406 | . . . 4
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ≠ 0) ∧ ∃𝑑 ∈ {〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)}∃𝑒 ∈ {〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)} (𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉)) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ ((𝑥↑2) − (𝐷 · (𝑦↑2))) = 1) | 
| 137 | 136 | adantlrr 721 | . . 3
⊢
(((((𝐷 ∈
ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ ℤ) ∧ (𝑎 ≠ 0 ∧ {〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)} ≈ ℕ)) ∧ ∃𝑑 ∈ {〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)}∃𝑒 ∈ {〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)} (𝑑 ≠ 𝑒 ∧ 〈((1st ‘𝑑) mod (abs‘𝑎)), ((2nd
‘𝑑) mod
(abs‘𝑎))〉 =
〈((1st ‘𝑒) mod (abs‘𝑎)), ((2nd ‘𝑒) mod (abs‘𝑎))〉)) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ ((𝑥↑2) − (𝐷 · (𝑦↑2))) = 1) | 
| 138 | 41, 137 | mpdan 687 | . 2
⊢ ((((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) ∧ 𝑎 ∈
ℤ) ∧ (𝑎 ≠ 0
∧ {〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)} ≈ ℕ)) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ ((𝑥↑2) − (𝐷 · (𝑦↑2))) = 1) | 
| 139 |  | pellexlem5 42849 | . 2
⊢ ((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) → ∃𝑎
∈ ℤ (𝑎 ≠ 0
∧ {〈𝑏, 𝑐〉 ∣ ((𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ) ∧ ((𝑏↑2) − (𝐷 · (𝑐↑2))) = 𝑎)} ≈ ℕ)) | 
| 140 | 138, 139 | r19.29a 3161 | 1
⊢ ((𝐷 ∈ ℕ ∧ ¬
(√‘𝐷) ∈
ℚ) → ∃𝑥
∈ ℕ ∃𝑦
∈ ℕ ((𝑥↑2)
− (𝐷 · (𝑦↑2))) = 1) |