Step | Hyp | Ref
| Expression |
1 | | rmspecnonsq 41631 |
. . . . 5
β’ (π΄ β
(β€β₯β2) β ((π΄β2) β 1) β (β β
β»NN)) |
2 | 1 | adantr 482 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄β2) β 1) β (β β
β»NN)) |
3 | | pell14qrval 41572 |
. . . 4
β’ (((π΄β2) β 1) β
(β β β»NN) β (Pell14QRβ((π΄β2) β 1)) = {π β β β£
βπ β
β0 βπ β β€ (π = (π + ((ββ((π΄β2) β 1)) Β· π)) β§ ((πβ2) β (((π΄β2) β 1) Β· (πβ2))) =
1)}) |
4 | 2, 3 | syl 17 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β
(Pell14QRβ((π΄β2)
β 1)) = {π β
β β£ βπ
β β0 βπ β β€ (π = (π + ((ββ((π΄β2) β 1)) Β· π)) β§ ((πβ2) β (((π΄β2) β 1) Β· (πβ2))) =
1)}) |
5 | | simpl 484 |
. . . . . . . . . 10
β’ ((π = (π + ((ββ((π΄β2) β 1)) Β· π)) β§ ((πβ2) β (((π΄β2) β 1) Β· (πβ2))) = 1) β π = (π + ((ββ((π΄β2) β 1)) Β· π))) |
6 | 5 | reximi 3085 |
. . . . . . . . 9
β’
(βπ β
β€ (π = (π + ((ββ((π΄β2) β 1)) Β·
π)) β§ ((πβ2) β (((π΄β2) β 1) Β·
(πβ2))) = 1) β
βπ β β€
π = (π + ((ββ((π΄β2) β 1)) Β· π))) |
7 | 6 | reximi 3085 |
. . . . . . . 8
β’
(βπ β
β0 βπ β β€ (π = (π + ((ββ((π΄β2) β 1)) Β· π)) β§ ((πβ2) β (((π΄β2) β 1) Β· (πβ2))) = 1) β
βπ β
β0 βπ β β€ π = (π + ((ββ((π΄β2) β 1)) Β· π))) |
8 | 7 | rgenw 3066 |
. . . . . . 7
β’
βπ β
β (βπ β
β0 βπ β β€ (π = (π + ((ββ((π΄β2) β 1)) Β· π)) β§ ((πβ2) β (((π΄β2) β 1) Β· (πβ2))) = 1) β
βπ β
β0 βπ β β€ π = (π + ((ββ((π΄β2) β 1)) Β· π))) |
9 | 8 | a1i 11 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β βπ β β (βπ β β0
βπ β β€
(π = (π + ((ββ((π΄β2) β 1)) Β· π)) β§ ((πβ2) β (((π΄β2) β 1) Β· (πβ2))) = 1) β
βπ β
β0 βπ β β€ π = (π + ((ββ((π΄β2) β 1)) Β· π)))) |
10 | | ss2rab 4068 |
. . . . . 6
β’ ({π β β β£
βπ β
β0 βπ β β€ (π = (π + ((ββ((π΄β2) β 1)) Β· π)) β§ ((πβ2) β (((π΄β2) β 1) Β· (πβ2))) = 1)} β {π β β β£
βπ β
β0 βπ β β€ π = (π + ((ββ((π΄β2) β 1)) Β· π))} β βπ β β (βπ β β0
βπ β β€
(π = (π + ((ββ((π΄β2) β 1)) Β· π)) β§ ((πβ2) β (((π΄β2) β 1) Β· (πβ2))) = 1) β
βπ β
β0 βπ β β€ π = (π + ((ββ((π΄β2) β 1)) Β· π)))) |
11 | 9, 10 | sylibr 233 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β {π β β β£ βπ β β0
βπ β β€
(π = (π + ((ββ((π΄β2) β 1)) Β· π)) β§ ((πβ2) β (((π΄β2) β 1) Β· (πβ2))) = 1)} β {π β β β£
βπ β
β0 βπ β β€ π = (π + ((ββ((π΄β2) β 1)) Β· π))}) |
12 | | ssv 4006 |
. . . . . 6
β’ β
β V |
13 | | rabss2 4075 |
. . . . . 6
β’ (β
β V β {π β
β β£ βπ
β β0 βπ β β€ π = (π + ((ββ((π΄β2) β 1)) Β· π))} β {π β V β£ βπ β β0 βπ β β€ π = (π + ((ββ((π΄β2) β 1)) Β· π))}) |
14 | 12, 13 | ax-mp 5 |
. . . . 5
β’ {π β β β£
βπ β
β0 βπ β β€ π = (π + ((ββ((π΄β2) β 1)) Β· π))} β {π β V β£ βπ β β0 βπ β β€ π = (π + ((ββ((π΄β2) β 1)) Β· π))} |
15 | 11, 14 | sstrdi 3994 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β {π β β β£ βπ β β0
βπ β β€
(π = (π + ((ββ((π΄β2) β 1)) Β· π)) β§ ((πβ2) β (((π΄β2) β 1) Β· (πβ2))) = 1)} β {π β V β£ βπ β β0
βπ β β€
π = (π + ((ββ((π΄β2) β 1)) Β· π))}) |
16 | | rabab 3503 |
. . . 4
β’ {π β V β£ βπ β β0
βπ β β€
π = (π + ((ββ((π΄β2) β 1)) Β· π))} = {π β£ βπ β β0 βπ β β€ π = (π + ((ββ((π΄β2) β 1)) Β· π))} |
17 | 15, 16 | sseqtrdi 4032 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β {π β β β£ βπ β β0
βπ β β€
(π = (π + ((ββ((π΄β2) β 1)) Β· π)) β§ ((πβ2) β (((π΄β2) β 1) Β· (πβ2))) = 1)} β {π β£ βπ β β0
βπ β β€
π = (π + ((ββ((π΄β2) β 1)) Β· π))}) |
18 | 4, 17 | eqsstrd 4020 |
. 2
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β
(Pell14QRβ((π΄β2)
β 1)) β {π
β£ βπ β
β0 βπ β β€ π = (π + ((ββ((π΄β2) β 1)) Β· π))}) |
19 | | simpr 486 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β π β β€) |
20 | | rmspecfund 41633 |
. . . . . . 7
β’ (π΄ β
(β€β₯β2) β (PellFundβ((π΄β2) β 1)) = (π΄ + (ββ((π΄β2) β 1)))) |
21 | 20 | adantr 482 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β
(PellFundβ((π΄β2)
β 1)) = (π΄ +
(ββ((π΄β2)
β 1)))) |
22 | 21 | eqcomd 2739 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ + (ββ((π΄β2) β 1))) =
(PellFundβ((π΄β2)
β 1))) |
23 | 22 | oveq1d 7421 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ + (ββ((π΄β2) β 1)))βπ) = ((PellFundβ((π΄β2) β 1))βπ)) |
24 | | oveq2 7414 |
. . . . 5
β’ (π = π β ((PellFundβ((π΄β2) β 1))βπ) = ((PellFundβ((π΄β2) β 1))βπ)) |
25 | 24 | rspceeqv 3633 |
. . . 4
β’ ((π β β€ β§ ((π΄ + (ββ((π΄β2) β 1)))βπ) = ((PellFundβ((π΄β2) β 1))βπ)) β βπ β β€ ((π΄ + (ββ((π΄β2) β 1)))βπ) = ((PellFundβ((π΄β2) β 1))βπ)) |
26 | 19, 23, 25 | syl2anc 585 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β βπ β β€ ((π΄ + (ββ((π΄β2) β 1)))βπ) = ((PellFundβ((π΄β2) β 1))βπ)) |
27 | | pellfund14b 41623 |
. . . 4
β’ (((π΄β2) β 1) β
(β β β»NN) β (((π΄ + (ββ((π΄β2) β 1)))βπ) β (Pell14QRβ((π΄β2) β 1)) β βπ β β€ ((π΄ + (ββ((π΄β2) β 1)))βπ) = ((PellFundβ((π΄β2) β 1))βπ))) |
28 | 2, 27 | syl 17 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (((π΄ + (ββ((π΄β2) β 1)))βπ) β (Pell14QRβ((π΄β2) β 1)) β βπ β β€ ((π΄ + (ββ((π΄β2) β 1)))βπ) = ((PellFundβ((π΄β2) β 1))βπ))) |
29 | 26, 28 | mpbird 257 |
. 2
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ + (ββ((π΄β2) β 1)))βπ) β (Pell14QRβ((π΄β2) β 1))) |
30 | 18, 29 | sseldd 3983 |
1
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ + (ββ((π΄β2) β 1)))βπ) β {π β£ βπ β β0 βπ β β€ π = (π + ((ββ((π΄β2) β 1)) Β· π))}) |