This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nnsum3primesgbe

Description: Any even Goldbach number is the sum of at most 3 (actually 2) primes. (Contributed by AV, 2-Aug-2020)

Ref Expression
Assertion nnsum3primesgbe ( 𝑁 ∈ GoldbachEven → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 isgbe ⊢ ( 𝑁 ∈ GoldbachEven ↔ ( 𝑁 ∈ Even ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑁 = ( 𝑝 + 𝑞 ) ) ) )
2 2nn ⊢ 2 ∈ ℕ
3 2 a1i ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑁 = ( 𝑝 + 𝑞 ) ) ) → 2 ∈ ℕ )
4 oveq2 ⊢ ( 𝑑 = 2 → ( 1 ... 𝑑 ) = ( 1 ... 2 ) )
5 df-2 ⊢ 2 = ( 1 + 1 )
6 5 oveq2i ⊢ ( 1 ... 2 ) = ( 1 ... ( 1 + 1 ) )
7 1z ⊢ 1 ∈ ℤ
8 fzpr ⊢ ( 1 ∈ ℤ → ( 1 ... ( 1 + 1 ) ) = { 1 , ( 1 + 1 ) } )
9 7 8 ax-mp ⊢ ( 1 ... ( 1 + 1 ) ) = { 1 , ( 1 + 1 ) }
10 1p1e2 ⊢ ( 1 + 1 ) = 2
11 10 preq2i ⊢ { 1 , ( 1 + 1 ) } = { 1 , 2 }
12 6 9 11 3eqtri ⊢ ( 1 ... 2 ) = { 1 , 2 }
13 4 12 eqtrdi ⊢ ( 𝑑 = 2 → ( 1 ... 𝑑 ) = { 1 , 2 } )
14 13 oveq2d ⊢ ( 𝑑 = 2 → ( ℙ ↑m ( 1 ... 𝑑 ) ) = ( ℙ ↑m { 1 , 2 } ) )
15 breq1 ⊢ ( 𝑑 = 2 → ( 𝑑 ≤ 3 ↔ 2 ≤ 3 ) )
16 13 sumeq1d ⊢ ( 𝑑 = 2 → Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) )
17 16 eqeq2d ⊢ ( 𝑑 = 2 → ( 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ↔ 𝑁 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) ) )
18 15 17 anbi12d ⊢ ( 𝑑 = 2 → ( ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ↔ ( 2 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) ) ) )
19 14 18 rexeqbidv ⊢ ( 𝑑 = 2 → ( ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ↔ ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) ) ) )
20 19 adantl ⊢ ( ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑁 = ( 𝑝 + 𝑞 ) ) ) ∧ 𝑑 = 2 ) → ( ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ↔ ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) ) ) )
21 1ne2 ⊢ 1 ≠ 2
22 1ex ⊢ 1 ∈ V
23 2ex ⊢ 2 ∈ V
24 vex ⊢ 𝑝 ∈ V
25 vex ⊢ 𝑞 ∈ V
26 22 23 24 25 fpr ⊢ ( 1 ≠ 2 → { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } : { 1 , 2 } ⟶ { 𝑝 , 𝑞 } )
27 21 26 mp1i ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } : { 1 , 2 } ⟶ { 𝑝 , 𝑞 } )
28 prssi ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → { 𝑝 , 𝑞 } ⊆ ℙ )
29 27 28 fssd ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } : { 1 , 2 } ⟶ ℙ )
30 prmex ⊢ ℙ ∈ V
31 prex ⊢ { 1 , 2 } ∈ V
32 30 31 pm3.2i ⊢ ( ℙ ∈ V ∧ { 1 , 2 } ∈ V )
33 elmapg ⊢ ( ( ℙ ∈ V ∧ { 1 , 2 } ∈ V ) → ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ∈ ( ℙ ↑m { 1 , 2 } ) ↔ { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } : { 1 , 2 } ⟶ ℙ ) )
34 32 33 mp1i ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ∈ ( ℙ ↑m { 1 , 2 } ) ↔ { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } : { 1 , 2 } ⟶ ℙ ) )
35 29 34 mpbird ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ∈ ( ℙ ↑m { 1 , 2 } ) )
36 fveq1 ⊢ ( 𝑓 = { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } → ( 𝑓 ‘ 𝑘 ) = ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 𝑘 ) )
37 36 adantr ⊢ ( ( 𝑓 = { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ∧ 𝑘 ∈ { 1 , 2 } ) → ( 𝑓 ‘ 𝑘 ) = ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 𝑘 ) )
38 37 sumeq2dv ⊢ ( 𝑓 = { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } → Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) = Σ 𝑘 ∈ { 1 , 2 } ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 𝑘 ) )
39 38 eqeq1d ⊢ ( 𝑓 = { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } → ( Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) = ( 𝑝 + 𝑞 ) ↔ Σ 𝑘 ∈ { 1 , 2 } ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 𝑘 ) = ( 𝑝 + 𝑞 ) ) )
40 39 anbi2d ⊢ ( 𝑓 = { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } → ( ( 2 ≤ 3 ∧ Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) = ( 𝑝 + 𝑞 ) ) ↔ ( 2 ≤ 3 ∧ Σ 𝑘 ∈ { 1 , 2 } ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 𝑘 ) = ( 𝑝 + 𝑞 ) ) ) )
41 40 adantl ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑓 = { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ) → ( ( 2 ≤ 3 ∧ Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) = ( 𝑝 + 𝑞 ) ) ↔ ( 2 ≤ 3 ∧ Σ 𝑘 ∈ { 1 , 2 } ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 𝑘 ) = ( 𝑝 + 𝑞 ) ) ) )
42 prmz ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
43 prmz ⊢ ( 𝑞 ∈ ℙ → 𝑞 ∈ ℤ )
44 fveq2 ⊢ ( 𝑘 = 1 → ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 𝑘 ) = ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 1 ) )
45 22 24 fvpr1 ⊢ ( 1 ≠ 2 → ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 1 ) = 𝑝 )
46 21 45 ax-mp ⊢ ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 1 ) = 𝑝
47 44 46 eqtrdi ⊢ ( 𝑘 = 1 → ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 𝑘 ) = 𝑝 )
48 fveq2 ⊢ ( 𝑘 = 2 → ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 𝑘 ) = ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 2 ) )
49 23 25 fvpr2 ⊢ ( 1 ≠ 2 → ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 2 ) = 𝑞 )
50 21 49 ax-mp ⊢ ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 2 ) = 𝑞
51 48 50 eqtrdi ⊢ ( 𝑘 = 2 → ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 𝑘 ) = 𝑞 )
52 zcn ⊢ ( 𝑝 ∈ ℤ → 𝑝 ∈ ℂ )
53 zcn ⊢ ( 𝑞 ∈ ℤ → 𝑞 ∈ ℂ )
54 52 53 anim12i ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) → ( 𝑝 ∈ ℂ ∧ 𝑞 ∈ ℂ ) )
55 7 2 pm3.2i ⊢ ( 1 ∈ ℤ ∧ 2 ∈ ℕ )
56 55 a1i ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) → ( 1 ∈ ℤ ∧ 2 ∈ ℕ ) )
57 21 a1i ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) → 1 ≠ 2 )
58 47 51 54 56 57 sumpr ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) → Σ 𝑘 ∈ { 1 , 2 } ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 𝑘 ) = ( 𝑝 + 𝑞 ) )
59 42 43 58 syl2an ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → Σ 𝑘 ∈ { 1 , 2 } ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 𝑘 ) = ( 𝑝 + 𝑞 ) )
60 2re ⊢ 2 ∈ ℝ
61 3re ⊢ 3 ∈ ℝ
62 2lt3 ⊢ 2 < 3
63 60 61 62 ltleii ⊢ 2 ≤ 3
64 59 63 jctil ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → ( 2 ≤ 3 ∧ Σ 𝑘 ∈ { 1 , 2 } ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ } ‘ 𝑘 ) = ( 𝑝 + 𝑞 ) ) )
65 35 41 64 rspcedvd ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) = ( 𝑝 + 𝑞 ) ) )
66 65 adantr ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑁 = ( 𝑝 + 𝑞 ) ) ) → ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) = ( 𝑝 + 𝑞 ) ) )
67 eqeq1 ⊢ ( 𝑁 = ( 𝑝 + 𝑞 ) → ( 𝑁 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) ↔ ( 𝑝 + 𝑞 ) = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) ) )
68 eqcom ⊢ ( ( 𝑝 + 𝑞 ) = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) ↔ Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) = ( 𝑝 + 𝑞 ) )
69 67 68 bitrdi ⊢ ( 𝑁 = ( 𝑝 + 𝑞 ) → ( 𝑁 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) ↔ Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) = ( 𝑝 + 𝑞 ) ) )
70 69 anbi2d ⊢ ( 𝑁 = ( 𝑝 + 𝑞 ) → ( ( 2 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) ) ↔ ( 2 ≤ 3 ∧ Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) = ( 𝑝 + 𝑞 ) ) ) )
71 70 rexbidv ⊢ ( 𝑁 = ( 𝑝 + 𝑞 ) → ( ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) ) ↔ ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) = ( 𝑝 + 𝑞 ) ) ) )
72 71 3ad2ant3 ⊢ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑁 = ( 𝑝 + 𝑞 ) ) → ( ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) ) ↔ ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) = ( 𝑝 + 𝑞 ) ) ) )
73 72 adantl ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑁 = ( 𝑝 + 𝑞 ) ) ) → ( ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) ) ↔ ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) = ( 𝑝 + 𝑞 ) ) ) )
74 66 73 mpbird ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑁 = ( 𝑝 + 𝑞 ) ) ) → ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) ) )
75 3 20 74 rspcedvd ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑁 = ( 𝑝 + 𝑞 ) ) ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
76 75 a1d ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑁 = ( 𝑝 + 𝑞 ) ) ) → ( 𝑁 ∈ Even → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ) )
77 76 ex ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑁 = ( 𝑝 + 𝑞 ) ) → ( 𝑁 ∈ Even → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ) ) )
78 77 rexlimivv ⊢ ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑁 = ( 𝑝 + 𝑞 ) ) → ( 𝑁 ∈ Even → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ) )
79 78 impcom ⊢ ( ( 𝑁 ∈ Even ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑁 = ( 𝑝 + 𝑞 ) ) ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
80 1 79 sylbi ⊢ ( 𝑁 ∈ GoldbachEven → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )