| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | smu01lem.1 | . . . . . 6
⊢ (𝜑 → 𝐴 ⊆
ℕ0) | 
| 2 |  | smu01lem.2 | . . . . . 6
⊢ (𝜑 → 𝐵 ⊆
ℕ0) | 
| 3 |  | smucl 16522 | . . . . . 6
⊢ ((𝐴 ⊆ ℕ0
∧ 𝐵 ⊆
ℕ0) → (𝐴 smul 𝐵) ⊆
ℕ0) | 
| 4 | 1, 2, 3 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (𝐴 smul 𝐵) ⊆
ℕ0) | 
| 5 | 4 | sseld 3981 | . . . 4
⊢ (𝜑 → (𝑘 ∈ (𝐴 smul 𝐵) → 𝑘 ∈
ℕ0)) | 
| 6 |  | noel 4337 | . . . . . . 7
⊢  ¬
𝑘 ∈
∅ | 
| 7 |  | peano2nn0 12568 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ0) | 
| 8 |  | fveqeq2 6914 | . . . . . . . . . . . 12
⊢ (𝑥 = 0 → ((seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑥) = ∅ ↔ (seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘0) =
∅)) | 
| 9 | 8 | imbi2d 340 | . . . . . . . . . . 11
⊢ (𝑥 = 0 → ((𝜑 → (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑥) = ∅) ↔ (𝜑 → (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘0) =
∅))) | 
| 10 |  | fveqeq2 6914 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑘 → ((seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑥) = ∅ ↔ (seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘) = ∅)) | 
| 11 | 10 | imbi2d 340 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑘 → ((𝜑 → (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑥) = ∅) ↔ (𝜑 → (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘) = ∅))) | 
| 12 |  | fveqeq2 6914 | . . . . . . . . . . . 12
⊢ (𝑥 = (𝑘 + 1) → ((seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑥) = ∅ ↔ (seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1)) =
∅)) | 
| 13 | 12 | imbi2d 340 | . . . . . . . . . . 11
⊢ (𝑥 = (𝑘 + 1) → ((𝜑 → (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑥) = ∅) ↔ (𝜑 → (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1)) =
∅))) | 
| 14 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
seq0((𝑝 ∈
𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) = seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) | 
| 15 | 1, 2, 14 | smup0 16517 | . . . . . . . . . . 11
⊢ (𝜑 → (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘0) =
∅) | 
| 16 |  | oveq1 7439 | . . . . . . . . . . . . . 14
⊢
((seq0((𝑝 ∈
𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘) = ∅ → ((seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) = (∅ sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)})) | 
| 17 | 1 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐴 ⊆
ℕ0) | 
| 18 | 2 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐵 ⊆
ℕ0) | 
| 19 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) | 
| 20 | 17, 18, 14, 19 | smupp1 16518 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1)) = ((seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘) sadd {𝑛 ∈ ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)})) | 
| 21 |  | smu01lem.3 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0))
→ ¬ (𝑘 ∈
𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)) | 
| 22 | 21 | anassrs 467 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑛 ∈ ℕ0)
→ ¬ (𝑘 ∈
𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)) | 
| 23 | 22 | ralrimiva 3145 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
∀𝑛 ∈
ℕ0 ¬ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)) | 
| 24 |  | rabeq0 4387 | . . . . . . . . . . . . . . . . . 18
⊢ ({𝑛 ∈ ℕ0
∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} = ∅ ↔ ∀𝑛 ∈ ℕ0
¬ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)) | 
| 25 | 23, 24 | sylibr 234 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → {𝑛 ∈ ℕ0
∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} = ∅) | 
| 26 | 25 | oveq2d 7448 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (∅
sadd {𝑛 ∈
ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) = (∅ sadd
∅)) | 
| 27 |  | 0ss 4399 | . . . . . . . . . . . . . . . . 17
⊢ ∅
⊆ ℕ0 | 
| 28 |  | sadid1 16506 | . . . . . . . . . . . . . . . . 17
⊢ (∅
⊆ ℕ0 → (∅ sadd ∅) =
∅) | 
| 29 | 27, 28 | mp1i 13 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (∅
sadd ∅) = ∅) | 
| 30 | 26, 29 | eqtr2d 2777 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ∅ =
(∅ sadd {𝑛 ∈
ℕ0 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)})) | 
| 31 | 20, 30 | eqeq12d 2752 | . . . . . . . . . . . . . 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 ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}))) | 
| 32 | 16, 31 | imbitrrid 246 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
((seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘) = ∅ → (seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1)) =
∅)) | 
| 33 | 32 | expcom 413 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ (𝜑 →
((seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘) = ∅ → (seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1)) =
∅))) | 
| 34 | 33 | a2d 29 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ ((𝜑 →
(seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘𝑘) = ∅) → (𝜑 → (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1)) =
∅))) | 
| 35 | 9, 11, 13, 13, 15, 34 | nn0ind 12715 | . . . . . . . . . 10
⊢ ((𝑘 + 1) ∈ ℕ0
→ (𝜑 → (seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1)) =
∅)) | 
| 36 | 7, 35 | syl 17 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ (𝜑 → (seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1)) =
∅)) | 
| 37 | 36 | impcom 407 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1)) =
∅) | 
| 38 | 37 | eleq2d 2826 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 ∈ (seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1)) ↔ 𝑘 ∈ ∅)) | 
| 39 | 6, 38 | mtbiri 327 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ¬
𝑘 ∈ (seq0((𝑝 ∈ 𝒫
ℕ0, 𝑚
∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1))) | 
| 40 | 17, 18, 14, 19 | smuval 16519 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 ∈ (𝐴 smul 𝐵) ↔ 𝑘 ∈ (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0
↦ (𝑝 sadd {𝑛 ∈ ℕ0
∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1)))) | 
| 41 | 39, 40 | mtbird 325 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ¬
𝑘 ∈ (𝐴 smul 𝐵)) | 
| 42 | 41 | ex 412 | . . . 4
⊢ (𝜑 → (𝑘 ∈ ℕ0 → ¬
𝑘 ∈ (𝐴 smul 𝐵))) | 
| 43 | 5, 42 | syld 47 | . . 3
⊢ (𝜑 → (𝑘 ∈ (𝐴 smul 𝐵) → ¬ 𝑘 ∈ (𝐴 smul 𝐵))) | 
| 44 | 43 | pm2.01d 190 | . 2
⊢ (𝜑 → ¬ 𝑘 ∈ (𝐴 smul 𝐵)) | 
| 45 | 44 | eq0rdv 4406 | 1
⊢ (𝜑 → (𝐴 smul 𝐵) = ∅) |