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 
|- { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( a ` 3 ) = ( ( a ` 1 ) ^ ( a ` 2 ) ) } e. ( Dioph ` 3 )

Proof

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