Metamath Proof Explorer

Theorem rmxdiophlem

Description: X can be expressed in terms of Y, so it is also Diophantine. (Contributed by Stefan O'Rear, 15-Oct-2014)

Ref Expression
Assertion rmxdiophlem 
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 /\ X e. NN0 ) -> ( X = ( A rmX N ) <-> E. y e. NN0 ( y = ( A rmY N ) /\ ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = 1 ) ) )

Proof

Step Hyp Ref Expression
1 nn0sqcl 
 |-  ( X e. NN0 -> ( X ^ 2 ) e. NN0 )
2 1 3ad2ant3 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 /\ X e. NN0 ) -> ( X ^ 2 ) e. NN0 )
3 2 nn0cnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 /\ X e. NN0 ) -> ( X ^ 2 ) e. CC )
4 simp1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 /\ X e. NN0 ) -> A e. ( ZZ>= ` 2 ) )
5 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
6 5 3ad2ant2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 /\ X e. NN0 ) -> N e. ZZ )
7 frmx 
 |-  rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
8 7 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. NN0 )
9 4 6 8 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 /\ X e. NN0 ) -> ( A rmX N ) e. NN0 )
10 nn0sqcl 
 |-  ( ( A rmX N ) e. NN0 -> ( ( A rmX N ) ^ 2 ) e. NN0 )
11 9 10 syl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 /\ X e. NN0 ) -> ( ( A rmX N ) ^ 2 ) e. NN0 )
12 11 nn0cnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 /\ X e. NN0 ) -> ( ( A rmX N ) ^ 2 ) e. CC )
13 rmspecnonsq 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. ( NN \ []NN ) )
14 13 eldifad 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. NN )
15 14 nnnn0d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. NN0 )
16 15 3ad2ant1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 /\ X e. NN0 ) -> ( ( A ^ 2 ) - 1 ) e. NN0 )
17 rmynn0 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( A rmY N ) e. NN0 )
18 17 3adant3 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 /\ X e. NN0 ) -> ( A rmY N ) e. NN0 )
19 nn0sqcl 
 |-  ( ( A rmY N ) e. NN0 -> ( ( A rmY N ) ^ 2 ) e. NN0 )
20 18 19 syl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 /\ X e. NN0 ) -> ( ( A rmY N ) ^ 2 ) e. NN0 )
21 16 20 nn0mulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 /\ X e. NN0 ) -> ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) ^ 2 ) ) e. NN0 )
22 21 nn0cnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 /\ X e. NN0 ) -> ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) ^ 2 ) ) e. CC )
23 3 12 22 subcan2ad 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 /\ X e. NN0 ) -> ( ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) ^ 2 ) ) ) = ( ( ( A rmX N ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) ^ 2 ) ) ) <-> ( X ^ 2 ) = ( ( A rmX N ) ^ 2 ) ) )
24 rmxynorm 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( A rmX N ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) ^ 2 ) ) ) = 1 )
25 4 6 24 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 /\ X e. NN0 ) -> ( ( ( A rmX N ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) ^ 2 ) ) ) = 1 )
26 25 eqeq2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 /\ X e. NN0 ) -> ( ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) ^ 2 ) ) ) = ( ( ( A rmX N ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) ^ 2 ) ) ) <-> ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) ^ 2 ) ) ) = 1 ) )
27 nn0re 
 |-  ( X e. NN0 -> X e. RR )
28 nn0ge0 
 |-  ( X e. NN0 -> 0 <_ X )
29 27 28 jca 
 |-  ( X e. NN0 -> ( X e. RR /\ 0 <_ X ) )
30 29 3ad2ant3 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 /\ X e. NN0 ) -> ( X e. RR /\ 0 <_ X ) )
31 nn0re 
 |-  ( ( A rmX N ) e. NN0 -> ( A rmX N ) e. RR )
32 nn0ge0 
 |-  ( ( A rmX N ) e. NN0 -> 0 <_ ( A rmX N ) )
33 31 32 jca 
 |-  ( ( A rmX N ) e. NN0 -> ( ( A rmX N ) e. RR /\ 0 <_ ( A rmX N ) ) )
34 9 33 syl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 /\ X e. NN0 ) -> ( ( A rmX N ) e. RR /\ 0 <_ ( A rmX N ) ) )
35 sq11 
 |-  ( ( ( X e. RR /\ 0 <_ X ) /\ ( ( A rmX N ) e. RR /\ 0 <_ ( A rmX N ) ) ) -> ( ( X ^ 2 ) = ( ( A rmX N ) ^ 2 ) <-> X = ( A rmX N ) ) )
36 30 34 35 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 /\ X e. NN0 ) -> ( ( X ^ 2 ) = ( ( A rmX N ) ^ 2 ) <-> X = ( A rmX N ) ) )
37 23 26 36 3bitr3rd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 /\ X e. NN0 ) -> ( X = ( A rmX N ) <-> ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) ^ 2 ) ) ) = 1 ) )
38 oveq1 
 |-  ( y = ( A rmY N ) -> ( y ^ 2 ) = ( ( A rmY N ) ^ 2 ) )
39 38 oveq2d 
 |-  ( y = ( A rmY N ) -> ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) = ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) ^ 2 ) ) )
40 39 oveq2d 
 |-  ( y = ( A rmY N ) -> ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) ^ 2 ) ) ) )
41 40 eqeq1d 
 |-  ( y = ( A rmY N ) -> ( ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = 1 <-> ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) ^ 2 ) ) ) = 1 ) )
42 41 ceqsrexv 
 |-  ( ( A rmY N ) e. NN0 -> ( E. y e. NN0 ( y = ( A rmY N ) /\ ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = 1 ) <-> ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) ^ 2 ) ) ) = 1 ) )
43 18 42 syl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 /\ X e. NN0 ) -> ( E. y e. NN0 ( y = ( A rmY N ) /\ ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = 1 ) <-> ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) ^ 2 ) ) ) = 1 ) )
44 37 43 bitr4d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 /\ X e. NN0 ) -> ( X = ( A rmX N ) <-> E. y e. NN0 ( y = ( A rmY N ) /\ ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = 1 ) ) )