Step | Hyp | Ref
| Expression |
1 | | smuval2.m |
. 2
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘(𝑁 + 1))) |
2 | | fveq2 6668 |
. . . . . 6
⊢ (𝑥 = (𝑁 + 1) → (𝑃‘𝑥) = (𝑃‘(𝑁 + 1))) |
3 | 2 | eleq2d 2818 |
. . . . 5
⊢ (𝑥 = (𝑁 + 1) → (𝑁 ∈ (𝑃‘𝑥) ↔ 𝑁 ∈ (𝑃‘(𝑁 + 1)))) |
4 | 3 | bibi2d 346 |
. . . 4
⊢ (𝑥 = (𝑁 + 1) → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥)) ↔ (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑁 + 1))))) |
5 | 4 | imbi2d 344 |
. . 3
⊢ (𝑥 = (𝑁 + 1) → ((𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥))) ↔ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑁 + 1)))))) |
6 | | fveq2 6668 |
. . . . . 6
⊢ (𝑥 = 𝑘 → (𝑃‘𝑥) = (𝑃‘𝑘)) |
7 | 6 | eleq2d 2818 |
. . . . 5
⊢ (𝑥 = 𝑘 → (𝑁 ∈ (𝑃‘𝑥) ↔ 𝑁 ∈ (𝑃‘𝑘))) |
8 | 7 | bibi2d 346 |
. . . 4
⊢ (𝑥 = 𝑘 → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥)) ↔ (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘)))) |
9 | 8 | imbi2d 344 |
. . 3
⊢ (𝑥 = 𝑘 → ((𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥))) ↔ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘))))) |
10 | | fveq2 6668 |
. . . . . 6
⊢ (𝑥 = (𝑘 + 1) → (𝑃‘𝑥) = (𝑃‘(𝑘 + 1))) |
11 | 10 | eleq2d 2818 |
. . . . 5
⊢ (𝑥 = (𝑘 + 1) → (𝑁 ∈ (𝑃‘𝑥) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1)))) |
12 | 11 | bibi2d 346 |
. . . 4
⊢ (𝑥 = (𝑘 + 1) → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥)) ↔ (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1))))) |
13 | 12 | imbi2d 344 |
. . 3
⊢ (𝑥 = (𝑘 + 1) → ((𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥))) ↔ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1)))))) |
14 | | fveq2 6668 |
. . . . . 6
⊢ (𝑥 = 𝑀 → (𝑃‘𝑥) = (𝑃‘𝑀)) |
15 | 14 | eleq2d 2818 |
. . . . 5
⊢ (𝑥 = 𝑀 → (𝑁 ∈ (𝑃‘𝑥) ↔ 𝑁 ∈ (𝑃‘𝑀))) |
16 | 15 | bibi2d 346 |
. . . 4
⊢ (𝑥 = 𝑀 → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥)) ↔ (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑀)))) |
17 | 16 | imbi2d 344 |
. . 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 15917 |
. . 3
⊢ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑁 + 1)))) |
23 | 18 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝐴 ⊆
ℕ0) |
24 | 19 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝐵 ⊆
ℕ0) |
25 | | peano2nn0 12009 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
26 | 21, 25 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) |
27 | | eluznn0 12392 |
. . . . . . . . . . 11
⊢ (((𝑁 + 1) ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘(𝑁 + 1))) → 𝑘 ∈ ℕ0) |
28 | 26, 27 | sylan 583 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑘 ∈
ℕ0) |
29 | 23, 24, 20, 28 | smupp1 15916 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑃‘(𝑘 + 1)) = ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)})) |
30 | 29 | eleq2d 2818 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑁 ∈ (𝑃‘(𝑘 + 1)) ↔ 𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}))) |
31 | 23, 24, 20 | smupf 15914 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑃:ℕ0⟶𝒫
ℕ0) |
32 | 31, 28 | ffvelrnd 6856 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑃‘𝑘) ∈ 𝒫
ℕ0) |
33 | 32 | elpwid 4496 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑃‘𝑘) ⊆
ℕ0) |
34 | | ssrab2 3967 |
. . . . . . . . . . . . . 14
⊢ {𝑛 ∈ ℕ0
∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ⊆
ℕ0 |
35 | 34 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → {𝑛 ∈ ℕ0
∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ⊆
ℕ0) |
36 | 26 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑁 + 1) ∈
ℕ0) |
37 | 33, 35, 36 | sadeq 15908 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∩ (0..^(𝑁 + 1))) = ((((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ({𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1)))) ∩ (0..^(𝑁 + 1)))) |
38 | | inrab2 4194 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑛 ∈ ℕ0
∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1))) = {𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1))) ∣
(𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} |
39 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑛 ∈
(ℕ0 ∩ (0..^(𝑁 + 1)))) |
40 | 39 | elin1d 4086 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑛 ∈
ℕ0) |
41 | 40 | nn0red 12030 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑛 ∈
ℝ) |
42 | 21 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈
ℕ0) |
43 | 42 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑁 ∈
ℕ0) |
44 | 43 | nn0red 12030 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑁 ∈
ℝ) |
45 | | 1red 10713 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) → 1
∈ ℝ) |
46 | 44, 45 | readdcld 10741 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
(𝑁 + 1) ∈
ℝ) |
47 | 28 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑘 ∈
ℕ0) |
48 | 47 | nn0red 12030 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑘 ∈
ℝ) |
49 | 39 | elin2d 4087 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑛 ∈ (0..^(𝑁 + 1))) |
50 | | elfzolt2 13131 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ (0..^(𝑁 + 1)) → 𝑛 < (𝑁 + 1)) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑛 < (𝑁 + 1)) |
52 | | eluzle 12330 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈
(ℤ≥‘(𝑁 + 1)) → (𝑁 + 1) ≤ 𝑘) |
53 | 52 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
(𝑁 + 1) ≤ 𝑘) |
54 | 41, 46, 48, 51, 53 | ltletrd 10871 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑛 < 𝑘) |
55 | 41, 48 | ltnled 10858 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
(𝑛 < 𝑘 ↔ ¬ 𝑘 ≤ 𝑛)) |
56 | 54, 55 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
¬ 𝑘 ≤ 𝑛) |
57 | 24 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝐵 ⊆
ℕ0) |
58 | 57 | sseld 3874 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
((𝑛 − 𝑘) ∈ 𝐵 → (𝑛 − 𝑘) ∈
ℕ0)) |
59 | | nn0ge0 11994 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑛 − 𝑘) ∈ ℕ0 → 0 ≤
(𝑛 − 𝑘)) |
60 | 58, 59 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
((𝑛 − 𝑘) ∈ 𝐵 → 0 ≤ (𝑛 − 𝑘))) |
61 | 41, 48 | subge0d 11301 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) → (0
≤ (𝑛 − 𝑘) ↔ 𝑘 ≤ 𝑛)) |
62 | 60, 61 | sylibd 242 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
((𝑛 − 𝑘) ∈ 𝐵 → 𝑘 ≤ 𝑛)) |
63 | 62 | adantld 494 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
((𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵) → 𝑘 ≤ 𝑛)) |
64 | 56, 63 | mtod 201 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
¬ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)) |
65 | 64 | ralrimiva 3096 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ∀𝑛 ∈ (ℕ0
∩ (0..^(𝑁 + 1))) ¬
(𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)) |
66 | | rabeq0 4270 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑛 ∈ (ℕ0
∩ (0..^(𝑁 + 1)))
∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} = ∅ ↔ ∀𝑛 ∈ (ℕ0
∩ (0..^(𝑁 + 1))) ¬
(𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)) |
67 | 65, 66 | sylibr 237 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → {𝑛 ∈ (ℕ0
∩ (0..^(𝑁 + 1)))
∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} = ∅) |
68 | 38, 67 | syl5eq 2785 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ({𝑛 ∈ ℕ0
∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1))) = ∅) |
69 | 68 | oveq2d 7180 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ({𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1)))) = (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ∅)) |
70 | | inss1 4117 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ⊆ (𝑃‘𝑘) |
71 | 70, 33 | sstrid 3886 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ⊆
ℕ0) |
72 | | sadid1 15904 |
. . . . . . . . . . . . . . . 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 2773 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ({𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1)))) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1)))) |
75 | 74 | ineq1d 4100 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ((((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ({𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1)))) ∩ (0..^(𝑁 + 1))) = (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ∩ (0..^(𝑁 + 1)))) |
76 | | inass 4108 |
. . . . . . . . . . . . . 14
⊢ (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ∩ (0..^(𝑁 + 1))) = ((𝑃‘𝑘) ∩ ((0..^(𝑁 + 1)) ∩ (0..^(𝑁 + 1)))) |
77 | | inidm 4107 |
. . . . . . . . . . . . . . 15
⊢
((0..^(𝑁 + 1)) ∩
(0..^(𝑁 + 1))) =
(0..^(𝑁 +
1)) |
78 | 77 | ineq2i 4098 |
. . . . . . . . . . . . . 14
⊢ ((𝑃‘𝑘) ∩ ((0..^(𝑁 + 1)) ∩ (0..^(𝑁 + 1)))) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) |
79 | 76, 78 | eqtri 2761 |
. . . . . . . . . . . . 13
⊢ (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ∩ (0..^(𝑁 + 1))) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) |
80 | 75, 79 | eqtrdi 2789 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ((((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ({𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1)))) ∩ (0..^(𝑁 + 1))) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1)))) |
81 | 37, 80 | eqtrd 2773 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∩ (0..^(𝑁 + 1))) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1)))) |
82 | 81 | eleq2d 2818 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑁 ∈ (((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∩ (0..^(𝑁 + 1))) ↔ 𝑁 ∈ ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))))) |
83 | | elin 3857 |
. . . . . . . . . 10
⊢ (𝑁 ∈ (((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∩ (0..^(𝑁 + 1))) ↔ (𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∧ 𝑁 ∈ (0..^(𝑁 + 1)))) |
84 | | elin 3857 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ↔ (𝑁 ∈ (𝑃‘𝑘) ∧ 𝑁 ∈ (0..^(𝑁 + 1)))) |
85 | 82, 83, 84 | 3bitr3g 316 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ((𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∧ 𝑁 ∈ (0..^(𝑁 + 1))) ↔ (𝑁 ∈ (𝑃‘𝑘) ∧ 𝑁 ∈ (0..^(𝑁 + 1))))) |
86 | | nn0uz 12355 |
. . . . . . . . . . . . 13
⊢
ℕ0 = (ℤ≥‘0) |
87 | 42, 86 | eleqtrdi 2843 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈
(ℤ≥‘0)) |
88 | | eluzfz2 12999 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘0) → 𝑁 ∈ (0...𝑁)) |
89 | 87, 88 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈ (0...𝑁)) |
90 | 42 | nn0zd 12159 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈ ℤ) |
91 | | fzval3 13190 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ →
(0...𝑁) = (0..^(𝑁 + 1))) |
92 | 90, 91 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (0...𝑁) = (0..^(𝑁 + 1))) |
93 | 89, 92 | eleqtrd 2835 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈ (0..^(𝑁 + 1))) |
94 | 93 | biantrud 535 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ↔ (𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∧ 𝑁 ∈ (0..^(𝑁 + 1))))) |
95 | 93 | biantrud 535 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑁 ∈ (𝑃‘𝑘) ↔ (𝑁 ∈ (𝑃‘𝑘) ∧ 𝑁 ∈ (0..^(𝑁 + 1))))) |
96 | 85, 94, 95 | 3bitr4d 314 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ↔ 𝑁 ∈ (𝑃‘𝑘))) |
97 | 30, 96 | bitrd 282 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑁 ∈ (𝑃‘(𝑘 + 1)) ↔ 𝑁 ∈ (𝑃‘𝑘))) |
98 | 97 | bibi2d 346 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1))) ↔ (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘)))) |
99 | 98 | biimprd 251 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘)) → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1))))) |
100 | 99 | expcom 417 |
. . . 4
⊢ (𝑘 ∈
(ℤ≥‘(𝑁 + 1)) → (𝜑 → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘)) → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1)))))) |
101 | 100 | a2d 29 |
. . 3
⊢ (𝑘 ∈
(ℤ≥‘(𝑁 + 1)) → ((𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘))) → (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1)))))) |
102 | 5, 9, 13, 17, 22, 101 | uzind4i 12385 |
. 2
⊢ (𝑀 ∈
(ℤ≥‘(𝑁 + 1)) → (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑀)))) |
103 | 1, 102 | mpcom 38 |
1
⊢ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑀))) |