Metamath Proof Explorer

Theorem smu01lem

Description: Lemma for smu01 and smu02 . (Contributed by Mario Carneiro, 19-Sep-2016)

Ref Expression
Hypotheses smu01lem.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
smu01lem.2 ⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
smu01lem.3 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) )
Assertion smu01lem ( 𝜑 → ( 𝐴 smul 𝐵 ) = ∅ )

Proof

Step Hyp Ref Expression
1 smu01lem.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
2 smu01lem.2 ⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
3 smu01lem.3 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) )
4 smucl ⊢ ( ( 𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0 ) → ( 𝐴 smul 𝐵 ) ⊆ ℕ0 )
5 1 2 4 syl2anc ⊢ ( 𝜑 → ( 𝐴 smul 𝐵 ) ⊆ ℕ0 )
6 5 sseld ⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐴 smul 𝐵 ) → 𝑘 ∈ ℕ0 ) )
7 noel ⊢ ¬ 𝑘 ∈ ∅
8 peano2nn0 ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ0 )
9 fveqeq2 ⊢ ( 𝑥 = 0 → ( ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑥 ) = ∅ ↔ ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 0 ) = ∅ ) )
10 9 imbi2d ⊢ ( 𝑥 = 0 → ( ( 𝜑 → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑥 ) = ∅ ) ↔ ( 𝜑 → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 0 ) = ∅ ) ) )
11 fveqeq2 ⊢ ( 𝑥 = 𝑘 → ( ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑥 ) = ∅ ↔ ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) = ∅ ) )
12 11 imbi2d ⊢ ( 𝑥 = 𝑘 → ( ( 𝜑 → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑥 ) = ∅ ) ↔ ( 𝜑 → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) = ∅ ) ) )
13 fveqeq2 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑥 ) = ∅ ↔ ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ∅ ) )
14 13 imbi2d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝜑 → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑥 ) = ∅ ) ↔ ( 𝜑 → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ∅ ) ) )
15 eqid ⊢ seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) = seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
16 1 2 15 smup0 ⊢ ( 𝜑 → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 0 ) = ∅ )
17 oveq1 ⊢ ( ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) = ∅ → ( ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) = ( ∅ sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) )
18 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ⊆ ℕ0 )
19 2 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐵 ⊆ ℕ0 )
20 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
21 18 19 15 20 smupp1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) )
22 3 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) )
23 22 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ∀ 𝑛 ∈ ℕ0 ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) )
24 rabeq0 ⊢ ( { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } = ∅ ↔ ∀ 𝑛 ∈ ℕ0 ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) )
25 23 24 sylibr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } = ∅ )
26 25 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ∅ sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) = ( ∅ sadd ∅ ) )
27 0ss ⊢ ∅ ⊆ ℕ0
28 sadid1 ⊢ ( ∅ ⊆ ℕ0 → ( ∅ sadd ∅ ) = ∅ )
29 27 28 mp1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ∅ sadd ∅ ) = ∅ )
30 26 29 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ∅ = ( ∅ sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) )
31 21 30 eqeq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ∅ ↔ ( ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) = ( ∅ sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) ) )
32 17 31 syl5ibr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) = ∅ → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ∅ ) )
33 32 expcom ⊢ ( 𝑘 ∈ ℕ0 → ( 𝜑 → ( ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) = ∅ → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ∅ ) ) )
34 33 a2d ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝜑 → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑘 ) = ∅ ) → ( 𝜑 → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ∅ ) ) )
35 10 12 14 14 16 34 nn0ind ⊢ ( ( 𝑘 + 1 ) ∈ ℕ0 → ( 𝜑 → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ∅ ) )
36 8 35 syl ⊢ ( 𝑘 ∈ ℕ0 → ( 𝜑 → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ∅ ) )
37 36 impcom ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) = ∅ )
38 37 eleq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ∈ ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) ↔ 𝑘 ∈ ∅ ) )
39 7 38 mtbiri ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ¬ 𝑘 ∈ ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) )
40 18 19 15 20 smuval ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑘 ∈ ( seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑘 + 1 ) ) ) )
41 39 40 mtbird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ¬ 𝑘 ∈ ( 𝐴 smul 𝐵 ) )
42 41 ex ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 → ¬ 𝑘 ∈ ( 𝐴 smul 𝐵 ) ) )
43 6 42 syld ⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐴 smul 𝐵 ) → ¬ 𝑘 ∈ ( 𝐴 smul 𝐵 ) ) )
44 43 pm2.01d ⊢ ( 𝜑 → ¬ 𝑘 ∈ ( 𝐴 smul 𝐵 ) )
45 44 eq0rdv ⊢ ( 𝜑 → ( 𝐴 smul 𝐵 ) = ∅ )