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 ) ) )