| Step | Hyp | Ref
| Expression |
| 1 | | rmspecnonsq 42918 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴↑2) − 1) ∈ (ℕ ∖
◻NN)) |
| 2 | 1 | 3ad2ant1 1134 |
. . 3
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) → ((𝐴↑2) − 1) ∈
(ℕ ∖ ◻NN)) |
| 3 | | pellfund14b 42910 |
. . 3
⊢ (((𝐴↑2) − 1) ∈
(ℕ ∖ ◻NN) → ((𝑋 + ((√‘((𝐴↑2) − 1)) · 𝑌)) ∈
(Pell14QR‘((𝐴↑2)
− 1)) ↔ ∃𝑛
∈ ℤ (𝑋 +
((√‘((𝐴↑2)
− 1)) · 𝑌)) =
((PellFund‘((𝐴↑2) − 1))↑𝑛))) |
| 4 | 2, 3 | syl 17 |
. 2
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) → ((𝑋 + ((√‘((𝐴↑2) − 1)) ·
𝑌)) ∈
(Pell14QR‘((𝐴↑2)
− 1)) ↔ ∃𝑛
∈ ℤ (𝑋 +
((√‘((𝐴↑2)
− 1)) · 𝑌)) =
((PellFund‘((𝐴↑2) − 1))↑𝑛))) |
| 5 | | nn0re 12535 |
. . . . . 6
⊢ (𝑋 ∈ ℕ0
→ 𝑋 ∈
ℝ) |
| 6 | 5 | 3ad2ant2 1135 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) → 𝑋 ∈
ℝ) |
| 7 | | rmspecpos 42928 |
. . . . . . . . 9
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴↑2) − 1) ∈
ℝ+) |
| 8 | 7 | rpsqrtcld 15450 |
. . . . . . . 8
⊢ (𝐴 ∈
(ℤ≥‘2) → (√‘((𝐴↑2) − 1)) ∈
ℝ+) |
| 9 | 8 | rpred 13077 |
. . . . . . 7
⊢ (𝐴 ∈
(ℤ≥‘2) → (√‘((𝐴↑2) − 1)) ∈
ℝ) |
| 10 | 9 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) →
(√‘((𝐴↑2)
− 1)) ∈ ℝ) |
| 11 | | zre 12617 |
. . . . . . 7
⊢ (𝑌 ∈ ℤ → 𝑌 ∈
ℝ) |
| 12 | 11 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) → 𝑌 ∈
ℝ) |
| 13 | 10, 12 | remulcld 11291 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) →
((√‘((𝐴↑2)
− 1)) · 𝑌)
∈ ℝ) |
| 14 | 6, 13 | readdcld 11290 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) → (𝑋 + ((√‘((𝐴↑2) − 1)) ·
𝑌)) ∈
ℝ) |
| 15 | 14 | biantrurd 532 |
. . 3
⊢ ((𝐴 ∈
(ℤ≥‘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 1193 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ ((𝑋↑2) − (((𝐴↑2) − 1) ·
(𝑌↑2))) = 1) →
𝑋 ∈
ℕ0) |
| 17 | | simpl3 1194 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ ((𝑋↑2) − (((𝐴↑2) − 1) ·
(𝑌↑2))) = 1) →
𝑌 ∈
ℤ) |
| 18 | | eqidd 2738 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ ((𝑋↑2) − (((𝐴↑2) − 1) ·
(𝑌↑2))) = 1) →
(𝑋 +
((√‘((𝐴↑2)
− 1)) · 𝑌)) =
(𝑋 +
((√‘((𝐴↑2)
− 1)) · 𝑌))) |
| 19 | | simpr 484 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ ((𝑋↑2) − (((𝐴↑2) − 1) ·
(𝑌↑2))) = 1) →
((𝑋↑2) −
(((𝐴↑2) − 1)
· (𝑌↑2))) =
1) |
| 20 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝑥 + ((√‘((𝐴↑2) − 1)) · 𝑦)) = (𝑋 + ((√‘((𝐴↑2) − 1)) · 𝑦))) |
| 21 | 20 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → ((𝑋 + ((√‘((𝐴↑2) − 1)) · 𝑌)) = (𝑥 + ((√‘((𝐴↑2) − 1)) · 𝑦)) ↔ (𝑋 + ((√‘((𝐴↑2) − 1)) · 𝑌)) = (𝑋 + ((√‘((𝐴↑2) − 1)) · 𝑦)))) |
| 22 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → (𝑥↑2) = (𝑋↑2)) |
| 23 | 22 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → ((𝑥↑2) − (((𝐴↑2) − 1) · (𝑦↑2))) = ((𝑋↑2) − (((𝐴↑2) − 1) · (𝑦↑2)))) |
| 24 | 23 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (((𝑥↑2) − (((𝐴↑2) − 1) · (𝑦↑2))) = 1 ↔ ((𝑋↑2) − (((𝐴↑2) − 1) ·
(𝑦↑2))) =
1)) |
| 25 | 21, 24 | anbi12d 632 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (((𝑋 + ((√‘((𝐴↑2) − 1)) · 𝑌)) = (𝑥 + ((√‘((𝐴↑2) − 1)) · 𝑦)) ∧ ((𝑥↑2) − (((𝐴↑2) − 1) · (𝑦↑2))) = 1) ↔ ((𝑋 + ((√‘((𝐴↑2) − 1)) ·
𝑌)) = (𝑋 + ((√‘((𝐴↑2) − 1)) · 𝑦)) ∧ ((𝑋↑2) − (((𝐴↑2) − 1) · (𝑦↑2))) =
1))) |
| 26 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑌 → ((√‘((𝐴↑2) − 1)) · 𝑦) = ((√‘((𝐴↑2) − 1)) ·
𝑌)) |
| 27 | 26 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑦 = 𝑌 → (𝑋 + ((√‘((𝐴↑2) − 1)) · 𝑦)) = (𝑋 + ((√‘((𝐴↑2) − 1)) · 𝑌))) |
| 28 | 27 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑦 = 𝑌 → ((𝑋 + ((√‘((𝐴↑2) − 1)) · 𝑌)) = (𝑋 + ((√‘((𝐴↑2) − 1)) · 𝑦)) ↔ (𝑋 + ((√‘((𝐴↑2) − 1)) · 𝑌)) = (𝑋 + ((√‘((𝐴↑2) − 1)) · 𝑌)))) |
| 29 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑌 → (𝑦↑2) = (𝑌↑2)) |
| 30 | 29 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑌 → (((𝐴↑2) − 1) · (𝑦↑2)) = (((𝐴↑2) − 1) · (𝑌↑2))) |
| 31 | 30 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑦 = 𝑌 → ((𝑋↑2) − (((𝐴↑2) − 1) · (𝑦↑2))) = ((𝑋↑2) − (((𝐴↑2) − 1) · (𝑌↑2)))) |
| 32 | 31 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑦 = 𝑌 → (((𝑋↑2) − (((𝐴↑2) − 1) · (𝑦↑2))) = 1 ↔ ((𝑋↑2) − (((𝐴↑2) − 1) ·
(𝑌↑2))) =
1)) |
| 33 | 28, 32 | anbi12d 632 |
. . . . . . 7
⊢ (𝑦 = 𝑌 → (((𝑋 + ((√‘((𝐴↑2) − 1)) · 𝑌)) = (𝑋 + ((√‘((𝐴↑2) − 1)) · 𝑦)) ∧ ((𝑋↑2) − (((𝐴↑2) − 1) · (𝑦↑2))) = 1) ↔ ((𝑋 + ((√‘((𝐴↑2) − 1)) ·
𝑌)) = (𝑋 + ((√‘((𝐴↑2) − 1)) · 𝑌)) ∧ ((𝑋↑2) − (((𝐴↑2) − 1) · (𝑌↑2))) =
1))) |
| 34 | 25, 33 | rspc2ev 3635 |
. . . . . 6
⊢ ((𝑋 ∈ ℕ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 1376 |
. . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ ((𝑋↑2) − (((𝐴↑2) − 1) ·
(𝑌↑2))) = 1) →
∃𝑥 ∈
ℕ0 ∃𝑦 ∈ ℤ ((𝑋 + ((√‘((𝐴↑2) − 1)) · 𝑌)) = (𝑥 + ((√‘((𝐴↑2) − 1)) · 𝑦)) ∧ ((𝑥↑2) − (((𝐴↑2) − 1) · (𝑦↑2))) =
1)) |
| 36 | 35 | ex 412 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) → (((𝑋↑2) − (((𝐴↑2) − 1) ·
(𝑌↑2))) = 1 →
∃𝑥 ∈
ℕ0 ∃𝑦 ∈ ℤ ((𝑋 + ((√‘((𝐴↑2) − 1)) · 𝑌)) = (𝑥 + ((√‘((𝐴↑2) − 1)) · 𝑦)) ∧ ((𝑥↑2) − (((𝐴↑2) − 1) · (𝑦↑2))) =
1))) |
| 37 | | rmspecsqrtnq 42917 |
. . . . . . . . . . 11
⊢ (𝐴 ∈
(ℤ≥‘2) → (√‘((𝐴↑2) − 1)) ∈ (ℂ ∖
ℚ)) |
| 38 | 37 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) →
(√‘((𝐴↑2)
− 1)) ∈ (ℂ ∖ ℚ)) |
| 39 | 38 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ 𝑦 ∈ ℤ))
→ (√‘((𝐴↑2) − 1)) ∈ (ℂ ∖
ℚ)) |
| 40 | | nn0ssq 12999 |
. . . . . . . . . . 11
⊢
ℕ0 ⊆ ℚ |
| 41 | | simp2 1138 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) → 𝑋 ∈
ℕ0) |
| 42 | 40, 41 | sselid 3981 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) → 𝑋 ∈
ℚ) |
| 43 | 42 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ 𝑦 ∈ ℤ))
→ 𝑋 ∈
ℚ) |
| 44 | | zq 12996 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ ℤ → 𝑌 ∈
ℚ) |
| 45 | 44 | 3ad2ant3 1136 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) → 𝑌 ∈
ℚ) |
| 46 | 45 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ 𝑦 ∈ ℤ))
→ 𝑌 ∈
ℚ) |
| 47 | 40 | sseli 3979 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℕ0
→ 𝑥 ∈
ℚ) |
| 48 | 47 | ad2antrl 728 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ 𝑦 ∈ ℤ))
→ 𝑥 ∈
ℚ) |
| 49 | | zq 12996 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℚ) |
| 50 | 49 | ad2antll 729 |
. . . . . . . . 9
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ 𝑦 ∈ ℤ))
→ 𝑦 ∈
ℚ) |
| 51 | | qirropth 42919 |
. . . . . . . . 9
⊢
(((√‘((𝐴↑2) − 1)) ∈ (ℂ ∖
ℚ) ∧ (𝑋 ∈
ℚ ∧ 𝑌 ∈
ℚ) ∧ (𝑥 ∈
ℚ ∧ 𝑦 ∈
ℚ)) → ((𝑋 +
((√‘((𝐴↑2)
− 1)) · 𝑌)) =
(𝑥 +
((√‘((𝐴↑2)
− 1)) · 𝑦))
↔ (𝑋 = 𝑥 ∧ 𝑌 = 𝑦))) |
| 52 | 39, 43, 46, 48, 50, 51 | syl122anc 1381 |
. . . . . . . 8
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ 𝑦 ∈ ℤ))
→ ((𝑋 +
((√‘((𝐴↑2)
− 1)) · 𝑌)) =
(𝑥 +
((√‘((𝐴↑2)
− 1)) · 𝑦))
↔ (𝑋 = 𝑥 ∧ 𝑌 = 𝑦))) |
| 53 | 52 | biimpd 229 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ 𝑦 ∈ ℤ))
→ ((𝑋 +
((√‘((𝐴↑2)
− 1)) · 𝑌)) =
(𝑥 +
((√‘((𝐴↑2)
− 1)) · 𝑦))
→ (𝑋 = 𝑥 ∧ 𝑌 = 𝑦))) |
| 54 | 53 | anim1d 611 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ 𝑦 ∈ ℤ))
→ (((𝑋 +
((√‘((𝐴↑2)
− 1)) · 𝑌)) =
(𝑥 +
((√‘((𝐴↑2)
− 1)) · 𝑦))
∧ ((𝑥↑2) −
(((𝐴↑2) − 1)
· (𝑦↑2))) = 1)
→ ((𝑋 = 𝑥 ∧ 𝑌 = 𝑦) ∧ ((𝑥↑2) − (((𝐴↑2) − 1) · (𝑦↑2))) =
1))) |
| 55 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑋 = 𝑥 → (𝑋↑2) = (𝑥↑2)) |
| 56 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝑌 = 𝑦 → (𝑌↑2) = (𝑦↑2)) |
| 57 | 56 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑌 = 𝑦 → (((𝐴↑2) − 1) · (𝑌↑2)) = (((𝐴↑2) − 1) · (𝑦↑2))) |
| 58 | 55, 57 | oveqan12d 7450 |
. . . . . . . . 9
⊢ ((𝑋 = 𝑥 ∧ 𝑌 = 𝑦) → ((𝑋↑2) − (((𝐴↑2) − 1) · (𝑌↑2))) = ((𝑥↑2) − (((𝐴↑2) − 1) ·
(𝑦↑2)))) |
| 59 | 58 | eqcomd 2743 |
. . . . . . . 8
⊢ ((𝑋 = 𝑥 ∧ 𝑌 = 𝑦) → ((𝑥↑2) − (((𝐴↑2) − 1) · (𝑦↑2))) = ((𝑋↑2) − (((𝐴↑2) − 1) · (𝑌↑2)))) |
| 60 | 59 | eqeq1d 2739 |
. . . . . . 7
⊢ ((𝑋 = 𝑥 ∧ 𝑌 = 𝑦) → (((𝑥↑2) − (((𝐴↑2) − 1) · (𝑦↑2))) = 1 ↔ ((𝑋↑2) − (((𝐴↑2) − 1) ·
(𝑌↑2))) =
1)) |
| 61 | 60 | biimpa 476 |
. . . . . 6
⊢ (((𝑋 = 𝑥 ∧ 𝑌 = 𝑦) ∧ ((𝑥↑2) − (((𝐴↑2) − 1) · (𝑦↑2))) = 1) → ((𝑋↑2) − (((𝐴↑2) − 1) ·
(𝑌↑2))) =
1) |
| 62 | 54, 61 | syl6 35 |
. . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ (𝑥 ∈ ℕ0
∧ 𝑦 ∈ ℤ))
→ (((𝑋 +
((√‘((𝐴↑2)
− 1)) · 𝑌)) =
(𝑥 +
((√‘((𝐴↑2)
− 1)) · 𝑦))
∧ ((𝑥↑2) −
(((𝐴↑2) − 1)
· (𝑦↑2))) = 1)
→ ((𝑋↑2) −
(((𝐴↑2) − 1)
· (𝑌↑2))) =
1)) |
| 63 | 62 | rexlimdvva 3213 |
. . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) →
(∃𝑥 ∈
ℕ0 ∃𝑦 ∈ ℤ ((𝑋 + ((√‘((𝐴↑2) − 1)) · 𝑌)) = (𝑥 + ((√‘((𝐴↑2) − 1)) · 𝑦)) ∧ ((𝑥↑2) − (((𝐴↑2) − 1) · (𝑦↑2))) = 1) → ((𝑋↑2) − (((𝐴↑2) − 1) ·
(𝑌↑2))) =
1)) |
| 64 | 36, 63 | impbid 212 |
. . 3
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) → (((𝑋↑2) − (((𝐴↑2) − 1) ·
(𝑌↑2))) = 1 ↔
∃𝑥 ∈
ℕ0 ∃𝑦 ∈ ℤ ((𝑋 + ((√‘((𝐴↑2) − 1)) · 𝑌)) = (𝑥 + ((√‘((𝐴↑2) − 1)) · 𝑦)) ∧ ((𝑥↑2) − (((𝐴↑2) − 1) · (𝑦↑2))) =
1))) |
| 65 | | elpell14qr 42860 |
. . . 4
⊢ (((𝐴↑2) − 1) ∈
(ℕ ∖ ◻NN) → ((𝑋 + ((√‘((𝐴↑2) − 1)) · 𝑌)) ∈
(Pell14QR‘((𝐴↑2)
− 1)) ↔ ((𝑋 +
((√‘((𝐴↑2)
− 1)) · 𝑌))
∈ ℝ ∧ ∃𝑥 ∈ ℕ0 ∃𝑦 ∈ ℤ ((𝑋 + ((√‘((𝐴↑2) − 1)) ·
𝑌)) = (𝑥 + ((√‘((𝐴↑2) − 1)) · 𝑦)) ∧ ((𝑥↑2) − (((𝐴↑2) − 1) · (𝑦↑2))) =
1)))) |
| 66 | 2, 65 | syl 17 |
. . 3
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) → ((𝑋 + ((√‘((𝐴↑2) − 1)) ·
𝑌)) ∈
(Pell14QR‘((𝐴↑2)
− 1)) ↔ ((𝑋 +
((√‘((𝐴↑2)
− 1)) · 𝑌))
∈ ℝ ∧ ∃𝑥 ∈ ℕ0 ∃𝑦 ∈ ℤ ((𝑋 + ((√‘((𝐴↑2) − 1)) ·
𝑌)) = (𝑥 + ((√‘((𝐴↑2) − 1)) · 𝑦)) ∧ ((𝑥↑2) − (((𝐴↑2) − 1) · (𝑦↑2))) =
1)))) |
| 67 | 15, 64, 66 | 3bitr4d 311 |
. 2
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) → (((𝑋↑2) − (((𝐴↑2) − 1) ·
(𝑌↑2))) = 1 ↔
(𝑋 +
((√‘((𝐴↑2)
− 1)) · 𝑌))
∈ (Pell14QR‘((𝐴↑2) − 1)))) |
| 68 | 38 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ 𝑛 ∈ ℤ) →
(√‘((𝐴↑2)
− 1)) ∈ (ℂ ∖ ℚ)) |
| 69 | 42 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → 𝑋 ∈
ℚ) |
| 70 | 45 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → 𝑌 ∈
ℚ) |
| 71 | | frmx 42925 |
. . . . . . . 8
⊢
Xrm :((ℤ≥‘2) ×
ℤ)⟶ℕ0 |
| 72 | 71 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ 𝑛 ∈ ℤ) →
Xrm :((ℤ≥‘2) ×
ℤ)⟶ℕ0) |
| 73 | | simpl1 1192 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → 𝐴 ∈
(ℤ≥‘2)) |
| 74 | | simpr 484 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → 𝑛 ∈
ℤ) |
| 75 | 72, 73, 74 | fovcdmd 7605 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → (𝐴 Xrm 𝑛) ∈
ℕ0) |
| 76 | 40, 75 | sselid 3981 |
. . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → (𝐴 Xrm 𝑛) ∈
ℚ) |
| 77 | | zssq 12998 |
. . . . . 6
⊢ ℤ
⊆ ℚ |
| 78 | | frmy 42926 |
. . . . . . . 8
⊢
Yrm :((ℤ≥‘2) ×
ℤ)⟶ℤ |
| 79 | 78 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ 𝑛 ∈ ℤ) →
Yrm :((ℤ≥‘2) ×
ℤ)⟶ℤ) |
| 80 | 79, 73, 74 | fovcdmd 7605 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → (𝐴 Yrm 𝑛) ∈
ℤ) |
| 81 | 77, 80 | sselid 3981 |
. . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → (𝐴 Yrm 𝑛) ∈
ℚ) |
| 82 | | qirropth 42919 |
. . . . 5
⊢
(((√‘((𝐴↑2) − 1)) ∈ (ℂ ∖
ℚ) ∧ (𝑋 ∈
ℚ ∧ 𝑌 ∈
ℚ) ∧ ((𝐴
Xrm 𝑛) ∈
ℚ ∧ (𝐴
Yrm 𝑛) ∈
ℚ)) → ((𝑋 +
((√‘((𝐴↑2)
− 1)) · 𝑌)) =
((𝐴 Xrm 𝑛) + ((√‘((𝐴↑2) − 1)) ·
(𝐴 Yrm 𝑛))) ↔ (𝑋 = (𝐴 Xrm 𝑛) ∧ 𝑌 = (𝐴 Yrm 𝑛)))) |
| 83 | 68, 69, 70, 76, 81, 82 | syl122anc 1381 |
. . . 4
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → ((𝑋 + ((√‘((𝐴↑2) − 1)) ·
𝑌)) = ((𝐴 Xrm 𝑛) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑛))) ↔ (𝑋 = (𝐴 Xrm 𝑛) ∧ 𝑌 = (𝐴 Yrm 𝑛)))) |
| 84 | | rmxyval 42927 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑛 ∈ ℤ) → ((𝐴 Xrm 𝑛) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑛))) = ((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑛)) |
| 85 | 84 | 3ad2antl1 1186 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → ((𝐴 Xrm 𝑛) + ((√‘((𝐴↑2) − 1)) ·
(𝐴 Yrm 𝑛))) = ((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑛)) |
| 86 | | rmspecfund 42920 |
. . . . . . . . 9
⊢ (𝐴 ∈
(ℤ≥‘2) → (PellFund‘((𝐴↑2) − 1)) = (𝐴 + (√‘((𝐴↑2) − 1)))) |
| 87 | 86 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) →
(PellFund‘((𝐴↑2)
− 1)) = (𝐴 +
(√‘((𝐴↑2)
− 1)))) |
| 88 | 87 | adantr 480 |
. . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ 𝑛 ∈ ℤ) →
(PellFund‘((𝐴↑2)
− 1)) = (𝐴 +
(√‘((𝐴↑2)
− 1)))) |
| 89 | 88 | oveq1d 7446 |
. . . . . 6
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ 𝑛 ∈ ℤ) →
((PellFund‘((𝐴↑2) − 1))↑𝑛) = ((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑛)) |
| 90 | 85, 89 | eqtr4d 2780 |
. . . . 5
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → ((𝐴 Xrm 𝑛) + ((√‘((𝐴↑2) − 1)) ·
(𝐴 Yrm 𝑛))) = ((PellFund‘((𝐴↑2) − 1))↑𝑛)) |
| 91 | 90 | eqeq2d 2748 |
. . . 4
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → ((𝑋 + ((√‘((𝐴↑2) − 1)) ·
𝑌)) = ((𝐴 Xrm 𝑛) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑛))) ↔ (𝑋 + ((√‘((𝐴↑2) − 1)) · 𝑌)) = ((PellFund‘((𝐴↑2) − 1))↑𝑛))) |
| 92 | 83, 91 | bitr3d 281 |
. . 3
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → ((𝑋 = (𝐴 Xrm 𝑛) ∧ 𝑌 = (𝐴 Yrm 𝑛)) ↔ (𝑋 + ((√‘((𝐴↑2) − 1)) · 𝑌)) = ((PellFund‘((𝐴↑2) − 1))↑𝑛))) |
| 93 | 92 | rexbidva 3177 |
. 2
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) →
(∃𝑛 ∈ ℤ
(𝑋 = (𝐴 Xrm 𝑛) ∧ 𝑌 = (𝐴 Yrm 𝑛)) ↔ ∃𝑛 ∈ ℤ (𝑋 + ((√‘((𝐴↑2) − 1)) · 𝑌)) = ((PellFund‘((𝐴↑2) − 1))↑𝑛))) |
| 94 | 4, 67, 93 | 3bitr4d 311 |
1
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) → (((𝑋↑2) − (((𝐴↑2) − 1) ·
(𝑌↑2))) = 1 ↔
∃𝑛 ∈ ℤ
(𝑋 = (𝐴 Xrm 𝑛) ∧ 𝑌 = (𝐴 Yrm 𝑛)))) |