Metamath Proof Explorer

Theorem smupvallem

Description: If A only has elements less than N , then all elements of the partial sum sequence past N already equal the final value. (Contributed by Mario Carneiro, 20-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 )
smupvallem.a ⊢ ( 𝜑 → 𝐴 ⊆ ( 0 ..^ 𝑁 ) )
smupvallem.m ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) )
Assertion smupvallem ( 𝜑 → ( 𝑃 ‘ 𝑀 ) = ( 𝐴 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 smupvallem.a ⊢ ( 𝜑 → 𝐴 ⊆ ( 0 ..^ 𝑁 ) )
6 smupvallem.m ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) )
7 1 2 3 smupf ⊢ ( 𝜑 → 𝑃 : ℕ0 ⟶ 𝒫 ℕ0 )
8 eluznn0 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑀 ∈ ℕ0 )
9 4 6 8 syl2anc ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
10 7 9 ffvelrnd ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑀 ) ∈ 𝒫 ℕ0 )
11 10 elpwid ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑀 ) ⊆ ℕ0 )
12 11 sseld ⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝑃 ‘ 𝑀 ) → 𝑘 ∈ ℕ0 ) )
13 1 2 3 smufval ⊢ ( 𝜑 → ( 𝐴 smul 𝐵 ) = { 𝑘 ∈ ℕ0 ∣ 𝑘 ∈ ( 𝑃 ‘ ( 𝑘 + 1 ) ) } )
14 ssrab2 ⊢ { 𝑘 ∈ ℕ0 ∣ 𝑘 ∈ ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ℕ0
15 13 14 eqsstrdi ⊢ ( 𝜑 → ( 𝐴 smul 𝐵 ) ⊆ ℕ0 )
16 15 sseld ⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐴 smul 𝐵 ) → 𝑘 ∈ ℕ0 ) )
17 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ) → 𝐴 ⊆ ℕ0 )
18 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ) → 𝐵 ⊆ ℕ0 )
19 simplr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ) → 𝑘 ∈ ℕ0 )
20 6 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) )
21 uztrn ⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ) → 𝑀 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) )
22 20 21 sylan ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ) → 𝑀 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) )
23 17 18 3 19 22 smuval2 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ) → ( 𝑘 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑘 ∈ ( 𝑃 ‘ 𝑀 ) ) )
24 23 bicomd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ) → ( 𝑘 ∈ ( 𝑃 ‘ 𝑀 ) ↔ 𝑘 ∈ ( 𝐴 smul 𝐵 ) ) )
25 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) )
26 simpll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝜑 )
27 fveqeq2 ⊢ ( 𝑥 = 𝑁 → ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑁 ) ↔ ( 𝑃 ‘ 𝑁 ) = ( 𝑃 ‘ 𝑁 ) ) )
28 27 imbi2d ⊢ ( 𝑥 = 𝑁 → ( ( 𝜑 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑁 ) ) ↔ ( 𝜑 → ( 𝑃 ‘ 𝑁 ) = ( 𝑃 ‘ 𝑁 ) ) ) )
29 fveqeq2 ⊢ ( 𝑥 = 𝑘 → ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑁 ) ↔ ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑁 ) ) )
30 29 imbi2d ⊢ ( 𝑥 = 𝑘 → ( ( 𝜑 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑁 ) ) ↔ ( 𝜑 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑁 ) ) ) )
31 fveqeq2 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑁 ) ↔ ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 𝑁 ) ) )
32 31 imbi2d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝜑 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑁 ) ) ↔ ( 𝜑 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 𝑁 ) ) ) )
33 fveqeq2 ⊢ ( 𝑥 = 𝑀 → ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑁 ) ↔ ( 𝑃 ‘ 𝑀 ) = ( 𝑃 ‘ 𝑁 ) ) )
34 33 imbi2d ⊢ ( 𝑥 = 𝑀 → ( ( 𝜑 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑁 ) ) ↔ ( 𝜑 → ( 𝑃 ‘ 𝑀 ) = ( 𝑃 ‘ 𝑁 ) ) ) )
35 eqidd ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑁 ) = ( 𝑃 ‘ 𝑁 ) )
36 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝐴 ⊆ ℕ0 )
37 2 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝐵 ⊆ ℕ0 )
38 eluznn0 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑘 ∈ ℕ0 )
39 4 38 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑘 ∈ ℕ0 )
40 36 37 3 39 smupp1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑃 ‘ 𝑘 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) )
41 4 nn0red ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
42 41 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ℝ )
43 39 nn0red ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑘 ∈ ℝ )
44 eluzle ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑁 ≤ 𝑘 )
45 44 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ≤ 𝑘 )
46 42 43 45 lensymd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ¬ 𝑘 < 𝑁 )
47 5 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝐴 ⊆ ( 0 ..^ 𝑁 ) )
48 47 sseld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑘 ∈ 𝐴 → 𝑘 ∈ ( 0 ..^ 𝑁 ) ) )
49 elfzolt2 ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → 𝑘 < 𝑁 )
50 48 49 syl6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑘 ∈ 𝐴 → 𝑘 < 𝑁 ) )
51 50 adantrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) → 𝑘 < 𝑁 ) )
52 46 51 mtod ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) )
53 52 ralrimivw ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ∀ 𝑛 ∈ ℕ0 ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) )
54 rabeq0 ⊢ ( { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } = ∅ ↔ ∀ 𝑛 ∈ ℕ0 ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) )
55 53 54 sylibr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } = ∅ )
56 55 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑃 ‘ 𝑘 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) = ( ( 𝑃 ‘ 𝑘 ) sadd ∅ ) )
57 7 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑃 : ℕ0 ⟶ 𝒫 ℕ0 )
58 57 39 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑃 ‘ 𝑘 ) ∈ 𝒫 ℕ0 )
59 58 elpwid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑃 ‘ 𝑘 ) ⊆ ℕ0 )
60 sadid1 ⊢ ( ( 𝑃 ‘ 𝑘 ) ⊆ ℕ0 → ( ( 𝑃 ‘ 𝑘 ) sadd ∅ ) = ( 𝑃 ‘ 𝑘 ) )
61 59 60 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑃 ‘ 𝑘 ) sadd ∅ ) = ( 𝑃 ‘ 𝑘 ) )
62 40 56 61 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 𝑘 ) )
63 62 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 𝑁 ) ↔ ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑁 ) ) )
64 63 biimprd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑁 ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 𝑁 ) ) )
65 64 expcom ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝜑 → ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑁 ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 𝑁 ) ) ) )
66 65 a2d ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → ( ( 𝜑 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑁 ) ) → ( 𝜑 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 𝑁 ) ) ) )
67 28 30 32 34 35 66 uzind4i ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝜑 → ( 𝑃 ‘ 𝑀 ) = ( 𝑃 ‘ 𝑁 ) ) )
68 25 26 67 sylc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑃 ‘ 𝑀 ) = ( 𝑃 ‘ 𝑁 ) )
69 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
70 28 30 32 32 35 66 uzind4i ⊢ ( ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝜑 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 𝑁 ) ) )
71 69 26 70 sylc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 𝑁 ) )
72 68 71 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑃 ‘ 𝑀 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
73 72 eleq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑘 ∈ ( 𝑃 ‘ 𝑀 ) ↔ 𝑘 ∈ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
74 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝐴 ⊆ ℕ0 )
75 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝐵 ⊆ ℕ0 )
76 simplr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑘 ∈ ℕ0 )
77 74 75 3 76 smuval ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑘 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑘 ∈ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
78 73 77 bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑘 ∈ ( 𝑃 ‘ 𝑀 ) ↔ 𝑘 ∈ ( 𝐴 smul 𝐵 ) ) )
79 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
80 79 nn0zd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℤ )
81 80 peano2zd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 + 1 ) ∈ ℤ )
82 4 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
83 82 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
84 uztric ⊢ ( ( ( 𝑘 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ∨ ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) )
85 81 83 84 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ∨ ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) )
86 24 78 85 mpjaodan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ∈ ( 𝑃 ‘ 𝑀 ) ↔ 𝑘 ∈ ( 𝐴 smul 𝐵 ) ) )
87 86 ex ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 → ( 𝑘 ∈ ( 𝑃 ‘ 𝑀 ) ↔ 𝑘 ∈ ( 𝐴 smul 𝐵 ) ) ) )
88 12 16 87 pm5.21ndd ⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝑃 ‘ 𝑀 ) ↔ 𝑘 ∈ ( 𝐴 smul 𝐵 ) ) )
89 88 eqrdv ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑀 ) = ( 𝐴 smul 𝐵 ) )