Step | Hyp | Ref
| Expression |
1 | | smu01lem.1 |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆
ℕ0) |
2 | | smu01lem.2 |
. . . . . 6
⊢ (𝜑 → 𝐵 ⊆
ℕ0) |
3 | | smucl 15044 |
. . . . . 6
⊢ ((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0) → (𝐴 smul 𝐵) ⊆
ℕ0) |
4 | 1, 2, 3 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (𝐴 smul 𝐵) ⊆
ℕ0) |
5 | 4 | sseld 3567 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ (𝐴 smul 𝐵) → 𝑘 ∈
ℕ0)) |
6 | | noel 3878 |
. . . . . . 7
⊢ ¬
𝑘 ∈
∅ |
7 | | peano2nn0 11210 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ0) |
8 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 0 → (seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑥) = (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 −
1))))‘0)) |
9 | 8 | eqeq1d 2612 |
. . . . . . . . . . . 12
⊢ (𝑥 = 0 → ((seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑥) = ∅ ↔ (seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘0) =
∅)) |
10 | 9 | imbi2d 329 |
. . . . . . . . . . 11
⊢ (𝑥 = 0 → ((𝜑 → (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑥) = ∅) ↔ (𝜑 → (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘0) =
∅))) |
11 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑘 → (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑥) = (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘)) |
12 | 11 | eqeq1d 2612 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑘 → ((seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑥) = ∅ ↔ (seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘) = ∅)) |
13 | 12 | imbi2d 329 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑘 → ((𝜑 → (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑥) = ∅) ↔ (𝜑 → (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘) = ∅))) |
14 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑘 + 1) → (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑥) = (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1))) |
15 | 14 | eqeq1d 2612 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑘 + 1) → ((seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑥) = ∅ ↔ (seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1)) =
∅)) |
16 | 15 | imbi2d 329 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑘 + 1) → ((𝜑 → (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑥) = ∅) ↔ (𝜑 → (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1)) =
∅))) |
17 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
seq0((𝑝 ∈
𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) = seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) |
18 | 1, 2, 17 | smup0 15039 |
. . . . . . . . . . 11
⊢ (𝜑 → (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘0) =
∅) |
19 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢
((seq0((𝑝 ∈
𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘) = ∅ → ((seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) = (∅ sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)})) |
20 | 1 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐴 ⊆
ℕ0) |
21 | 2 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐵 ⊆
ℕ0) |
22 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
23 | 20, 21, 17, 22 | smupp1 15040 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1)) = ((seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)})) |
24 | | smu01lem.3 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ ¬ (𝑘 ∈
𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)) |
25 | 24 | anassrs 678 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
→ ¬ (𝑘 ∈
𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)) |
26 | 25 | ralrimiva 2949 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
∀𝑛 ∈
ℕ0 ¬ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)) |
27 | | rabeq0 3911 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑛 ∈ ℕ0
∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} = ∅ ↔ ∀𝑛 ∈ ℕ0
¬ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)) |
28 | 26, 27 | sylibr 223 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → {𝑛 ∈ ℕ0
∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} = ∅) |
29 | 28 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (∅
sadd {𝑛 ∈
ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) = (∅ sadd
∅)) |
30 | | 0ss 3924 |
. . . . . . . . . . . . . . . . 17
⊢ ∅
⊆ ℕ0 |
31 | | sadid1 15028 |
. . . . . . . . . . . . . . . . 17
⊢ (∅
⊆ ℕ0 → (∅ sadd ∅) =
∅) |
32 | 30, 31 | mp1i 13 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (∅
sadd ∅) = ∅) |
33 | 29, 32 | eqtr2d 2645 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ∅ =
(∅ sadd {𝑛 ∈
ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)})) |
34 | 23, 33 | eqeq12d 2625 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
((seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1)) = ∅ ↔
((seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) = (∅ sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}))) |
35 | 19, 34 | syl5ibr 235 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
((seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘) = ∅ → (seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1)) =
∅)) |
36 | 35 | expcom 450 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ (𝜑 →
((seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘) = ∅ → (seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1)) =
∅))) |
37 | 36 | a2d 29 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ ((𝜑 →
(seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘) = ∅) → (𝜑 → (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1)) =
∅))) |
38 | 10, 13, 16, 16, 18, 37 | nn0ind 11348 |
. . . . . . . . . 10
⊢ ((𝑘 + 1) ∈ ℕ0
→ (𝜑 → (seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1)) =
∅)) |
39 | 7, 38 | syl 17 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ (𝜑 → (seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1)) =
∅)) |
40 | 39 | impcom 445 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1)) =
∅) |
41 | 40 | eleq2d 2673 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 ∈ (seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1)) ↔ 𝑘 ∈ ∅)) |
42 | 6, 41 | mtbiri 316 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ¬
𝑘 ∈ (seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1))) |
43 | 20, 21, 17, 22 | smuval 15041 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 ∈ (𝐴 smul 𝐵) ↔ 𝑘 ∈ (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1)))) |
44 | 42, 43 | mtbird 314 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ¬
𝑘 ∈ (𝐴 smul 𝐵)) |
45 | 44 | ex 449 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ ℕ0 → ¬
𝑘 ∈ (𝐴 smul 𝐵))) |
46 | 5, 45 | syld 46 |
. . 3
⊢ (𝜑 → (𝑘 ∈ (𝐴 smul 𝐵) → ¬ 𝑘 ∈ (𝐴 smul 𝐵))) |
47 | 46 | pm2.01d 180 |
. 2
⊢ (𝜑 → ¬ 𝑘 ∈ (𝐴 smul 𝐵)) |
48 | 47 | eq0rdv 3931 |
1
⊢ (𝜑 → (𝐴 smul 𝐵) = ∅) |