| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | smuval2.m | . 2
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘(𝑁 + 1))) | 
| 2 |  | fveq2 6906 | . . . . . 6
⊢ (𝑥 = (𝑁 + 1) → (𝑃‘𝑥) = (𝑃‘(𝑁 + 1))) | 
| 3 | 2 | eleq2d 2827 | . . . . 5
⊢ (𝑥 = (𝑁 + 1) → (𝑁 ∈ (𝑃‘𝑥) ↔ 𝑁 ∈ (𝑃‘(𝑁 + 1)))) | 
| 4 | 3 | bibi2d 342 | . . . 4
⊢ (𝑥 = (𝑁 + 1) → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥)) ↔ (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑁 + 1))))) | 
| 5 | 4 | imbi2d 340 | . . 3
⊢ (𝑥 = (𝑁 + 1) → ((𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥))) ↔ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑁 + 1)))))) | 
| 6 |  | fveq2 6906 | . . . . . 6
⊢ (𝑥 = 𝑘 → (𝑃‘𝑥) = (𝑃‘𝑘)) | 
| 7 | 6 | eleq2d 2827 | . . . . 5
⊢ (𝑥 = 𝑘 → (𝑁 ∈ (𝑃‘𝑥) ↔ 𝑁 ∈ (𝑃‘𝑘))) | 
| 8 | 7 | bibi2d 342 | . . . 4
⊢ (𝑥 = 𝑘 → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥)) ↔ (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘)))) | 
| 9 | 8 | imbi2d 340 | . . 3
⊢ (𝑥 = 𝑘 → ((𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥))) ↔ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘))))) | 
| 10 |  | fveq2 6906 | . . . . . 6
⊢ (𝑥 = (𝑘 + 1) → (𝑃‘𝑥) = (𝑃‘(𝑘 + 1))) | 
| 11 | 10 | eleq2d 2827 | . . . . 5
⊢ (𝑥 = (𝑘 + 1) → (𝑁 ∈ (𝑃‘𝑥) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1)))) | 
| 12 | 11 | bibi2d 342 | . . . 4
⊢ (𝑥 = (𝑘 + 1) → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥)) ↔ (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1))))) | 
| 13 | 12 | imbi2d 340 | . . 3
⊢ (𝑥 = (𝑘 + 1) → ((𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥))) ↔ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1)))))) | 
| 14 |  | fveq2 6906 | . . . . . 6
⊢ (𝑥 = 𝑀 → (𝑃‘𝑥) = (𝑃‘𝑀)) | 
| 15 | 14 | eleq2d 2827 | . . . . 5
⊢ (𝑥 = 𝑀 → (𝑁 ∈ (𝑃‘𝑥) ↔ 𝑁 ∈ (𝑃‘𝑀))) | 
| 16 | 15 | bibi2d 342 | . . . 4
⊢ (𝑥 = 𝑀 → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥)) ↔ (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑀)))) | 
| 17 | 16 | imbi2d 340 | . . 3
⊢ (𝑥 = 𝑀 → ((𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥))) ↔ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑀))))) | 
| 18 |  | smuval.a | . . . 4
⊢ (𝜑 → 𝐴 ⊆
ℕ0) | 
| 19 |  | smuval.b | . . . 4
⊢ (𝜑 → 𝐵 ⊆
ℕ0) | 
| 20 |  | smuval.p | . . . 4
⊢ 𝑃 = seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) | 
| 21 |  | smuval.n | . . . 4
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 22 | 18, 19, 20, 21 | smuval 16518 | . . 3
⊢ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑁 + 1)))) | 
| 23 | 18 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝐴 ⊆
ℕ0) | 
| 24 | 19 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝐵 ⊆
ℕ0) | 
| 25 |  | peano2nn0 12566 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) | 
| 26 | 21, 25 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) | 
| 27 |  | eluznn0 12959 | . . . . . . . . . . 11
⊢ (((𝑁 + 1) ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘(𝑁 + 1))) → 𝑘 ∈ ℕ0) | 
| 28 | 26, 27 | sylan 580 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑘 ∈
ℕ0) | 
| 29 | 23, 24, 20, 28 | smupp1 16517 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑃‘(𝑘 + 1)) = ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)})) | 
| 30 | 29 | eleq2d 2827 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑁 ∈ (𝑃‘(𝑘 + 1)) ↔ 𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}))) | 
| 31 | 23, 24, 20 | smupf 16515 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑃:ℕ0⟶𝒫
ℕ0) | 
| 32 | 31, 28 | ffvelcdmd 7105 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑃‘𝑘) ∈ 𝒫
ℕ0) | 
| 33 | 32 | elpwid 4609 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑃‘𝑘) ⊆
ℕ0) | 
| 34 |  | ssrab2 4080 | . . . . . . . . . . . . . 14
⊢ {𝑛 ∈ ℕ0
∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ⊆
ℕ0 | 
| 35 | 34 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → {𝑛 ∈ ℕ0
∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ⊆
ℕ0) | 
| 36 | 26 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑁 + 1) ∈
ℕ0) | 
| 37 | 33, 35, 36 | sadeq 16509 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∩ (0..^(𝑁 + 1))) = ((((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ({𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1)))) ∩ (0..^(𝑁 + 1)))) | 
| 38 |  | inrab2 4317 | . . . . . . . . . . . . . . . . 17
⊢ ({𝑛 ∈ ℕ0
∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1))) = {𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1))) ∣
(𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} | 
| 39 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑛 ∈
(ℕ0 ∩ (0..^(𝑁 + 1)))) | 
| 40 | 39 | elin1d 4204 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑛 ∈
ℕ0) | 
| 41 | 40 | nn0red 12588 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑛 ∈
ℝ) | 
| 42 | 21 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈
ℕ0) | 
| 43 | 42 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑁 ∈
ℕ0) | 
| 44 | 43 | nn0red 12588 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑁 ∈
ℝ) | 
| 45 |  | 1red 11262 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) → 1
∈ ℝ) | 
| 46 | 44, 45 | readdcld 11290 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
(𝑁 + 1) ∈
ℝ) | 
| 47 | 28 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑘 ∈
ℕ0) | 
| 48 | 47 | nn0red 12588 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑘 ∈
ℝ) | 
| 49 | 39 | elin2d 4205 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑛 ∈ (0..^(𝑁 + 1))) | 
| 50 |  | elfzolt2 13708 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ (0..^(𝑁 + 1)) → 𝑛 < (𝑁 + 1)) | 
| 51 | 49, 50 | syl 17 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑛 < (𝑁 + 1)) | 
| 52 |  | eluzle 12891 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈
(ℤ≥‘(𝑁 + 1)) → (𝑁 + 1) ≤ 𝑘) | 
| 53 | 52 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
(𝑁 + 1) ≤ 𝑘) | 
| 54 | 41, 46, 48, 51, 53 | ltletrd 11421 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑛 < 𝑘) | 
| 55 | 41, 48 | ltnled 11408 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
(𝑛 < 𝑘 ↔ ¬ 𝑘 ≤ 𝑛)) | 
| 56 | 54, 55 | mpbid 232 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
¬ 𝑘 ≤ 𝑛) | 
| 57 | 24 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝐵 ⊆
ℕ0) | 
| 58 | 57 | sseld 3982 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
((𝑛 − 𝑘) ∈ 𝐵 → (𝑛 − 𝑘) ∈
ℕ0)) | 
| 59 |  | nn0ge0 12551 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑛 − 𝑘) ∈ ℕ0 → 0 ≤
(𝑛 − 𝑘)) | 
| 60 | 58, 59 | syl6 35 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
((𝑛 − 𝑘) ∈ 𝐵 → 0 ≤ (𝑛 − 𝑘))) | 
| 61 | 41, 48 | subge0d 11853 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) → (0
≤ (𝑛 − 𝑘) ↔ 𝑘 ≤ 𝑛)) | 
| 62 | 60, 61 | sylibd 239 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
((𝑛 − 𝑘) ∈ 𝐵 → 𝑘 ≤ 𝑛)) | 
| 63 | 62 | adantld 490 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
((𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵) → 𝑘 ≤ 𝑛)) | 
| 64 | 56, 63 | mtod 198 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
¬ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)) | 
| 65 | 64 | ralrimiva 3146 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ∀𝑛 ∈ (ℕ0
∩ (0..^(𝑁 + 1))) ¬
(𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)) | 
| 66 |  | rabeq0 4388 | . . . . . . . . . . . . . . . . . 18
⊢ ({𝑛 ∈ (ℕ0
∩ (0..^(𝑁 + 1)))
∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} = ∅ ↔ ∀𝑛 ∈ (ℕ0
∩ (0..^(𝑁 + 1))) ¬
(𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)) | 
| 67 | 65, 66 | sylibr 234 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → {𝑛 ∈ (ℕ0
∩ (0..^(𝑁 + 1)))
∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} = ∅) | 
| 68 | 38, 67 | eqtrid 2789 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ({𝑛 ∈ ℕ0
∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1))) = ∅) | 
| 69 | 68 | oveq2d 7447 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ({𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1)))) = (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ∅)) | 
| 70 |  | inss1 4237 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ⊆ (𝑃‘𝑘) | 
| 71 | 70, 33 | sstrid 3995 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ⊆
ℕ0) | 
| 72 |  | sadid1 16505 | . . . . . . . . . . . . . . . 16
⊢ (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ⊆ ℕ0 →
(((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ∅) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1)))) | 
| 73 | 71, 72 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ∅) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1)))) | 
| 74 | 69, 73 | eqtrd 2777 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ({𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1)))) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1)))) | 
| 75 | 74 | ineq1d 4219 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ((((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ({𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1)))) ∩ (0..^(𝑁 + 1))) = (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ∩ (0..^(𝑁 + 1)))) | 
| 76 |  | inass 4228 | . . . . . . . . . . . . . 14
⊢ (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ∩ (0..^(𝑁 + 1))) = ((𝑃‘𝑘) ∩ ((0..^(𝑁 + 1)) ∩ (0..^(𝑁 + 1)))) | 
| 77 |  | inidm 4227 | . . . . . . . . . . . . . . 15
⊢
((0..^(𝑁 + 1)) ∩
(0..^(𝑁 + 1))) =
(0..^(𝑁 +
1)) | 
| 78 | 77 | ineq2i 4217 | . . . . . . . . . . . . . 14
⊢ ((𝑃‘𝑘) ∩ ((0..^(𝑁 + 1)) ∩ (0..^(𝑁 + 1)))) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) | 
| 79 | 76, 78 | eqtri 2765 | . . . . . . . . . . . . 13
⊢ (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ∩ (0..^(𝑁 + 1))) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) | 
| 80 | 75, 79 | eqtrdi 2793 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ((((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ({𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1)))) ∩ (0..^(𝑁 + 1))) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1)))) | 
| 81 | 37, 80 | eqtrd 2777 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∩ (0..^(𝑁 + 1))) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1)))) | 
| 82 | 81 | eleq2d 2827 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑁 ∈ (((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∩ (0..^(𝑁 + 1))) ↔ 𝑁 ∈ ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))))) | 
| 83 |  | elin 3967 | . . . . . . . . . 10
⊢ (𝑁 ∈ (((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∩ (0..^(𝑁 + 1))) ↔ (𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∧ 𝑁 ∈ (0..^(𝑁 + 1)))) | 
| 84 |  | elin 3967 | . . . . . . . . . 10
⊢ (𝑁 ∈ ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ↔ (𝑁 ∈ (𝑃‘𝑘) ∧ 𝑁 ∈ (0..^(𝑁 + 1)))) | 
| 85 | 82, 83, 84 | 3bitr3g 313 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ((𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∧ 𝑁 ∈ (0..^(𝑁 + 1))) ↔ (𝑁 ∈ (𝑃‘𝑘) ∧ 𝑁 ∈ (0..^(𝑁 + 1))))) | 
| 86 |  | nn0uz 12920 | . . . . . . . . . . . . 13
⊢
ℕ0 = (ℤ≥‘0) | 
| 87 | 42, 86 | eleqtrdi 2851 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈
(ℤ≥‘0)) | 
| 88 |  | eluzfz2 13572 | . . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘0) → 𝑁 ∈ (0...𝑁)) | 
| 89 | 87, 88 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈ (0...𝑁)) | 
| 90 | 42 | nn0zd 12639 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈ ℤ) | 
| 91 |  | fzval3 13773 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ →
(0...𝑁) = (0..^(𝑁 + 1))) | 
| 92 | 90, 91 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (0...𝑁) = (0..^(𝑁 + 1))) | 
| 93 | 89, 92 | eleqtrd 2843 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈ (0..^(𝑁 + 1))) | 
| 94 | 93 | biantrud 531 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ↔ (𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∧ 𝑁 ∈ (0..^(𝑁 + 1))))) | 
| 95 | 93 | biantrud 531 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑁 ∈ (𝑃‘𝑘) ↔ (𝑁 ∈ (𝑃‘𝑘) ∧ 𝑁 ∈ (0..^(𝑁 + 1))))) | 
| 96 | 85, 94, 95 | 3bitr4d 311 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ↔ 𝑁 ∈ (𝑃‘𝑘))) | 
| 97 | 30, 96 | bitrd 279 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑁 ∈ (𝑃‘(𝑘 + 1)) ↔ 𝑁 ∈ (𝑃‘𝑘))) | 
| 98 | 97 | bibi2d 342 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1))) ↔ (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘)))) | 
| 99 | 98 | biimprd 248 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘)) → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1))))) | 
| 100 | 99 | expcom 413 | . . . 4
⊢ (𝑘 ∈
(ℤ≥‘(𝑁 + 1)) → (𝜑 → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘)) → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1)))))) | 
| 101 | 100 | a2d 29 | . . 3
⊢ (𝑘 ∈
(ℤ≥‘(𝑁 + 1)) → ((𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘))) → (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1)))))) | 
| 102 | 5, 9, 13, 17, 22, 101 | uzind4i 12952 | . 2
⊢ (𝑀 ∈
(ℤ≥‘(𝑁 + 1)) → (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑀)))) | 
| 103 | 1, 102 | mpcom 38 | 1
⊢ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑀))) |