Proof of Theorem sticksstones9
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sticksstones9.2 | . . . . 5
⊢ (𝜑 → 𝐾 = 0) | 
| 2 | 1 | iftrued 4532 | . . . 4
⊢ (𝜑 → if(𝐾 = 0, {〈1, 𝑁〉}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))))) = {〈1,
𝑁〉}) | 
| 3 | 2 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → if(𝐾 = 0, {〈1, 𝑁〉}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))))) = {〈1,
𝑁〉}) | 
| 4 |  | eqid 2736 | . . . . . . . . . . 11
⊢ {〈1,
𝑁〉} = {〈1, 𝑁〉} | 
| 5 |  | 1nn 12278 | . . . . . . . . . . . . 13
⊢ 1 ∈
ℕ | 
| 6 | 5 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℕ) | 
| 7 |  | sticksstones9.1 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 8 |  | fsng 7156 | . . . . . . . . . . . 12
⊢ ((1
∈ ℕ ∧ 𝑁
∈ ℕ0) → ({〈1, 𝑁〉}:{1}⟶{𝑁} ↔ {〈1, 𝑁〉} = {〈1, 𝑁〉})) | 
| 9 | 6, 7, 8 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → ({〈1, 𝑁〉}:{1}⟶{𝑁} ↔ {〈1, 𝑁〉} = {〈1, 𝑁〉})) | 
| 10 | 4, 9 | mpbiri 258 | . . . . . . . . . 10
⊢ (𝜑 → {〈1, 𝑁〉}:{1}⟶{𝑁}) | 
| 11 | 7 | snssd 4808 | . . . . . . . . . 10
⊢ (𝜑 → {𝑁} ⊆
ℕ0) | 
| 12 | 10, 11 | jca 511 | . . . . . . . . 9
⊢ (𝜑 → ({〈1, 𝑁〉}:{1}⟶{𝑁} ∧ {𝑁} ⊆
ℕ0)) | 
| 13 |  | fss 6751 | . . . . . . . . 9
⊢
(({〈1, 𝑁〉}:{1}⟶{𝑁} ∧ {𝑁} ⊆ ℕ0) →
{〈1, 𝑁〉}:{1}⟶ℕ0) | 
| 14 | 12, 13 | syl 17 | . . . . . . . 8
⊢ (𝜑 → {〈1, 𝑁〉}:{1}⟶ℕ0) | 
| 15 | 1 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐾 + 1) = (0 + 1)) | 
| 16 |  | 0p1e1 12389 | . . . . . . . . . . . . 13
⊢ (0 + 1) =
1 | 
| 17 | 15, 16 | eqtrdi 2792 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐾 + 1) = 1) | 
| 18 | 17 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (𝜑 → (1...(𝐾 + 1)) = (1...1)) | 
| 19 |  | 1zzd 12650 | . . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℤ) | 
| 20 |  | fzsn 13607 | . . . . . . . . . . . 12
⊢ (1 ∈
ℤ → (1...1) = {1}) | 
| 21 | 19, 20 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (1...1) =
{1}) | 
| 22 | 18, 21 | eqtrd 2776 | . . . . . . . . . 10
⊢ (𝜑 → (1...(𝐾 + 1)) = {1}) | 
| 23 | 22 | eqcomd 2742 | . . . . . . . . 9
⊢ (𝜑 → {1} = (1...(𝐾 + 1))) | 
| 24 | 23 | feq2d 6721 | . . . . . . . 8
⊢ (𝜑 → ({〈1, 𝑁〉}:{1}⟶ℕ0
↔ {〈1, 𝑁〉}:(1...(𝐾 +
1))⟶ℕ0)) | 
| 25 | 14, 24 | mpbid 232 | . . . . . . 7
⊢ (𝜑 → {〈1, 𝑁〉}:(1...(𝐾 +
1))⟶ℕ0) | 
| 26 | 22 | sumeq1d 15737 | . . . . . . . 8
⊢ (𝜑 → Σ𝑖 ∈ (1...(𝐾 + 1))({〈1, 𝑁〉}‘𝑖) = Σ𝑖 ∈ {1} ({〈1, 𝑁〉}‘𝑖)) | 
| 27 |  | fvsng 7201 | . . . . . . . . . . . . 13
⊢ ((1
∈ ℕ ∧ 𝑁
∈ ℕ0) → ({〈1, 𝑁〉}‘1) = 𝑁) | 
| 28 | 6, 7, 27 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → ({〈1, 𝑁〉}‘1) = 𝑁) | 
| 29 | 7 | nn0cnd 12591 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℂ) | 
| 30 | 28, 29 | eqeltrd 2840 | . . . . . . . . . . 11
⊢ (𝜑 → ({〈1, 𝑁〉}‘1) ∈
ℂ) | 
| 31 | 6, 30 | jca 511 | . . . . . . . . . 10
⊢ (𝜑 → (1 ∈ ℕ ∧
({〈1, 𝑁〉}‘1) ∈
ℂ)) | 
| 32 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑖 = 1 → ({〈1, 𝑁〉}‘𝑖) = ({〈1, 𝑁〉}‘1)) | 
| 33 | 32 | sumsn 15783 | . . . . . . . . . 10
⊢ ((1
∈ ℕ ∧ ({〈1, 𝑁〉}‘1) ∈ ℂ) →
Σ𝑖 ∈ {1}
({〈1, 𝑁〉}‘𝑖) = ({〈1, 𝑁〉}‘1)) | 
| 34 | 31, 33 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → Σ𝑖 ∈ {1} ({〈1, 𝑁〉}‘𝑖) = ({〈1, 𝑁〉}‘1)) | 
| 35 | 6, 7 | jca 511 | . . . . . . . . . 10
⊢ (𝜑 → (1 ∈ ℕ ∧
𝑁 ∈
ℕ0)) | 
| 36 | 35, 27 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → ({〈1, 𝑁〉}‘1) = 𝑁) | 
| 37 | 34, 36 | eqtrd 2776 | . . . . . . . 8
⊢ (𝜑 → Σ𝑖 ∈ {1} ({〈1, 𝑁〉}‘𝑖) = 𝑁) | 
| 38 | 26, 37 | eqtrd 2776 | . . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ (1...(𝐾 + 1))({〈1, 𝑁〉}‘𝑖) = 𝑁) | 
| 39 | 25, 38 | jca 511 | . . . . . 6
⊢ (𝜑 → ({〈1, 𝑁〉}:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))({〈1, 𝑁〉}‘𝑖) = 𝑁)) | 
| 40 | 39 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ({〈1, 𝑁〉}:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))({〈1, 𝑁〉}‘𝑖) = 𝑁)) | 
| 41 |  | snex 5435 | . . . . . 6
⊢ {〈1,
𝑁〉} ∈
V | 
| 42 |  | feq1 6715 | . . . . . . . 8
⊢ (𝑔 = {〈1, 𝑁〉} → (𝑔:(1...(𝐾 + 1))⟶ℕ0 ↔
{〈1, 𝑁〉}:(1...(𝐾 +
1))⟶ℕ0)) | 
| 43 |  | simpl 482 | . . . . . . . . . . 11
⊢ ((𝑔 = {〈1, 𝑁〉} ∧ 𝑖 ∈ (1...(𝐾 + 1))) → 𝑔 = {〈1, 𝑁〉}) | 
| 44 | 43 | fveq1d 6907 | . . . . . . . . . 10
⊢ ((𝑔 = {〈1, 𝑁〉} ∧ 𝑖 ∈ (1...(𝐾 + 1))) → (𝑔‘𝑖) = ({〈1, 𝑁〉}‘𝑖)) | 
| 45 | 44 | sumeq2dv 15739 | . . . . . . . . 9
⊢ (𝑔 = {〈1, 𝑁〉} → Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = Σ𝑖 ∈ (1...(𝐾 + 1))({〈1, 𝑁〉}‘𝑖)) | 
| 46 | 45 | eqeq1d 2738 | . . . . . . . 8
⊢ (𝑔 = {〈1, 𝑁〉} → (Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁 ↔ Σ𝑖 ∈ (1...(𝐾 + 1))({〈1, 𝑁〉}‘𝑖) = 𝑁)) | 
| 47 | 42, 46 | anbi12d 632 | . . . . . . 7
⊢ (𝑔 = {〈1, 𝑁〉} → ((𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁) ↔ ({〈1, 𝑁〉}:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))({〈1, 𝑁〉}‘𝑖) = 𝑁))) | 
| 48 | 47 | elabg 3675 | . . . . . 6
⊢
({〈1, 𝑁〉}
∈ V → ({〈1, 𝑁〉} ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} ↔ ({〈1, 𝑁〉}:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))({〈1, 𝑁〉}‘𝑖) = 𝑁))) | 
| 49 | 41, 48 | ax-mp 5 | . . . . 5
⊢
({〈1, 𝑁〉}
∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} ↔ ({〈1, 𝑁〉}:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))({〈1, 𝑁〉}‘𝑖) = 𝑁)) | 
| 50 | 40, 49 | sylibr 234 | . . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → {〈1, 𝑁〉} ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}) | 
| 51 |  | sticksstones9.4 | . . . . 5
⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} | 
| 52 | 51 | a1i 11 | . . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}) | 
| 53 | 50, 52 | eleqtrrd 2843 | . . 3
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → {〈1, 𝑁〉} ∈ 𝐴) | 
| 54 | 3, 53 | eqeltrd 2840 | . 2
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → if(𝐾 = 0, {〈1, 𝑁〉}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))))) ∈ 𝐴) | 
| 55 |  | sticksstones9.3 | . 2
⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ if(𝐾 = 0, {〈1, 𝑁〉}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) −
1)))))) | 
| 56 | 54, 55 | fmptd 7133 | 1
⊢ (𝜑 → 𝐺:𝐵⟶𝐴) |