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 sselid โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 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 fovcdmd โŠข ( ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„ค ) โˆง ๐‘› โˆˆ โ„ค ) โ†’ ( ๐ด Xrm ๐‘› ) โˆˆ โ„•0 )
76 40 75 sselid โŠข ( ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„ค ) โˆง ๐‘› โˆˆ โ„ค ) โ†’ ( ๐ด Xrm ๐‘› ) โˆˆ โ„š )
77 zssq โŠข โ„ค โŠ† โ„š
78 frmy โŠข Yrm : ( ( โ„คโ‰ฅ โ€˜ 2 ) ร— โ„ค ) โŸถ โ„ค
79 78 a1i โŠข ( ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„ค ) โˆง ๐‘› โˆˆ โ„ค ) โ†’ Yrm : ( ( โ„คโ‰ฅ โ€˜ 2 ) ร— โ„ค ) โŸถ โ„ค )
80 79 73 74 fovcdmd โŠข ( ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„ค ) โˆง ๐‘› โˆˆ โ„ค ) โ†’ ( ๐ด Yrm ๐‘› ) โˆˆ โ„ค )
81 77 80 sselid โŠข ( ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 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 ๐‘› ) ) ) )