Metamath Proof Explorer

Theorem 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 { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) ↑ ( 𝑎 ‘ 2 ) ) } ∈ ( Dioph ‘ 3 )

Proof

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