This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fprodexp

Description: Positive integer exponentiation of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses fprodexp.kph ⊢ Ⅎ 𝑘 𝜑
fprodexp.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
fprodexp.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fprodexp.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
Assertion fprodexp ( 𝜑 → ∏ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 𝑁 ) = ( ∏ 𝑘 ∈ 𝐴 𝐵 ↑ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 fprodexp.kph ⊢ Ⅎ 𝑘 𝜑
2 fprodexp.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
3 fprodexp.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
4 fprodexp.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
5 prodeq1 ⊢ ( 𝑥 = ∅ → ∏ 𝑘 ∈ 𝑥 ( 𝐵 ↑ 𝑁 ) = ∏ 𝑘 ∈ ∅ ( 𝐵 ↑ 𝑁 ) )
6 prodeq1 ⊢ ( 𝑥 = ∅ → ∏ 𝑘 ∈ 𝑥 𝐵 = ∏ 𝑘 ∈ ∅ 𝐵 )
7 6 oveq1d ⊢ ( 𝑥 = ∅ → ( ∏ 𝑘 ∈ 𝑥 𝐵 ↑ 𝑁 ) = ( ∏ 𝑘 ∈ ∅ 𝐵 ↑ 𝑁 ) )
8 5 7 eqeq12d ⊢ ( 𝑥 = ∅ → ( ∏ 𝑘 ∈ 𝑥 ( 𝐵 ↑ 𝑁 ) = ( ∏ 𝑘 ∈ 𝑥 𝐵 ↑ 𝑁 ) ↔ ∏ 𝑘 ∈ ∅ ( 𝐵 ↑ 𝑁 ) = ( ∏ 𝑘 ∈ ∅ 𝐵 ↑ 𝑁 ) ) )
9 prodeq1 ⊢ ( 𝑥 = 𝑦 → ∏ 𝑘 ∈ 𝑥 ( 𝐵 ↑ 𝑁 ) = ∏ 𝑘 ∈ 𝑦 ( 𝐵 ↑ 𝑁 ) )
10 prodeq1 ⊢ ( 𝑥 = 𝑦 → ∏ 𝑘 ∈ 𝑥 𝐵 = ∏ 𝑘 ∈ 𝑦 𝐵 )
11 10 oveq1d ⊢ ( 𝑥 = 𝑦 → ( ∏ 𝑘 ∈ 𝑥 𝐵 ↑ 𝑁 ) = ( ∏ 𝑘 ∈ 𝑦 𝐵 ↑ 𝑁 ) )
12 9 11 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ∏ 𝑘 ∈ 𝑥 ( 𝐵 ↑ 𝑁 ) = ( ∏ 𝑘 ∈ 𝑥 𝐵 ↑ 𝑁 ) ↔ ∏ 𝑘 ∈ 𝑦 ( 𝐵 ↑ 𝑁 ) = ( ∏ 𝑘 ∈ 𝑦 𝐵 ↑ 𝑁 ) ) )
13 prodeq1 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ∏ 𝑘 ∈ 𝑥 ( 𝐵 ↑ 𝑁 ) = ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ↑ 𝑁 ) )
14 prodeq1 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ∏ 𝑘 ∈ 𝑥 𝐵 = ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 )
15 14 oveq1d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ∏ 𝑘 ∈ 𝑥 𝐵 ↑ 𝑁 ) = ( ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ↑ 𝑁 ) )
16 13 15 eqeq12d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ∏ 𝑘 ∈ 𝑥 ( 𝐵 ↑ 𝑁 ) = ( ∏ 𝑘 ∈ 𝑥 𝐵 ↑ 𝑁 ) ↔ ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ↑ 𝑁 ) = ( ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ↑ 𝑁 ) ) )
17 prodeq1 ⊢ ( 𝑥 = 𝐴 → ∏ 𝑘 ∈ 𝑥 ( 𝐵 ↑ 𝑁 ) = ∏ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 𝑁 ) )
18 prodeq1 ⊢ ( 𝑥 = 𝐴 → ∏ 𝑘 ∈ 𝑥 𝐵 = ∏ 𝑘 ∈ 𝐴 𝐵 )
19 18 oveq1d ⊢ ( 𝑥 = 𝐴 → ( ∏ 𝑘 ∈ 𝑥 𝐵 ↑ 𝑁 ) = ( ∏ 𝑘 ∈ 𝐴 𝐵 ↑ 𝑁 ) )
20 17 19 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ∏ 𝑘 ∈ 𝑥 ( 𝐵 ↑ 𝑁 ) = ( ∏ 𝑘 ∈ 𝑥 𝐵 ↑ 𝑁 ) ↔ ∏ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 𝑁 ) = ( ∏ 𝑘 ∈ 𝐴 𝐵 ↑ 𝑁 ) ) )
21 2 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
22 1exp ⊢ ( 𝑁 ∈ ℤ → ( 1 ↑ 𝑁 ) = 1 )
23 21 22 syl ⊢ ( 𝜑 → ( 1 ↑ 𝑁 ) = 1 )
24 23 eqcomd ⊢ ( 𝜑 → 1 = ( 1 ↑ 𝑁 ) )
25 prod0 ⊢ ∏ 𝑘 ∈ ∅ ( 𝐵 ↑ 𝑁 ) = 1
26 25 a1i ⊢ ( 𝜑 → ∏ 𝑘 ∈ ∅ ( 𝐵 ↑ 𝑁 ) = 1 )
27 prod0 ⊢ ∏ 𝑘 ∈ ∅ 𝐵 = 1
28 27 oveq1i ⊢ ( ∏ 𝑘 ∈ ∅ 𝐵 ↑ 𝑁 ) = ( 1 ↑ 𝑁 )
29 28 a1i ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ∅ 𝐵 ↑ 𝑁 ) = ( 1 ↑ 𝑁 ) )
30 24 26 29 3eqtr4d ⊢ ( 𝜑 → ∏ 𝑘 ∈ ∅ ( 𝐵 ↑ 𝑁 ) = ( ∏ 𝑘 ∈ ∅ 𝐵 ↑ 𝑁 ) )
31 nfv ⊢ Ⅎ 𝑘 ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) )
32 1 31 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) )
33 3 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ) → 𝐴 ∈ Fin )
34 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ) → 𝑦 ⊆ 𝐴 )
35 ssfi ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑦 ⊆ 𝐴 ) → 𝑦 ∈ Fin )
36 33 34 35 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ) → 𝑦 ∈ Fin )
37 36 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → 𝑦 ∈ Fin )
38 simpll ⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑘 ∈ 𝑦 ) → 𝜑 )
39 34 sselda ⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑘 ∈ 𝑦 ) → 𝑘 ∈ 𝐴 )
40 38 39 4 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑘 ∈ 𝑦 ) → 𝐵 ∈ ℂ )
41 40 adantlrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝐵 ∈ ℂ )
42 32 37 41 fprodclf ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ∏ 𝑘 ∈ 𝑦 𝐵 ∈ ℂ )
43 simpl ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → 𝜑 )
44 simprr ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) )
45 44 eldifad ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → 𝑧 ∈ 𝐴 )
46 nfv ⊢ Ⅎ 𝑘 𝑧 ∈ 𝐴
47 1 46 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑧 ∈ 𝐴 )
48 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑧 / 𝑘 ⦌ 𝐵
49 48 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℂ
50 47 49 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℂ )
51 eleq1w ⊢ ( 𝑘 = 𝑧 → ( 𝑘 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
52 51 anbi2d ⊢ ( 𝑘 = 𝑧 → ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ) )
53 csbeq1a ⊢ ( 𝑘 = 𝑧 → 𝐵 = ⦋ 𝑧 / 𝑘 ⦌ 𝐵 )
54 53 eleq1d ⊢ ( 𝑘 = 𝑧 → ( 𝐵 ∈ ℂ ↔ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℂ ) )
55 52 54 imbi12d ⊢ ( 𝑘 = 𝑧 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℂ ) ) )
56 50 55 4 chvarfv ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℂ )
57 43 45 56 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℂ )
58 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → 𝑁 ∈ ℕ0 )
59 mulexp ⊢ ( ( ∏ 𝑘 ∈ 𝑦 𝐵 ∈ ℂ ∧ ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( ∏ 𝑘 ∈ 𝑦 𝐵 · ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ↑ 𝑁 ) = ( ( ∏ 𝑘 ∈ 𝑦 𝐵 ↑ 𝑁 ) · ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ↑ 𝑁 ) ) )
60 42 57 58 59 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ( ∏ 𝑘 ∈ 𝑦 𝐵 · ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ↑ 𝑁 ) = ( ( ∏ 𝑘 ∈ 𝑦 𝐵 ↑ 𝑁 ) · ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ↑ 𝑁 ) ) )
61 60 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ( ∏ 𝑘 ∈ 𝑦 𝐵 ↑ 𝑁 ) · ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ↑ 𝑁 ) ) = ( ( ∏ 𝑘 ∈ 𝑦 𝐵 · ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ↑ 𝑁 ) )
62 61 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ∏ 𝑘 ∈ 𝑦 ( 𝐵 ↑ 𝑁 ) = ( ∏ 𝑘 ∈ 𝑦 𝐵 ↑ 𝑁 ) ) → ( ( ∏ 𝑘 ∈ 𝑦 𝐵 ↑ 𝑁 ) · ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ↑ 𝑁 ) ) = ( ( ∏ 𝑘 ∈ 𝑦 𝐵 · ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ↑ 𝑁 ) )
63 nfcv ⊢ Ⅎ 𝑘 ↑
64 nfcv ⊢ Ⅎ 𝑘 𝑁
65 48 63 64 nfov ⊢ Ⅎ 𝑘 ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ↑ 𝑁 )
66 44 eldifbd ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ¬ 𝑧 ∈ 𝑦 )
67 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑘 ∈ 𝑦 ) → 𝑁 ∈ ℕ0 )
68 40 67 expcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑘 ∈ 𝑦 ) → ( 𝐵 ↑ 𝑁 ) ∈ ℂ )
69 68 adantlrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ 𝑘 ∈ 𝑦 ) → ( 𝐵 ↑ 𝑁 ) ∈ ℂ )
70 53 oveq1d ⊢ ( 𝑘 = 𝑧 → ( 𝐵 ↑ 𝑁 ) = ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ↑ 𝑁 ) )
71 57 58 expcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ↑ 𝑁 ) ∈ ℂ )
72 32 65 37 44 66 69 70 71 fprodsplitsn ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ↑ 𝑁 ) = ( ∏ 𝑘 ∈ 𝑦 ( 𝐵 ↑ 𝑁 ) · ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ↑ 𝑁 ) ) )
73 72 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ∏ 𝑘 ∈ 𝑦 ( 𝐵 ↑ 𝑁 ) = ( ∏ 𝑘 ∈ 𝑦 𝐵 ↑ 𝑁 ) ) → ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ↑ 𝑁 ) = ( ∏ 𝑘 ∈ 𝑦 ( 𝐵 ↑ 𝑁 ) · ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ↑ 𝑁 ) ) )
74 oveq1 ⊢ ( ∏ 𝑘 ∈ 𝑦 ( 𝐵 ↑ 𝑁 ) = ( ∏ 𝑘 ∈ 𝑦 𝐵 ↑ 𝑁 ) → ( ∏ 𝑘 ∈ 𝑦 ( 𝐵 ↑ 𝑁 ) · ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ↑ 𝑁 ) ) = ( ( ∏ 𝑘 ∈ 𝑦 𝐵 ↑ 𝑁 ) · ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ↑ 𝑁 ) ) )
75 74 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ∏ 𝑘 ∈ 𝑦 ( 𝐵 ↑ 𝑁 ) = ( ∏ 𝑘 ∈ 𝑦 𝐵 ↑ 𝑁 ) ) → ( ∏ 𝑘 ∈ 𝑦 ( 𝐵 ↑ 𝑁 ) · ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ↑ 𝑁 ) ) = ( ( ∏ 𝑘 ∈ 𝑦 𝐵 ↑ 𝑁 ) · ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ↑ 𝑁 ) ) )
76 73 75 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ∏ 𝑘 ∈ 𝑦 ( 𝐵 ↑ 𝑁 ) = ( ∏ 𝑘 ∈ 𝑦 𝐵 ↑ 𝑁 ) ) → ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ↑ 𝑁 ) = ( ( ∏ 𝑘 ∈ 𝑦 𝐵 ↑ 𝑁 ) · ( ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ↑ 𝑁 ) ) )
77 32 48 37 44 66 41 53 57 fprodsplitsn ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 = ( ∏ 𝑘 ∈ 𝑦 𝐵 · ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
78 77 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ∏ 𝑘 ∈ 𝑦 ( 𝐵 ↑ 𝑁 ) = ( ∏ 𝑘 ∈ 𝑦 𝐵 ↑ 𝑁 ) ) → ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 = ( ∏ 𝑘 ∈ 𝑦 𝐵 · ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) )
79 78 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ∏ 𝑘 ∈ 𝑦 ( 𝐵 ↑ 𝑁 ) = ( ∏ 𝑘 ∈ 𝑦 𝐵 ↑ 𝑁 ) ) → ( ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ↑ 𝑁 ) = ( ( ∏ 𝑘 ∈ 𝑦 𝐵 · ⦋ 𝑧 / 𝑘 ⦌ 𝐵 ) ↑ 𝑁 ) )
80 62 76 79 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) ∧ ∏ 𝑘 ∈ 𝑦 ( 𝐵 ↑ 𝑁 ) = ( ∏ 𝑘 ∈ 𝑦 𝐵 ↑ 𝑁 ) ) → ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ↑ 𝑁 ) = ( ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ↑ 𝑁 ) )
81 80 ex ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( ∏ 𝑘 ∈ 𝑦 ( 𝐵 ↑ 𝑁 ) = ( ∏ 𝑘 ∈ 𝑦 𝐵 ↑ 𝑁 ) → ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) ( 𝐵 ↑ 𝑁 ) = ( ∏ 𝑘 ∈ ( 𝑦 ∪ { 𝑧 } ) 𝐵 ↑ 𝑁 ) ) )
82 8 12 16 20 30 81 3 findcard2d ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 ( 𝐵 ↑ 𝑁 ) = ( ∏ 𝑘 ∈ 𝐴 𝐵 ↑ 𝑁 ) )