expdioph

Description: The exponential function is Diophantine. This result completes and encapsulates our development using Pell equation solution sequences and is sometimes regarded as Matiyasevich's theorem properly. (Contributed by Stefan O'Rear, 17-Oct-2014)

		Ref	Expression
	Assertion	expdioph	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (3) = {a (1)}^{a (2)}\} \in Dioph (3)$

Proof

Step	Hyp	Ref	Expression
1		pm4.42	$⊢ a (3) = {a (1)}^{a (2)} \leftrightarrow ((a (3) = {a (1)}^{a (2)} \land a (2) \in ℕ) \lor (a (3) = {a (1)}^{a (2)} \land \neg a (2) \in ℕ))$
2		ancom	$⊢ (a (3) = {a (1)}^{a (2)} \land a (2) \in ℕ) \leftrightarrow (a (2) \in ℕ \land a (3) = {a (1)}^{a (2)})$
3		elmapi	$⊢ a \in ({ℕ_{0}}^{(1 \dots 3)}) \to a : (1 \dots 3) ⟶ ℕ_{0}$
4		df-2	$⊢ 2 = 1 + 1$
5		df-3	$⊢ 3 = 2 + 1$
6		ssid	$⊢ (1 \dots 3) \subseteq (1 \dots 3)$
7	5 6	jm2.27dlem5	$⊢ (1 \dots 2) \subseteq (1 \dots 3)$
8	4 7	jm2.27dlem5	$⊢ (1 \dots 1) \subseteq (1 \dots 3)$
9		1nn	$⊢ 1 \in ℕ$
10	9	jm2.27dlem3	$⊢ 1 \in (1 \dots 1)$
11	8 10	sselii	$⊢ 1 \in (1 \dots 3)$
12		ffvelcdm	$⊢ (a : (1 \dots 3) ⟶ ℕ_{0} \land 1 \in (1 \dots 3)) \to a (1) \in ℕ_{0}$
13	3 11 12	sylancl	$⊢ a \in ({ℕ_{0}}^{(1 \dots 3)}) \to a (1) \in ℕ_{0}$
14	13	adantr	$⊢ (a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (2) \in ℕ) \to a (1) \in ℕ_{0}$
15		elnn0	$⊢ a (1) \in ℕ_{0} \leftrightarrow (a (1) \in ℕ \lor a (1) = 0)$
16	14 15	sylib	$⊢ (a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (2) \in ℕ) \to (a (1) \in ℕ \lor a (1) = 0)$
17		elnn1uz2	$⊢ a (1) \in ℕ \leftrightarrow (a (1) = 1 \lor a (1) \in ℤ_{\geq 2})$
18	17	biimpi	$⊢ a (1) \in ℕ \to (a (1) = 1 \lor a (1) \in ℤ_{\geq 2})$
19	18	orim1i	$⊢ (a (1) \in ℕ \lor a (1) = 0) \to ((a (1) = 1 \lor a (1) \in ℤ_{\geq 2}) \lor a (1) = 0)$
20	16 19	syl	$⊢ (a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (2) \in ℕ) \to ((a (1) = 1 \lor a (1) \in ℤ_{\geq 2}) \lor a (1) = 0)$
21	20	biantrurd	$⊢ (a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (2) \in ℕ) \to (a (3) = {a (1)}^{a (2)} \leftrightarrow (((a (1) = 1 \lor a (1) \in ℤ_{\geq 2}) \lor a (1) = 0) \land a (3) = {a (1)}^{a (2)}))$
22		andir	$⊢ (((a (1) = 1 \lor a (1) \in ℤ_{\geq 2}) \lor a (1) = 0) \land a (3) = {a (1)}^{a (2)}) \leftrightarrow (((a (1) = 1 \lor a (1) \in ℤ_{\geq 2}) \land a (3) = {a (1)}^{a (2)}) \lor (a (1) = 0 \land a (3) = {a (1)}^{a (2)}))$
23		andir	$⊢ ((a (1) = 1 \lor a (1) \in ℤ_{\geq 2}) \land a (3) = {a (1)}^{a (2)}) \leftrightarrow ((a (1) = 1 \land a (3) = {a (1)}^{a (2)}) \lor (a (1) \in ℤ_{\geq 2} \land a (3) = {a (1)}^{a (2)}))$
24	23	orbi1i	$⊢ (((a (1) = 1 \lor a (1) \in ℤ_{\geq 2}) \land a (3) = {a (1)}^{a (2)}) \lor (a (1) = 0 \land a (3) = {a (1)}^{a (2)})) \leftrightarrow (((a (1) = 1 \land a (3) = {a (1)}^{a (2)}) \lor (a (1) \in ℤ_{\geq 2} \land a (3) = {a (1)}^{a (2)})) \lor (a (1) = 0 \land a (3) = {a (1)}^{a (2)}))$
25	22 24	bitri	$⊢ (((a (1) = 1 \lor a (1) \in ℤ_{\geq 2}) \lor a (1) = 0) \land a (3) = {a (1)}^{a (2)}) \leftrightarrow (((a (1) = 1 \land a (3) = {a (1)}^{a (2)}) \lor (a (1) \in ℤ_{\geq 2} \land a (3) = {a (1)}^{a (2)})) \lor (a (1) = 0 \land a (3) = {a (1)}^{a (2)}))$
26		nnz	$⊢ a (2) \in ℕ \to a (2) \in ℤ$
27		1exp	$⊢ a (2) \in ℤ \to 1^{a (2)} = 1$
28	26 27	syl	$⊢ a (2) \in ℕ \to 1^{a (2)} = 1$
29	28	adantl	$⊢ (a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (2) \in ℕ) \to 1^{a (2)} = 1$
30	29	eqeq2d	$⊢ (a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (2) \in ℕ) \to (a (3) = 1^{a (2)} \leftrightarrow a (3) = 1)$
31		oveq1	$⊢ a (1) = 1 \to {a (1)}^{a (2)} = 1^{a (2)}$
32	31	eqeq2d	$⊢ a (1) = 1 \to (a (3) = {a (1)}^{a (2)} \leftrightarrow a (3) = 1^{a (2)})$
33	32	bibi1d	$⊢ a (1) = 1 \to ((a (3) = {a (1)}^{a (2)} \leftrightarrow a (3) = 1) \leftrightarrow (a (3) = 1^{a (2)} \leftrightarrow a (3) = 1))$
34	30 33	syl5ibrcom	$⊢ (a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (2) \in ℕ) \to (a (1) = 1 \to (a (3) = {a (1)}^{a (2)} \leftrightarrow a (3) = 1))$
35	34	pm5.32d	$⊢ (a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (2) \in ℕ) \to ((a (1) = 1 \land a (3) = {a (1)}^{a (2)}) \leftrightarrow (a (1) = 1 \land a (3) = 1))$
36		iba	$⊢ a (2) \in ℕ \to (a (1) \in ℤ_{\geq 2} \leftrightarrow (a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ))$
37	36	adantl	$⊢ (a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (2) \in ℕ) \to (a (1) \in ℤ_{\geq 2} \leftrightarrow (a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ))$
38	37	anbi1d	$⊢ (a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (2) \in ℕ) \to ((a (1) \in ℤ_{\geq 2} \land a (3) = {a (1)}^{a (2)}) \leftrightarrow ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land a (3) = {a (1)}^{a (2)}))$
39	35 38	orbi12d	$⊢ (a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (2) \in ℕ) \to (((a (1) = 1 \land a (3) = {a (1)}^{a (2)}) \lor (a (1) \in ℤ_{\geq 2} \land a (3) = {a (1)}^{a (2)})) \leftrightarrow ((a (1) = 1 \land a (3) = 1) \lor ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land a (3) = {a (1)}^{a (2)})))$
40		0exp	$⊢ a (2) \in ℕ \to 0^{a (2)} = 0$
41	40	adantl	$⊢ (a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (2) \in ℕ) \to 0^{a (2)} = 0$
42	41	eqeq2d	$⊢ (a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (2) \in ℕ) \to (a (3) = 0^{a (2)} \leftrightarrow a (3) = 0)$
43		oveq1	$⊢ a (1) = 0 \to {a (1)}^{a (2)} = 0^{a (2)}$
44	43	eqeq2d	$⊢ a (1) = 0 \to (a (3) = {a (1)}^{a (2)} \leftrightarrow a (3) = 0^{a (2)})$
45	44	bibi1d	$⊢ a (1) = 0 \to ((a (3) = {a (1)}^{a (2)} \leftrightarrow a (3) = 0) \leftrightarrow (a (3) = 0^{a (2)} \leftrightarrow a (3) = 0))$
46	42 45	syl5ibrcom	$⊢ (a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (2) \in ℕ) \to (a (1) = 0 \to (a (3) = {a (1)}^{a (2)} \leftrightarrow a (3) = 0))$
47	46	pm5.32d	$⊢ (a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (2) \in ℕ) \to ((a (1) = 0 \land a (3) = {a (1)}^{a (2)}) \leftrightarrow (a (1) = 0 \land a (3) = 0))$
48	39 47	orbi12d	$⊢ (a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (2) \in ℕ) \to ((((a (1) = 1 \land a (3) = {a (1)}^{a (2)}) \lor (a (1) \in ℤ_{\geq 2} \land a (3) = {a (1)}^{a (2)})) \lor (a (1) = 0 \land a (3) = {a (1)}^{a (2)})) \leftrightarrow (((a (1) = 1 \land a (3) = 1) \lor ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land a (3) = {a (1)}^{a (2)})) \lor (a (1) = 0 \land a (3) = 0)))$
49	25 48	bitrid	$⊢ (a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (2) \in ℕ) \to ((((a (1) = 1 \lor a (1) \in ℤ_{\geq 2}) \lor a (1) = 0) \land a (3) = {a (1)}^{a (2)}) \leftrightarrow (((a (1) = 1 \land a (3) = 1) \lor ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land a (3) = {a (1)}^{a (2)})) \lor (a (1) = 0 \land a (3) = 0)))$
50	21 49	bitrd	$⊢ (a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (2) \in ℕ) \to (a (3) = {a (1)}^{a (2)} \leftrightarrow (((a (1) = 1 \land a (3) = 1) \lor ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land a (3) = {a (1)}^{a (2)})) \lor (a (1) = 0 \land a (3) = 0)))$
51	50	pm5.32da	$⊢ a \in ({ℕ_{0}}^{(1 \dots 3)}) \to ((a (2) \in ℕ \land a (3) = {a (1)}^{a (2)}) \leftrightarrow (a (2) \in ℕ \land (((a (1) = 1 \land a (3) = 1) \lor ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land a (3) = {a (1)}^{a (2)})) \lor (a (1) = 0 \land a (3) = 0))))$
52	2 51	bitrid	$⊢ a \in ({ℕ_{0}}^{(1 \dots 3)}) \to ((a (3) = {a (1)}^{a (2)} \land a (2) \in ℕ) \leftrightarrow (a (2) \in ℕ \land (((a (1) = 1 \land a (3) = 1) \lor ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land a (3) = {a (1)}^{a (2)})) \lor (a (1) = 0 \land a (3) = 0))))$
53		ancom	$⊢ (a (3) = {a (1)}^{a (2)} \land \neg a (2) \in ℕ) \leftrightarrow (\neg a (2) \in ℕ \land a (3) = {a (1)}^{a (2)})$
54		2nn	$⊢ 2 \in ℕ$
55	54	jm2.27dlem3	$⊢ 2 \in (1 \dots 2)$
56	7 55	sselii	$⊢ 2 \in (1 \dots 3)$
57		ffvelcdm	$⊢ (a : (1 \dots 3) ⟶ ℕ_{0} \land 2 \in (1 \dots 3)) \to a (2) \in ℕ_{0}$
58	3 56 57	sylancl	$⊢ a \in ({ℕ_{0}}^{(1 \dots 3)}) \to a (2) \in ℕ_{0}$
59		elnn0	$⊢ a (2) \in ℕ_{0} \leftrightarrow (a (2) \in ℕ \lor a (2) = 0)$
60		pm2.53	$⊢ (a (2) \in ℕ \lor a (2) = 0) \to (\neg a (2) \in ℕ \to a (2) = 0)$
61	59 60	sylbi	$⊢ a (2) \in ℕ_{0} \to (\neg a (2) \in ℕ \to a (2) = 0)$
62		0nnn	$⊢ \neg 0 \in ℕ$
63		eleq1	$⊢ a (2) = 0 \to (a (2) \in ℕ \leftrightarrow 0 \in ℕ)$
64	62 63	mtbiri	$⊢ a (2) = 0 \to \neg a (2) \in ℕ$
65	61 64	impbid1	$⊢ a (2) \in ℕ_{0} \to (\neg a (2) \in ℕ \leftrightarrow a (2) = 0)$
66	58 65	syl	$⊢ a \in ({ℕ_{0}}^{(1 \dots 3)}) \to (\neg a (2) \in ℕ \leftrightarrow a (2) = 0)$
67	66	anbi1d	$⊢ a \in ({ℕ_{0}}^{(1 \dots 3)}) \to ((\neg a (2) \in ℕ \land a (3) = {a (1)}^{a (2)}) \leftrightarrow (a (2) = 0 \land a (3) = {a (1)}^{a (2)}))$
68	13	nn0cnd	$⊢ a \in ({ℕ_{0}}^{(1 \dots 3)}) \to a (1) \in ℂ$
69	68	exp0d	$⊢ a \in ({ℕ_{0}}^{(1 \dots 3)}) \to {a (1)}^{0} = 1$
70	69	eqeq2d	$⊢ a \in ({ℕ_{0}}^{(1 \dots 3)}) \to (a (3) = {a (1)}^{0} \leftrightarrow a (3) = 1)$
71		oveq2	$⊢ a (2) = 0 \to {a (1)}^{a (2)} = {a (1)}^{0}$
72	71	eqeq2d	$⊢ a (2) = 0 \to (a (3) = {a (1)}^{a (2)} \leftrightarrow a (3) = {a (1)}^{0})$
73	72	bibi1d	$⊢ a (2) = 0 \to ((a (3) = {a (1)}^{a (2)} \leftrightarrow a (3) = 1) \leftrightarrow (a (3) = {a (1)}^{0} \leftrightarrow a (3) = 1))$
74	70 73	syl5ibrcom	$⊢ a \in ({ℕ_{0}}^{(1 \dots 3)}) \to (a (2) = 0 \to (a (3) = {a (1)}^{a (2)} \leftrightarrow a (3) = 1))$
75	74	pm5.32d	$⊢ a \in ({ℕ_{0}}^{(1 \dots 3)}) \to ((a (2) = 0 \land a (3) = {a (1)}^{a (2)}) \leftrightarrow (a (2) = 0 \land a (3) = 1))$
76	67 75	bitrd	$⊢ a \in ({ℕ_{0}}^{(1 \dots 3)}) \to ((\neg a (2) \in ℕ \land a (3) = {a (1)}^{a (2)}) \leftrightarrow (a (2) = 0 \land a (3) = 1))$
77	53 76	bitrid	$⊢ a \in ({ℕ_{0}}^{(1 \dots 3)}) \to ((a (3) = {a (1)}^{a (2)} \land \neg a (2) \in ℕ) \leftrightarrow (a (2) = 0 \land a (3) = 1))$
78	52 77	orbi12d	$⊢ a \in ({ℕ_{0}}^{(1 \dots 3)}) \to (((a (3) = {a (1)}^{a (2)} \land a (2) \in ℕ) \lor (a (3) = {a (1)}^{a (2)} \land \neg a (2) \in ℕ)) \leftrightarrow ((a (2) \in ℕ \land (((a (1) = 1 \land a (3) = 1) \lor ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land a (3) = {a (1)}^{a (2)})) \lor (a (1) = 0 \land a (3) = 0))) \lor (a (2) = 0 \land a (3) = 1)))$
79	1 78	bitrid	$⊢ a \in ({ℕ_{0}}^{(1 \dots 3)}) \to (a (3) = {a (1)}^{a (2)} \leftrightarrow ((a (2) \in ℕ \land (((a (1) = 1 \land a (3) = 1) \lor ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land a (3) = {a (1)}^{a (2)})) \lor (a (1) = 0 \land a (3) = 0))) \lor (a (2) = 0 \land a (3) = 1)))$
80	79	rabbiia	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (3) = {a (1)}^{a (2)}\} = \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| ((a (2) \in ℕ \land (((a (1) = 1 \land a (3) = 1) \lor ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land a (3) = {a (1)}^{a (2)})) \lor (a (1) = 0 \land a (3) = 0))) \lor (a (2) = 0 \land a (3) = 1))\}$
81		3nn0	$⊢ 3 \in ℕ_{0}$
82		ovex	$⊢ (1 \dots 3) \in V$
83		mzpproj	$⊢ ((1 \dots 3) \in V \land 2 \in (1 \dots 3)) \to (a \in (ℤ^{(1 \dots 3)}) ⟼ a (2)) \in mzPoly ((1 \dots 3))$
84	82 56 83	mp2an	$⊢ (a \in (ℤ^{(1 \dots 3)}) ⟼ a (2)) \in mzPoly ((1 \dots 3))$
85		elnnrabdioph	$⊢ (3 \in ℕ_{0} \land (a \in (ℤ^{(1 \dots 3)}) ⟼ a (2)) \in mzPoly ((1 \dots 3))) \to \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (2) \in ℕ\} \in Dioph (3)$
86	81 84 85	mp2an	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (2) \in ℕ\} \in Dioph (3)$
87		mzpproj	$⊢ ((1 \dots 3) \in V \land 1 \in (1 \dots 3)) \to (a \in (ℤ^{(1 \dots 3)}) ⟼ a (1)) \in mzPoly ((1 \dots 3))$
88	82 11 87	mp2an	$⊢ (a \in (ℤ^{(1 \dots 3)}) ⟼ a (1)) \in mzPoly ((1 \dots 3))$
89		1z	$⊢ 1 \in ℤ$
90		mzpconstmpt	$⊢ ((1 \dots 3) \in V \land 1 \in ℤ) \to (a \in (ℤ^{(1 \dots 3)}) ⟼ 1) \in mzPoly ((1 \dots 3))$
91	82 89 90	mp2an	$⊢ (a \in (ℤ^{(1 \dots 3)}) ⟼ 1) \in mzPoly ((1 \dots 3))$
92		eqrabdioph	$⊢ (3 \in ℕ_{0} \land (a \in (ℤ^{(1 \dots 3)}) ⟼ a (1)) \in mzPoly ((1 \dots 3)) \land (a \in (ℤ^{(1 \dots 3)}) ⟼ 1) \in mzPoly ((1 \dots 3))) \to \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (1) = 1\} \in Dioph (3)$
93	81 88 91 92	mp3an	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (1) = 1\} \in Dioph (3)$
94		3nn	$⊢ 3 \in ℕ$
95	94	jm2.27dlem3	$⊢ 3 \in (1 \dots 3)$
96		mzpproj	$⊢ ((1 \dots 3) \in V \land 3 \in (1 \dots 3)) \to (a \in (ℤ^{(1 \dots 3)}) ⟼ a (3)) \in mzPoly ((1 \dots 3))$
97	82 95 96	mp2an	$⊢ (a \in (ℤ^{(1 \dots 3)}) ⟼ a (3)) \in mzPoly ((1 \dots 3))$
98		eqrabdioph	$⊢ (3 \in ℕ_{0} \land (a \in (ℤ^{(1 \dots 3)}) ⟼ a (3)) \in mzPoly ((1 \dots 3)) \land (a \in (ℤ^{(1 \dots 3)}) ⟼ 1) \in mzPoly ((1 \dots 3))) \to \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (3) = 1\} \in Dioph (3)$
99	81 97 91 98	mp3an	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (3) = 1\} \in Dioph (3)$
100		anrabdioph	$⊢ (\{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (1) = 1\} \in Dioph (3) \land \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (3) = 1\} \in Dioph (3)) \to \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (1) = 1 \land a (3) = 1)\} \in Dioph (3)$
101	93 99 100	mp2an	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (1) = 1 \land a (3) = 1)\} \in Dioph (3)$
102		expdiophlem2	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land a (3) = {a (1)}^{a (2)})\} \in Dioph (3)$
103		orrabdioph	$⊢ (\{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (1) = 1 \land a (3) = 1)\} \in Dioph (3) \land \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land a (3) = {a (1)}^{a (2)})\} \in Dioph (3)) \to \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| ((a (1) = 1 \land a (3) = 1) \lor ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land a (3) = {a (1)}^{a (2)}))\} \in Dioph (3)$
104	101 102 103	mp2an	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| ((a (1) = 1 \land a (3) = 1) \lor ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land a (3) = {a (1)}^{a (2)}))\} \in Dioph (3)$
105		eq0rabdioph	$⊢ (3 \in ℕ_{0} \land (a \in (ℤ^{(1 \dots 3)}) ⟼ a (1)) \in mzPoly ((1 \dots 3))) \to \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (1) = 0\} \in Dioph (3)$
106	81 88 105	mp2an	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (1) = 0\} \in Dioph (3)$
107		eq0rabdioph	$⊢ (3 \in ℕ_{0} \land (a \in (ℤ^{(1 \dots 3)}) ⟼ a (3)) \in mzPoly ((1 \dots 3))) \to \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (3) = 0\} \in Dioph (3)$
108	81 97 107	mp2an	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (3) = 0\} \in Dioph (3)$
109		anrabdioph	$⊢ (\{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (1) = 0\} \in Dioph (3) \land \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (3) = 0\} \in Dioph (3)) \to \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (1) = 0 \land a (3) = 0)\} \in Dioph (3)$
110	106 108 109	mp2an	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (1) = 0 \land a (3) = 0)\} \in Dioph (3)$
111		orrabdioph	$⊢ (\{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| ((a (1) = 1 \land a (3) = 1) \lor ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land a (3) = {a (1)}^{a (2)}))\} \in Dioph (3) \land \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (1) = 0 \land a (3) = 0)\} \in Dioph (3)) \to \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (((a (1) = 1 \land a (3) = 1) \lor ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land a (3) = {a (1)}^{a (2)})) \lor (a (1) = 0 \land a (3) = 0))\} \in Dioph (3)$
112	104 110 111	mp2an	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (((a (1) = 1 \land a (3) = 1) \lor ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land a (3) = {a (1)}^{a (2)})) \lor (a (1) = 0 \land a (3) = 0))\} \in Dioph (3)$
113		anrabdioph	$⊢ (\{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (2) \in ℕ\} \in Dioph (3) \land \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (((a (1) = 1 \land a (3) = 1) \lor ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land a (3) = {a (1)}^{a (2)})) \lor (a (1) = 0 \land a (3) = 0))\} \in Dioph (3)) \to \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (2) \in ℕ \land (((a (1) = 1 \land a (3) = 1) \lor ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land a (3) = {a (1)}^{a (2)})) \lor (a (1) = 0 \land a (3) = 0)))\} \in Dioph (3)$
114	86 112 113	mp2an	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (2) \in ℕ \land (((a (1) = 1 \land a (3) = 1) \lor ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land a (3) = {a (1)}^{a (2)})) \lor (a (1) = 0 \land a (3) = 0)))\} \in Dioph (3)$
115		eq0rabdioph	$⊢ (3 \in ℕ_{0} \land (a \in (ℤ^{(1 \dots 3)}) ⟼ a (2)) \in mzPoly ((1 \dots 3))) \to \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (2) = 0\} \in Dioph (3)$
116	81 84 115	mp2an	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (2) = 0\} \in Dioph (3)$
117		anrabdioph	$⊢ (\{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (2) = 0\} \in Dioph (3) \land \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (3) = 1\} \in Dioph (3)) \to \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (2) = 0 \land a (3) = 1)\} \in Dioph (3)$
118	116 99 117	mp2an	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (2) = 0 \land a (3) = 1)\} \in Dioph (3)$
119		orrabdioph	$⊢ (\{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (2) \in ℕ \land (((a (1) = 1 \land a (3) = 1) \lor ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land a (3) = {a (1)}^{a (2)})) \lor (a (1) = 0 \land a (3) = 0)))\} \in Dioph (3) \land \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (2) = 0 \land a (3) = 1)\} \in Dioph (3)) \to \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| ((a (2) \in ℕ \land (((a (1) = 1 \land a (3) = 1) \lor ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land a (3) = {a (1)}^{a (2)})) \lor (a (1) = 0 \land a (3) = 0))) \lor (a (2) = 0 \land a (3) = 1))\} \in Dioph (3)$
120	114 118 119	mp2an	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| ((a (2) \in ℕ \land (((a (1) = 1 \land a (3) = 1) \lor ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land a (3) = {a (1)}^{a (2)})) \lor (a (1) = 0 \land a (3) = 0))) \lor (a (2) = 0 \land a (3) = 1))\} \in Dioph (3)$
121	80 120	eqeltri	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (3) = {a (1)}^{a (2)}\} \in Dioph (3)$

Metamath Proof Explorer

Theorem expdioph

Proof