Step | Hyp | Ref
| Expression |
1 | | rmspecnonsq 41948 |
. . . 4
β’ (π΄ β
(β€β₯β2) β ((π΄β2) β 1) β (β β
β»NN)) |
2 | 1 | 3ad2ant1 1132 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β ((π΄β2) β 1) β
(β β β»NN)) |
3 | | pellfund14b 41940 |
. . 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 12486 |
. . . . . 6
β’ (π β β0
β π β
β) |
6 | 5 | 3ad2ant2 1133 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β π β
β) |
7 | | rmspecpos 41958 |
. . . . . . . . 9
β’ (π΄ β
(β€β₯β2) β ((π΄β2) β 1) β
β+) |
8 | 7 | rpsqrtcld 15363 |
. . . . . . . 8
β’ (π΄ β
(β€β₯β2) β (ββ((π΄β2) β 1)) β
β+) |
9 | 8 | rpred 13021 |
. . . . . . 7
β’ (π΄ β
(β€β₯β2) β (ββ((π΄β2) β 1)) β
β) |
10 | 9 | 3ad2ant1 1132 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β
(ββ((π΄β2)
β 1)) β β) |
11 | | zre 12567 |
. . . . . . 7
β’ (π β β€ β π β
β) |
12 | 11 | 3ad2ant3 1134 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β π β
β) |
13 | 10, 12 | remulcld 11249 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β
((ββ((π΄β2)
β 1)) Β· π)
β β) |
14 | 6, 13 | readdcld 11248 |
. . . 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 1191 |
. . . . . 6
β’ (((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β§ ((πβ2) β (((π΄β2) β 1) Β·
(πβ2))) = 1) β
π β
β0) |
17 | | simpl3 1192 |
. . . . . 6
β’ (((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β§ ((πβ2) β (((π΄β2) β 1) Β·
(πβ2))) = 1) β
π β
β€) |
18 | | eqidd 2732 |
. . . . . 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 7419 |
. . . . . . . . 9
β’ (π₯ = π β (π₯ + ((ββ((π΄β2) β 1)) Β· π¦)) = (π + ((ββ((π΄β2) β 1)) Β· π¦))) |
21 | 20 | eqeq2d 2742 |
. . . . . . . 8
β’ (π₯ = π β ((π + ((ββ((π΄β2) β 1)) Β· π)) = (π₯ + ((ββ((π΄β2) β 1)) Β· π¦)) β (π + ((ββ((π΄β2) β 1)) Β· π)) = (π + ((ββ((π΄β2) β 1)) Β· π¦)))) |
22 | | oveq1 7419 |
. . . . . . . . . 10
β’ (π₯ = π β (π₯β2) = (πβ2)) |
23 | 22 | oveq1d 7427 |
. . . . . . . . 9
β’ (π₯ = π β ((π₯β2) β (((π΄β2) β 1) Β· (π¦β2))) = ((πβ2) β (((π΄β2) β 1) Β· (π¦β2)))) |
24 | 23 | eqeq1d 2733 |
. . . . . . . 8
β’ (π₯ = π β (((π₯β2) β (((π΄β2) β 1) Β· (π¦β2))) = 1 β ((πβ2) β (((π΄β2) β 1) Β·
(π¦β2))) =
1)) |
25 | 21, 24 | anbi12d 630 |
. . . . . . 7
β’ (π₯ = π β (((π + ((ββ((π΄β2) β 1)) Β· π)) = (π₯ + ((ββ((π΄β2) β 1)) Β· π¦)) β§ ((π₯β2) β (((π΄β2) β 1) Β· (π¦β2))) = 1) β ((π + ((ββ((π΄β2) β 1)) Β·
π)) = (π + ((ββ((π΄β2) β 1)) Β· π¦)) β§ ((πβ2) β (((π΄β2) β 1) Β· (π¦β2))) =
1))) |
26 | | oveq2 7420 |
. . . . . . . . . 10
β’ (π¦ = π β ((ββ((π΄β2) β 1)) Β· π¦) = ((ββ((π΄β2) β 1)) Β·
π)) |
27 | 26 | oveq2d 7428 |
. . . . . . . . 9
β’ (π¦ = π β (π + ((ββ((π΄β2) β 1)) Β· π¦)) = (π + ((ββ((π΄β2) β 1)) Β· π))) |
28 | 27 | eqeq2d 2742 |
. . . . . . . 8
β’ (π¦ = π β ((π + ((ββ((π΄β2) β 1)) Β· π)) = (π + ((ββ((π΄β2) β 1)) Β· π¦)) β (π + ((ββ((π΄β2) β 1)) Β· π)) = (π + ((ββ((π΄β2) β 1)) Β· π)))) |
29 | | oveq1 7419 |
. . . . . . . . . . 11
β’ (π¦ = π β (π¦β2) = (πβ2)) |
30 | 29 | oveq2d 7428 |
. . . . . . . . . 10
β’ (π¦ = π β (((π΄β2) β 1) Β· (π¦β2)) = (((π΄β2) β 1) Β· (πβ2))) |
31 | 30 | oveq2d 7428 |
. . . . . . . . 9
β’ (π¦ = π β ((πβ2) β (((π΄β2) β 1) Β· (π¦β2))) = ((πβ2) β (((π΄β2) β 1) Β· (πβ2)))) |
32 | 31 | eqeq1d 2733 |
. . . . . . . 8
β’ (π¦ = π β (((πβ2) β (((π΄β2) β 1) Β· (π¦β2))) = 1 β ((πβ2) β (((π΄β2) β 1) Β·
(πβ2))) =
1)) |
33 | 28, 32 | anbi12d 630 |
. . . . . . 7
β’ (π¦ = π β (((π + ((ββ((π΄β2) β 1)) Β· π)) = (π + ((ββ((π΄β2) β 1)) Β· π¦)) β§ ((πβ2) β (((π΄β2) β 1) Β· (π¦β2))) = 1) β ((π + ((ββ((π΄β2) β 1)) Β·
π)) = (π + ((ββ((π΄β2) β 1)) Β· π)) β§ ((πβ2) β (((π΄β2) β 1) Β· (πβ2))) =
1))) |
34 | 25, 33 | rspc2ev 3624 |
. . . . . 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 1373 |
. . . . 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 41947 |
. . . . . . . . . . 11
β’ (π΄ β
(β€β₯β2) β (ββ((π΄β2) β 1)) β (β β
β)) |
38 | 37 | 3ad2ant1 1132 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β
(ββ((π΄β2)
β 1)) β (β β β)) |
39 | 38 | adantr 480 |
. . . . . . . . 9
β’ (((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β§ (π₯ β β0
β§ π¦ β β€))
β (ββ((π΄β2) β 1)) β (β β
β)) |
40 | | nn0ssq 12946 |
. . . . . . . . . . 11
β’
β0 β β |
41 | | simp2 1136 |
. . . . . . . . . . 11
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β π β
β0) |
42 | 40, 41 | sselid 3980 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β π β
β) |
43 | 42 | adantr 480 |
. . . . . . . . 9
β’ (((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β§ (π₯ β β0
β§ π¦ β β€))
β π β
β) |
44 | | zq 12943 |
. . . . . . . . . . 11
β’ (π β β€ β π β
β) |
45 | 44 | 3ad2ant3 1134 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β π β
β) |
46 | 45 | adantr 480 |
. . . . . . . . 9
β’ (((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β§ (π₯ β β0
β§ π¦ β β€))
β π β
β) |
47 | 40 | sseli 3978 |
. . . . . . . . . 10
β’ (π₯ β β0
β π₯ β
β) |
48 | 47 | ad2antrl 725 |
. . . . . . . . 9
β’ (((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β§ (π₯ β β0
β§ π¦ β β€))
β π₯ β
β) |
49 | | zq 12943 |
. . . . . . . . . 10
β’ (π¦ β β€ β π¦ β
β) |
50 | 49 | ad2antll 726 |
. . . . . . . . 9
β’ (((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β§ (π₯ β β0
β§ π¦ β β€))
β π¦ β
β) |
51 | | qirropth 41949 |
. . . . . . . . 9
β’
(((ββ((π΄β2) β 1)) β (β β
β) β§ (π β
β β§ π β
β) β§ (π₯ β
β β§ π¦ β
β)) β ((π +
((ββ((π΄β2)
β 1)) Β· π)) =
(π₯ +
((ββ((π΄β2)
β 1)) Β· π¦))
β (π = π₯ β§ π = π¦))) |
52 | 39, 43, 46, 48, 50, 51 | syl122anc 1378 |
. . . . . . . 8
β’ (((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β§ (π₯ β β0
β§ π¦ β β€))
β ((π +
((ββ((π΄β2)
β 1)) Β· π)) =
(π₯ +
((ββ((π΄β2)
β 1)) Β· π¦))
β (π = π₯ β§ π = π¦))) |
53 | 52 | biimpd 228 |
. . . . . . 7
β’ (((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β§ (π₯ β β0
β§ π¦ β β€))
β ((π +
((ββ((π΄β2)
β 1)) Β· π)) =
(π₯ +
((ββ((π΄β2)
β 1)) Β· π¦))
β (π = π₯ β§ π = π¦))) |
54 | 53 | anim1d 610 |
. . . . . 6
β’ (((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β§ (π₯ β β0
β§ π¦ β β€))
β (((π +
((ββ((π΄β2)
β 1)) Β· π)) =
(π₯ +
((ββ((π΄β2)
β 1)) Β· π¦))
β§ ((π₯β2) β
(((π΄β2) β 1)
Β· (π¦β2))) = 1)
β ((π = π₯ β§ π = π¦) β§ ((π₯β2) β (((π΄β2) β 1) Β· (π¦β2))) =
1))) |
55 | | oveq1 7419 |
. . . . . . . . . 10
β’ (π = π₯ β (πβ2) = (π₯β2)) |
56 | | oveq1 7419 |
. . . . . . . . . . 11
β’ (π = π¦ β (πβ2) = (π¦β2)) |
57 | 56 | oveq2d 7428 |
. . . . . . . . . 10
β’ (π = π¦ β (((π΄β2) β 1) Β· (πβ2)) = (((π΄β2) β 1) Β· (π¦β2))) |
58 | 55, 57 | oveqan12d 7431 |
. . . . . . . . 9
β’ ((π = π₯ β§ π = π¦) β ((πβ2) β (((π΄β2) β 1) Β· (πβ2))) = ((π₯β2) β (((π΄β2) β 1) Β·
(π¦β2)))) |
59 | 58 | eqcomd 2737 |
. . . . . . . 8
β’ ((π = π₯ β§ π = π¦) β ((π₯β2) β (((π΄β2) β 1) Β· (π¦β2))) = ((πβ2) β (((π΄β2) β 1) Β· (πβ2)))) |
60 | 59 | eqeq1d 2733 |
. . . . . . 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 3210 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β
(βπ₯ β
β0 βπ¦ β β€ ((π + ((ββ((π΄β2) β 1)) Β· π)) = (π₯ + ((ββ((π΄β2) β 1)) Β· π¦)) β§ ((π₯β2) β (((π΄β2) β 1) Β· (π¦β2))) = 1) β ((πβ2) β (((π΄β2) β 1) Β·
(πβ2))) =
1)) |
64 | 36, 63 | impbid 211 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β (((πβ2) β (((π΄β2) β 1) Β·
(πβ2))) = 1 β
βπ₯ β
β0 βπ¦ β β€ ((π + ((ββ((π΄β2) β 1)) Β· π)) = (π₯ + ((ββ((π΄β2) β 1)) Β· π¦)) β§ ((π₯β2) β (((π΄β2) β 1) Β· (π¦β2))) =
1))) |
65 | | elpell14qr 41890 |
. . . 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 41955 |
. . . . . . . 8
β’
Xrm :((β€β₯β2) Γ
β€)βΆβ0 |
72 | 71 | a1i 11 |
. . . . . . 7
β’ (((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β§ π β β€) β
Xrm :((β€β₯β2) Γ
β€)βΆβ0) |
73 | | simpl1 1190 |
. . . . . . 7
β’ (((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β§ π β β€) β π΄ β
(β€β₯β2)) |
74 | | simpr 484 |
. . . . . . 7
β’ (((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β§ π β β€) β π β
β€) |
75 | 72, 73, 74 | fovcdmd 7583 |
. . . . . 6
β’ (((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β§ π β β€) β (π΄ Xrm π) β
β0) |
76 | 40, 75 | sselid 3980 |
. . . . 5
β’ (((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β§ π β β€) β (π΄ Xrm π) β
β) |
77 | | zssq 12945 |
. . . . . 6
β’ β€
β β |
78 | | frmy 41956 |
. . . . . . . 8
β’
Yrm :((β€β₯β2) Γ
β€)βΆβ€ |
79 | 78 | a1i 11 |
. . . . . . 7
β’ (((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β§ π β β€) β
Yrm :((β€β₯β2) Γ
β€)βΆβ€) |
80 | 79, 73, 74 | fovcdmd 7583 |
. . . . . 6
β’ (((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β§ π β β€) β (π΄ Yrm π) β
β€) |
81 | 77, 80 | sselid 3980 |
. . . . 5
β’ (((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β§ π β β€) β (π΄ Yrm π) β
β) |
82 | | qirropth 41949 |
. . . . 5
β’
(((ββ((π΄β2) β 1)) β (β β
β) β§ (π β
β β§ π β
β) β§ ((π΄
Xrm π) β
β β§ (π΄
Yrm π) β
β)) β ((π +
((ββ((π΄β2)
β 1)) Β· π)) =
((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β·
(π΄ Yrm π))) β (π = (π΄ Xrm π) β§ π = (π΄ Yrm π)))) |
83 | 68, 69, 70, 76, 81, 82 | syl122anc 1378 |
. . . 4
β’ (((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β§ π β β€) β ((π + ((ββ((π΄β2) β 1)) Β·
π)) = ((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β· (π΄ Yrm π))) β (π = (π΄ Xrm π) β§ π = (π΄ Yrm π)))) |
84 | | rmxyval 41957 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β· (π΄ Yrm π))) = ((π΄ + (ββ((π΄β2) β 1)))βπ)) |
85 | 84 | 3ad2antl1 1184 |
. . . . . 6
β’ (((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β§ π β β€) β ((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β·
(π΄ Yrm π))) = ((π΄ + (ββ((π΄β2) β 1)))βπ)) |
86 | | rmspecfund 41950 |
. . . . . . . . 9
β’ (π΄ β
(β€β₯β2) β (PellFundβ((π΄β2) β 1)) = (π΄ + (ββ((π΄β2) β 1)))) |
87 | 86 | 3ad2ant1 1132 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β
(PellFundβ((π΄β2)
β 1)) = (π΄ +
(ββ((π΄β2)
β 1)))) |
88 | 87 | adantr 480 |
. . . . . . 7
β’ (((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β§ π β β€) β
(PellFundβ((π΄β2)
β 1)) = (π΄ +
(ββ((π΄β2)
β 1)))) |
89 | 88 | oveq1d 7427 |
. . . . . 6
β’ (((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β§ π β β€) β
((PellFundβ((π΄β2) β 1))βπ) = ((π΄ + (ββ((π΄β2) β 1)))βπ)) |
90 | 85, 89 | eqtr4d 2774 |
. . . . 5
β’ (((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β€) β§ π β β€) β ((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β·
(π΄ Yrm π))) = ((PellFundβ((π΄β2) β 1))βπ)) |
91 | 90 | eqeq2d 2742 |
. . . 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 3175 |
. 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 π)))) |