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 ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {K}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\wedge {K}{Y}_{\mathrm{rm}}\left({N}+1\right)\le {A}\right)\to {{K}}^{{N}}=\left(\left({A}{X}_{\mathrm{rm}}{N}\right)-\left({A}-{K}\right)\left({A}{Y}_{\mathrm{rm}}{N}\right)\right)\mathrm{mod}\left(2{A}{K}-{{K}}^{2}-1\right)$

Proof

Step Hyp Ref Expression
1 simpl1 ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {K}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\wedge {K}{Y}_{\mathrm{rm}}\left({N}+1\right)\le {A}\right)\to {A}\in {ℤ}_{\ge 2}$
2 simpl2 ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {K}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\wedge {K}{Y}_{\mathrm{rm}}\left({N}+1\right)\le {A}\right)\to {K}\in {ℤ}_{\ge 2}$
3 simpl3 ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {K}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\wedge {K}{Y}_{\mathrm{rm}}\left({N}+1\right)\le {A}\right)\to {N}\in ℕ$
4 simpr ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {K}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\wedge {K}{Y}_{\mathrm{rm}}\left({N}+1\right)\le {A}\right)\to {K}{Y}_{\mathrm{rm}}\left({N}+1\right)\le {A}$
5 1 2 3 4 jm3.1lem2 ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {K}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\wedge {K}{Y}_{\mathrm{rm}}\left({N}+1\right)\le {A}\right)\to {{K}}^{{N}}<2{A}{K}-{{K}}^{2}-1$
6 eluzge2nn0 ${⊢}{K}\in {ℤ}_{\ge 2}\to {K}\in {ℕ}_{0}$
7 6 3ad2ant2 ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {K}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\to {K}\in {ℕ}_{0}$
8 7 adantr ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {K}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\wedge {K}{Y}_{\mathrm{rm}}\left({N}+1\right)\le {A}\right)\to {K}\in {ℕ}_{0}$
9 3 nnnn0d ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {K}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\wedge {K}{Y}_{\mathrm{rm}}\left({N}+1\right)\le {A}\right)\to {N}\in {ℕ}_{0}$
10 jm2.18 ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left(2{A}{K}-{{K}}^{2}-1\right)\parallel \left(\left({A}{X}_{\mathrm{rm}}{N}\right)-\left({A}-{K}\right)\left({A}{Y}_{\mathrm{rm}}{N}\right)-{{K}}^{{N}}\right)$
11 1 8 9 10 syl3anc ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {K}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\wedge {K}{Y}_{\mathrm{rm}}\left({N}+1\right)\le {A}\right)\to \left(2{A}{K}-{{K}}^{2}-1\right)\parallel \left(\left({A}{X}_{\mathrm{rm}}{N}\right)-\left({A}-{K}\right)\left({A}{Y}_{\mathrm{rm}}{N}\right)-{{K}}^{{N}}\right)$
12 simp1 ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {K}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\to {A}\in {ℤ}_{\ge 2}$
13 nnz ${⊢}{N}\in ℕ\to {N}\in ℤ$
14 13 3ad2ant3 ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {K}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\to {N}\in ℤ$
15 frmx ${⊢}{X}_{\mathrm{rm}}:{ℤ}_{\ge 2}×ℤ⟶{ℕ}_{0}$
16 15 fovcl ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to {A}{X}_{\mathrm{rm}}{N}\in {ℕ}_{0}$
17 12 14 16 syl2anc ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {K}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\to {A}{X}_{\mathrm{rm}}{N}\in {ℕ}_{0}$
18 17 nn0zd ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {K}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\to {A}{X}_{\mathrm{rm}}{N}\in ℤ$
19 eluzelz ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}\in ℤ$
20 eluzelz ${⊢}{K}\in {ℤ}_{\ge 2}\to {K}\in ℤ$
21 zsubcl ${⊢}\left({A}\in ℤ\wedge {K}\in ℤ\right)\to {A}-{K}\in ℤ$
22 19 20 21 syl2an ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {K}\in {ℤ}_{\ge 2}\right)\to {A}-{K}\in ℤ$
23 22 3adant3 ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {K}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\to {A}-{K}\in ℤ$
24 frmy ${⊢}{Y}_{\mathrm{rm}}:{ℤ}_{\ge 2}×ℤ⟶ℤ$
25 24 fovcl ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to {A}{Y}_{\mathrm{rm}}{N}\in ℤ$
26 12 14 25 syl2anc ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {K}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\to {A}{Y}_{\mathrm{rm}}{N}\in ℤ$
27 23 26 zmulcld ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {K}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\to \left({A}-{K}\right)\left({A}{Y}_{\mathrm{rm}}{N}\right)\in ℤ$
28 18 27 zsubcld ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {K}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\to \left({A}{X}_{\mathrm{rm}}{N}\right)-\left({A}-{K}\right)\left({A}{Y}_{\mathrm{rm}}{N}\right)\in ℤ$
29 28 adantr ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {K}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\wedge {K}{Y}_{\mathrm{rm}}\left({N}+1\right)\le {A}\right)\to \left({A}{X}_{\mathrm{rm}}{N}\right)-\left({A}-{K}\right)\left({A}{Y}_{\mathrm{rm}}{N}\right)\in ℤ$
30 1 2 3 4 jm3.1lem3 ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {K}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\wedge {K}{Y}_{\mathrm{rm}}\left({N}+1\right)\le {A}\right)\to 2{A}{K}-{{K}}^{2}-1\in ℕ$
31 nnnn0 ${⊢}{N}\in ℕ\to {N}\in {ℕ}_{0}$
32 31 3ad2ant3 ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {K}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\to {N}\in {ℕ}_{0}$
33 7 32 nn0expcld ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {K}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\to {{K}}^{{N}}\in {ℕ}_{0}$
34 33 adantr ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {K}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\wedge {K}{Y}_{\mathrm{rm}}\left({N}+1\right)\le {A}\right)\to {{K}}^{{N}}\in {ℕ}_{0}$
35 divalgmodcl ${⊢}\left(\left({A}{X}_{\mathrm{rm}}{N}\right)-\left({A}-{K}\right)\left({A}{Y}_{\mathrm{rm}}{N}\right)\in ℤ\wedge 2{A}{K}-{{K}}^{2}-1\in ℕ\wedge {{K}}^{{N}}\in {ℕ}_{0}\right)\to \left({{K}}^{{N}}=\left(\left({A}{X}_{\mathrm{rm}}{N}\right)-\left({A}-{K}\right)\left({A}{Y}_{\mathrm{rm}}{N}\right)\right)\mathrm{mod}\left(2{A}{K}-{{K}}^{2}-1\right)↔\left({{K}}^{{N}}<2{A}{K}-{{K}}^{2}-1\wedge \left(2{A}{K}-{{K}}^{2}-1\right)\parallel \left(\left({A}{X}_{\mathrm{rm}}{N}\right)-\left({A}-{K}\right)\left({A}{Y}_{\mathrm{rm}}{N}\right)-{{K}}^{{N}}\right)\right)\right)$
36 29 30 34 35 syl3anc ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {K}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\wedge {K}{Y}_{\mathrm{rm}}\left({N}+1\right)\le {A}\right)\to \left({{K}}^{{N}}=\left(\left({A}{X}_{\mathrm{rm}}{N}\right)-\left({A}-{K}\right)\left({A}{Y}_{\mathrm{rm}}{N}\right)\right)\mathrm{mod}\left(2{A}{K}-{{K}}^{2}-1\right)↔\left({{K}}^{{N}}<2{A}{K}-{{K}}^{2}-1\wedge \left(2{A}{K}-{{K}}^{2}-1\right)\parallel \left(\left({A}{X}_{\mathrm{rm}}{N}\right)-\left({A}-{K}\right)\left({A}{Y}_{\mathrm{rm}}{N}\right)-{{K}}^{{N}}\right)\right)\right)$
37 5 11 36 mpbir2and ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {K}\in {ℤ}_{\ge 2}\wedge {N}\in ℕ\right)\wedge {K}{Y}_{\mathrm{rm}}\left({N}+1\right)\le {A}\right)\to {{K}}^{{N}}=\left(\left({A}{X}_{\mathrm{rm}}{N}\right)-\left({A}-{K}\right)\left({A}{Y}_{\mathrm{rm}}{N}\right)\right)\mathrm{mod}\left(2{A}{K}-{{K}}^{2}-1\right)$