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 \in ℤ_{\geq 2} \land K \in ℤ_{\geq 2} \land N \in ℕ) \land K Y_{rm} (N + 1) \leq A) \to K^{N} = ((A X_{rm} N) - (A - K) (A Y_{rm} N)) \mod (2 A K - K^{2} - 1)$

Proof

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

Metamath Proof Explorer

Theorem jm3.1

Proof