Metamath Proof Explorer

Theorem rabren3dioph

Description: Change variable numbers in a 3-variable Diophantine class abstraction. (Contributed by Stefan O'Rear, 17-Oct-2014)

Ref Expression
Hypotheses rabren3dioph.a ⊢ ( ( ( 𝑎 ‘ 1 ) = ( 𝑏 ‘ 𝑋 ) ∧ ( 𝑎 ‘ 2 ) = ( 𝑏 ‘ 𝑌 ) ∧ ( 𝑎 ‘ 3 ) = ( 𝑏 ‘ 𝑍 ) ) → ( 𝜑 ↔ 𝜓 ) )
rabren3dioph.b ⊢ 𝑋 ∈ ( 1 ... 𝑁 )
rabren3dioph.c ⊢ 𝑌 ∈ ( 1 ... 𝑁 )
rabren3dioph.d ⊢ 𝑍 ∈ ( 1 ... 𝑁 )
Assertion rabren3dioph ( ( 𝑁 ∈ ℕ0 ∧ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∣ 𝜑 } ∈ ( Dioph ‘ 3 ) ) → { 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝜓 } ∈ ( Dioph ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 rabren3dioph.a ⊢ ( ( ( 𝑎 ‘ 1 ) = ( 𝑏 ‘ 𝑋 ) ∧ ( 𝑎 ‘ 2 ) = ( 𝑏 ‘ 𝑌 ) ∧ ( 𝑎 ‘ 3 ) = ( 𝑏 ‘ 𝑍 ) ) → ( 𝜑 ↔ 𝜓 ) )
2 rabren3dioph.b ⊢ 𝑋 ∈ ( 1 ... 𝑁 )
3 rabren3dioph.c ⊢ 𝑌 ∈ ( 1 ... 𝑁 )
4 rabren3dioph.d ⊢ 𝑍 ∈ ( 1 ... 𝑁 )
5 vex ⊢ 𝑏 ∈ V
6 tpex ⊢ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ∈ V
7 5 6 coex ⊢ ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) ∈ V
8 1ne2 ⊢ 1 ≠ 2
9 1re ⊢ 1 ∈ ℝ
10 1lt3 ⊢ 1 < 3
11 9 10 ltneii ⊢ 1 ≠ 3
12 2re ⊢ 2 ∈ ℝ
13 2lt3 ⊢ 2 < 3
14 12 13 ltneii ⊢ 2 ≠ 3
15 1ex ⊢ 1 ∈ V
16 2ex ⊢ 2 ∈ V
17 3ex ⊢ 3 ∈ V
18 2 elexi ⊢ 𝑋 ∈ V
19 3 elexi ⊢ 𝑌 ∈ V
20 4 elexi ⊢ 𝑍 ∈ V
21 15 16 17 18 19 20 fntp ⊢ ( ( 1 ≠ 2 ∧ 1 ≠ 3 ∧ 2 ≠ 3 ) → { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } Fn { 1 , 2 , 3 } )
22 8 11 14 21 mp3an ⊢ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } Fn { 1 , 2 , 3 }
23 15 tpid1 ⊢ 1 ∈ { 1 , 2 , 3 }
24 fvco2 ⊢ ( ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } Fn { 1 , 2 , 3 } ∧ 1 ∈ { 1 , 2 , 3 } ) → ( ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) ‘ 1 ) = ( 𝑏 ‘ ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ‘ 1 ) ) )
25 22 23 24 mp2an ⊢ ( ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) ‘ 1 ) = ( 𝑏 ‘ ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ‘ 1 ) )
26 15 18 fvtp1 ⊢ ( ( 1 ≠ 2 ∧ 1 ≠ 3 ) → ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ‘ 1 ) = 𝑋 )
27 8 11 26 mp2an ⊢ ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ‘ 1 ) = 𝑋
28 27 fveq2i ⊢ ( 𝑏 ‘ ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ‘ 1 ) ) = ( 𝑏 ‘ 𝑋 )
29 25 28 eqtri ⊢ ( ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) ‘ 1 ) = ( 𝑏 ‘ 𝑋 )
30 16 tpid2 ⊢ 2 ∈ { 1 , 2 , 3 }
31 fvco2 ⊢ ( ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } Fn { 1 , 2 , 3 } ∧ 2 ∈ { 1 , 2 , 3 } ) → ( ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) ‘ 2 ) = ( 𝑏 ‘ ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ‘ 2 ) ) )
32 22 30 31 mp2an ⊢ ( ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) ‘ 2 ) = ( 𝑏 ‘ ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ‘ 2 ) )
33 16 19 fvtp2 ⊢ ( ( 1 ≠ 2 ∧ 2 ≠ 3 ) → ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ‘ 2 ) = 𝑌 )
34 8 14 33 mp2an ⊢ ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ‘ 2 ) = 𝑌
35 34 fveq2i ⊢ ( 𝑏 ‘ ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ‘ 2 ) ) = ( 𝑏 ‘ 𝑌 )
36 32 35 eqtri ⊢ ( ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) ‘ 2 ) = ( 𝑏 ‘ 𝑌 )
37 17 tpid3 ⊢ 3 ∈ { 1 , 2 , 3 }
38 fvco2 ⊢ ( ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } Fn { 1 , 2 , 3 } ∧ 3 ∈ { 1 , 2 , 3 } ) → ( ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) ‘ 3 ) = ( 𝑏 ‘ ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ‘ 3 ) ) )
39 22 37 38 mp2an ⊢ ( ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) ‘ 3 ) = ( 𝑏 ‘ ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ‘ 3 ) )
40 17 20 fvtp3 ⊢ ( ( 1 ≠ 3 ∧ 2 ≠ 3 ) → ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ‘ 3 ) = 𝑍 )
41 11 14 40 mp2an ⊢ ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ‘ 3 ) = 𝑍
42 41 fveq2i ⊢ ( 𝑏 ‘ ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ‘ 3 ) ) = ( 𝑏 ‘ 𝑍 )
43 39 42 eqtri ⊢ ( ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) ‘ 3 ) = ( 𝑏 ‘ 𝑍 )
44 29 36 43 3pm3.2i ⊢ ( ( ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) ‘ 1 ) = ( 𝑏 ‘ 𝑋 ) ∧ ( ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) ‘ 2 ) = ( 𝑏 ‘ 𝑌 ) ∧ ( ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) ‘ 3 ) = ( 𝑏 ‘ 𝑍 ) )
45 fveq1 ⊢ ( 𝑎 = ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) → ( 𝑎 ‘ 1 ) = ( ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) ‘ 1 ) )
46 45 eqeq1d ⊢ ( 𝑎 = ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) → ( ( 𝑎 ‘ 1 ) = ( 𝑏 ‘ 𝑋 ) ↔ ( ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) ‘ 1 ) = ( 𝑏 ‘ 𝑋 ) ) )
47 fveq1 ⊢ ( 𝑎 = ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) → ( 𝑎 ‘ 2 ) = ( ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) ‘ 2 ) )
48 47 eqeq1d ⊢ ( 𝑎 = ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) → ( ( 𝑎 ‘ 2 ) = ( 𝑏 ‘ 𝑌 ) ↔ ( ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) ‘ 2 ) = ( 𝑏 ‘ 𝑌 ) ) )
49 fveq1 ⊢ ( 𝑎 = ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) → ( 𝑎 ‘ 3 ) = ( ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) ‘ 3 ) )
50 49 eqeq1d ⊢ ( 𝑎 = ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) → ( ( 𝑎 ‘ 3 ) = ( 𝑏 ‘ 𝑍 ) ↔ ( ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) ‘ 3 ) = ( 𝑏 ‘ 𝑍 ) ) )
51 46 48 50 3anbi123d ⊢ ( 𝑎 = ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) → ( ( ( 𝑎 ‘ 1 ) = ( 𝑏 ‘ 𝑋 ) ∧ ( 𝑎 ‘ 2 ) = ( 𝑏 ‘ 𝑌 ) ∧ ( 𝑎 ‘ 3 ) = ( 𝑏 ‘ 𝑍 ) ) ↔ ( ( ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) ‘ 1 ) = ( 𝑏 ‘ 𝑋 ) ∧ ( ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) ‘ 2 ) = ( 𝑏 ‘ 𝑌 ) ∧ ( ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) ‘ 3 ) = ( 𝑏 ‘ 𝑍 ) ) ) )
52 44 51 mpbiri ⊢ ( 𝑎 = ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) → ( ( 𝑎 ‘ 1 ) = ( 𝑏 ‘ 𝑋 ) ∧ ( 𝑎 ‘ 2 ) = ( 𝑏 ‘ 𝑌 ) ∧ ( 𝑎 ‘ 3 ) = ( 𝑏 ‘ 𝑍 ) ) )
53 52 1 syl ⊢ ( 𝑎 = ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) → ( 𝜑 ↔ 𝜓 ) )
54 7 53 sbcie ⊢ ( [ ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) / 𝑎 ] 𝜑 ↔ 𝜓 )
55 54 rabbii ⊢ { 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ [ ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) / 𝑎 ] 𝜑 } = { 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝜓 }
56 15 16 17 18 19 20 8 11 14 ftp ⊢ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } : { 1 , 2 , 3 } ⟶ { 𝑋 , 𝑌 , 𝑍 }
57 1z ⊢ 1 ∈ ℤ
58 fztp ⊢ ( 1 ∈ ℤ → ( 1 ... ( 1 + 2 ) ) = { 1 , ( 1 + 1 ) , ( 1 + 2 ) } )
59 57 58 ax-mp ⊢ ( 1 ... ( 1 + 2 ) ) = { 1 , ( 1 + 1 ) , ( 1 + 2 ) }
60 1p2e3 ⊢ ( 1 + 2 ) = 3
61 60 oveq2i ⊢ ( 1 ... ( 1 + 2 ) ) = ( 1 ... 3 )
62 eqidd ⊢ ( 1 ∈ ℤ → 1 = 1 )
63 1p1e2 ⊢ ( 1 + 1 ) = 2
64 63 a1i ⊢ ( 1 ∈ ℤ → ( 1 + 1 ) = 2 )
65 60 a1i ⊢ ( 1 ∈ ℤ → ( 1 + 2 ) = 3 )
66 62 64 65 tpeq123d ⊢ ( 1 ∈ ℤ → { 1 , ( 1 + 1 ) , ( 1 + 2 ) } = { 1 , 2 , 3 } )
67 57 66 ax-mp ⊢ { 1 , ( 1 + 1 ) , ( 1 + 2 ) } = { 1 , 2 , 3 }
68 59 61 67 3eqtr3i ⊢ ( 1 ... 3 ) = { 1 , 2 , 3 }
69 68 feq2i ⊢ ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } : ( 1 ... 3 ) ⟶ { 𝑋 , 𝑌 , 𝑍 } ↔ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } : { 1 , 2 , 3 } ⟶ { 𝑋 , 𝑌 , 𝑍 } )
70 56 69 mpbir ⊢ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } : ( 1 ... 3 ) ⟶ { 𝑋 , 𝑌 , 𝑍 }
71 2 3 4 3pm3.2i ⊢ ( 𝑋 ∈ ( 1 ... 𝑁 ) ∧ 𝑌 ∈ ( 1 ... 𝑁 ) ∧ 𝑍 ∈ ( 1 ... 𝑁 ) )
72 18 19 20 tpss ⊢ ( ( 𝑋 ∈ ( 1 ... 𝑁 ) ∧ 𝑌 ∈ ( 1 ... 𝑁 ) ∧ 𝑍 ∈ ( 1 ... 𝑁 ) ) ↔ { 𝑋 , 𝑌 , 𝑍 } ⊆ ( 1 ... 𝑁 ) )
73 71 72 mpbi ⊢ { 𝑋 , 𝑌 , 𝑍 } ⊆ ( 1 ... 𝑁 )
74 fss ⊢ ( ( { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } : ( 1 ... 3 ) ⟶ { 𝑋 , 𝑌 , 𝑍 } ∧ { 𝑋 , 𝑌 , 𝑍 } ⊆ ( 1 ... 𝑁 ) ) → { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } : ( 1 ... 3 ) ⟶ ( 1 ... 𝑁 ) )
75 70 73 74 mp2an ⊢ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } : ( 1 ... 3 ) ⟶ ( 1 ... 𝑁 )
76 rabrenfdioph ⊢ ( ( 𝑁 ∈ ℕ0 ∧ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } : ( 1 ... 3 ) ⟶ ( 1 ... 𝑁 ) ∧ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∣ 𝜑 } ∈ ( Dioph ‘ 3 ) ) → { 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ [ ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) / 𝑎 ] 𝜑 } ∈ ( Dioph ‘ 𝑁 ) )
77 75 76 mp3an2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∣ 𝜑 } ∈ ( Dioph ‘ 3 ) ) → { 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ [ ( 𝑏 ∘ { ⟨ 1 , 𝑋 ⟩ , ⟨ 2 , 𝑌 ⟩ , ⟨ 3 , 𝑍 ⟩ } ) / 𝑎 ] 𝜑 } ∈ ( Dioph ‘ 𝑁 ) )
78 55 77 eqeltrrid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ { 𝑎 ∈ ( ℕ0 ↑m ( 1 ... 3 ) ) ∣ 𝜑 } ∈ ( Dioph ‘ 3 ) ) → { 𝑏 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ∣ 𝜓 } ∈ ( Dioph ‘ 𝑁 ) )