| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sadcl 16499 | . . . . 5
⊢ ((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0) → (𝐴 sadd 𝐵) ⊆
ℕ0) | 
| 2 |  | sadcl 16499 | . . . . 5
⊢ (((𝐴 sadd 𝐵) ⊆ ℕ0 ∧ 𝐶 ⊆ ℕ0)
→ ((𝐴 sadd 𝐵) sadd 𝐶) ⊆
ℕ0) | 
| 3 | 1, 2 | stoic3 1776 | . . . 4
⊢ ((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0 ∧ 𝐶
⊆ ℕ0) → ((𝐴 sadd 𝐵) sadd 𝐶) ⊆
ℕ0) | 
| 4 | 3 | sseld 3982 | . . 3
⊢ ((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0 ∧ 𝐶
⊆ ℕ0) → (𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) → 𝑘 ∈
ℕ0)) | 
| 5 |  | simp1 1137 | . . . . 5
⊢ ((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0 ∧ 𝐶
⊆ ℕ0) → 𝐴 ⊆
ℕ0) | 
| 6 |  | sadcl 16499 | . . . . . 6
⊢ ((𝐵 ⊆ ℕ0
∧ 𝐶 ⊆
ℕ0) → (𝐵 sadd 𝐶) ⊆
ℕ0) | 
| 7 | 6 | 3adant1 1131 | . . . . 5
⊢ ((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0 ∧ 𝐶
⊆ ℕ0) → (𝐵 sadd 𝐶) ⊆
ℕ0) | 
| 8 |  | sadcl 16499 | . . . . 5
⊢ ((𝐴 ⊆ ℕ0
∧ (𝐵 sadd 𝐶) ⊆ ℕ0)
→ (𝐴 sadd (𝐵 sadd 𝐶)) ⊆
ℕ0) | 
| 9 | 5, 7, 8 | syl2anc 584 | . . . 4
⊢ ((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0 ∧ 𝐶
⊆ ℕ0) → (𝐴 sadd (𝐵 sadd 𝐶)) ⊆
ℕ0) | 
| 10 | 9 | sseld 3982 | . . 3
⊢ ((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0 ∧ 𝐶
⊆ ℕ0) → (𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶)) → 𝑘 ∈
ℕ0)) | 
| 11 |  | simpl1 1192 | . . . . . . . 8
⊢ (((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0 ∧ 𝐶
⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝐴 ⊆
ℕ0) | 
| 12 |  | simpl2 1193 | . . . . . . . 8
⊢ (((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0 ∧ 𝐶
⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝐵 ⊆
ℕ0) | 
| 13 |  | simpl3 1194 | . . . . . . . 8
⊢ (((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0 ∧ 𝐶
⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝐶 ⊆
ℕ0) | 
| 14 |  | simpr 484 | . . . . . . . . 9
⊢ (((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0 ∧ 𝐶
⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) | 
| 15 |  | 1nn0 12542 | . . . . . . . . . 10
⊢ 1 ∈
ℕ0 | 
| 16 | 15 | a1i 11 | . . . . . . . . 9
⊢ (((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0 ∧ 𝐶
⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 1 ∈
ℕ0) | 
| 17 | 14, 16 | nn0addcld 12591 | . . . . . . . 8
⊢ (((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0 ∧ 𝐶
⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ∈
ℕ0) | 
| 18 | 11, 12, 13, 17 | sadasslem 16507 | . . . . . . 7
⊢ (((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0 ∧ 𝐶
⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^(𝑘 + 1))) = ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^(𝑘 + 1)))) | 
| 19 | 18 | eleq2d 2827 | . . . . . 6
⊢ (((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0 ∧ 𝐶
⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑘 ∈ (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^(𝑘 + 1))) ↔ 𝑘 ∈ ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^(𝑘 + 1))))) | 
| 20 |  | elin 3967 | . . . . . 6
⊢ (𝑘 ∈ (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^(𝑘 + 1))) ↔ (𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) ∧ 𝑘 ∈ (0..^(𝑘 + 1)))) | 
| 21 |  | elin 3967 | . . . . . 6
⊢ (𝑘 ∈ ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^(𝑘 + 1))) ↔ (𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶)) ∧ 𝑘 ∈ (0..^(𝑘 + 1)))) | 
| 22 | 19, 20, 21 | 3bitr3g 313 | . . . . 5
⊢ (((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0 ∧ 𝐶
⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → ((𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) ∧ 𝑘 ∈ (0..^(𝑘 + 1))) ↔ (𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶)) ∧ 𝑘 ∈ (0..^(𝑘 + 1))))) | 
| 23 |  | nn0uz 12920 | . . . . . . . . 9
⊢
ℕ0 = (ℤ≥‘0) | 
| 24 | 14, 23 | eleqtrdi 2851 | . . . . . . . 8
⊢ (((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0 ∧ 𝐶
⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
(ℤ≥‘0)) | 
| 25 |  | eluzfz2 13572 | . . . . . . . 8
⊢ (𝑘 ∈
(ℤ≥‘0) → 𝑘 ∈ (0...𝑘)) | 
| 26 | 24, 25 | syl 17 | . . . . . . 7
⊢ (((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0 ∧ 𝐶
⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ (0...𝑘)) | 
| 27 | 14 | nn0zd 12639 | . . . . . . . 8
⊢ (((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0 ∧ 𝐶
⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℤ) | 
| 28 |  | fzval3 13773 | . . . . . . . 8
⊢ (𝑘 ∈ ℤ →
(0...𝑘) = (0..^(𝑘 + 1))) | 
| 29 | 27, 28 | syl 17 | . . . . . . 7
⊢ (((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0 ∧ 𝐶
⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) →
(0...𝑘) = (0..^(𝑘 + 1))) | 
| 30 | 26, 29 | eleqtrd 2843 | . . . . . 6
⊢ (((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0 ∧ 𝐶
⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ (0..^(𝑘 + 1))) | 
| 31 | 30 | biantrud 531 | . . . . 5
⊢ (((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0 ∧ 𝐶
⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) ↔ (𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) ∧ 𝑘 ∈ (0..^(𝑘 + 1))))) | 
| 32 | 30 | biantrud 531 | . . . . 5
⊢ (((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0 ∧ 𝐶
⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶)) ↔ (𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶)) ∧ 𝑘 ∈ (0..^(𝑘 + 1))))) | 
| 33 | 22, 31, 32 | 3bitr4d 311 | . . . 4
⊢ (((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0 ∧ 𝐶
⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) ↔ 𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶)))) | 
| 34 | 33 | ex 412 | . . 3
⊢ ((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0 ∧ 𝐶
⊆ ℕ0) → (𝑘 ∈ ℕ0 → (𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) ↔ 𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶))))) | 
| 35 | 4, 10, 34 | pm5.21ndd 379 | . 2
⊢ ((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0 ∧ 𝐶
⊆ ℕ0) → (𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) ↔ 𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶)))) | 
| 36 | 35 | eqrdv 2735 | 1
⊢ ((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0 ∧ 𝐶
⊆ ℕ0) → ((𝐴 sadd 𝐵) sadd 𝐶) = (𝐴 sadd (𝐵 sadd 𝐶))) |