Metamath Proof Explorer

Theorem eulerpartlemb

Description: Lemma for eulerpart . The set of all partitions of N is finite. (Contributed by Mario Carneiro, 26-Jan-2015)

Ref Expression
Hypotheses eulerpart.p ⊢ 𝑃 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) }
eulerpart.o ⊢ 𝑂 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ( ◡ 𝑔 “ ℕ ) ¬ 2 ∥ 𝑛 }
eulerpart.d ⊢ 𝐷 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ≤ 1 }
eulerpart.j ⊢ 𝐽 = { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 }
eulerpart.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐽 , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) )
eulerpart.h ⊢ 𝐻 = { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin }
eulerpart.m ⊢ 𝑀 = ( 𝑟 ∈ 𝐻 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } )
Assertion eulerpartlemb 𝑃 ∈ Fin

Proof

Step Hyp Ref Expression
1 eulerpart.p ⊢ 𝑃 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) }
2 eulerpart.o ⊢ 𝑂 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ( ◡ 𝑔 “ ℕ ) ¬ 2 ∥ 𝑛 }
3 eulerpart.d ⊢ 𝐷 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ≤ 1 }
4 eulerpart.j ⊢ 𝐽 = { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 }
5 eulerpart.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐽 , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) )
6 eulerpart.h ⊢ 𝐻 = { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin }
7 eulerpart.m ⊢ 𝑀 = ( 𝑟 ∈ 𝐻 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } )
8 fzfid ⊢ ( ⊤ → ( 1 ... 𝑁 ) ∈ Fin )
9 fzfi ⊢ ( 0 ... 𝑁 ) ∈ Fin
10 snfi ⊢ { 0 } ∈ Fin
11 9 10 ifcli ⊢ if ( 𝑥 ∈ ( 1 ... 𝑁 ) , ( 0 ... 𝑁 ) , { 0 } ) ∈ Fin
12 11 a1i ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℕ ) → if ( 𝑥 ∈ ( 1 ... 𝑁 ) , ( 0 ... 𝑁 ) , { 0 } ) ∈ Fin )
13 eldifn ⊢ ( 𝑥 ∈ ( ℕ ∖ ( 1 ... 𝑁 ) ) → ¬ 𝑥 ∈ ( 1 ... 𝑁 ) )
14 13 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( ℕ ∖ ( 1 ... 𝑁 ) ) ) → ¬ 𝑥 ∈ ( 1 ... 𝑁 ) )
15 iffalse ⊢ ( ¬ 𝑥 ∈ ( 1 ... 𝑁 ) → if ( 𝑥 ∈ ( 1 ... 𝑁 ) , ( 0 ... 𝑁 ) , { 0 } ) = { 0 } )
16 eqimss ⊢ ( if ( 𝑥 ∈ ( 1 ... 𝑁 ) , ( 0 ... 𝑁 ) , { 0 } ) = { 0 } → if ( 𝑥 ∈ ( 1 ... 𝑁 ) , ( 0 ... 𝑁 ) , { 0 } ) ⊆ { 0 } )
17 14 15 16 3syl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( ℕ ∖ ( 1 ... 𝑁 ) ) ) → if ( 𝑥 ∈ ( 1 ... 𝑁 ) , ( 0 ... 𝑁 ) , { 0 } ) ⊆ { 0 } )
18 8 12 17 ixpfi2 ⊢ ( ⊤ → X 𝑥 ∈ ℕ if ( 𝑥 ∈ ( 1 ... 𝑁 ) , ( 0 ... 𝑁 ) , { 0 } ) ∈ Fin )
19 18 mptru ⊢ X 𝑥 ∈ ℕ if ( 𝑥 ∈ ( 1 ... 𝑁 ) , ( 0 ... 𝑁 ) , { 0 } ) ∈ Fin
20 1 eulerpartleme ⊢ ( 𝑔 ∈ 𝑃 ↔ ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
21 ffn ⊢ ( 𝑔 : ℕ ⟶ ℕ0 → 𝑔 Fn ℕ )
22 21 3ad2ant1 ⊢ ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) → 𝑔 Fn ℕ )
23 ffvelcdm ⊢ ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ 𝑥 ∈ ℕ ) → ( 𝑔 ‘ 𝑥 ) ∈ ℕ0 )
24 23 3ad2antl1 ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → ( 𝑔 ‘ 𝑥 ) ∈ ℕ0 )
25 24 nn0red ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → ( 𝑔 ‘ 𝑥 ) ∈ ℝ )
26 nnre ⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℝ )
27 26 adantl ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → 𝑥 ∈ ℝ )
28 25 27 remulcld ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → ( ( 𝑔 ‘ 𝑥 ) · 𝑥 ) ∈ ℝ )
29 cnvimass ⊢ ( ◡ 𝑔 “ ℕ ) ⊆ dom 𝑔
30 fdm ⊢ ( 𝑔 : ℕ ⟶ ℕ0 → dom 𝑔 = ℕ )
31 30 adantr ⊢ ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) → dom 𝑔 = ℕ )
32 29 31 sseqtrid ⊢ ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) → ( ◡ 𝑔 “ ℕ ) ⊆ ℕ )
33 32 sselda ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ) → 𝑘 ∈ ℕ )
34 ffvelcdm ⊢ ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ℕ ) → ( 𝑔 ‘ 𝑘 ) ∈ ℕ0 )
35 34 adantlr ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ 𝑘 ∈ ℕ ) → ( 𝑔 ‘ 𝑘 ) ∈ ℕ0 )
36 33 35 syldan ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ) → ( 𝑔 ‘ 𝑘 ) ∈ ℕ0 )
37 33 nnnn0d ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ) → 𝑘 ∈ ℕ0 )
38 36 37 nn0mulcld ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ) → ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) ∈ ℕ0 )
39 38 nn0cnd ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ) → ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) ∈ ℂ )
40 simpl ⊢ ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) → 𝑔 : ℕ ⟶ ℕ0 )
41 nnex ⊢ ℕ ∈ V
42 fcdmnn0supp ⊢ ( ( ℕ ∈ V ∧ 𝑔 : ℕ ⟶ ℕ0 ) → ( 𝑔 supp 0 ) = ( ◡ 𝑔 “ ℕ ) )
43 41 42 mpan ⊢ ( 𝑔 : ℕ ⟶ ℕ0 → ( 𝑔 supp 0 ) = ( ◡ 𝑔 “ ℕ ) )
44 43 adantr ⊢ ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) → ( 𝑔 supp 0 ) = ( ◡ 𝑔 “ ℕ ) )
45 eqimss ⊢ ( ( 𝑔 supp 0 ) = ( ◡ 𝑔 “ ℕ ) → ( 𝑔 supp 0 ) ⊆ ( ◡ 𝑔 “ ℕ ) )
46 44 45 syl ⊢ ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) → ( 𝑔 supp 0 ) ⊆ ( ◡ 𝑔 “ ℕ ) )
47 41 a1i ⊢ ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) → ℕ ∈ V )
48 0nn0 ⊢ 0 ∈ ℕ0
49 48 a1i ⊢ ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) → 0 ∈ ℕ0 )
50 40 46 47 49 suppssr ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝑔 “ ℕ ) ) ) → ( 𝑔 ‘ 𝑘 ) = 0 )
51 50 oveq1d ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝑔 “ ℕ ) ) ) → ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = ( 0 · 𝑘 ) )
52 eldifi ⊢ ( 𝑘 ∈ ( ℕ ∖ ( ◡ 𝑔 “ ℕ ) ) → 𝑘 ∈ ℕ )
53 52 adantl ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝑔 “ ℕ ) ) ) → 𝑘 ∈ ℕ )
54 nncn ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℂ )
55 mul02 ⊢ ( 𝑘 ∈ ℂ → ( 0 · 𝑘 ) = 0 )
56 53 54 55 3syl ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝑔 “ ℕ ) ) ) → ( 0 · 𝑘 ) = 0 )
57 51 56 eqtrd ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝑔 “ ℕ ) ) ) → ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 0 )
58 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
59 58 eqimssi ⊢ ℕ ⊆ ( ℤ≥ ‘ 1 )
60 59 a1i ⊢ ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) → ℕ ⊆ ( ℤ≥ ‘ 1 ) )
61 32 39 57 60 sumss ⊢ ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) → Σ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) )
62 simpr ⊢ ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) → ( ◡ 𝑔 “ ℕ ) ∈ Fin )
63 62 38 fsumnn0cl ⊢ ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) → Σ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) ∈ ℕ0 )
64 61 63 eqeltrrd ⊢ ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) → Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) ∈ ℕ0 )
65 eleq1 ⊢ ( Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 → ( Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) ∈ ℕ0 ↔ 𝑁 ∈ ℕ0 ) )
66 64 65 syl5ibcom ⊢ ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) → ( Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 → 𝑁 ∈ ℕ0 ) )
67 66 3impia ⊢ ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) → 𝑁 ∈ ℕ0 )
68 67 adantr ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → 𝑁 ∈ ℕ0 )
69 68 nn0red ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → 𝑁 ∈ ℝ )
70 24 nn0ge0d ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → 0 ≤ ( 𝑔 ‘ 𝑥 ) )
71 nnge1 ⊢ ( 𝑥 ∈ ℕ → 1 ≤ 𝑥 )
72 71 adantl ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → 1 ≤ 𝑥 )
73 25 27 70 72 lemulge11d ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → ( 𝑔 ‘ 𝑥 ) ≤ ( ( 𝑔 ‘ 𝑥 ) · 𝑥 ) )
74 62 adantr ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∈ ( ◡ 𝑔 “ ℕ ) ) ) → ( ◡ 𝑔 “ ℕ ) ∈ Fin )
75 38 nn0red ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ) → ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) ∈ ℝ )
76 75 adantlr ⊢ ( ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∈ ( ◡ 𝑔 “ ℕ ) ) ) ∧ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ) → ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) ∈ ℝ )
77 38 nn0ge0d ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ) → 0 ≤ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) )
78 77 adantlr ⊢ ( ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∈ ( ◡ 𝑔 “ ℕ ) ) ) ∧ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ) → 0 ≤ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) )
79 fveq2 ⊢ ( 𝑘 = 𝑥 → ( 𝑔 ‘ 𝑘 ) = ( 𝑔 ‘ 𝑥 ) )
80 id ⊢ ( 𝑘 = 𝑥 → 𝑘 = 𝑥 )
81 79 80 oveq12d ⊢ ( 𝑘 = 𝑥 → ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = ( ( 𝑔 ‘ 𝑥 ) · 𝑥 ) )
82 simprr ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∈ ( ◡ 𝑔 “ ℕ ) ) ) → 𝑥 ∈ ( ◡ 𝑔 “ ℕ ) )
83 74 76 78 81 82 fsumge1 ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑥 ∈ ( ◡ 𝑔 “ ℕ ) ) ) → ( ( 𝑔 ‘ 𝑥 ) · 𝑥 ) ≤ Σ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) )
84 83 expr ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ 𝑥 ∈ ℕ ) → ( 𝑥 ∈ ( ◡ 𝑔 “ ℕ ) → ( ( 𝑔 ‘ 𝑥 ) · 𝑥 ) ≤ Σ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) ) )
85 eldif ⊢ ( 𝑥 ∈ ( ℕ ∖ ( ◡ 𝑔 “ ℕ ) ) ↔ ( 𝑥 ∈ ℕ ∧ ¬ 𝑥 ∈ ( ◡ 𝑔 “ ℕ ) ) )
86 57 ralrimiva ⊢ ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) → ∀ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝑔 “ ℕ ) ) ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 0 )
87 81 eqeq1d ⊢ ( 𝑘 = 𝑥 → ( ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 0 ↔ ( ( 𝑔 ‘ 𝑥 ) · 𝑥 ) = 0 ) )
88 87 rspccva ⊢ ( ( ∀ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝑔 “ ℕ ) ) ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 0 ∧ 𝑥 ∈ ( ℕ ∖ ( ◡ 𝑔 “ ℕ ) ) ) → ( ( 𝑔 ‘ 𝑥 ) · 𝑥 ) = 0 )
89 86 88 sylan ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ 𝑥 ∈ ( ℕ ∖ ( ◡ 𝑔 “ ℕ ) ) ) → ( ( 𝑔 ‘ 𝑥 ) · 𝑥 ) = 0 )
90 85 89 sylan2br ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ ( 𝑥 ∈ ℕ ∧ ¬ 𝑥 ∈ ( ◡ 𝑔 “ ℕ ) ) ) → ( ( 𝑔 ‘ 𝑥 ) · 𝑥 ) = 0 )
91 62 adantr ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ 𝑥 ∈ ℕ ) → ( ◡ 𝑔 “ ℕ ) ∈ Fin )
92 38 adantlr ⊢ ( ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ 𝑥 ∈ ℕ ) ∧ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ) → ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) ∈ ℕ0 )
93 92 nn0red ⊢ ( ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ 𝑥 ∈ ℕ ) ∧ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ) → ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) ∈ ℝ )
94 92 nn0ge0d ⊢ ( ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ 𝑥 ∈ ℕ ) ∧ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ) → 0 ≤ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) )
95 91 93 94 fsumge0 ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ 𝑥 ∈ ℕ ) → 0 ≤ Σ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) )
96 95 adantrr ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ ( 𝑥 ∈ ℕ ∧ ¬ 𝑥 ∈ ( ◡ 𝑔 “ ℕ ) ) ) → 0 ≤ Σ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) )
97 90 96 eqbrtrd ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ ( 𝑥 ∈ ℕ ∧ ¬ 𝑥 ∈ ( ◡ 𝑔 “ ℕ ) ) ) → ( ( 𝑔 ‘ 𝑥 ) · 𝑥 ) ≤ Σ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) )
98 97 expr ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ 𝑥 ∈ ℕ ) → ( ¬ 𝑥 ∈ ( ◡ 𝑔 “ ℕ ) → ( ( 𝑔 ‘ 𝑥 ) · 𝑥 ) ≤ Σ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) ) )
99 84 98 pm2.61d ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ 𝑥 ∈ ℕ ) → ( ( 𝑔 ‘ 𝑥 ) · 𝑥 ) ≤ Σ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) )
100 61 adantr ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ 𝑥 ∈ ℕ ) → Σ 𝑘 ∈ ( ◡ 𝑔 “ ℕ ) ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) )
101 99 100 breqtrd ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ) ∧ 𝑥 ∈ ℕ ) → ( ( 𝑔 ‘ 𝑥 ) · 𝑥 ) ≤ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) )
102 101 3adantl3 ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → ( ( 𝑔 ‘ 𝑥 ) · 𝑥 ) ≤ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) )
103 simpl3 ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 )
104 102 103 breqtrd ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → ( ( 𝑔 ‘ 𝑥 ) · 𝑥 ) ≤ 𝑁 )
105 25 28 69 73 104 letrd ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → ( 𝑔 ‘ 𝑥 ) ≤ 𝑁 )
106 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
107 24 106 eleqtrdi ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → ( 𝑔 ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 0 ) )
108 68 nn0zd ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → 𝑁 ∈ ℤ )
109 elfz5 ⊢ ( ( ( 𝑔 ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝑔 ‘ 𝑥 ) ∈ ( 0 ... 𝑁 ) ↔ ( 𝑔 ‘ 𝑥 ) ≤ 𝑁 ) )
110 107 108 109 syl2anc ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → ( ( 𝑔 ‘ 𝑥 ) ∈ ( 0 ... 𝑁 ) ↔ ( 𝑔 ‘ 𝑥 ) ≤ 𝑁 ) )
111 105 110 mpbird ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → ( 𝑔 ‘ 𝑥 ) ∈ ( 0 ... 𝑁 ) )
112 111 adantr ⊢ ( ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) → ( 𝑔 ‘ 𝑥 ) ∈ ( 0 ... 𝑁 ) )
113 iftrue ⊢ ( 𝑥 ∈ ( 1 ... 𝑁 ) → if ( 𝑥 ∈ ( 1 ... 𝑁 ) , ( 0 ... 𝑁 ) , { 0 } ) = ( 0 ... 𝑁 ) )
114 113 adantl ⊢ ( ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) → if ( 𝑥 ∈ ( 1 ... 𝑁 ) , ( 0 ... 𝑁 ) , { 0 } ) = ( 0 ... 𝑁 ) )
115 112 114 eleqtrrd ⊢ ( ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) → ( 𝑔 ‘ 𝑥 ) ∈ if ( 𝑥 ∈ ( 1 ... 𝑁 ) , ( 0 ... 𝑁 ) , { 0 } ) )
116 nnge1 ⊢ ( ( 𝑔 ‘ 𝑥 ) ∈ ℕ → 1 ≤ ( 𝑔 ‘ 𝑥 ) )
117 nnnn0 ⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℕ0 )
118 117 adantl ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → 𝑥 ∈ ℕ0 )
119 118 nn0ge0d ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → 0 ≤ 𝑥 )
120 lemulge12 ⊢ ( ( ( 𝑥 ∈ ℝ ∧ ( 𝑔 ‘ 𝑥 ) ∈ ℝ ) ∧ ( 0 ≤ 𝑥 ∧ 1 ≤ ( 𝑔 ‘ 𝑥 ) ) ) → 𝑥 ≤ ( ( 𝑔 ‘ 𝑥 ) · 𝑥 ) )
121 120 expr ⊢ ( ( ( 𝑥 ∈ ℝ ∧ ( 𝑔 ‘ 𝑥 ) ∈ ℝ ) ∧ 0 ≤ 𝑥 ) → ( 1 ≤ ( 𝑔 ‘ 𝑥 ) → 𝑥 ≤ ( ( 𝑔 ‘ 𝑥 ) · 𝑥 ) ) )
122 27 25 119 121 syl21anc ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → ( 1 ≤ ( 𝑔 ‘ 𝑥 ) → 𝑥 ≤ ( ( 𝑔 ‘ 𝑥 ) · 𝑥 ) ) )
123 letr ⊢ ( ( 𝑥 ∈ ℝ ∧ ( ( 𝑔 ‘ 𝑥 ) · 𝑥 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑥 ≤ ( ( 𝑔 ‘ 𝑥 ) · 𝑥 ) ∧ ( ( 𝑔 ‘ 𝑥 ) · 𝑥 ) ≤ 𝑁 ) → 𝑥 ≤ 𝑁 ) )
124 27 28 69 123 syl3anc ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → ( ( 𝑥 ≤ ( ( 𝑔 ‘ 𝑥 ) · 𝑥 ) ∧ ( ( 𝑔 ‘ 𝑥 ) · 𝑥 ) ≤ 𝑁 ) → 𝑥 ≤ 𝑁 ) )
125 104 124 mpan2d ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → ( 𝑥 ≤ ( ( 𝑔 ‘ 𝑥 ) · 𝑥 ) → 𝑥 ≤ 𝑁 ) )
126 122 125 syld ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → ( 1 ≤ ( 𝑔 ‘ 𝑥 ) → 𝑥 ≤ 𝑁 ) )
127 116 126 syl5 ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → ( ( 𝑔 ‘ 𝑥 ) ∈ ℕ → 𝑥 ≤ 𝑁 ) )
128 simpr ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → 𝑥 ∈ ℕ )
129 128 58 eleqtrdi ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → 𝑥 ∈ ( ℤ≥ ‘ 1 ) )
130 elfz5 ⊢ ( ( 𝑥 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑥 ∈ ( 1 ... 𝑁 ) ↔ 𝑥 ≤ 𝑁 ) )
131 129 108 130 syl2anc ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → ( 𝑥 ∈ ( 1 ... 𝑁 ) ↔ 𝑥 ≤ 𝑁 ) )
132 127 131 sylibrd ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → ( ( 𝑔 ‘ 𝑥 ) ∈ ℕ → 𝑥 ∈ ( 1 ... 𝑁 ) ) )
133 132 con3d ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → ( ¬ 𝑥 ∈ ( 1 ... 𝑁 ) → ¬ ( 𝑔 ‘ 𝑥 ) ∈ ℕ ) )
134 elnn0 ⊢ ( ( 𝑔 ‘ 𝑥 ) ∈ ℕ0 ↔ ( ( 𝑔 ‘ 𝑥 ) ∈ ℕ ∨ ( 𝑔 ‘ 𝑥 ) = 0 ) )
135 24 134 sylib ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → ( ( 𝑔 ‘ 𝑥 ) ∈ ℕ ∨ ( 𝑔 ‘ 𝑥 ) = 0 ) )
136 135 ord ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → ( ¬ ( 𝑔 ‘ 𝑥 ) ∈ ℕ → ( 𝑔 ‘ 𝑥 ) = 0 ) )
137 133 136 syld ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → ( ¬ 𝑥 ∈ ( 1 ... 𝑁 ) → ( 𝑔 ‘ 𝑥 ) = 0 ) )
138 137 imp ⊢ ( ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) ∧ ¬ 𝑥 ∈ ( 1 ... 𝑁 ) ) → ( 𝑔 ‘ 𝑥 ) = 0 )
139 fvex ⊢ ( 𝑔 ‘ 𝑥 ) ∈ V
140 139 elsn ⊢ ( ( 𝑔 ‘ 𝑥 ) ∈ { 0 } ↔ ( 𝑔 ‘ 𝑥 ) = 0 )
141 138 140 sylibr ⊢ ( ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) ∧ ¬ 𝑥 ∈ ( 1 ... 𝑁 ) ) → ( 𝑔 ‘ 𝑥 ) ∈ { 0 } )
142 15 adantl ⊢ ( ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) ∧ ¬ 𝑥 ∈ ( 1 ... 𝑁 ) ) → if ( 𝑥 ∈ ( 1 ... 𝑁 ) , ( 0 ... 𝑁 ) , { 0 } ) = { 0 } )
143 141 142 eleqtrrd ⊢ ( ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) ∧ ¬ 𝑥 ∈ ( 1 ... 𝑁 ) ) → ( 𝑔 ‘ 𝑥 ) ∈ if ( 𝑥 ∈ ( 1 ... 𝑁 ) , ( 0 ... 𝑁 ) , { 0 } ) )
144 115 143 pm2.61dan ⊢ ( ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ∧ 𝑥 ∈ ℕ ) → ( 𝑔 ‘ 𝑥 ) ∈ if ( 𝑥 ∈ ( 1 ... 𝑁 ) , ( 0 ... 𝑁 ) , { 0 } ) )
145 144 ralrimiva ⊢ ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) → ∀ 𝑥 ∈ ℕ ( 𝑔 ‘ 𝑥 ) ∈ if ( 𝑥 ∈ ( 1 ... 𝑁 ) , ( 0 ... 𝑁 ) , { 0 } ) )
146 vex ⊢ 𝑔 ∈ V
147 146 elixp ⊢ ( 𝑔 ∈ X 𝑥 ∈ ℕ if ( 𝑥 ∈ ( 1 ... 𝑁 ) , ( 0 ... 𝑁 ) , { 0 } ) ↔ ( 𝑔 Fn ℕ ∧ ∀ 𝑥 ∈ ℕ ( 𝑔 ‘ 𝑥 ) ∈ if ( 𝑥 ∈ ( 1 ... 𝑁 ) , ( 0 ... 𝑁 ) , { 0 } ) ) )
148 22 145 147 sylanbrc ⊢ ( ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝑔 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑔 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) → 𝑔 ∈ X 𝑥 ∈ ℕ if ( 𝑥 ∈ ( 1 ... 𝑁 ) , ( 0 ... 𝑁 ) , { 0 } ) )
149 20 148 sylbi ⊢ ( 𝑔 ∈ 𝑃 → 𝑔 ∈ X 𝑥 ∈ ℕ if ( 𝑥 ∈ ( 1 ... 𝑁 ) , ( 0 ... 𝑁 ) , { 0 } ) )
150 149 ssriv ⊢ 𝑃 ⊆ X 𝑥 ∈ ℕ if ( 𝑥 ∈ ( 1 ... 𝑁 ) , ( 0 ... 𝑁 ) , { 0 } )
151 ssfi ⊢ ( ( X 𝑥 ∈ ℕ if ( 𝑥 ∈ ( 1 ... 𝑁 ) , ( 0 ... 𝑁 ) , { 0 } ) ∈ Fin ∧ 𝑃 ⊆ X 𝑥 ∈ ℕ if ( 𝑥 ∈ ( 1 ... 𝑁 ) , ( 0 ... 𝑁 ) , { 0 } ) ) → 𝑃 ∈ Fin )
152 19 150 151 mp2an ⊢ 𝑃 ∈ Fin