Metamath Proof Explorer

Theorem rmxycomplete

Description: The X and Y sequences taken together enumerate all solutions to the corresponding Pell equation in the right half-plane. This is Metamath 100 proof #39. (Contributed by Stefan O'Rear, 22-Sep-2014)

Ref Expression
Assertion rmxycomplete ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) → ( ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑌 ↑ 2 ) ) ) = 1 ↔ ∃ 𝑛 ∈ ℤ ( 𝑋 = ( 𝐴 Xrm 𝑛 ) ∧ 𝑌 = ( 𝐴 Yrm 𝑛 ) ) ) )

Proof

Step Hyp Ref Expression
1 rmspecnonsq ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ( ℕ ∖ ◻NN ) )
2 1 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ( ℕ ∖ ◻NN ) )
3 pellfund14b ⊢ ( ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ( ℕ ∖ ◻NN ) → ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) ∈ ( Pell14QR ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↔ ∃ 𝑛 ∈ ℤ ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↑ 𝑛 ) ) )
4 2 3 syl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) → ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) ∈ ( Pell14QR ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↔ ∃ 𝑛 ∈ ℤ ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↑ 𝑛 ) ) )
5 nn0re ⊢ ( 𝑋 ∈ ℕ0 → 𝑋 ∈ ℝ )
6 5 3ad2ant2 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) → 𝑋 ∈ ℝ )
7 rmspecpos ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℝ+ )
8 7 rpsqrtcld ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ℝ+ )
9 8 rpred ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ℝ )
10 9 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) → ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ℝ )
11 zre ⊢ ( 𝑌 ∈ ℤ → 𝑌 ∈ ℝ )
12 11 3ad2ant3 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) → 𝑌 ∈ ℝ )
13 10 12 remulcld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) → ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ∈ ℝ )
14 6 13 readdcld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) → ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) ∈ ℝ )
15 14 biantrurd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) → ( ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℤ ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( 𝑥 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑦 ) ) ∧ ( ( 𝑥 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) = 1 ) ↔ ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) ∈ ℝ ∧ ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℤ ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( 𝑥 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑦 ) ) ∧ ( ( 𝑥 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) = 1 ) ) ) )
16 simpl2 ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑌 ↑ 2 ) ) ) = 1 ) → 𝑋 ∈ ℕ0 )
17 simpl3 ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑌 ↑ 2 ) ) ) = 1 ) → 𝑌 ∈ ℤ )
18 eqidd ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑌 ↑ 2 ) ) ) = 1 ) → ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) )
19 simpr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑌 ↑ 2 ) ) ) = 1 ) → ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑌 ↑ 2 ) ) ) = 1 )
20 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑦 ) ) = ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑦 ) ) )
21 20 eqeq2d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( 𝑥 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑦 ) ) ↔ ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑦 ) ) ) )
22 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ↑ 2 ) = ( 𝑋 ↑ 2 ) )
23 22 oveq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) = ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) )
24 23 eqeq1d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑥 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) = 1 ↔ ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) = 1 ) )
25 21 24 anbi12d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( 𝑥 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑦 ) ) ∧ ( ( 𝑥 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) = 1 ) ↔ ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑦 ) ) ∧ ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) = 1 ) ) )
26 oveq2 ⊢ ( 𝑦 = 𝑌 → ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑦 ) = ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) )
27 26 oveq2d ⊢ ( 𝑦 = 𝑌 → ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑦 ) ) = ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) )
28 27 eqeq2d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑦 ) ) ↔ ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) ) )
29 oveq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 ↑ 2 ) = ( 𝑌 ↑ 2 ) )
30 29 oveq2d ⊢ ( 𝑦 = 𝑌 → ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) = ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑌 ↑ 2 ) ) )
31 30 oveq2d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) = ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑌 ↑ 2 ) ) ) )
32 31 eqeq1d ⊢ ( 𝑦 = 𝑌 → ( ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) = 1 ↔ ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑌 ↑ 2 ) ) ) = 1 ) )
33 28 32 anbi12d ⊢ ( 𝑦 = 𝑌 → ( ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑦 ) ) ∧ ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) = 1 ) ↔ ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) ∧ ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑌 ↑ 2 ) ) ) = 1 ) ) )
34 25 33 rspc2ev ⊢ ( ( 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ∧ ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) ∧ ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑌 ↑ 2 ) ) ) = 1 ) ) → ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℤ ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( 𝑥 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑦 ) ) ∧ ( ( 𝑥 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) = 1 ) )
35 16 17 18 19 34 syl112anc ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑌 ↑ 2 ) ) ) = 1 ) → ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℤ ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( 𝑥 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑦 ) ) ∧ ( ( 𝑥 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) = 1 ) )
36 35 ex ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) → ( ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑌 ↑ 2 ) ) ) = 1 → ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℤ ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( 𝑥 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑦 ) ) ∧ ( ( 𝑥 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) = 1 ) ) )
37 rmspecsqrtnq ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ( ℂ ∖ ℚ ) )
38 37 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) → ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ( ℂ ∖ ℚ ) )
39 38 adantr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℤ ) ) → ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ( ℂ ∖ ℚ ) )
40 nn0ssq ⊢ ℕ0 ⊆ ℚ
41 simp2 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) → 𝑋 ∈ ℕ0 )
42 40 41 sseldi ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) → 𝑋 ∈ ℚ )
43 42 adantr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℤ ) ) → 𝑋 ∈ ℚ )
44 zq ⊢ ( 𝑌 ∈ ℤ → 𝑌 ∈ ℚ )
45 44 3ad2ant3 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) → 𝑌 ∈ ℚ )
46 45 adantr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℤ ) ) → 𝑌 ∈ ℚ )
47 40 sseli ⊢ ( 𝑥 ∈ ℕ0 → 𝑥 ∈ ℚ )
48 47 ad2antrl ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℤ ) ) → 𝑥 ∈ ℚ )
49 zq ⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℚ )
50 49 ad2antll ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℤ ) ) → 𝑦 ∈ ℚ )
51 qirropth ⊢ ( ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ( ℂ ∖ ℚ ) ∧ ( 𝑋 ∈ ℚ ∧ 𝑌 ∈ ℚ ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( 𝑥 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑦 ) ) ↔ ( 𝑋 = 𝑥 ∧ 𝑌 = 𝑦 ) ) )
52 39 43 46 48 50 51 syl122anc ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( 𝑥 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑦 ) ) ↔ ( 𝑋 = 𝑥 ∧ 𝑌 = 𝑦 ) ) )
53 52 biimpd ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( 𝑥 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑦 ) ) → ( 𝑋 = 𝑥 ∧ 𝑌 = 𝑦 ) ) )
54 53 anim1d ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℤ ) ) → ( ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( 𝑥 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑦 ) ) ∧ ( ( 𝑥 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) = 1 ) → ( ( 𝑋 = 𝑥 ∧ 𝑌 = 𝑦 ) ∧ ( ( 𝑥 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) = 1 ) ) )
55 oveq1 ⊢ ( 𝑋 = 𝑥 → ( 𝑋 ↑ 2 ) = ( 𝑥 ↑ 2 ) )
56 oveq1 ⊢ ( 𝑌 = 𝑦 → ( 𝑌 ↑ 2 ) = ( 𝑦 ↑ 2 ) )
57 56 oveq2d ⊢ ( 𝑌 = 𝑦 → ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑌 ↑ 2 ) ) = ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) )
58 55 57 oveqan12d ⊢ ( ( 𝑋 = 𝑥 ∧ 𝑌 = 𝑦 ) → ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑌 ↑ 2 ) ) ) = ( ( 𝑥 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) )
59 58 eqcomd ⊢ ( ( 𝑋 = 𝑥 ∧ 𝑌 = 𝑦 ) → ( ( 𝑥 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) = ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑌 ↑ 2 ) ) ) )
60 59 eqeq1d ⊢ ( ( 𝑋 = 𝑥 ∧ 𝑌 = 𝑦 ) → ( ( ( 𝑥 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) = 1 ↔ ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑌 ↑ 2 ) ) ) = 1 ) )
61 60 biimpa ⊢ ( ( ( 𝑋 = 𝑥 ∧ 𝑌 = 𝑦 ) ∧ ( ( 𝑥 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) = 1 ) → ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑌 ↑ 2 ) ) ) = 1 )
62 54 61 syl6 ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℤ ) ) → ( ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( 𝑥 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑦 ) ) ∧ ( ( 𝑥 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) = 1 ) → ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑌 ↑ 2 ) ) ) = 1 ) )
63 62 rexlimdvva ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) → ( ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℤ ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( 𝑥 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑦 ) ) ∧ ( ( 𝑥 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) = 1 ) → ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑌 ↑ 2 ) ) ) = 1 ) )
64 36 63 impbid ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) → ( ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑌 ↑ 2 ) ) ) = 1 ↔ ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℤ ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( 𝑥 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑦 ) ) ∧ ( ( 𝑥 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) = 1 ) ) )
65 elpell14qr ⊢ ( ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ( ℕ ∖ ◻NN ) → ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) ∈ ( Pell14QR ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↔ ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) ∈ ℝ ∧ ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℤ ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( 𝑥 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑦 ) ) ∧ ( ( 𝑥 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) = 1 ) ) ) )
66 2 65 syl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) → ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) ∈ ( Pell14QR ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↔ ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) ∈ ℝ ∧ ∃ 𝑥 ∈ ℕ0 ∃ 𝑦 ∈ ℤ ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( 𝑥 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑦 ) ) ∧ ( ( 𝑥 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) = 1 ) ) ) )
67 15 64 66 3bitr4d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) → ( ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑌 ↑ 2 ) ) ) = 1 ↔ ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) ∈ ( Pell14QR ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) )
68 38 adantr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ( ℂ ∖ ℚ ) )
69 42 adantr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → 𝑋 ∈ ℚ )
70 45 adantr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → 𝑌 ∈ ℚ )
71 frmx ⊢ Xrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℕ0
72 71 a1i ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → Xrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℕ0 )
73 simpl1 ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
74 simpr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → 𝑛 ∈ ℤ )
75 72 73 74 fovrnd ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → ( 𝐴 Xrm 𝑛 ) ∈ ℕ0 )
76 40 75 sseldi ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → ( 𝐴 Xrm 𝑛 ) ∈ ℚ )
77 zssq ⊢ ℤ ⊆ ℚ
78 frmy ⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
79 78 a1i ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ )
80 79 73 74 fovrnd ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → ( 𝐴 Yrm 𝑛 ) ∈ ℤ )
81 77 80 sseldi ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → ( 𝐴 Yrm 𝑛 ) ∈ ℚ )
82 qirropth ⊢ ( ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ( ℂ ∖ ℚ ) ∧ ( 𝑋 ∈ ℚ ∧ 𝑌 ∈ ℚ ) ∧ ( ( 𝐴 Xrm 𝑛 ) ∈ ℚ ∧ ( 𝐴 Yrm 𝑛 ) ∈ ℚ ) ) → ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( ( 𝐴 Xrm 𝑛 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑛 ) ) ) ↔ ( 𝑋 = ( 𝐴 Xrm 𝑛 ) ∧ 𝑌 = ( 𝐴 Yrm 𝑛 ) ) ) )
83 68 69 70 76 81 82 syl122anc ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( ( 𝐴 Xrm 𝑛 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑛 ) ) ) ↔ ( 𝑋 = ( 𝐴 Xrm 𝑛 ) ∧ 𝑌 = ( 𝐴 Yrm 𝑛 ) ) ) )
84 rmxyval ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑛 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑛 ) ) ) = ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 ) )
85 84 3ad2antl1 ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑛 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑛 ) ) ) = ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 ) )
86 rmspecfund ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) = ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) )
87 86 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) → ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) = ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) )
88 87 adantr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) = ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) )
89 88 oveq1d ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → ( ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↑ 𝑛 ) = ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 ) )
90 85 89 eqtr4d ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑛 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑛 ) ) ) = ( ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↑ 𝑛 ) )
91 90 eqeq2d ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → ( ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( ( 𝐴 Xrm 𝑛 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 𝑛 ) ) ) ↔ ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↑ 𝑛 ) ) )
92 83 91 bitr3d ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → ( ( 𝑋 = ( 𝐴 Xrm 𝑛 ) ∧ 𝑌 = ( 𝐴 Yrm 𝑛 ) ) ↔ ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↑ 𝑛 ) ) )
93 92 rexbidva ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) → ( ∃ 𝑛 ∈ ℤ ( 𝑋 = ( 𝐴 Xrm 𝑛 ) ∧ 𝑌 = ( 𝐴 Yrm 𝑛 ) ) ↔ ∃ 𝑛 ∈ ℤ ( 𝑋 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑌 ) ) = ( ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↑ 𝑛 ) ) )
94 4 67 93 3bitr4d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) → ( ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑌 ↑ 2 ) ) ) = 1 ↔ ∃ 𝑛 ∈ ℤ ( 𝑋 = ( 𝐴 Xrm 𝑛 ) ∧ 𝑌 = ( 𝐴 Yrm 𝑛 ) ) ) )