Metamath Proof Explorer

Theorem jm3.1

Description: Diophantine expression for exponentiation. Lemma 3.1 of JonesMatijasevic p. 698. (Contributed by Stefan O'Rear, 16-Oct-2014)

Ref Expression
Assertion jm3.1 ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 Yrm ( 𝑁 + 1 ) ) ≤ 𝐴 ) → ( 𝐾 ↑ 𝑁 ) = ( ( ( 𝐴 Xrm 𝑁 ) − ( ( 𝐴 − 𝐾 ) · ( 𝐴 Yrm 𝑁 ) ) ) mod ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) ) )

Proof

Step Hyp Ref Expression
1 simpl1 ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 Yrm ( 𝑁 + 1 ) ) ≤ 𝐴 ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
2 simpl2 ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 Yrm ( 𝑁 + 1 ) ) ≤ 𝐴 ) → 𝐾 ∈ ( ℤ≥ ‘ 2 ) )
3 simpl3 ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 Yrm ( 𝑁 + 1 ) ) ≤ 𝐴 ) → 𝑁 ∈ ℕ )
4 simpr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 Yrm ( 𝑁 + 1 ) ) ≤ 𝐴 ) → ( 𝐾 Yrm ( 𝑁 + 1 ) ) ≤ 𝐴 )
5 1 2 3 4 jm3.1lem2 ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 Yrm ( 𝑁 + 1 ) ) ≤ 𝐴 ) → ( 𝐾 ↑ 𝑁 ) < ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) )
6 eluzge2nn0 ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) → 𝐾 ∈ ℕ0 )
7 6 3ad2ant2 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 𝐾 ∈ ℕ0 )
8 7 adantr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 Yrm ( 𝑁 + 1 ) ) ≤ 𝐴 ) → 𝐾 ∈ ℕ0 )
9 3 nnnn0d ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 Yrm ( 𝑁 + 1 ) ) ≤ 𝐴 ) → 𝑁 ∈ ℕ0 )
10 jm2.18 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) ∥ ( ( ( 𝐴 Xrm 𝑁 ) − ( ( 𝐴 − 𝐾 ) · ( 𝐴 Yrm 𝑁 ) ) ) − ( 𝐾 ↑ 𝑁 ) ) )
11 1 8 9 10 syl3anc ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 Yrm ( 𝑁 + 1 ) ) ≤ 𝐴 ) → ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) ∥ ( ( ( 𝐴 Xrm 𝑁 ) − ( ( 𝐴 − 𝐾 ) · ( 𝐴 Yrm 𝑁 ) ) ) − ( 𝐾 ↑ 𝑁 ) ) )
12 simp1 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
13 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
14 13 3ad2ant3 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℤ )
15 frmx ⊢ Xrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℕ0
16 15 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 )
17 12 14 16 syl2anc ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 )
18 17 nn0zd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℤ )
19 eluzelz ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℤ )
20 eluzelz ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) → 𝐾 ∈ ℤ )
21 zsubcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐴 − 𝐾 ) ∈ ℤ )
22 19 20 21 syl2an ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 − 𝐾 ) ∈ ℤ )
23 22 3adant3 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 − 𝐾 ) ∈ ℤ )
24 frmy ⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
25 24 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
26 12 14 25 syl2anc ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
27 23 26 zmulcld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 − 𝐾 ) · ( 𝐴 Yrm 𝑁 ) ) ∈ ℤ )
28 18 27 zsubcld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Xrm 𝑁 ) − ( ( 𝐴 − 𝐾 ) · ( 𝐴 Yrm 𝑁 ) ) ) ∈ ℤ )
29 28 adantr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 Yrm ( 𝑁 + 1 ) ) ≤ 𝐴 ) → ( ( 𝐴 Xrm 𝑁 ) − ( ( 𝐴 − 𝐾 ) · ( 𝐴 Yrm 𝑁 ) ) ) ∈ ℤ )
30 1 2 3 4 jm3.1lem3 ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 Yrm ( 𝑁 + 1 ) ) ≤ 𝐴 ) → ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) ∈ ℕ )
31 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
32 31 3ad2ant3 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ0 )
33 7 32 nn0expcld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐾 ↑ 𝑁 ) ∈ ℕ0 )
34 33 adantr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 Yrm ( 𝑁 + 1 ) ) ≤ 𝐴 ) → ( 𝐾 ↑ 𝑁 ) ∈ ℕ0 )
35 divalgmodcl ⊢ ( ( ( ( 𝐴 Xrm 𝑁 ) − ( ( 𝐴 − 𝐾 ) · ( 𝐴 Yrm 𝑁 ) ) ) ∈ ℤ ∧ ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) ∈ ℕ ∧ ( 𝐾 ↑ 𝑁 ) ∈ ℕ0 ) → ( ( 𝐾 ↑ 𝑁 ) = ( ( ( 𝐴 Xrm 𝑁 ) − ( ( 𝐴 − 𝐾 ) · ( 𝐴 Yrm 𝑁 ) ) ) mod ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) ) ↔ ( ( 𝐾 ↑ 𝑁 ) < ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) ∧ ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) ∥ ( ( ( 𝐴 Xrm 𝑁 ) − ( ( 𝐴 − 𝐾 ) · ( 𝐴 Yrm 𝑁 ) ) ) − ( 𝐾 ↑ 𝑁 ) ) ) ) )
36 29 30 34 35 syl3anc ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 Yrm ( 𝑁 + 1 ) ) ≤ 𝐴 ) → ( ( 𝐾 ↑ 𝑁 ) = ( ( ( 𝐴 Xrm 𝑁 ) − ( ( 𝐴 − 𝐾 ) · ( 𝐴 Yrm 𝑁 ) ) ) mod ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) ) ↔ ( ( 𝐾 ↑ 𝑁 ) < ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) ∧ ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) ∥ ( ( ( 𝐴 Xrm 𝑁 ) − ( ( 𝐴 − 𝐾 ) · ( 𝐴 Yrm 𝑁 ) ) ) − ( 𝐾 ↑ 𝑁 ) ) ) ) )
37 5 11 36 mpbir2and ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 Yrm ( 𝑁 + 1 ) ) ≤ 𝐴 ) → ( 𝐾 ↑ 𝑁 ) = ( ( ( 𝐴 Xrm 𝑁 ) − ( ( 𝐴 − 𝐾 ) · ( 𝐴 Yrm 𝑁 ) ) ) mod ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) ) )