Step | Hyp | Ref
| Expression |
1 | | smuval2.m |
. 2
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘(𝑁 + 1))) |
2 | | fveq2 6191 |
. . . . . 6
⊢ (𝑥 = (𝑁 + 1) → (𝑃‘𝑥) = (𝑃‘(𝑁 + 1))) |
3 | 2 | eleq2d 2687 |
. . . . 5
⊢ (𝑥 = (𝑁 + 1) → (𝑁 ∈ (𝑃‘𝑥) ↔ 𝑁 ∈ (𝑃‘(𝑁 + 1)))) |
4 | 3 | bibi2d 332 |
. . . 4
⊢ (𝑥 = (𝑁 + 1) → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥)) ↔ (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑁 + 1))))) |
5 | 4 | imbi2d 330 |
. . 3
⊢ (𝑥 = (𝑁 + 1) → ((𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥))) ↔ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑁 + 1)))))) |
6 | | fveq2 6191 |
. . . . . 6
⊢ (𝑥 = 𝑘 → (𝑃‘𝑥) = (𝑃‘𝑘)) |
7 | 6 | eleq2d 2687 |
. . . . 5
⊢ (𝑥 = 𝑘 → (𝑁 ∈ (𝑃‘𝑥) ↔ 𝑁 ∈ (𝑃‘𝑘))) |
8 | 7 | bibi2d 332 |
. . . 4
⊢ (𝑥 = 𝑘 → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥)) ↔ (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘)))) |
9 | 8 | imbi2d 330 |
. . 3
⊢ (𝑥 = 𝑘 → ((𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥))) ↔ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘))))) |
10 | | fveq2 6191 |
. . . . . 6
⊢ (𝑥 = (𝑘 + 1) → (𝑃‘𝑥) = (𝑃‘(𝑘 + 1))) |
11 | 10 | eleq2d 2687 |
. . . . 5
⊢ (𝑥 = (𝑘 + 1) → (𝑁 ∈ (𝑃‘𝑥) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1)))) |
12 | 11 | bibi2d 332 |
. . . 4
⊢ (𝑥 = (𝑘 + 1) → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥)) ↔ (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1))))) |
13 | 12 | imbi2d 330 |
. . 3
⊢ (𝑥 = (𝑘 + 1) → ((𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥))) ↔ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1)))))) |
14 | | fveq2 6191 |
. . . . . 6
⊢ (𝑥 = 𝑀 → (𝑃‘𝑥) = (𝑃‘𝑀)) |
15 | 14 | eleq2d 2687 |
. . . . 5
⊢ (𝑥 = 𝑀 → (𝑁 ∈ (𝑃‘𝑥) ↔ 𝑁 ∈ (𝑃‘𝑀))) |
16 | 15 | bibi2d 332 |
. . . 4
⊢ (𝑥 = 𝑀 → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥)) ↔ (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑀)))) |
17 | 16 | imbi2d 330 |
. . 3
⊢ (𝑥 = 𝑀 → ((𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥))) ↔ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑀))))) |
18 | | smuval.a |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆
ℕ0) |
19 | | smuval.b |
. . . . 5
⊢ (𝜑 → 𝐵 ⊆
ℕ0) |
20 | | smuval.p |
. . . . 5
⊢ 𝑃 = seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) |
21 | | smuval.n |
. . . . 5
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
22 | 18, 19, 20, 21 | smuval 15203 |
. . . 4
⊢ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑁 + 1)))) |
23 | 22 | a1i 11 |
. . 3
⊢ ((𝑁 + 1) ∈ ℤ →
(𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑁 + 1))))) |
24 | 18 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝐴 ⊆
ℕ0) |
25 | 19 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝐵 ⊆
ℕ0) |
26 | | peano2nn0 11333 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
27 | 21, 26 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) |
28 | | eluznn0 11757 |
. . . . . . . . . . 11
⊢ (((𝑁 + 1) ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘(𝑁 + 1))) → 𝑘 ∈ ℕ0) |
29 | 27, 28 | sylan 488 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑘 ∈
ℕ0) |
30 | 24, 25, 20, 29 | smupp1 15202 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑃‘(𝑘 + 1)) = ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)})) |
31 | 30 | eleq2d 2687 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑁 ∈ (𝑃‘(𝑘 + 1)) ↔ 𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}))) |
32 | 24, 25, 20 | smupf 15200 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑃:ℕ0⟶𝒫
ℕ0) |
33 | 32, 29 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑃‘𝑘) ∈ 𝒫
ℕ0) |
34 | 33 | elpwid 4170 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑃‘𝑘) ⊆
ℕ0) |
35 | | ssrab2 3687 |
. . . . . . . . . . . . . 14
⊢ {𝑛 ∈ ℕ0
∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ⊆
ℕ0 |
36 | 35 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → {𝑛 ∈ ℕ0
∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ⊆
ℕ0) |
37 | 27 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑁 + 1) ∈
ℕ0) |
38 | 34, 36, 37 | sadeq 15194 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∩ (0..^(𝑁 + 1))) = ((((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ({𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1)))) ∩ (0..^(𝑁 + 1)))) |
39 | | inrab2 3900 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑛 ∈ ℕ0
∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1))) = {𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1))) ∣
(𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} |
40 | | inss1 3833 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(ℕ0 ∩ (0..^(𝑁 + 1))) ⊆
ℕ0 |
41 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑛 ∈
(ℕ0 ∩ (0..^(𝑁 + 1)))) |
42 | 40, 41 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑛 ∈
ℕ0) |
43 | 42 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑛 ∈
ℝ) |
44 | 21 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈
ℕ0) |
45 | 44 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑁 ∈
ℕ0) |
46 | 45 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑁 ∈
ℝ) |
47 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) → 1
∈ ℝ) |
48 | 46, 47 | readdcld 10069 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
(𝑁 + 1) ∈
ℝ) |
49 | 29 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑘 ∈
ℕ0) |
50 | 49 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑘 ∈
ℝ) |
51 | | inss2 3834 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(ℕ0 ∩ (0..^(𝑁 + 1))) ⊆ (0..^(𝑁 + 1)) |
52 | 51, 41 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑛 ∈ (0..^(𝑁 + 1))) |
53 | | elfzolt2 12479 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ (0..^(𝑁 + 1)) → 𝑛 < (𝑁 + 1)) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑛 < (𝑁 + 1)) |
55 | | eluzle 11700 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈
(ℤ≥‘(𝑁 + 1)) → (𝑁 + 1) ≤ 𝑘) |
56 | 55 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
(𝑁 + 1) ≤ 𝑘) |
57 | 43, 48, 50, 54, 56 | ltletrd 10197 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑛 < 𝑘) |
58 | 43, 50 | ltnled 10184 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
(𝑛 < 𝑘 ↔ ¬ 𝑘 ≤ 𝑛)) |
59 | 57, 58 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
¬ 𝑘 ≤ 𝑛) |
60 | 25 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝐵 ⊆
ℕ0) |
61 | 60 | sseld 3602 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
((𝑛 − 𝑘) ∈ 𝐵 → (𝑛 − 𝑘) ∈
ℕ0)) |
62 | | nn0ge0 11318 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑛 − 𝑘) ∈ ℕ0 → 0 ≤
(𝑛 − 𝑘)) |
63 | 61, 62 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
((𝑛 − 𝑘) ∈ 𝐵 → 0 ≤ (𝑛 − 𝑘))) |
64 | 43, 50 | subge0d 10617 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) → (0
≤ (𝑛 − 𝑘) ↔ 𝑘 ≤ 𝑛)) |
65 | 63, 64 | sylibd 229 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
((𝑛 − 𝑘) ∈ 𝐵 → 𝑘 ≤ 𝑛)) |
66 | 65 | adantld 483 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
((𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵) → 𝑘 ≤ 𝑛)) |
67 | 59, 66 | mtod 189 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
¬ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)) |
68 | 67 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ∀𝑛 ∈ (ℕ0
∩ (0..^(𝑁 + 1))) ¬
(𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)) |
69 | | rabeq0 3957 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑛 ∈ (ℕ0
∩ (0..^(𝑁 + 1)))
∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} = ∅ ↔ ∀𝑛 ∈ (ℕ0
∩ (0..^(𝑁 + 1))) ¬
(𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)) |
70 | 68, 69 | sylibr 224 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → {𝑛 ∈ (ℕ0
∩ (0..^(𝑁 + 1)))
∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} = ∅) |
71 | 39, 70 | syl5eq 2668 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ({𝑛 ∈ ℕ0
∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1))) = ∅) |
72 | 71 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ({𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1)))) = (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ∅)) |
73 | | inss1 3833 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ⊆ (𝑃‘𝑘) |
74 | 73, 34 | syl5ss 3614 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ⊆
ℕ0) |
75 | | sadid1 15190 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ⊆ ℕ0 →
(((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ∅) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1)))) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ∅) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1)))) |
77 | 72, 76 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ({𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1)))) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1)))) |
78 | 77 | ineq1d 3813 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ((((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ({𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1)))) ∩ (0..^(𝑁 + 1))) = (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ∩ (0..^(𝑁 + 1)))) |
79 | | inass 3823 |
. . . . . . . . . . . . . 14
⊢ (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ∩ (0..^(𝑁 + 1))) = ((𝑃‘𝑘) ∩ ((0..^(𝑁 + 1)) ∩ (0..^(𝑁 + 1)))) |
80 | | inidm 3822 |
. . . . . . . . . . . . . . 15
⊢
((0..^(𝑁 + 1)) ∩
(0..^(𝑁 + 1))) =
(0..^(𝑁 +
1)) |
81 | 80 | ineq2i 3811 |
. . . . . . . . . . . . . 14
⊢ ((𝑃‘𝑘) ∩ ((0..^(𝑁 + 1)) ∩ (0..^(𝑁 + 1)))) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) |
82 | 79, 81 | eqtri 2644 |
. . . . . . . . . . . . 13
⊢ (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ∩ (0..^(𝑁 + 1))) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) |
83 | 78, 82 | syl6eq 2672 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ((((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ({𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1)))) ∩ (0..^(𝑁 + 1))) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1)))) |
84 | 38, 83 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∩ (0..^(𝑁 + 1))) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1)))) |
85 | 84 | eleq2d 2687 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑁 ∈ (((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∩ (0..^(𝑁 + 1))) ↔ 𝑁 ∈ ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))))) |
86 | | elin 3796 |
. . . . . . . . . 10
⊢ (𝑁 ∈ (((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∩ (0..^(𝑁 + 1))) ↔ (𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∧ 𝑁 ∈ (0..^(𝑁 + 1)))) |
87 | | elin 3796 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ↔ (𝑁 ∈ (𝑃‘𝑘) ∧ 𝑁 ∈ (0..^(𝑁 + 1)))) |
88 | 85, 86, 87 | 3bitr3g 302 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ((𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∧ 𝑁 ∈ (0..^(𝑁 + 1))) ↔ (𝑁 ∈ (𝑃‘𝑘) ∧ 𝑁 ∈ (0..^(𝑁 + 1))))) |
89 | | nn0uz 11722 |
. . . . . . . . . . . . 13
⊢
ℕ0 = (ℤ≥‘0) |
90 | 44, 89 | syl6eleq 2711 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈
(ℤ≥‘0)) |
91 | | eluzfz2 12349 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘0) → 𝑁 ∈ (0...𝑁)) |
92 | 90, 91 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈ (0...𝑁)) |
93 | 44 | nn0zd 11480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈ ℤ) |
94 | | fzval3 12536 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ →
(0...𝑁) = (0..^(𝑁 + 1))) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (0...𝑁) = (0..^(𝑁 + 1))) |
96 | 92, 95 | eleqtrd 2703 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈ (0..^(𝑁 + 1))) |
97 | 96 | biantrud 528 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ↔ (𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∧ 𝑁 ∈ (0..^(𝑁 + 1))))) |
98 | 96 | biantrud 528 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑁 ∈ (𝑃‘𝑘) ↔ (𝑁 ∈ (𝑃‘𝑘) ∧ 𝑁 ∈ (0..^(𝑁 + 1))))) |
99 | 88, 97, 98 | 3bitr4d 300 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ↔ 𝑁 ∈ (𝑃‘𝑘))) |
100 | 31, 99 | bitrd 268 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑁 ∈ (𝑃‘(𝑘 + 1)) ↔ 𝑁 ∈ (𝑃‘𝑘))) |
101 | 100 | bibi2d 332 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1))) ↔ (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘)))) |
102 | 101 | biimprd 238 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘)) → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1))))) |
103 | 102 | expcom 451 |
. . . 4
⊢ (𝑘 ∈
(ℤ≥‘(𝑁 + 1)) → (𝜑 → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘)) → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1)))))) |
104 | 103 | a2d 29 |
. . 3
⊢ (𝑘 ∈
(ℤ≥‘(𝑁 + 1)) → ((𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘))) → (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1)))))) |
105 | 5, 9, 13, 17, 23, 104 | uzind4 11746 |
. 2
⊢ (𝑀 ∈
(ℤ≥‘(𝑁 + 1)) → (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑀)))) |
106 | 1, 105 | mpcom 38 |
1
⊢ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑀))) |