Metamath Proof Explorer

Theorem smuval2

Description: The partial sum sequence stabilizes at N after the N + 1 -th element of the sequence; this stable value is the value of the sequence multiplication. (Contributed by Mario Carneiro, 9-Sep-2016)

Ref Expression
Hypotheses smuval.a ⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
smuval.b ⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
smuval.p ⊢ 𝑃 = seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
smuval.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
smuval2.m ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) )
Assertion smuval2 ( 𝜑 → ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 smuval.a ⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
2 smuval.b ⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
3 smuval.p ⊢ 𝑃 = seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
4 smuval.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5 smuval2.m ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) )
6 fveq2 ⊢ ( 𝑥 = ( 𝑁 + 1 ) → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑁 + 1 ) ) )
7 6 eleq2d ⊢ ( 𝑥 = ( 𝑁 + 1 ) → ( 𝑁 ∈ ( 𝑃 ‘ 𝑥 ) ↔ 𝑁 ∈ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) )
8 7 bibi2d ⊢ ( 𝑥 = ( 𝑁 + 1 ) → ( ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ 𝑥 ) ) ↔ ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) )
9 8 imbi2d ⊢ ( 𝑥 = ( 𝑁 + 1 ) → ( ( 𝜑 → ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) ) ) )
10 fveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑘 ) )
11 10 eleq2d ⊢ ( 𝑥 = 𝑘 → ( 𝑁 ∈ ( 𝑃 ‘ 𝑥 ) ↔ 𝑁 ∈ ( 𝑃 ‘ 𝑘 ) ) )
12 11 bibi2d ⊢ ( 𝑥 = 𝑘 → ( ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ 𝑥 ) ) ↔ ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ 𝑘 ) ) ) )
13 12 imbi2d ⊢ ( 𝑥 = 𝑘 → ( ( 𝜑 → ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ 𝑘 ) ) ) ) )
14 fveq2 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
15 14 eleq2d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝑁 ∈ ( 𝑃 ‘ 𝑥 ) ↔ 𝑁 ∈ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
16 15 bibi2d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ 𝑥 ) ) ↔ ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) )
17 16 imbi2d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝜑 → ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) ) )
18 fveq2 ⊢ ( 𝑥 = 𝑀 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑀 ) )
19 18 eleq2d ⊢ ( 𝑥 = 𝑀 → ( 𝑁 ∈ ( 𝑃 ‘ 𝑥 ) ↔ 𝑁 ∈ ( 𝑃 ‘ 𝑀 ) ) )
20 19 bibi2d ⊢ ( 𝑥 = 𝑀 → ( ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ 𝑥 ) ) ↔ ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ 𝑀 ) ) ) )
21 20 imbi2d ⊢ ( 𝑥 = 𝑀 → ( ( 𝜑 → ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ 𝑀 ) ) ) ) )
22 1 2 3 4 smuval ⊢ ( 𝜑 → ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) )
23 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝐴 ⊆ ℕ0 )
24 2 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝐵 ⊆ ℕ0 )
25 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
26 4 25 syl ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ0 )
27 eluznn0 ⊢ ( ( ( 𝑁 + 1 ) ∈ ℕ0 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ℕ0 )
28 26 27 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ℕ0 )
29 23 24 3 28 smupp1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑃 ‘ 𝑘 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) )
30 29 eleq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( 𝑁 ∈ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ↔ 𝑁 ∈ ( ( 𝑃 ‘ 𝑘 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) ) )
31 23 24 3 smupf ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑃 : ℕ0 ⟶ 𝒫 ℕ0 )
32 31 28 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( 𝑃 ‘ 𝑘 ) ∈ 𝒫 ℕ0 )
33 32 elpwid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( 𝑃 ‘ 𝑘 ) ⊆ ℕ0 )
34 ssrab2 ⊢ { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ⊆ ℕ0
35 34 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ⊆ ℕ0 )
36 26 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( 𝑁 + 1 ) ∈ ℕ0 )
37 33 35 36 sadeq ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( ( ( 𝑃 ‘ 𝑘 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) = ( ( ( ( 𝑃 ‘ 𝑘 ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) sadd ( { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
38 inrab2 ⊢ ( { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) = { 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) }
39 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) → 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
40 39 elin1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) → 𝑛 ∈ ℕ0 )
41 40 nn0red ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) → 𝑛 ∈ ℝ )
42 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑁 ∈ ℕ0 )
43 42 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) → 𝑁 ∈ ℕ0 )
44 43 nn0red ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) → 𝑁 ∈ ℝ )
45 1red ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) → 1 ∈ ℝ )
46 44 45 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) → ( 𝑁 + 1 ) ∈ ℝ )
47 28 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) → 𝑘 ∈ ℕ0 )
48 47 nn0red ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) → 𝑘 ∈ ℝ )
49 39 elin2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) → 𝑛 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
50 elfzolt2 ⊢ ( 𝑛 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) → 𝑛 < ( 𝑁 + 1 ) )
51 49 50 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) → 𝑛 < ( 𝑁 + 1 ) )
52 eluzle ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) → ( 𝑁 + 1 ) ≤ 𝑘 )
53 52 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) → ( 𝑁 + 1 ) ≤ 𝑘 )
54 41 46 48 51 53 ltletrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) → 𝑛 < 𝑘 )
55 41 48 ltnled ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) → ( 𝑛 < 𝑘 ↔ ¬ 𝑘 ≤ 𝑛 ) )
56 54 55 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) → ¬ 𝑘 ≤ 𝑛 )
57 24 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) → 𝐵 ⊆ ℕ0 )
58 57 sseld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) → ( ( 𝑛 − 𝑘 ) ∈ 𝐵 → ( 𝑛 − 𝑘 ) ∈ ℕ0 ) )
59 nn0ge0 ⊢ ( ( 𝑛 − 𝑘 ) ∈ ℕ0 → 0 ≤ ( 𝑛 − 𝑘 ) )
60 58 59 syl6 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) → ( ( 𝑛 − 𝑘 ) ∈ 𝐵 → 0 ≤ ( 𝑛 − 𝑘 ) ) )
61 41 48 subge0d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) → ( 0 ≤ ( 𝑛 − 𝑘 ) ↔ 𝑘 ≤ 𝑛 ) )
62 60 61 sylibd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) → ( ( 𝑛 − 𝑘 ) ∈ 𝐵 → 𝑘 ≤ 𝑛 ) )
63 62 adantld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) → ( ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) → 𝑘 ≤ 𝑛 ) )
64 56 63 mtod ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) → ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) )
65 64 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ∀ 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) )
66 rabeq0 ⊢ ( { 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } = ∅ ↔ ∀ 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) )
67 65 66 sylibr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → { 𝑛 ∈ ( ℕ0 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } = ∅ )
68 38 67 syl5eq ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) = ∅ )
69 68 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( ( ( 𝑃 ‘ 𝑘 ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) sadd ( { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) = ( ( ( 𝑃 ‘ 𝑘 ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) sadd ∅ ) )
70 inss1 ⊢ ( ( 𝑃 ‘ 𝑘 ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ⊆ ( 𝑃 ‘ 𝑘 )
71 70 33 sstrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( ( 𝑃 ‘ 𝑘 ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ⊆ ℕ0 )
72 sadid1 ⊢ ( ( ( 𝑃 ‘ 𝑘 ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ⊆ ℕ0 → ( ( ( 𝑃 ‘ 𝑘 ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) sadd ∅ ) = ( ( 𝑃 ‘ 𝑘 ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
73 71 72 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( ( ( 𝑃 ‘ 𝑘 ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) sadd ∅ ) = ( ( 𝑃 ‘ 𝑘 ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
74 69 73 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( ( ( 𝑃 ‘ 𝑘 ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) sadd ( { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) = ( ( 𝑃 ‘ 𝑘 ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
75 74 ineq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( ( ( ( 𝑃 ‘ 𝑘 ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) sadd ( { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) = ( ( ( 𝑃 ‘ 𝑘 ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
76 inass ⊢ ( ( ( 𝑃 ‘ 𝑘 ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) = ( ( 𝑃 ‘ 𝑘 ) ∩ ( ( 0 ..^ ( 𝑁 + 1 ) ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
77 inidm ⊢ ( ( 0 ..^ ( 𝑁 + 1 ) ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) = ( 0 ..^ ( 𝑁 + 1 ) )
78 77 ineq2i ⊢ ( ( 𝑃 ‘ 𝑘 ) ∩ ( ( 0 ..^ ( 𝑁 + 1 ) ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) = ( ( 𝑃 ‘ 𝑘 ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) )
79 76 78 eqtri ⊢ ( ( ( 𝑃 ‘ 𝑘 ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) = ( ( 𝑃 ‘ 𝑘 ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) )
80 75 79 syl6eq ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( ( ( ( 𝑃 ‘ 𝑘 ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) sadd ( { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) = ( ( 𝑃 ‘ 𝑘 ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
81 37 80 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( ( ( 𝑃 ‘ 𝑘 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) = ( ( 𝑃 ‘ 𝑘 ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
82 81 eleq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( 𝑁 ∈ ( ( ( 𝑃 ‘ 𝑘 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ↔ 𝑁 ∈ ( ( 𝑃 ‘ 𝑘 ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) )
83 elin ⊢ ( 𝑁 ∈ ( ( ( 𝑃 ‘ 𝑘 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ↔ ( 𝑁 ∈ ( ( 𝑃 ‘ 𝑘 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) ∧ 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
84 elin ⊢ ( 𝑁 ∈ ( ( 𝑃 ‘ 𝑘 ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ↔ ( 𝑁 ∈ ( 𝑃 ‘ 𝑘 ) ∧ 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
85 82 83 84 3bitr3g ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( ( 𝑁 ∈ ( ( 𝑃 ‘ 𝑘 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) ∧ 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) ↔ ( 𝑁 ∈ ( 𝑃 ‘ 𝑘 ) ∧ 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) )
86 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
87 42 86 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
88 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → 𝑁 ∈ ( 0 ... 𝑁 ) )
89 87 88 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑁 ∈ ( 0 ... 𝑁 ) )
90 42 nn0zd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑁 ∈ ℤ )
91 fzval3 ⊢ ( 𝑁 ∈ ℤ → ( 0 ... 𝑁 ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
92 90 91 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( 0 ... 𝑁 ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
93 89 92 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
94 93 biantrud ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( 𝑁 ∈ ( ( 𝑃 ‘ 𝑘 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) ↔ ( 𝑁 ∈ ( ( 𝑃 ‘ 𝑘 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) ∧ 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) )
95 93 biantrud ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( 𝑁 ∈ ( 𝑃 ‘ 𝑘 ) ↔ ( 𝑁 ∈ ( 𝑃 ‘ 𝑘 ) ∧ 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) )
96 85 94 95 3bitr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( 𝑁 ∈ ( ( 𝑃 ‘ 𝑘 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) ↔ 𝑁 ∈ ( 𝑃 ‘ 𝑘 ) ) )
97 30 96 bitrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( 𝑁 ∈ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ↔ 𝑁 ∈ ( 𝑃 ‘ 𝑘 ) ) )
98 97 bibi2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ↔ ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ 𝑘 ) ) ) )
99 98 biimprd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ 𝑘 ) ) → ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) )
100 99 expcom ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) → ( 𝜑 → ( ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ 𝑘 ) ) → ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) ) )
101 100 a2d ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) → ( ( 𝜑 → ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ 𝑘 ) ) ) → ( 𝜑 → ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) ) ) )
102 9 13 17 21 22 101 uzind4i ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) → ( 𝜑 → ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ 𝑀 ) ) ) )
103 5 102 mpcom ⊢ ( 𝜑 → ( 𝑁 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑁 ∈ ( 𝑃 ‘ 𝑀 ) ) )