# 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
`|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K rmY ( N + 1 ) ) <_ A ) -> ( K ^ N ) = ( ( ( A rmX N ) - ( ( A - K ) x. ( A rmY N ) ) ) mod ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) ) )`

### Proof

Step Hyp Ref Expression
1 simpl1
` |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K rmY ( N + 1 ) ) <_ A ) -> A e. ( ZZ>= ` 2 ) )`
2 simpl2
` |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K rmY ( N + 1 ) ) <_ A ) -> K e. ( ZZ>= ` 2 ) )`
3 simpl3
` |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K rmY ( N + 1 ) ) <_ A ) -> N e. NN )`
4 simpr
` |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K rmY ( N + 1 ) ) <_ A ) -> ( K rmY ( N + 1 ) ) <_ A )`
5 1 2 3 4 jm3.1lem2
` |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K rmY ( N + 1 ) ) <_ A ) -> ( K ^ N ) < ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) )`
6 eluzge2nn0
` |-  ( K e. ( ZZ>= ` 2 ) -> K e. NN0 )`
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) -> K e. NN0 )`
` |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K rmY ( N + 1 ) ) <_ A ) -> K e. NN0 )`
9 3 nnnn0d
` |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K rmY ( N + 1 ) ) <_ A ) -> N e. NN0 )`
10 jm2.18
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 /\ N e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) || ( ( ( A rmX N ) - ( ( A - K ) x. ( A rmY N ) ) ) - ( K ^ N ) ) )`
11 1 8 9 10 syl3anc
` |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K rmY ( N + 1 ) ) <_ A ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) || ( ( ( A rmX N ) - ( ( A - K ) x. ( A rmY N ) ) ) - ( K ^ N ) ) )`
12 simp1
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) -> A e. ( ZZ>= ` 2 ) )`
13 nnz
` |-  ( N e. NN -> N e. ZZ )`
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) -> N e. ZZ )`
15 frmx
` |-  rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0`
16 15 fovcl
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. NN0 )`
17 12 14 16 syl2anc
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmX N ) e. NN0 )`
18 17 nn0zd
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmX N ) e. ZZ )`
19 eluzelz
` |-  ( A e. ( ZZ>= ` 2 ) -> A e. ZZ )`
20 eluzelz
` |-  ( K e. ( ZZ>= ` 2 ) -> K e. ZZ )`
21 zsubcl
` |-  ( ( A e. ZZ /\ K e. ZZ ) -> ( A - K ) e. ZZ )`
22 19 20 21 syl2an
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) ) -> ( A - K ) e. ZZ )`
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A - K ) e. ZZ )`
24 frmy
` |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ`
25 24 fovcl
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. ZZ )`
26 12 14 25 syl2anc
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A rmY N ) e. ZZ )`
27 23 26 zmulcld
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( A - K ) x. ( A rmY N ) ) e. ZZ )`
28 18 27 zsubcld
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( A rmX N ) - ( ( A - K ) x. ( A rmY N ) ) ) e. ZZ )`
` |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K rmY ( N + 1 ) ) <_ A ) -> ( ( A rmX N ) - ( ( A - K ) x. ( A rmY N ) ) ) e. ZZ )`
30 1 2 3 4 jm3.1lem3
` |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K rmY ( N + 1 ) ) <_ A ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. NN )`
31 nnnn0
` |-  ( N e. NN -> N e. NN0 )`
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) -> N e. NN0 )`
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( K ^ N ) e. NN0 )`
` |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K rmY ( N + 1 ) ) <_ A ) -> ( K ^ N ) e. NN0 )`
` |-  ( ( ( ( A rmX N ) - ( ( A - K ) x. ( A rmY N ) ) ) e. ZZ /\ ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. NN /\ ( K ^ N ) e. NN0 ) -> ( ( K ^ N ) = ( ( ( A rmX N ) - ( ( A - K ) x. ( A rmY N ) ) ) mod ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) ) <-> ( ( K ^ N ) < ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) /\ ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) || ( ( ( A rmX N ) - ( ( A - K ) x. ( A rmY N ) ) ) - ( K ^ N ) ) ) ) )`
` |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K rmY ( N + 1 ) ) <_ A ) -> ( ( K ^ N ) = ( ( ( A rmX N ) - ( ( A - K ) x. ( A rmY N ) ) ) mod ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) ) <-> ( ( K ^ N ) < ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) /\ ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) || ( ( ( A rmX N ) - ( ( A - K ) x. ( A rmY N ) ) ) - ( K ^ N ) ) ) ) )`
` |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K rmY ( N + 1 ) ) <_ A ) -> ( K ^ N ) = ( ( ( A rmX N ) - ( ( A - K ) x. ( A rmY N ) ) ) mod ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) ) )`