Step | Hyp | Ref
| Expression |
1 | | smuval2.m |
. 2
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘(𝑁 + 1))) |
2 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = (𝑁 + 1) → (𝑃‘𝑥) = (𝑃‘(𝑁 + 1))) |
3 | 2 | eleq2d 2673 |
. . . . 5
⊢ (𝑥 = (𝑁 + 1) → (𝑁 ∈ (𝑃‘𝑥) ↔ 𝑁 ∈ (𝑃‘(𝑁 + 1)))) |
4 | 3 | bibi2d 331 |
. . . 4
⊢ (𝑥 = (𝑁 + 1) → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥)) ↔ (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑁 + 1))))) |
5 | 4 | imbi2d 329 |
. . 3
⊢ (𝑥 = (𝑁 + 1) → ((𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥))) ↔ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑁 + 1)))))) |
6 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = 𝑘 → (𝑃‘𝑥) = (𝑃‘𝑘)) |
7 | 6 | eleq2d 2673 |
. . . . 5
⊢ (𝑥 = 𝑘 → (𝑁 ∈ (𝑃‘𝑥) ↔ 𝑁 ∈ (𝑃‘𝑘))) |
8 | 7 | bibi2d 331 |
. . . 4
⊢ (𝑥 = 𝑘 → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥)) ↔ (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘)))) |
9 | 8 | imbi2d 329 |
. . 3
⊢ (𝑥 = 𝑘 → ((𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥))) ↔ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘))))) |
10 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = (𝑘 + 1) → (𝑃‘𝑥) = (𝑃‘(𝑘 + 1))) |
11 | 10 | eleq2d 2673 |
. . . . 5
⊢ (𝑥 = (𝑘 + 1) → (𝑁 ∈ (𝑃‘𝑥) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1)))) |
12 | 11 | bibi2d 331 |
. . . 4
⊢ (𝑥 = (𝑘 + 1) → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥)) ↔ (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1))))) |
13 | 12 | imbi2d 329 |
. . 3
⊢ (𝑥 = (𝑘 + 1) → ((𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥))) ↔ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1)))))) |
14 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = 𝑀 → (𝑃‘𝑥) = (𝑃‘𝑀)) |
15 | 14 | eleq2d 2673 |
. . . . 5
⊢ (𝑥 = 𝑀 → (𝑁 ∈ (𝑃‘𝑥) ↔ 𝑁 ∈ (𝑃‘𝑀))) |
16 | 15 | bibi2d 331 |
. . . 4
⊢ (𝑥 = 𝑀 → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥)) ↔ (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑀)))) |
17 | 16 | imbi2d 329 |
. . 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 15041 |
. . . 4
⊢ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑁 + 1)))) |
23 | 22 | a1i 11 |
. . 3
⊢ ((𝑁 + 1) ∈ ℤ →
(𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑁 + 1))))) |
24 | 18 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝐴 ⊆
ℕ0) |
25 | 19 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝐵 ⊆
ℕ0) |
26 | | peano2nn0 11210 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
27 | 21, 26 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) |
28 | | eluznn0 11633 |
. . . . . . . . . . 11
⊢ (((𝑁 + 1) ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘(𝑁 + 1))) → 𝑘 ∈ ℕ0) |
29 | 27, 28 | sylan 487 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑘 ∈
ℕ0) |
30 | 24, 25, 20, 29 | smupp1 15040 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑃‘(𝑘 + 1)) = ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)})) |
31 | 30 | eleq2d 2673 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑁 ∈ (𝑃‘(𝑘 + 1)) ↔ 𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}))) |
32 | 24, 25, 20 | smupf 15038 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑃:ℕ0⟶𝒫
ℕ0) |
33 | 32, 29 | ffvelrnd 6268 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑃‘𝑘) ∈ 𝒫
ℕ0) |
34 | 33 | elpwid 4118 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑃‘𝑘) ⊆
ℕ0) |
35 | | ssrab2 3650 |
. . . . . . . . . . . . . 14
⊢ {𝑛 ∈ ℕ0
∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ⊆
ℕ0 |
36 | 35 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → {𝑛 ∈ ℕ0
∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ⊆
ℕ0) |
37 | 27 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑁 + 1) ∈
ℕ0) |
38 | 34, 36, 37 | sadeq 15032 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∩ (0..^(𝑁 + 1))) = ((((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ({𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1)))) ∩ (0..^(𝑁 + 1)))) |
39 | | inrab2 3859 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑛 ∈ ℕ0
∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1))) = {𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1))) ∣
(𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} |
40 | | inss1 3795 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(ℕ0 ∩ (0..^(𝑁 + 1))) ⊆
ℕ0 |
41 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑛 ∈
(ℕ0 ∩ (0..^(𝑁 + 1)))) |
42 | 40, 41 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑛 ∈
ℕ0) |
43 | 42 | nn0red 11229 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑛 ∈
ℝ) |
44 | 21 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈
ℕ0) |
45 | 44 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑁 ∈
ℕ0) |
46 | 45 | nn0red 11229 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑁 ∈
ℝ) |
47 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) → 1
∈ ℝ) |
48 | 46, 47 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
(𝑁 + 1) ∈
ℝ) |
49 | 29 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑘 ∈
ℕ0) |
50 | 49 | nn0red 11229 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑘 ∈
ℝ) |
51 | | inss2 3796 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(ℕ0 ∩ (0..^(𝑁 + 1))) ⊆ (0..^(𝑁 + 1)) |
52 | 51, 41 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑛 ∈ (0..^(𝑁 + 1))) |
53 | | elfzolt2 12348 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ (0..^(𝑁 + 1)) → 𝑛 < (𝑁 + 1)) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑛 < (𝑁 + 1)) |
55 | | eluzle 11576 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈
(ℤ≥‘(𝑁 + 1)) → (𝑁 + 1) ≤ 𝑘) |
56 | 55 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
(𝑁 + 1) ≤ 𝑘) |
57 | 43, 48, 50, 54, 56 | ltletrd 10076 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝑛 < 𝑘) |
58 | 43, 50 | ltnled 10063 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
(𝑛 < 𝑘 ↔ ¬ 𝑘 ≤ 𝑛)) |
59 | 57, 58 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
¬ 𝑘 ≤ 𝑛) |
60 | 25 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
𝐵 ⊆
ℕ0) |
61 | 60 | sseld 3567 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
((𝑛 − 𝑘) ∈ 𝐵 → (𝑛 − 𝑘) ∈
ℕ0)) |
62 | | nn0ge0 11195 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑛 − 𝑘) ∈ ℕ0 → 0 ≤
(𝑛 − 𝑘)) |
63 | 61, 62 | syl6 34 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
((𝑛 − 𝑘) ∈ 𝐵 → 0 ≤ (𝑛 − 𝑘))) |
64 | 43, 50 | subge0d 10496 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) → (0
≤ (𝑛 − 𝑘) ↔ 𝑘 ≤ 𝑛)) |
65 | 63, 64 | sylibd 228 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
((𝑛 − 𝑘) ∈ 𝐵 → 𝑘 ≤ 𝑛)) |
66 | 65 | adantld 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
((𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵) → 𝑘 ≤ 𝑛)) |
67 | 59, 66 | mtod 188 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ0 ∩
(0..^(𝑁 + 1)))) →
¬ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)) |
68 | 67 | ralrimiva 2949 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ∀𝑛 ∈ (ℕ0
∩ (0..^(𝑁 + 1))) ¬
(𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)) |
69 | | rabeq0 3911 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑛 ∈ (ℕ0
∩ (0..^(𝑁 + 1)))
∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} = ∅ ↔ ∀𝑛 ∈ (ℕ0
∩ (0..^(𝑁 + 1))) ¬
(𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)) |
70 | 68, 69 | sylibr 223 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → {𝑛 ∈ (ℕ0
∩ (0..^(𝑁 + 1)))
∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} = ∅) |
71 | 39, 70 | syl5eq 2656 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ({𝑛 ∈ ℕ0
∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1))) = ∅) |
72 | 71 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ({𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1)))) = (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ∅)) |
73 | | inss1 3795 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ⊆ (𝑃‘𝑘) |
74 | 73, 34 | syl5ss 3579 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ⊆
ℕ0) |
75 | | sadid1 15028 |
. . . . . . . . . . . . . . . 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 2644 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ({𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1)))) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1)))) |
78 | 77 | ineq1d 3775 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ((((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ({𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1)))) ∩ (0..^(𝑁 + 1))) = (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ∩ (0..^(𝑁 + 1)))) |
79 | | inass 3785 |
. . . . . . . . . . . . . 14
⊢ (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ∩ (0..^(𝑁 + 1))) = ((𝑃‘𝑘) ∩ ((0..^(𝑁 + 1)) ∩ (0..^(𝑁 + 1)))) |
80 | | inidm 3784 |
. . . . . . . . . . . . . . 15
⊢
((0..^(𝑁 + 1)) ∩
(0..^(𝑁 + 1))) =
(0..^(𝑁 +
1)) |
81 | 80 | ineq2i 3773 |
. . . . . . . . . . . . . 14
⊢ ((𝑃‘𝑘) ∩ ((0..^(𝑁 + 1)) ∩ (0..^(𝑁 + 1)))) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) |
82 | 79, 81 | eqtri 2632 |
. . . . . . . . . . . . 13
⊢ (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ∩ (0..^(𝑁 + 1))) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) |
83 | 78, 82 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ((((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ({𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1)))) ∩ (0..^(𝑁 + 1))) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1)))) |
84 | 38, 83 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∩ (0..^(𝑁 + 1))) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1)))) |
85 | 84 | eleq2d 2673 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑁 ∈ (((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∩ (0..^(𝑁 + 1))) ↔ 𝑁 ∈ ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))))) |
86 | | elin 3758 |
. . . . . . . . . 10
⊢ (𝑁 ∈ (((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∩ (0..^(𝑁 + 1))) ↔ (𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∧ 𝑁 ∈ (0..^(𝑁 + 1)))) |
87 | | elin 3758 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ↔ (𝑁 ∈ (𝑃‘𝑘) ∧ 𝑁 ∈ (0..^(𝑁 + 1)))) |
88 | 85, 86, 87 | 3bitr3g 301 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ((𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∧ 𝑁 ∈ (0..^(𝑁 + 1))) ↔ (𝑁 ∈ (𝑃‘𝑘) ∧ 𝑁 ∈ (0..^(𝑁 + 1))))) |
89 | | nn0uz 11598 |
. . . . . . . . . . . . 13
⊢
ℕ0 = (ℤ≥‘0) |
90 | 44, 89 | syl6eleq 2698 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈
(ℤ≥‘0)) |
91 | | eluzfz2 12220 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘0) → 𝑁 ∈ (0...𝑁)) |
92 | 90, 91 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈ (0...𝑁)) |
93 | 44 | nn0zd 11356 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈ ℤ) |
94 | | fzval3 12404 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ →
(0...𝑁) = (0..^(𝑁 + 1))) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (0...𝑁) = (0..^(𝑁 + 1))) |
96 | 92, 95 | eleqtrd 2690 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈ (0..^(𝑁 + 1))) |
97 | 96 | biantrud 527 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ↔ (𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∧ 𝑁 ∈ (0..^(𝑁 + 1))))) |
98 | 96 | biantrud 527 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑁 ∈ (𝑃‘𝑘) ↔ (𝑁 ∈ (𝑃‘𝑘) ∧ 𝑁 ∈ (0..^(𝑁 + 1))))) |
99 | 88, 97, 98 | 3bitr4d 299 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ↔ 𝑁 ∈ (𝑃‘𝑘))) |
100 | 31, 99 | bitrd 267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑁 ∈ (𝑃‘(𝑘 + 1)) ↔ 𝑁 ∈ (𝑃‘𝑘))) |
101 | 100 | bibi2d 331 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1))) ↔ (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘)))) |
102 | 101 | biimprd 237 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘)) → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1))))) |
103 | 102 | expcom 450 |
. . . 4
⊢ (𝑘 ∈
(ℤ≥‘(𝑁 + 1)) → (𝜑 → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘)) → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1)))))) |
104 | 103 | a2d 29 |
. . 3
⊢ (𝑘 ∈
(ℤ≥‘(𝑁 + 1)) → ((𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘))) → (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1)))))) |
105 | 5, 9, 13, 17, 23, 104 | uzind4 11622 |
. 2
⊢ (𝑀 ∈
(ℤ≥‘(𝑁 + 1)) → (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑀)))) |
106 | 1, 105 | mpcom 37 |
1
⊢ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑀))) |