Metamath Proof Explorer

Theorem pellex

Description: Every Pell equation has a nontrivial solution. Theorem 62 in vandenDries p. 43. (Contributed by Stefan O'Rear, 19-Oct-2014)

Ref Expression
Assertion pellex ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ ( ( 𝑥 ↑ 2 ) − ( 𝐷 · ( 𝑦 ↑ 2 ) ) ) = 1 )

Proof

Step Hyp Ref Expression
1 fzfi ⊢ ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) ∈ Fin
2 xpfi ⊢ ( ( ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) ∈ Fin ∧ ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) ∈ Fin ) → ( ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) × ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) ) ∈ Fin )
3 1 1 2 mp2an ⊢ ( ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) × ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) ) ∈ Fin
4 isfinite ⊢ ( ( ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) × ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) ) ∈ Fin ↔ ( ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) × ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) ) ≺ ω )
5 3 4 mpbi ⊢ ( ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) × ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) ) ≺ ω
6 nnenom ⊢ ℕ ≈ ω
7 6 ensymi ⊢ ω ≈ ℕ
8 sdomentr ⊢ ( ( ( ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) × ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) ) ≺ ω ∧ ω ≈ ℕ ) → ( ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) × ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) ) ≺ ℕ )
9 5 7 8 mp2an ⊢ ( ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) × ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) ) ≺ ℕ
10 ensym ⊢ ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } ≈ ℕ → ℕ ≈ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } )
11 10 ad2antll ⊢ ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑎 ≠ 0 ∧ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } ≈ ℕ ) ) → ℕ ≈ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } )
12 sdomentr ⊢ ( ( ( ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) × ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) ) ≺ ℕ ∧ ℕ ≈ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } ) → ( ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) × ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) ) ≺ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } )
13 9 11 12 sylancr ⊢ ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑎 ≠ 0 ∧ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } ≈ ℕ ) ) → ( ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) × ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) ) ≺ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } )
14 opabssxp ⊢ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } ⊆ ( ℕ × ℕ )
15 14 sseli ⊢ ( 𝑑 ∈ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } → 𝑑 ∈ ( ℕ × ℕ ) )
16 simprrl ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑑 ) ∈ ℕ ∧ ( 2nd ‘ 𝑑 ) ∈ ℕ ) ) ) → ( 1st ‘ 𝑑 ) ∈ ℕ )
17 16 nnzd ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑑 ) ∈ ℕ ∧ ( 2nd ‘ 𝑑 ) ∈ ℕ ) ) ) → ( 1st ‘ 𝑑 ) ∈ ℤ )
18 simpllr ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑑 ) ∈ ℕ ∧ ( 2nd ‘ 𝑑 ) ∈ ℕ ) ) ) → 𝑎 ∈ ℤ )
19 simplr ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑑 ) ∈ ℕ ∧ ( 2nd ‘ 𝑑 ) ∈ ℕ ) ) ) → 𝑎 ≠ 0 )
20 nnabscl ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑎 ≠ 0 ) → ( abs ‘ 𝑎 ) ∈ ℕ )
21 18 19 20 syl2anc ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑑 ) ∈ ℕ ∧ ( 2nd ‘ 𝑑 ) ∈ ℕ ) ) ) → ( abs ‘ 𝑎 ) ∈ ℕ )
22 zmodfz ⊢ ( ( ( 1st ‘ 𝑑 ) ∈ ℤ ∧ ( abs ‘ 𝑎 ) ∈ ℕ ) → ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ∈ ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) )
23 17 21 22 syl2anc ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑑 ) ∈ ℕ ∧ ( 2nd ‘ 𝑑 ) ∈ ℕ ) ) ) → ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ∈ ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) )
24 simprrr ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑑 ) ∈ ℕ ∧ ( 2nd ‘ 𝑑 ) ∈ ℕ ) ) ) → ( 2nd ‘ 𝑑 ) ∈ ℕ )
25 24 nnzd ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑑 ) ∈ ℕ ∧ ( 2nd ‘ 𝑑 ) ∈ ℕ ) ) ) → ( 2nd ‘ 𝑑 ) ∈ ℤ )
26 zmodfz ⊢ ( ( ( 2nd ‘ 𝑑 ) ∈ ℤ ∧ ( abs ‘ 𝑎 ) ∈ ℕ ) → ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ∈ ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) )
27 25 21 26 syl2anc ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑑 ) ∈ ℕ ∧ ( 2nd ‘ 𝑑 ) ∈ ℕ ) ) ) → ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ∈ ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) )
28 23 27 jca ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑑 ) ∈ ℕ ∧ ( 2nd ‘ 𝑑 ) ∈ ℕ ) ) ) → ( ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ∈ ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) ∧ ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ∈ ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) ) )
29 28 ex ⊢ ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) → ( ( 𝑑 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑑 ) ∈ ℕ ∧ ( 2nd ‘ 𝑑 ) ∈ ℕ ) ) → ( ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ∈ ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) ∧ ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ∈ ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) ) ) )
30 elxp7 ⊢ ( 𝑑 ∈ ( ℕ × ℕ ) ↔ ( 𝑑 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑑 ) ∈ ℕ ∧ ( 2nd ‘ 𝑑 ) ∈ ℕ ) ) )
31 opelxp ⊢ ( ⟨ ( ( 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 ⊢ ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) → ( 𝑑 ∈ ( ℕ × ℕ ) → ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ ∈ ( ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) × ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) ) ) )
33 15 32 syl5 ⊢ ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) → ( 𝑑 ∈ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } → ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ ∈ ( ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) × ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) ) ) )
34 33 imp ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ 𝑑 ∈ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } ) → ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ ∈ ( ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) × ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) ) )
35 34 adantlrr ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑎 ≠ 0 ∧ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } ≈ ℕ ) ) ∧ 𝑑 ∈ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } ) → ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ ∈ ( ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) × ( 0 ... ( ( abs ‘ 𝑎 ) − 1 ) ) ) )
36 fveq2 ⊢ ( 𝑑 = 𝑒 → ( 1st ‘ 𝑑 ) = ( 1st ‘ 𝑒 ) )
37 36 oveq1d ⊢ ( 𝑑 = 𝑒 → ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) )
38 fveq2 ⊢ ( 𝑑 = 𝑒 → ( 2nd ‘ 𝑑 ) = ( 2nd ‘ 𝑒 ) )
39 38 oveq1d ⊢ ( 𝑑 = 𝑒 → ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) )
40 37 39 opeq12d ⊢ ( 𝑑 = 𝑒 → ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ )
41 13 35 40 fphpd ⊢ ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑎 ≠ 0 ∧ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } ≈ ℕ ) ) → ∃ 𝑑 ∈ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } ∃ 𝑒 ∈ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) )
42 eleq1w ⊢ ( 𝑏 = 𝑓 → ( 𝑏 ∈ ℕ ↔ 𝑓 ∈ ℕ ) )
43 eleq1w ⊢ ( 𝑐 = 𝑔 → ( 𝑐 ∈ ℕ ↔ 𝑔 ∈ ℕ ) )
44 42 43 bi2anan9 ⊢ ( ( 𝑏 = 𝑓 ∧ 𝑐 = 𝑔 ) → ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ↔ ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ) )
45 oveq1 ⊢ ( 𝑏 = 𝑓 → ( 𝑏 ↑ 2 ) = ( 𝑓 ↑ 2 ) )
46 oveq1 ⊢ ( 𝑐 = 𝑔 → ( 𝑐 ↑ 2 ) = ( 𝑔 ↑ 2 ) )
47 46 oveq2d ⊢ ( 𝑐 = 𝑔 → ( 𝐷 · ( 𝑐 ↑ 2 ) ) = ( 𝐷 · ( 𝑔 ↑ 2 ) ) )
48 45 47 oveqan12d ⊢ ( ( 𝑏 = 𝑓 ∧ 𝑐 = 𝑔 ) → ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) )
49 48 eqeq1d ⊢ ( ( 𝑏 = 𝑓 ∧ 𝑐 = 𝑔 ) → ( ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ↔ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) )
50 44 49 anbi12d ⊢ ( ( 𝑏 = 𝑓 ∧ 𝑐 = 𝑔 ) → ( ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ↔ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) ) )
51 50 cbvopabv ⊢ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) }
52 51 eleq2i ⊢ ( 𝑒 ∈ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } ↔ 𝑒 ∈ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) } )
53 52 biimpi ⊢ ( 𝑒 ∈ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } → 𝑒 ∈ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) } )
54 elopab ⊢ ( 𝑑 ∈ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } ↔ ∃ 𝑏 ∃ 𝑐 ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) )
55 elopab ⊢ ( 𝑒 ∈ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) } ↔ ∃ 𝑓 ∃ 𝑔 ( 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) ) )
56 simp3ll ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) → 𝑏 ∈ ℕ )
57 56 3expb ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) ) → 𝑏 ∈ ℕ )
58 57 3ad2ant1 ⊢ ( ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) ) ∧ ( 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) ) ∧ ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) ) → 𝑏 ∈ ℕ )
59 simp3lr ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) → 𝑐 ∈ ℕ )
60 59 3expb ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) ) → 𝑐 ∈ ℕ )
61 60 3ad2ant1 ⊢ ( ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) ) ∧ ( 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) ) ∧ ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) ) → 𝑐 ∈ ℕ )
62 simp1lr ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) ) ∧ ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) ) → 𝑎 ∈ ℤ )
63 62 3adant1r ⊢ ( ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) ) ∧ ( 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) ) ∧ ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) ) → 𝑎 ∈ ℤ )
64 simp-4l ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) ) → 𝐷 ∈ ℕ )
65 64 3ad2ant1 ⊢ ( ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) ) ∧ ( 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) ) ∧ ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) ) → 𝐷 ∈ ℕ )
66 simp-4r ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) ) → ¬ ( √ ‘ 𝐷 ) ∈ ℚ )
67 66 3ad2ant1 ⊢ ( ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) ) ∧ ( 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) ) ∧ ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) ) → ¬ ( √ ‘ 𝐷 ) ∈ ℚ )
68 simp2ll ⊢ ( ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) ) ∧ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) ∧ ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) ) → 𝑓 ∈ ℕ )
69 68 3adant2l ⊢ ( ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) ) ∧ ( 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) ) ∧ ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) ) → 𝑓 ∈ ℕ )
70 simp2lr ⊢ ( ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) ) ∧ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) ∧ ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) ) → 𝑔 ∈ ℕ )
71 70 3adant2l ⊢ ( ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) ) ∧ ( 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) ) ∧ ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) ) → 𝑔 ∈ ℕ )
72 simp2l ⊢ ( ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) ) ∧ ( 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) ) ∧ ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) ) → 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ )
73 simp1rl ⊢ ( ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) ) ∧ ( 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) ) ∧ ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) ) → 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ )
74 simp3l ⊢ ( ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) ) ∧ ( 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) ) ∧ ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) ) → 𝑑 ≠ 𝑒 )
75 simp3 ⊢ ( ( 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑑 ≠ 𝑒 ) → 𝑑 ≠ 𝑒 )
76 simp2 ⊢ ( ( 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑑 ≠ 𝑒 ) → 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ )
77 simp1 ⊢ ( ( 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑑 ≠ 𝑒 ) → 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ )
78 75 76 77 3netr3d ⊢ ( ( 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑑 ≠ 𝑒 ) → ⟨ 𝑏 , 𝑐 ⟩ ≠ ⟨ 𝑓 , 𝑔 ⟩ )
79 vex ⊢ 𝑏 ∈ V
80 vex ⊢ 𝑐 ∈ V
81 79 80 opth ⊢ ( ⟨ 𝑏 , 𝑐 ⟩ = ⟨ 𝑓 , 𝑔 ⟩ ↔ ( 𝑏 = 𝑓 ∧ 𝑐 = 𝑔 ) )
82 81 necon3abii ⊢ ( ⟨ 𝑏 , 𝑐 ⟩ ≠ ⟨ 𝑓 , 𝑔 ⟩ ↔ ¬ ( 𝑏 = 𝑓 ∧ 𝑐 = 𝑔 ) )
83 78 82 sylib ⊢ ( ( 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑑 ≠ 𝑒 ) → ¬ ( 𝑏 = 𝑓 ∧ 𝑐 = 𝑔 ) )
84 72 73 74 83 syl3anc ⊢ ( ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) ) ∧ ( 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) ) ∧ ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) ) → ¬ ( 𝑏 = 𝑓 ∧ 𝑐 = 𝑔 ) )
85 simp1lr ⊢ ( ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) ) ∧ ( 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) ) ∧ ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) ) → 𝑎 ≠ 0 )
86 simp1rr ⊢ ( ( ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) ∧ ( 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) ) ∧ ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) ) → ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 )
87 86 3adant1l ⊢ ( ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) ) ∧ ( 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) ) ∧ ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) ) → ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 )
88 simp2rr ⊢ ( ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) ) ∧ ( 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) ) ∧ ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) ) → ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 )
89 simp3r ⊢ ( ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 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 ⊢ ( ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ⟨ ( ( 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 ⊢ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ∈ V
92 ovex ⊢ ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ∈ V
93 91 92 opth ⊢ ( ⟨ ( ( 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 ⊢ ( ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ⟨ ( ( 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 ⊢ ( ( ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ∧ ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ) ) → ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) )
96 simpll ⊢ ( ( ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ∧ ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ) ) → 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ )
97 96 fveq2d ⊢ ( ( ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ∧ ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ) ) → ( 1st ‘ 𝑑 ) = ( 1st ‘ ⟨ 𝑏 , 𝑐 ⟩ ) )
98 79 80 op1st ⊢ ( 1st ‘ ⟨ 𝑏 , 𝑐 ⟩ ) = 𝑏
99 97 98 eqtrdi ⊢ ( ( ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ∧ ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ) ) → ( 1st ‘ 𝑑 ) = 𝑏 )
100 99 oveq1d ⊢ ( ( ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ∧ ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ) ) → ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( 𝑏 mod ( abs ‘ 𝑎 ) ) )
101 simplr ⊢ ( ( ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ∧ ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ) ) → 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ )
102 101 fveq2d ⊢ ( ( ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ∧ ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ) ) → ( 1st ‘ 𝑒 ) = ( 1st ‘ ⟨ 𝑓 , 𝑔 ⟩ ) )
103 vex ⊢ 𝑓 ∈ V
104 vex ⊢ 𝑔 ∈ V
105 103 104 op1st ⊢ ( 1st ‘ ⟨ 𝑓 , 𝑔 ⟩ ) = 𝑓
106 102 105 eqtrdi ⊢ ( ( ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ∧ ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ) ) → ( 1st ‘ 𝑒 ) = 𝑓 )
107 106 oveq1d ⊢ ( ( ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ∧ ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ) ) → ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) = ( 𝑓 mod ( abs ‘ 𝑎 ) ) )
108 95 100 107 3eqtr3d ⊢ ( ( ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ∧ ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ) ) → ( 𝑏 mod ( abs ‘ 𝑎 ) ) = ( 𝑓 mod ( abs ‘ 𝑎 ) ) )
109 simprr ⊢ ( ( ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ∧ ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ) ) → ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) )
110 96 fveq2d ⊢ ( ( ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ∧ ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ) ) → ( 2nd ‘ 𝑑 ) = ( 2nd ‘ ⟨ 𝑏 , 𝑐 ⟩ ) )
111 79 80 op2nd ⊢ ( 2nd ‘ ⟨ 𝑏 , 𝑐 ⟩ ) = 𝑐
112 110 111 eqtrdi ⊢ ( ( ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ∧ ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ) ) → ( 2nd ‘ 𝑑 ) = 𝑐 )
113 112 oveq1d ⊢ ( ( ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ∧ ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ) ) → ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( 𝑐 mod ( abs ‘ 𝑎 ) ) )
114 101 fveq2d ⊢ ( ( ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ∧ ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ) ) → ( 2nd ‘ 𝑒 ) = ( 2nd ‘ ⟨ 𝑓 , 𝑔 ⟩ ) )
115 103 104 op2nd ⊢ ( 2nd ‘ ⟨ 𝑓 , 𝑔 ⟩ ) = 𝑔
116 114 115 eqtrdi ⊢ ( ( ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ∧ ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ) ) → ( 2nd ‘ 𝑒 ) = 𝑔 )
117 116 oveq1d ⊢ ( ( ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ∧ ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ) ) → ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) = ( 𝑔 mod ( abs ‘ 𝑎 ) ) )
118 109 113 117 3eqtr3d ⊢ ( ( ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ∧ ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ) ) → ( 𝑐 mod ( abs ‘ 𝑎 ) ) = ( 𝑔 mod ( abs ‘ 𝑎 ) ) )
119 108 118 jca ⊢ ( ( ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ) ∧ ( ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ∧ ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ) ) → ( ( 𝑏 mod ( abs ‘ 𝑎 ) ) = ( 𝑓 mod ( abs ‘ 𝑎 ) ) ∧ ( 𝑐 mod ( abs ‘ 𝑎 ) ) = ( 𝑔 mod ( abs ‘ 𝑎 ) ) ) )
120 119 ex ⊢ ( ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ) → ( ( ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ∧ ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) = ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ) → ( ( 𝑏 mod ( abs ‘ 𝑎 ) ) = ( 𝑓 mod ( abs ‘ 𝑎 ) ) ∧ ( 𝑐 mod ( abs ‘ 𝑎 ) ) = ( 𝑔 mod ( abs ‘ 𝑎 ) ) ) ) )
121 120 3adant3 ⊢ ( ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ⟨ ( ( 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 ⊢ ( ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ⟨ ( ( 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 ⊢ ( ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 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 ⊢ ( ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) ) ∧ ( 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) ) ∧ ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) ) → ( 𝑏 mod ( abs ‘ 𝑎 ) ) = ( 𝑓 mod ( abs ‘ 𝑎 ) ) )
125 123 simprd ⊢ ( ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 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 ⊢ ( ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) ) ∧ ( 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) ) ∧ ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ ( ( 𝑥 ↑ 2 ) − ( 𝐷 · ( 𝑦 ↑ 2 ) ) ) = 1 )
127 126 3exp ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) ) → ( ( 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) ) → ( ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ ( ( 𝑥 ↑ 2 ) − ( 𝐷 · ( 𝑦 ↑ 2 ) ) ) = 1 ) ) )
128 127 exlimdvv ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) ) → ( ∃ 𝑓 ∃ 𝑔 ( 𝑒 = ⟨ 𝑓 , 𝑔 ⟩ ∧ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) ) → ( ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ ( ( 𝑥 ↑ 2 ) − ( 𝐷 · ( 𝑦 ↑ 2 ) ) ) = 1 ) ) )
129 55 128 biimtrid ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) ) → ( 𝑒 ∈ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) } → ( ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ ( ( 𝑥 ↑ 2 ) − ( 𝐷 · ( 𝑦 ↑ 2 ) ) ) = 1 ) ) )
130 129 ex ⊢ ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) → ( ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) → ( 𝑒 ∈ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) } → ( ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ ( ( 𝑥 ↑ 2 ) − ( 𝐷 · ( 𝑦 ↑ 2 ) ) ) = 1 ) ) ) )
131 130 exlimdvv ⊢ ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) → ( ∃ 𝑏 ∃ 𝑐 ( 𝑑 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) ) → ( 𝑒 ∈ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) } → ( ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ ( ( 𝑥 ↑ 2 ) − ( 𝐷 · ( 𝑦 ↑ 2 ) ) ) = 1 ) ) ) )
132 54 131 biimtrid ⊢ ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) → ( 𝑑 ∈ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } → ( 𝑒 ∈ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) } → ( ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ ( ( 𝑥 ↑ 2 ) − ( 𝐷 · ( 𝑦 ↑ 2 ) ) ) = 1 ) ) ) )
133 132 impd ⊢ ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) → ( ( 𝑑 ∈ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } ∧ 𝑒 ∈ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ℕ ∧ 𝑔 ∈ ℕ ) ∧ ( ( 𝑓 ↑ 2 ) − ( 𝐷 · ( 𝑔 ↑ 2 ) ) ) = 𝑎 ) } ) → ( ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ ( ( 𝑥 ↑ 2 ) − ( 𝐷 · ( 𝑦 ↑ 2 ) ) ) = 1 ) ) )
134 53 133 sylan2i ⊢ ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) → ( ( 𝑑 ∈ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } ∧ 𝑒 ∈ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } ) → ( ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ ( ( 𝑥 ↑ 2 ) − ( 𝐷 · ( 𝑦 ↑ 2 ) ) ) = 1 ) ) )
135 134 rexlimdvv ⊢ ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) → ( ∃ 𝑑 ∈ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } ∃ 𝑒 ∈ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ ( ( 𝑥 ↑ 2 ) − ( 𝐷 · ( 𝑦 ↑ 2 ) ) ) = 1 ) )
136 135 imp ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ≠ 0 ) ∧ ∃ 𝑑 ∈ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } ∃ 𝑒 ∈ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } ( 𝑑 ≠ 𝑒 ∧ ⟨ ( ( 1st ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑑 ) mod ( abs ‘ 𝑎 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) , ( ( 2nd ‘ 𝑒 ) mod ( abs ‘ 𝑎 ) ) ⟩ ) ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ ( ( 𝑥 ↑ 2 ) − ( 𝐷 · ( 𝑦 ↑ 2 ) ) ) = 1 )
137 136 adantlrr ⊢ ( ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑎 ≠ 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 ⊢ ( ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑎 ≠ 0 ∧ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } ≈ ℕ ) ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ ( ( 𝑥 ↑ 2 ) − ( 𝐷 · ( 𝑦 ↑ 2 ) ) ) = 1 )
139 pellexlem5 ⊢ ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ∃ 𝑎 ∈ ℤ ( 𝑎 ≠ 0 ∧ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ( ( 𝑏 ∈ ℕ ∧ 𝑐 ∈ ℕ ) ∧ ( ( 𝑏 ↑ 2 ) − ( 𝐷 · ( 𝑐 ↑ 2 ) ) ) = 𝑎 ) } ≈ ℕ ) )
140 138 139 r19.29a ⊢ ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ ( ( 𝑥 ↑ 2 ) − ( 𝐷 · ( 𝑦 ↑ 2 ) ) ) = 1 )