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 { 𝑎 ∈ ( ℕ0m ( 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 ( 𝑎 ∈ ( ℕ0m ( 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 ffvelrn ( ( 𝑎 : ( 1 ... 3 ) ⟶ ℕ0 ∧ 1 ∈ ( 1 ... 3 ) ) → ( 𝑎 ‘ 1 ) ∈ ℕ0 )
13 3 11 12 sylancl ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) → ( 𝑎 ‘ 1 ) ∈ ℕ0 )
14 13 adantr ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( 𝑎 ‘ 1 ) ∈ ℕ0 )
15 elnn0 ( ( 𝑎 ‘ 1 ) ∈ ℕ0 ↔ ( ( 𝑎 ‘ 1 ) ∈ ℕ ∨ ( 𝑎 ‘ 1 ) = 0 ) )
16 14 15 sylib ( ( 𝑎 ∈ ( ℕ0m ( 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 ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( ( ( 𝑎 ‘ 1 ) = 1 ∨ ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ) ∨ ( 𝑎 ‘ 1 ) = 0 ) )
21 20 biantrurd ( ( 𝑎 ∈ ( ℕ0m ( 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 ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( 1 ↑ ( 𝑎 ‘ 2 ) ) = 1 )
30 29 eqeq2d ( ( 𝑎 ∈ ( ℕ0m ( 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 ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( ( 𝑎 ‘ 1 ) = 1 → ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) ↑ ( 𝑎 ‘ 2 ) ) ↔ ( 𝑎 ‘ 3 ) = 1 ) ) )
35 34 pm5.32d ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( ( ( 𝑎 ‘ 1 ) = 1 ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) ↑ ( 𝑎 ‘ 2 ) ) ) ↔ ( ( 𝑎 ‘ 1 ) = 1 ∧ ( 𝑎 ‘ 3 ) = 1 ) ) )
36 iba ( ( 𝑎 ‘ 2 ) ∈ ℕ → ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ↔ ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ) )
37 36 adantl ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ↔ ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ) )
38 37 anbi1d ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) ↑ ( 𝑎 ‘ 2 ) ) ) ↔ ( ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) ↑ ( 𝑎 ‘ 2 ) ) ) ) )
39 35 38 orbi12d ( ( 𝑎 ∈ ( ℕ0m ( 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 ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( 0 ↑ ( 𝑎 ‘ 2 ) ) = 0 )
42 41 eqeq2d ( ( 𝑎 ∈ ( ℕ0m ( 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 ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( ( 𝑎 ‘ 1 ) = 0 → ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) ↑ ( 𝑎 ‘ 2 ) ) ↔ ( 𝑎 ‘ 3 ) = 0 ) ) )
47 46 pm5.32d ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( ( ( 𝑎 ‘ 1 ) = 0 ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) ↑ ( 𝑎 ‘ 2 ) ) ) ↔ ( ( 𝑎 ‘ 1 ) = 0 ∧ ( 𝑎 ‘ 3 ) = 0 ) ) )
48 39 47 orbi12d ( ( 𝑎 ∈ ( ℕ0m ( 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 syl5bb ( ( 𝑎 ∈ ( ℕ0m ( 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 ( ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) → ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) ↑ ( 𝑎 ‘ 2 ) ) ↔ ( ( ( ( 𝑎 ‘ 1 ) = 1 ∧ ( 𝑎 ‘ 3 ) = 1 ) ∨ ( ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) ↑ ( 𝑎 ‘ 2 ) ) ) ) ∨ ( ( 𝑎 ‘ 1 ) = 0 ∧ ( 𝑎 ‘ 3 ) = 0 ) ) ) )
51 50 pm5.32da ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) → ( ( ( 𝑎 ‘ 2 ) ∈ ℕ ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) ↑ ( 𝑎 ‘ 2 ) ) ) ↔ ( ( 𝑎 ‘ 2 ) ∈ ℕ ∧ ( ( ( ( 𝑎 ‘ 1 ) = 1 ∧ ( 𝑎 ‘ 3 ) = 1 ) ∨ ( ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) ↑ ( 𝑎 ‘ 2 ) ) ) ) ∨ ( ( 𝑎 ‘ 1 ) = 0 ∧ ( 𝑎 ‘ 3 ) = 0 ) ) ) ) )
52 2 51 syl5bb ( 𝑎 ∈ ( ℕ0m ( 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 ffvelrn ( ( 𝑎 : ( 1 ... 3 ) ⟶ ℕ0 ∧ 2 ∈ ( 1 ... 3 ) ) → ( 𝑎 ‘ 2 ) ∈ ℕ0 )
58 3 56 57 sylancl ( 𝑎 ∈ ( ℕ0m ( 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 ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) → ( ¬ ( 𝑎 ‘ 2 ) ∈ ℕ ↔ ( 𝑎 ‘ 2 ) = 0 ) )
67 66 anbi1d ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) → ( ( ¬ ( 𝑎 ‘ 2 ) ∈ ℕ ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) ↑ ( 𝑎 ‘ 2 ) ) ) ↔ ( ( 𝑎 ‘ 2 ) = 0 ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) ↑ ( 𝑎 ‘ 2 ) ) ) ) )
68 13 nn0cnd ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) → ( 𝑎 ‘ 1 ) ∈ ℂ )
69 68 exp0d ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) → ( ( 𝑎 ‘ 1 ) ↑ 0 ) = 1 )
70 69 eqeq2d ( 𝑎 ∈ ( ℕ0m ( 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 ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) → ( ( 𝑎 ‘ 2 ) = 0 → ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) ↑ ( 𝑎 ‘ 2 ) ) ↔ ( 𝑎 ‘ 3 ) = 1 ) ) )
75 74 pm5.32d ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) → ( ( ( 𝑎 ‘ 2 ) = 0 ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) ↑ ( 𝑎 ‘ 2 ) ) ) ↔ ( ( 𝑎 ‘ 2 ) = 0 ∧ ( 𝑎 ‘ 3 ) = 1 ) ) )
76 67 75 bitrd ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) → ( ( ¬ ( 𝑎 ‘ 2 ) ∈ ℕ ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) ↑ ( 𝑎 ‘ 2 ) ) ) ↔ ( ( 𝑎 ‘ 2 ) = 0 ∧ ( 𝑎 ‘ 3 ) = 1 ) ) )
77 53 76 syl5bb ( 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) → ( ( ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) ↑ ( 𝑎 ‘ 2 ) ) ∧ ¬ ( 𝑎 ‘ 2 ) ∈ ℕ ) ↔ ( ( 𝑎 ‘ 2 ) = 0 ∧ ( 𝑎 ‘ 3 ) = 1 ) ) )
78 52 77 orbi12d ( 𝑎 ∈ ( ℕ0m ( 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 syl5bb ( 𝑎 ∈ ( ℕ0m ( 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 { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) ↑ ( 𝑎 ‘ 2 ) ) } = { 𝑎 ∈ ( ℕ0m ( 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 ) ) ) → { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 2 ) ∈ ℕ } ∈ ( Dioph ‘ 3 ) )
86 81 84 85 mp2an { 𝑎 ∈ ( ℕ0m ( 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 ) ) ) → { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 1 ) = 1 } ∈ ( Dioph ‘ 3 ) )
93 81 88 91 92 mp3an { 𝑎 ∈ ( ℕ0m ( 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 ) ) ) → { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 3 ) = 1 } ∈ ( Dioph ‘ 3 ) )
99 81 97 91 98 mp3an { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 3 ) = 1 } ∈ ( Dioph ‘ 3 )
100 anrabdioph ( ( { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 1 ) = 1 } ∈ ( Dioph ‘ 3 ) ∧ { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 3 ) = 1 } ∈ ( Dioph ‘ 3 ) ) → { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( ( 𝑎 ‘ 1 ) = 1 ∧ ( 𝑎 ‘ 3 ) = 1 ) } ∈ ( Dioph ‘ 3 ) )
101 93 99 100 mp2an { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( ( 𝑎 ‘ 1 ) = 1 ∧ ( 𝑎 ‘ 3 ) = 1 ) } ∈ ( Dioph ‘ 3 )
102 expdiophlem2 { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) ↑ ( 𝑎 ‘ 2 ) ) ) } ∈ ( Dioph ‘ 3 )
103 orrabdioph ( ( { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( ( 𝑎 ‘ 1 ) = 1 ∧ ( 𝑎 ‘ 3 ) = 1 ) } ∈ ( Dioph ‘ 3 ) ∧ { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) ↑ ( 𝑎 ‘ 2 ) ) ) } ∈ ( Dioph ‘ 3 ) ) → { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( ( ( 𝑎 ‘ 1 ) = 1 ∧ ( 𝑎 ‘ 3 ) = 1 ) ∨ ( ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) ↑ ( 𝑎 ‘ 2 ) ) ) ) } ∈ ( Dioph ‘ 3 ) )
104 101 102 103 mp2an { 𝑎 ∈ ( ℕ0m ( 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 ) ) ) → { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 1 ) = 0 } ∈ ( Dioph ‘ 3 ) )
106 81 88 105 mp2an { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 1 ) = 0 } ∈ ( Dioph ‘ 3 )
107 eq0rabdioph ( ( 3 ∈ ℕ0 ∧ ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 3 ) ) ↦ ( 𝑎 ‘ 3 ) ) ∈ ( mzPoly ‘ ( 1 ... 3 ) ) ) → { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 3 ) = 0 } ∈ ( Dioph ‘ 3 ) )
108 81 97 107 mp2an { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 3 ) = 0 } ∈ ( Dioph ‘ 3 )
109 anrabdioph ( ( { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 1 ) = 0 } ∈ ( Dioph ‘ 3 ) ∧ { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 3 ) = 0 } ∈ ( Dioph ‘ 3 ) ) → { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( ( 𝑎 ‘ 1 ) = 0 ∧ ( 𝑎 ‘ 3 ) = 0 ) } ∈ ( Dioph ‘ 3 ) )
110 106 108 109 mp2an { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( ( 𝑎 ‘ 1 ) = 0 ∧ ( 𝑎 ‘ 3 ) = 0 ) } ∈ ( Dioph ‘ 3 )
111 orrabdioph ( ( { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( ( ( 𝑎 ‘ 1 ) = 1 ∧ ( 𝑎 ‘ 3 ) = 1 ) ∨ ( ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) ↑ ( 𝑎 ‘ 2 ) ) ) ) } ∈ ( Dioph ‘ 3 ) ∧ { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( ( 𝑎 ‘ 1 ) = 0 ∧ ( 𝑎 ‘ 3 ) = 0 ) } ∈ ( Dioph ‘ 3 ) ) → { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( ( ( ( 𝑎 ‘ 1 ) = 1 ∧ ( 𝑎 ‘ 3 ) = 1 ) ∨ ( ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) ↑ ( 𝑎 ‘ 2 ) ) ) ) ∨ ( ( 𝑎 ‘ 1 ) = 0 ∧ ( 𝑎 ‘ 3 ) = 0 ) ) } ∈ ( Dioph ‘ 3 ) )
112 104 110 111 mp2an { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( ( ( ( 𝑎 ‘ 1 ) = 1 ∧ ( 𝑎 ‘ 3 ) = 1 ) ∨ ( ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) ↑ ( 𝑎 ‘ 2 ) ) ) ) ∨ ( ( 𝑎 ‘ 1 ) = 0 ∧ ( 𝑎 ‘ 3 ) = 0 ) ) } ∈ ( Dioph ‘ 3 )
113 anrabdioph ( ( { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 2 ) ∈ ℕ } ∈ ( Dioph ‘ 3 ) ∧ { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( ( ( ( 𝑎 ‘ 1 ) = 1 ∧ ( 𝑎 ‘ 3 ) = 1 ) ∨ ( ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) ↑ ( 𝑎 ‘ 2 ) ) ) ) ∨ ( ( 𝑎 ‘ 1 ) = 0 ∧ ( 𝑎 ‘ 3 ) = 0 ) ) } ∈ ( Dioph ‘ 3 ) ) → { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( ( 𝑎 ‘ 2 ) ∈ ℕ ∧ ( ( ( ( 𝑎 ‘ 1 ) = 1 ∧ ( 𝑎 ‘ 3 ) = 1 ) ∨ ( ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) ↑ ( 𝑎 ‘ 2 ) ) ) ) ∨ ( ( 𝑎 ‘ 1 ) = 0 ∧ ( 𝑎 ‘ 3 ) = 0 ) ) ) } ∈ ( Dioph ‘ 3 ) )
114 86 112 113 mp2an { 𝑎 ∈ ( ℕ0m ( 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 ) ) ) → { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 2 ) = 0 } ∈ ( Dioph ‘ 3 ) )
116 81 84 115 mp2an { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 2 ) = 0 } ∈ ( Dioph ‘ 3 )
117 anrabdioph ( ( { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 2 ) = 0 } ∈ ( Dioph ‘ 3 ) ∧ { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 3 ) = 1 } ∈ ( Dioph ‘ 3 ) ) → { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( ( 𝑎 ‘ 2 ) = 0 ∧ ( 𝑎 ‘ 3 ) = 1 ) } ∈ ( Dioph ‘ 3 ) )
118 116 99 117 mp2an { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( ( 𝑎 ‘ 2 ) = 0 ∧ ( 𝑎 ‘ 3 ) = 1 ) } ∈ ( Dioph ‘ 3 )
119 orrabdioph ( ( { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( ( 𝑎 ‘ 2 ) ∈ ℕ ∧ ( ( ( ( 𝑎 ‘ 1 ) = 1 ∧ ( 𝑎 ‘ 3 ) = 1 ) ∨ ( ( ( 𝑎 ‘ 1 ) ∈ ( ℤ ‘ 2 ) ∧ ( 𝑎 ‘ 2 ) ∈ ℕ ) ∧ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) ↑ ( 𝑎 ‘ 2 ) ) ) ) ∨ ( ( 𝑎 ‘ 1 ) = 0 ∧ ( 𝑎 ‘ 3 ) = 0 ) ) ) } ∈ ( Dioph ‘ 3 ) ∧ { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( ( 𝑎 ‘ 2 ) = 0 ∧ ( 𝑎 ‘ 3 ) = 1 ) } ∈ ( Dioph ‘ 3 ) ) → { 𝑎 ∈ ( ℕ0m ( 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 { 𝑎 ∈ ( ℕ0m ( 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 { 𝑎 ∈ ( ℕ0m ( 1 ... 3 ) ) ∣ ( 𝑎 ‘ 3 ) = ( ( 𝑎 ‘ 1 ) ↑ ( 𝑎 ‘ 2 ) ) } ∈ ( Dioph ‘ 3 )