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 )
7 6 3ad2ant2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) -> K e. NN0 )
8 7 adantr 
 |-  ( ( ( 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 )
14 13 3ad2ant3 
 |-  ( ( 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 )
23 22 3adant3 
 |-  ( ( 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 )
29 28 adantr 
 |-  ( ( ( 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 )
32 31 3ad2ant3 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) -> N e. NN0 )
33 7 32 nn0expcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( K ^ N ) e. NN0 )
34 33 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K rmY ( N + 1 ) ) <_ A ) -> ( K ^ N ) e. NN0 )
35 divalgmodcl 
 |-  ( ( ( ( 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 ) ) ) ) )
36 29 30 34 35 syl3anc 
 |-  ( ( ( 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 ) ) ) ) )
37 5 11 36 mpbir2and 
 |-  ( ( ( 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 ) ) )