Metamath Proof Explorer

Theorem pell1234qrre

Description: General Pell solutions are (coded as) real numbers. (Contributed by Stefan O'Rear, 17-Sep-2014)

		Ref	Expression
	Assertion	pell1234qrre	\|- ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) -> A e. RR )

Proof

Step	Hyp	Ref	Expression
1		elpell1234qr	\|- ( D e. ( NN \ []NN ) -> ( A e. ( Pell1234QR ` D ) <-> ( A e. RR /\ E. a e. ZZ E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) ) )
2	1	simprbda	\|- ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) -> A e. RR )

Step

Hyp

Ref

Expression

elpell1234qr

 |-  ( D e. ( NN \ []NN ) -> ( A e. ( Pell1234QR ` D ) <-> ( A e. RR /\ E. a e. ZZ E. b e. ZZ ( A = ( a + ( ( sqrt ` D ) x. b ) ) /\ ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) ) )

simprbda

 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell1234QR ` D ) ) -> A e. RR )