Metamath Proof Explorer

Theorem pellexlem3

Description: Lemma for pellex . To each good rational approximation of ( sqrtD ) , there exists a near-solution. (Contributed by Stefan O'Rear, 14-Sep-2014)

Ref Expression
Assertion pellexlem3 ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → { 𝑥 ∈ ℚ ∣ ( 0 < 𝑥 ∧ ( abs ‘ ( 𝑥 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑥 ) ↑ - 2 ) ) } ≼ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } )

Proof

Step Hyp Ref Expression
1 nnex ⊢ ℕ ∈ V
2 1 1 xpex ⊢ ( ℕ × ℕ ) ∈ V
3 opabssxp ⊢ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ⊆ ( ℕ × ℕ )
4 2 3 ssexi ⊢ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ∈ V
5 simprl ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑎 ∈ ℚ ∧ ( 0 < 𝑎 ∧ ( abs ‘ ( 𝑎 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) ) ) → 𝑎 ∈ ℚ )
6 simprrl ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑎 ∈ ℚ ∧ ( 0 < 𝑎 ∧ ( abs ‘ ( 𝑎 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) ) ) → 0 < 𝑎 )
7 qgt0numnn ⊢ ( ( 𝑎 ∈ ℚ ∧ 0 < 𝑎 ) → ( numer ‘ 𝑎 ) ∈ ℕ )
8 5 6 7 syl2anc ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑎 ∈ ℚ ∧ ( 0 < 𝑎 ∧ ( abs ‘ ( 𝑎 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) ) ) → ( numer ‘ 𝑎 ) ∈ ℕ )
9 qdencl ⊢ ( 𝑎 ∈ ℚ → ( denom ‘ 𝑎 ) ∈ ℕ )
10 5 9 syl ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑎 ∈ ℚ ∧ ( 0 < 𝑎 ∧ ( abs ‘ ( 𝑎 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) ) ) → ( denom ‘ 𝑎 ) ∈ ℕ )
11 8 10 jca ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑎 ∈ ℚ ∧ ( 0 < 𝑎 ∧ ( abs ‘ ( 𝑎 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) ) ) → ( ( numer ‘ 𝑎 ) ∈ ℕ ∧ ( denom ‘ 𝑎 ) ∈ ℕ ) )
12 simpll ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑎 ∈ ℚ ∧ ( 0 < 𝑎 ∧ ( abs ‘ ( 𝑎 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) ) ) → 𝐷 ∈ ℕ )
13 simplr ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑎 ∈ ℚ ∧ ( 0 < 𝑎 ∧ ( abs ‘ ( 𝑎 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) ) ) → ¬ ( √ ‘ 𝐷 ) ∈ ℚ )
14 pellexlem1 ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ( numer ‘ 𝑎 ) ∈ ℕ ∧ ( denom ‘ 𝑎 ) ∈ ℕ ) ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( denom ‘ 𝑎 ) ↑ 2 ) ) ) ≠ 0 )
15 12 8 10 13 14 syl31anc ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑎 ∈ ℚ ∧ ( 0 < 𝑎 ∧ ( abs ‘ ( 𝑎 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) ) ) → ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( denom ‘ 𝑎 ) ↑ 2 ) ) ) ≠ 0 )
16 simprrr ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑎 ∈ ℚ ∧ ( 0 < 𝑎 ∧ ( abs ‘ ( 𝑎 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) ) ) → ( abs ‘ ( 𝑎 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) )
17 qeqnumdivden ⊢ ( 𝑎 ∈ ℚ → 𝑎 = ( ( numer ‘ 𝑎 ) / ( denom ‘ 𝑎 ) ) )
18 17 oveq1d ⊢ ( 𝑎 ∈ ℚ → ( 𝑎 − ( √ ‘ 𝐷 ) ) = ( ( ( numer ‘ 𝑎 ) / ( denom ‘ 𝑎 ) ) − ( √ ‘ 𝐷 ) ) )
19 18 fveq2d ⊢ ( 𝑎 ∈ ℚ → ( abs ‘ ( 𝑎 − ( √ ‘ 𝐷 ) ) ) = ( abs ‘ ( ( ( numer ‘ 𝑎 ) / ( denom ‘ 𝑎 ) ) − ( √ ‘ 𝐷 ) ) ) )
20 19 breq1d ⊢ ( 𝑎 ∈ ℚ → ( ( abs ‘ ( 𝑎 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ↔ ( abs ‘ ( ( ( numer ‘ 𝑎 ) / ( denom ‘ 𝑎 ) ) − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) )
21 5 20 syl ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑎 ∈ ℚ ∧ ( 0 < 𝑎 ∧ ( abs ‘ ( 𝑎 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) ) ) → ( ( abs ‘ ( 𝑎 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ↔ ( abs ‘ ( ( ( numer ‘ 𝑎 ) / ( denom ‘ 𝑎 ) ) − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) )
22 16 21 mpbid ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑎 ∈ ℚ ∧ ( 0 < 𝑎 ∧ ( abs ‘ ( 𝑎 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) ) ) → ( abs ‘ ( ( ( numer ‘ 𝑎 ) / ( denom ‘ 𝑎 ) ) − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) )
23 pellexlem2 ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ( numer ‘ 𝑎 ) ∈ ℕ ∧ ( denom ‘ 𝑎 ) ∈ ℕ ) ∧ ( abs ‘ ( ( ( numer ‘ 𝑎 ) / ( denom ‘ 𝑎 ) ) − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) → ( abs ‘ ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( denom ‘ 𝑎 ) ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) )
24 12 8 10 22 23 syl31anc ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑎 ∈ ℚ ∧ ( 0 < 𝑎 ∧ ( abs ‘ ( 𝑎 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) ) ) → ( abs ‘ ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( denom ‘ 𝑎 ) ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) )
25 11 15 24 jca32 ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑎 ∈ ℚ ∧ ( 0 < 𝑎 ∧ ( abs ‘ ( 𝑎 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) ) ) → ( ( ( numer ‘ 𝑎 ) ∈ ℕ ∧ ( denom ‘ 𝑎 ) ∈ ℕ ) ∧ ( ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( denom ‘ 𝑎 ) ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( denom ‘ 𝑎 ) ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) )
26 25 ex ⊢ ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ( ( 𝑎 ∈ ℚ ∧ ( 0 < 𝑎 ∧ ( abs ‘ ( 𝑎 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) ) → ( ( ( numer ‘ 𝑎 ) ∈ ℕ ∧ ( denom ‘ 𝑎 ) ∈ ℕ ) ∧ ( ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( denom ‘ 𝑎 ) ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( denom ‘ 𝑎 ) ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ) )
27 breq2 ⊢ ( 𝑥 = 𝑎 → ( 0 < 𝑥 ↔ 0 < 𝑎 ) )
28 fvoveq1 ⊢ ( 𝑥 = 𝑎 → ( abs ‘ ( 𝑥 − ( √ ‘ 𝐷 ) ) ) = ( abs ‘ ( 𝑎 − ( √ ‘ 𝐷 ) ) ) )
29 fveq2 ⊢ ( 𝑥 = 𝑎 → ( denom ‘ 𝑥 ) = ( denom ‘ 𝑎 ) )
30 29 oveq1d ⊢ ( 𝑥 = 𝑎 → ( ( denom ‘ 𝑥 ) ↑ - 2 ) = ( ( denom ‘ 𝑎 ) ↑ - 2 ) )
31 28 30 breq12d ⊢ ( 𝑥 = 𝑎 → ( ( abs ‘ ( 𝑥 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑥 ) ↑ - 2 ) ↔ ( abs ‘ ( 𝑎 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) )
32 27 31 anbi12d ⊢ ( 𝑥 = 𝑎 → ( ( 0 < 𝑥 ∧ ( abs ‘ ( 𝑥 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑥 ) ↑ - 2 ) ) ↔ ( 0 < 𝑎 ∧ ( abs ‘ ( 𝑎 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) ) )
33 32 elrab ⊢ ( 𝑎 ∈ { 𝑥 ∈ ℚ ∣ ( 0 < 𝑥 ∧ ( abs ‘ ( 𝑥 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑥 ) ↑ - 2 ) ) } ↔ ( 𝑎 ∈ ℚ ∧ ( 0 < 𝑎 ∧ ( abs ‘ ( 𝑎 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) ) )
34 fvex ⊢ ( numer ‘ 𝑎 ) ∈ V
35 fvex ⊢ ( denom ‘ 𝑎 ) ∈ V
36 eleq1 ⊢ ( 𝑦 = ( numer ‘ 𝑎 ) → ( 𝑦 ∈ ℕ ↔ ( numer ‘ 𝑎 ) ∈ ℕ ) )
37 36 anbi1d ⊢ ( 𝑦 = ( numer ‘ 𝑎 ) → ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ↔ ( ( numer ‘ 𝑎 ) ∈ ℕ ∧ 𝑧 ∈ ℕ ) ) )
38 oveq1 ⊢ ( 𝑦 = ( numer ‘ 𝑎 ) → ( 𝑦 ↑ 2 ) = ( ( numer ‘ 𝑎 ) ↑ 2 ) )
39 38 oveq1d ⊢ ( 𝑦 = ( numer ‘ 𝑎 ) → ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) )
40 39 neeq1d ⊢ ( 𝑦 = ( numer ‘ 𝑎 ) → ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ↔ ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ) )
41 39 fveq2d ⊢ ( 𝑦 = ( numer ‘ 𝑎 ) → ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) = ( abs ‘ ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) )
42 41 breq1d ⊢ ( 𝑦 = ( numer ‘ 𝑎 ) → ( ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ↔ ( abs ‘ ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) )
43 40 42 anbi12d ⊢ ( 𝑦 = ( numer ‘ 𝑎 ) → ( ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ↔ ( ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) )
44 37 43 anbi12d ⊢ ( 𝑦 = ( numer ‘ 𝑎 ) → ( ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ↔ ( ( ( numer ‘ 𝑎 ) ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ) )
45 eleq1 ⊢ ( 𝑧 = ( denom ‘ 𝑎 ) → ( 𝑧 ∈ ℕ ↔ ( denom ‘ 𝑎 ) ∈ ℕ ) )
46 45 anbi2d ⊢ ( 𝑧 = ( denom ‘ 𝑎 ) → ( ( ( numer ‘ 𝑎 ) ∈ ℕ ∧ 𝑧 ∈ ℕ ) ↔ ( ( numer ‘ 𝑎 ) ∈ ℕ ∧ ( denom ‘ 𝑎 ) ∈ ℕ ) ) )
47 oveq1 ⊢ ( 𝑧 = ( denom ‘ 𝑎 ) → ( 𝑧 ↑ 2 ) = ( ( denom ‘ 𝑎 ) ↑ 2 ) )
48 47 oveq2d ⊢ ( 𝑧 = ( denom ‘ 𝑎 ) → ( 𝐷 · ( 𝑧 ↑ 2 ) ) = ( 𝐷 · ( ( denom ‘ 𝑎 ) ↑ 2 ) ) )
49 48 oveq2d ⊢ ( 𝑧 = ( denom ‘ 𝑎 ) → ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) = ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( denom ‘ 𝑎 ) ↑ 2 ) ) ) )
50 49 neeq1d ⊢ ( 𝑧 = ( denom ‘ 𝑎 ) → ( ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ↔ ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( denom ‘ 𝑎 ) ↑ 2 ) ) ) ≠ 0 ) )
51 49 fveq2d ⊢ ( 𝑧 = ( denom ‘ 𝑎 ) → ( abs ‘ ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) = ( abs ‘ ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( denom ‘ 𝑎 ) ↑ 2 ) ) ) ) )
52 51 breq1d ⊢ ( 𝑧 = ( denom ‘ 𝑎 ) → ( ( abs ‘ ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ↔ ( abs ‘ ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( denom ‘ 𝑎 ) ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) )
53 50 52 anbi12d ⊢ ( 𝑧 = ( denom ‘ 𝑎 ) → ( ( ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ↔ ( ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( denom ‘ 𝑎 ) ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( denom ‘ 𝑎 ) ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) )
54 46 53 anbi12d ⊢ ( 𝑧 = ( denom ‘ 𝑎 ) → ( ( ( ( numer ‘ 𝑎 ) ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ↔ ( ( ( numer ‘ 𝑎 ) ∈ ℕ ∧ ( denom ‘ 𝑎 ) ∈ ℕ ) ∧ ( ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( denom ‘ 𝑎 ) ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( denom ‘ 𝑎 ) ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) ) )
55 34 35 44 54 opelopab ⊢ ( ⟨ ( numer ‘ 𝑎 ) , ( denom ‘ 𝑎 ) ⟩ ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ↔ ( ( ( numer ‘ 𝑎 ) ∈ ℕ ∧ ( denom ‘ 𝑎 ) ∈ ℕ ) ∧ ( ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( denom ‘ 𝑎 ) ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( ( numer ‘ 𝑎 ) ↑ 2 ) − ( 𝐷 · ( ( denom ‘ 𝑎 ) ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) )
56 26 33 55 3imtr4g ⊢ ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ( 𝑎 ∈ { 𝑥 ∈ ℚ ∣ ( 0 < 𝑥 ∧ ( abs ‘ ( 𝑥 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑥 ) ↑ - 2 ) ) } → ⟨ ( numer ‘ 𝑎 ) , ( denom ‘ 𝑎 ) ⟩ ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ) )
57 ssrab2 ⊢ { 𝑥 ∈ ℚ ∣ ( 0 < 𝑥 ∧ ( abs ‘ ( 𝑥 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑥 ) ↑ - 2 ) ) } ⊆ ℚ
58 simprl ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑎 ∈ { 𝑥 ∈ ℚ ∣ ( 0 < 𝑥 ∧ ( abs ‘ ( 𝑥 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑥 ) ↑ - 2 ) ) } ∧ 𝑏 ∈ { 𝑥 ∈ ℚ ∣ ( 0 < 𝑥 ∧ ( abs ‘ ( 𝑥 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑥 ) ↑ - 2 ) ) } ) ) → 𝑎 ∈ { 𝑥 ∈ ℚ ∣ ( 0 < 𝑥 ∧ ( abs ‘ ( 𝑥 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑥 ) ↑ - 2 ) ) } )
59 57 58 sseldi ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑎 ∈ { 𝑥 ∈ ℚ ∣ ( 0 < 𝑥 ∧ ( abs ‘ ( 𝑥 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑥 ) ↑ - 2 ) ) } ∧ 𝑏 ∈ { 𝑥 ∈ ℚ ∣ ( 0 < 𝑥 ∧ ( abs ‘ ( 𝑥 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑥 ) ↑ - 2 ) ) } ) ) → 𝑎 ∈ ℚ )
60 simprr ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑎 ∈ { 𝑥 ∈ ℚ ∣ ( 0 < 𝑥 ∧ ( abs ‘ ( 𝑥 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑥 ) ↑ - 2 ) ) } ∧ 𝑏 ∈ { 𝑥 ∈ ℚ ∣ ( 0 < 𝑥 ∧ ( abs ‘ ( 𝑥 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑥 ) ↑ - 2 ) ) } ) ) → 𝑏 ∈ { 𝑥 ∈ ℚ ∣ ( 0 < 𝑥 ∧ ( abs ‘ ( 𝑥 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑥 ) ↑ - 2 ) ) } )
61 57 60 sseldi ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑎 ∈ { 𝑥 ∈ ℚ ∣ ( 0 < 𝑥 ∧ ( abs ‘ ( 𝑥 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑥 ) ↑ - 2 ) ) } ∧ 𝑏 ∈ { 𝑥 ∈ ℚ ∣ ( 0 < 𝑥 ∧ ( abs ‘ ( 𝑥 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑥 ) ↑ - 2 ) ) } ) ) → 𝑏 ∈ ℚ )
62 34 35 opth ⊢ ( ⟨ ( numer ‘ 𝑎 ) , ( denom ‘ 𝑎 ) ⟩ = ⟨ ( numer ‘ 𝑏 ) , ( denom ‘ 𝑏 ) ⟩ ↔ ( ( numer ‘ 𝑎 ) = ( numer ‘ 𝑏 ) ∧ ( denom ‘ 𝑎 ) = ( denom ‘ 𝑏 ) ) )
63 simprl ⊢ ( ( ( 𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ ) ∧ ( ( numer ‘ 𝑎 ) = ( numer ‘ 𝑏 ) ∧ ( denom ‘ 𝑎 ) = ( denom ‘ 𝑏 ) ) ) → ( numer ‘ 𝑎 ) = ( numer ‘ 𝑏 ) )
64 simprr ⊢ ( ( ( 𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ ) ∧ ( ( numer ‘ 𝑎 ) = ( numer ‘ 𝑏 ) ∧ ( denom ‘ 𝑎 ) = ( denom ‘ 𝑏 ) ) ) → ( denom ‘ 𝑎 ) = ( denom ‘ 𝑏 ) )
65 63 64 oveq12d ⊢ ( ( ( 𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ ) ∧ ( ( numer ‘ 𝑎 ) = ( numer ‘ 𝑏 ) ∧ ( denom ‘ 𝑎 ) = ( denom ‘ 𝑏 ) ) ) → ( ( numer ‘ 𝑎 ) / ( denom ‘ 𝑎 ) ) = ( ( numer ‘ 𝑏 ) / ( denom ‘ 𝑏 ) ) )
66 simpll ⊢ ( ( ( 𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ ) ∧ ( ( numer ‘ 𝑎 ) = ( numer ‘ 𝑏 ) ∧ ( denom ‘ 𝑎 ) = ( denom ‘ 𝑏 ) ) ) → 𝑎 ∈ ℚ )
67 66 17 syl ⊢ ( ( ( 𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ ) ∧ ( ( numer ‘ 𝑎 ) = ( numer ‘ 𝑏 ) ∧ ( denom ‘ 𝑎 ) = ( denom ‘ 𝑏 ) ) ) → 𝑎 = ( ( numer ‘ 𝑎 ) / ( denom ‘ 𝑎 ) ) )
68 simplr ⊢ ( ( ( 𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ ) ∧ ( ( numer ‘ 𝑎 ) = ( numer ‘ 𝑏 ) ∧ ( denom ‘ 𝑎 ) = ( denom ‘ 𝑏 ) ) ) → 𝑏 ∈ ℚ )
69 qeqnumdivden ⊢ ( 𝑏 ∈ ℚ → 𝑏 = ( ( numer ‘ 𝑏 ) / ( denom ‘ 𝑏 ) ) )
70 68 69 syl ⊢ ( ( ( 𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ ) ∧ ( ( numer ‘ 𝑎 ) = ( numer ‘ 𝑏 ) ∧ ( denom ‘ 𝑎 ) = ( denom ‘ 𝑏 ) ) ) → 𝑏 = ( ( numer ‘ 𝑏 ) / ( denom ‘ 𝑏 ) ) )
71 65 67 70 3eqtr4d ⊢ ( ( ( 𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ ) ∧ ( ( numer ‘ 𝑎 ) = ( numer ‘ 𝑏 ) ∧ ( denom ‘ 𝑎 ) = ( denom ‘ 𝑏 ) ) ) → 𝑎 = 𝑏 )
72 71 ex ⊢ ( ( 𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ ) → ( ( ( numer ‘ 𝑎 ) = ( numer ‘ 𝑏 ) ∧ ( denom ‘ 𝑎 ) = ( denom ‘ 𝑏 ) ) → 𝑎 = 𝑏 ) )
73 62 72 syl5bi ⊢ ( ( 𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ ) → ( ⟨ ( numer ‘ 𝑎 ) , ( denom ‘ 𝑎 ) ⟩ = ⟨ ( numer ‘ 𝑏 ) , ( denom ‘ 𝑏 ) ⟩ → 𝑎 = 𝑏 ) )
74 fveq2 ⊢ ( 𝑎 = 𝑏 → ( numer ‘ 𝑎 ) = ( numer ‘ 𝑏 ) )
75 fveq2 ⊢ ( 𝑎 = 𝑏 → ( denom ‘ 𝑎 ) = ( denom ‘ 𝑏 ) )
76 74 75 opeq12d ⊢ ( 𝑎 = 𝑏 → ⟨ ( numer ‘ 𝑎 ) , ( denom ‘ 𝑎 ) ⟩ = ⟨ ( numer ‘ 𝑏 ) , ( denom ‘ 𝑏 ) ⟩ )
77 73 76 impbid1 ⊢ ( ( 𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ ) → ( ⟨ ( numer ‘ 𝑎 ) , ( denom ‘ 𝑎 ) ⟩ = ⟨ ( numer ‘ 𝑏 ) , ( denom ‘ 𝑏 ) ⟩ ↔ 𝑎 = 𝑏 ) )
78 59 61 77 syl2anc ⊢ ( ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) ∧ ( 𝑎 ∈ { 𝑥 ∈ ℚ ∣ ( 0 < 𝑥 ∧ ( abs ‘ ( 𝑥 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑥 ) ↑ - 2 ) ) } ∧ 𝑏 ∈ { 𝑥 ∈ ℚ ∣ ( 0 < 𝑥 ∧ ( abs ‘ ( 𝑥 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑥 ) ↑ - 2 ) ) } ) ) → ( ⟨ ( numer ‘ 𝑎 ) , ( denom ‘ 𝑎 ) ⟩ = ⟨ ( numer ‘ 𝑏 ) , ( denom ‘ 𝑏 ) ⟩ ↔ 𝑎 = 𝑏 ) )
79 78 ex ⊢ ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ( ( 𝑎 ∈ { 𝑥 ∈ ℚ ∣ ( 0 < 𝑥 ∧ ( abs ‘ ( 𝑥 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑥 ) ↑ - 2 ) ) } ∧ 𝑏 ∈ { 𝑥 ∈ ℚ ∣ ( 0 < 𝑥 ∧ ( abs ‘ ( 𝑥 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑥 ) ↑ - 2 ) ) } ) → ( ⟨ ( numer ‘ 𝑎 ) , ( denom ‘ 𝑎 ) ⟩ = ⟨ ( numer ‘ 𝑏 ) , ( denom ‘ 𝑏 ) ⟩ ↔ 𝑎 = 𝑏 ) ) )
80 56 79 dom2d ⊢ ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ( { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ∈ V → { 𝑥 ∈ ℚ ∣ ( 0 < 𝑥 ∧ ( abs ‘ ( 𝑥 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑥 ) ↑ - 2 ) ) } ≼ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ) )
81 4 80 mpi ⊢ ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → { 𝑥 ∈ ℚ ∣ ( 0 < 𝑥 ∧ ( abs ‘ ( 𝑥 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑥 ) ↑ - 2 ) ) } ≼ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } )