Theorem jm3.1 40828

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

Assertion

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

Proof of Theorem jm3.1

Step	Hyp	Ref	Expression
1		simpl1 1190	. . 3 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴) → 𝐴 ∈ (ℤ≥‘2))
2		simpl2 1191	. . 3 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴) → 𝐾 ∈ (ℤ≥‘2))
3		simpl3 1192	. . 3 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴) → 𝑁 ∈ ℕ)
4		simpr 485	. . 3 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴) → (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴)
5	1, 2, 3, 4	jm3.1lem2 40826	. 2 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴) → (𝐾↑𝑁) < ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1))
6		eluzge2nn0 12615	. . . . 5 ⊢ (𝐾 ∈ (ℤ≥‘2) → 𝐾 ∈ ℕ0)
7	6	3ad2ant2 1133	. . . 4 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) → 𝐾 ∈ ℕ0)
8	7	adantr 481	. . 3 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴) → 𝐾 ∈ ℕ0)
9	3	nnnn0d 12281	. . 3 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴) → 𝑁 ∈ ℕ0)
10		jm2.18 40796	. . 3 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑁) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑁))) − (𝐾↑𝑁)))
11	1, 8, 9, 10	syl3anc 1370	. 2 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑁) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑁))) − (𝐾↑𝑁)))
12		simp1 1135	. . . . . . 7 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) → 𝐴 ∈ (ℤ≥‘2))
13		nnz 12330	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
14	13	3ad2ant3 1134	. . . . . . 7 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℤ)
15		frmx 40721	. . . . . . . 8 ⊢ Xrm :((ℤ≥‘2) × ℤ)⟶ℕ0
16	15	fovcl 7393	. . . . . . 7 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) ∈ ℕ0)
17	12, 14, 16	syl2anc 584	. . . . . 6 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) → (𝐴 Xrm 𝑁) ∈ ℕ0)
18	17	nn0zd 12412	. . . . 5 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) → (𝐴 Xrm 𝑁) ∈ ℤ)
19		eluzelz 12580	. . . . . . . 8 ⊢ (𝐴 ∈ (ℤ≥‘2) → 𝐴 ∈ ℤ)
20		eluzelz 12580	. . . . . . . 8 ⊢ (𝐾 ∈ (ℤ≥‘2) → 𝐾 ∈ ℤ)
21		zsubcl 12350	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐴 − 𝐾) ∈ ℤ)
22	19, 20, 21	syl2an 596	. . . . . . 7 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ (ℤ≥‘2)) → (𝐴 − 𝐾) ∈ ℤ)
23	22	3adant3 1131	. . . . . 6 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) → (𝐴 − 𝐾) ∈ ℤ)
24		frmy 40722	. . . . . . . 8 ⊢ Yrm :((ℤ≥‘2) × ℤ)⟶ℤ
25	24	fovcl 7393	. . . . . . 7 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑁) ∈ ℤ)
26	12, 14, 25	syl2anc 584	. . . . . 6 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm 𝑁) ∈ ℤ)
27	23, 26	zmulcld 12420	. . . . 5 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) → ((𝐴 − 𝐾) · (𝐴 Yrm 𝑁)) ∈ ℤ)
28	18, 27	zsubcld 12419	. . . 4 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) → ((𝐴 Xrm 𝑁) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑁))) ∈ ℤ)
29	28	adantr 481	. . 3 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴) → ((𝐴 Xrm 𝑁) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑁))) ∈ ℤ)
30	1, 2, 3, 4	jm3.1lem3 40827	. . 3 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∈ ℕ)
31		nnnn0 12228	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
32	31	3ad2ant3 1134	. . . . 5 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℕ0)
33	7, 32	nn0expcld 13949	. . . 4 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) → (𝐾↑𝑁) ∈ ℕ0)
34	33	adantr 481	. . 3 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴) → (𝐾↑𝑁) ∈ ℕ0)
35		divalgmodcl 16104	. . 3 ⊢ ((((𝐴 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 1370	. 2 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴) → ((𝐾↑𝑁) = (((𝐴 Xrm 𝑁) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑁))) mod ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1)) ↔ ((𝐾↑𝑁) < ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∧ ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑁) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑁))) − (𝐾↑𝑁)))))
37	5, 11, 36	mpbir2and 710	1 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴) → (𝐾↑𝑁) = (((𝐴 Xrm 𝑁) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑁))) mod ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1086   = wceq 1539   ∈ wcel 2106   class class class wbr 5074  ‘cfv 6427  (class class class)co 7268  1c1 10860   + caddc 10862   · cmul 10864   < clt 10997   ≤ cle 10998   − cmin 11193  ℕcn 11961  2c2 12016  ℕ₀cn0 12221  ℤcz 12307  ℤ_≥cuz 12570   mod cmo 13577  ↑cexp 13770   ∥ cdvds 15951   X_rm crmx 40708   Y_rm crmy 40709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5222  ax-nul 5229  ax-pow 5287  ax-pr 5351  ax-un 7579  ax-inf2 9387  ax-cnex 10915  ax-resscn 10916  ax-1cn 10917  ax-icn 10918  ax-addcl 10919  ax-addrcl 10920  ax-mulcl 10921  ax-mulrcl 10922  ax-mulcom 10923  ax-addass 10924  ax-mulass 10925  ax-distr 10926  ax-i2m1 10927  ax-1ne0 10928  ax-1rid 10929  ax-rnegex 10930  ax-rrecex 10931  ax-cnre 10932  ax-pre-lttri 10933  ax-pre-lttrn 10934  ax-pre-ltadd 10935  ax-pre-mulgt0 10936  ax-pre-sup 10937  ax-addf 10938  ax-mulf 10939

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3432  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-tp 4567  df-op 4569  df-uni 4841  df-int 4881  df-iun 4927  df-iin 4928  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5485  df-eprel 5491  df-po 5499  df-so 5500  df-fr 5540  df-se 5541  df-we 5542  df-xp 5591  df-rel 5592  df-cnv 5593  df-co 5594  df-dm 5595  df-rn 5596  df-res 5597  df-ima 5598  df-pred 6196  df-ord 6263  df-on 6264  df-lim 6265  df-suc 6266  df-iota 6385  df-fun 6429  df-fn 6430  df-f 6431  df-f1 6432  df-fo 6433  df-f1o 6434  df-fv 6435  df-isom 6436  df-riota 7225  df-ov 7271  df-oprab 7272  df-mpo 7273  df-of 7524  df-om 7704  df-1st 7821  df-2nd 7822  df-supp 7966  df-frecs 8085  df-wrecs 8116  df-recs 8190  df-rdg 8229  df-1o 8285  df-2o 8286  df-oadd 8289  df-omul 8290  df-er 8486  df-map 8605  df-pm 8606  df-ixp 8674  df-en 8722  df-dom 8723  df-sdom 8724  df-fin 8725  df-fsupp 9117  df-fi 9158  df-sup 9189  df-inf 9190  df-oi 9257  df-card 9685  df-acn 9688  df-pnf 10999  df-mnf 11000  df-xr 11001  df-ltxr 11002  df-le 11003  df-sub 11195  df-neg 11196  df-div 11621  df-nn 11962  df-2 12024  df-3 12025  df-4 12026  df-5 12027  df-6 12028  df-7 12029  df-8 12030  df-9 12031  df-n0 12222  df-xnn0 12294  df-z 12308  df-dec 12426  df-uz 12571  df-q 12677  df-rp 12719  df-xneg 12836  df-xadd 12837  df-xmul 12838  df-ioo 13071  df-ioc 13072  df-ico 13073  df-icc 13074  df-fz 13228  df-fzo 13371  df-fl 13500  df-mod 13578  df-seq 13710  df-exp 13771  df-fac 13976  df-bc 14005  df-hash 14033  df-shft 14766  df-cj 14798  df-re 14799  df-im 14800  df-sqrt 14934  df-abs 14935  df-limsup 15168  df-clim 15185  df-rlim 15186  df-sum 15386  df-ef 15765  df-sin 15767  df-cos 15768  df-pi 15770  df-dvds 15952  df-gcd 16190  df-numer 16427  df-denom 16428  df-struct 16836  df-sets 16853  df-slot 16871  df-ndx 16883  df-base 16901  df-ress 16930  df-plusg 16963  df-mulr 16964  df-starv 16965  df-sca 16966  df-vsca 16967  df-ip 16968  df-tset 16969  df-ple 16970  df-ds 16972  df-unif 16973  df-hom 16974  df-cco 16975  df-rest 17121  df-topn 17122  df-0g 17140  df-gsum 17141  df-topgen 17142  df-pt 17143  df-prds 17146  df-xrs 17201  df-qtop 17206  df-imas 17207  df-xps 17209  df-mre 17283  df-mrc 17284  df-acs 17286  df-mgm 18314  df-sgrp 18363  df-mnd 18374  df-submnd 18419  df-mulg 18689  df-cntz 18911  df-cmn 19376  df-psmet 20577  df-xmet 20578  df-met 20579  df-bl 20580  df-mopn 20581  df-fbas 20582  df-fg 20583  df-cnfld 20586  df-top 22031  df-topon 22048  df-topsp 22070  df-bases 22084  df-cld 22158  df-ntr 22159  df-cls 22160  df-nei 22237  df-lp 22275  df-perf 22276  df-cn 22366  df-cnp 22367  df-haus 22454  df-tx 22701  df-hmeo 22894  df-fil 22985  df-fm 23077  df-flim 23078  df-flf 23079  df-xms 23461  df-ms 23462  df-tms 23463  df-cncf 24029  df-limc 25018  df-dv 25019  df-log 25700  df-squarenn 40649  df-pell1qr 40650  df-pell14qr 40651  df-pell1234qr 40652  df-pellfund 40653  df-rmx 40710  df-rmy 40711

This theorem is referenced by:  expdiophlem1  40829