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 ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℕ0 ) → ( 𝑋 = ( 𝐴 Xrm 𝑁 ) ↔ ∃ 𝑦 ∈ ℕ0 ( 𝑦 = ( 𝐴 Yrm 𝑁 ) ∧ ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) = 1 ) ) )

Proof

Step Hyp Ref Expression
1 nn0sqcl ⊢ ( 𝑋 ∈ ℕ0 → ( 𝑋 ↑ 2 ) ∈ ℕ0 )
2 1 3ad2ant3 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℕ0 ) → ( 𝑋 ↑ 2 ) ∈ ℕ0 )
3 2 nn0cnd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℕ0 ) → ( 𝑋 ↑ 2 ) ∈ ℂ )
4 simp1 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℕ0 ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
5 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
6 5 3ad2ant2 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
7 frmx ⊢ Xrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℕ0
8 7 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 )
9 4 6 8 syl2anc ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℕ0 ) → ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 )
10 nn0sqcl ⊢ ( ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 → ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) ∈ ℕ0 )
11 9 10 syl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℕ0 ) → ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) ∈ ℕ0 )
12 11 nn0cnd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℕ0 ) → ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) ∈ ℂ )
13 rmspecnonsq ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ( ℕ ∖ ◻NN ) )
14 13 eldifad ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℕ )
15 14 nnnn0d ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℕ0 )
16 15 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℕ0 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℕ0 )
17 rmynn0 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 Yrm 𝑁 ) ∈ ℕ0 )
18 17 3adant3 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℕ0 ) → ( 𝐴 Yrm 𝑁 ) ∈ ℕ0 )
19 nn0sqcl ⊢ ( ( 𝐴 Yrm 𝑁 ) ∈ ℕ0 → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∈ ℕ0 )
20 18 19 syl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℕ0 ) → ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ∈ ℕ0 )
21 16 20 nn0mulcld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℕ0 ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ) ∈ ℕ0 )
22 21 nn0cnd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℕ0 ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ) ∈ ℂ )
23 3 12 22 subcan2ad ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℕ0 ) → ( ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ) ) = ( ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ) ) ↔ ( 𝑋 ↑ 2 ) = ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) ) )
24 rmxynorm ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ) ) = 1 )
25 4 6 24 syl2anc ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℕ0 ) → ( ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ) ) = 1 )
26 25 eqeq2d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℕ0 ) → ( ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ) ) = ( ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ) ) ↔ ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ) ) = 1 ) )
27 nn0re ⊢ ( 𝑋 ∈ ℕ0 → 𝑋 ∈ ℝ )
28 nn0ge0 ⊢ ( 𝑋 ∈ ℕ0 → 0 ≤ 𝑋 )
29 27 28 jca ⊢ ( 𝑋 ∈ ℕ0 → ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) )
30 29 3ad2ant3 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℕ0 ) → ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) )
31 nn0re ⊢ ( ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 → ( 𝐴 Xrm 𝑁 ) ∈ ℝ )
32 nn0ge0 ⊢ ( ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 → 0 ≤ ( 𝐴 Xrm 𝑁 ) )
33 31 32 jca ⊢ ( ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 → ( ( 𝐴 Xrm 𝑁 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 Xrm 𝑁 ) ) )
34 9 33 syl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℕ0 ) → ( ( 𝐴 Xrm 𝑁 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 Xrm 𝑁 ) ) )
35 sq11 ⊢ ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( ( 𝐴 Xrm 𝑁 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 Xrm 𝑁 ) ) ) → ( ( 𝑋 ↑ 2 ) = ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) ↔ 𝑋 = ( 𝐴 Xrm 𝑁 ) ) )
36 30 34 35 syl2anc ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℕ0 ) → ( ( 𝑋 ↑ 2 ) = ( ( 𝐴 Xrm 𝑁 ) ↑ 2 ) ↔ 𝑋 = ( 𝐴 Xrm 𝑁 ) ) )
37 23 26 36 3bitr3rd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℕ0 ) → ( 𝑋 = ( 𝐴 Xrm 𝑁 ) ↔ ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ) ) = 1 ) )
38 oveq1 ⊢ ( 𝑦 = ( 𝐴 Yrm 𝑁 ) → ( 𝑦 ↑ 2 ) = ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) )
39 38 oveq2d ⊢ ( 𝑦 = ( 𝐴 Yrm 𝑁 ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) = ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ) )
40 39 oveq2d ⊢ ( 𝑦 = ( 𝐴 Yrm 𝑁 ) → ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) = ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ) ) )
41 40 eqeq1d ⊢ ( 𝑦 = ( 𝐴 Yrm 𝑁 ) → ( ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) = 1 ↔ ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ) ) = 1 ) )
42 41 ceqsrexv ⊢ ( ( 𝐴 Yrm 𝑁 ) ∈ ℕ0 → ( ∃ 𝑦 ∈ ℕ0 ( 𝑦 = ( 𝐴 Yrm 𝑁 ) ∧ ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) = 1 ) ↔ ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ) ) = 1 ) )
43 18 42 syl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℕ0 ) → ( ∃ 𝑦 ∈ ℕ0 ( 𝑦 = ( 𝐴 Yrm 𝑁 ) ∧ ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) = 1 ) ↔ ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝑁 ) ↑ 2 ) ) ) = 1 ) )
44 37 43 bitr4d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℕ0 ) → ( 𝑋 = ( 𝐴 Xrm 𝑁 ) ↔ ∃ 𝑦 ∈ ℕ0 ( 𝑦 = ( 𝐴 Yrm 𝑁 ) ∧ ( ( 𝑋 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑦 ↑ 2 ) ) ) = 1 ) ) )