Step |
Hyp |
Ref |
Expression |
1 |
|
prodmo.1 |
⊢ 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) |
2 |
|
prodmo.2 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ ) |
3 |
|
prodmo.3 |
⊢ 𝐺 = ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) |
4 |
|
prodmolem3.4 |
⊢ 𝐻 = ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝐾 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 ) |
5 |
|
prodmolem3.5 |
⊢ ( 𝜑 → ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ) |
6 |
|
prodmolem3.6 |
⊢ ( 𝜑 → 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 ) |
7 |
|
prodmolem3.7 |
⊢ ( 𝜑 → 𝐾 : ( 1 ... 𝑁 ) –1-1-onto→ 𝐴 ) |
8 |
|
mulcl |
⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( 𝑚 · 𝑗 ) ∈ ℂ ) |
9 |
8
|
adantl |
⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ) ) → ( 𝑚 · 𝑗 ) ∈ ℂ ) |
10 |
|
mulcom |
⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( 𝑚 · 𝑗 ) = ( 𝑗 · 𝑚 ) ) |
11 |
10
|
adantl |
⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ) ) → ( 𝑚 · 𝑗 ) = ( 𝑗 · 𝑚 ) ) |
12 |
|
mulass |
⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑚 · 𝑗 ) · 𝑧 ) = ( 𝑚 · ( 𝑗 · 𝑧 ) ) ) |
13 |
12
|
adantl |
⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( ( 𝑚 · 𝑗 ) · 𝑧 ) = ( 𝑚 · ( 𝑗 · 𝑧 ) ) ) |
14 |
5
|
simpld |
⊢ ( 𝜑 → 𝑀 ∈ ℕ ) |
15 |
|
nnuz |
⊢ ℕ = ( ℤ≥ ‘ 1 ) |
16 |
14 15
|
eleqtrdi |
⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 1 ) ) |
17 |
|
ssidd |
⊢ ( 𝜑 → ℂ ⊆ ℂ ) |
18 |
|
f1ocnv |
⊢ ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 → ◡ 𝑓 : 𝐴 –1-1-onto→ ( 1 ... 𝑀 ) ) |
19 |
6 18
|
syl |
⊢ ( 𝜑 → ◡ 𝑓 : 𝐴 –1-1-onto→ ( 1 ... 𝑀 ) ) |
20 |
|
f1oco |
⊢ ( ( ◡ 𝑓 : 𝐴 –1-1-onto→ ( 1 ... 𝑀 ) ∧ 𝐾 : ( 1 ... 𝑁 ) –1-1-onto→ 𝐴 ) → ( ◡ 𝑓 ∘ 𝐾 ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑀 ) ) |
21 |
19 7 20
|
syl2anc |
⊢ ( 𝜑 → ( ◡ 𝑓 ∘ 𝐾 ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑀 ) ) |
22 |
|
ovex |
⊢ ( 1 ... 𝑁 ) ∈ V |
23 |
22
|
f1oen |
⊢ ( ( ◡ 𝑓 ∘ 𝐾 ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑀 ) → ( 1 ... 𝑁 ) ≈ ( 1 ... 𝑀 ) ) |
24 |
21 23
|
syl |
⊢ ( 𝜑 → ( 1 ... 𝑁 ) ≈ ( 1 ... 𝑀 ) ) |
25 |
|
fzfi |
⊢ ( 1 ... 𝑁 ) ∈ Fin |
26 |
|
fzfi |
⊢ ( 1 ... 𝑀 ) ∈ Fin |
27 |
|
hashen |
⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ ( 1 ... 𝑀 ) ∈ Fin ) → ( ( ♯ ‘ ( 1 ... 𝑁 ) ) = ( ♯ ‘ ( 1 ... 𝑀 ) ) ↔ ( 1 ... 𝑁 ) ≈ ( 1 ... 𝑀 ) ) ) |
28 |
25 26 27
|
mp2an |
⊢ ( ( ♯ ‘ ( 1 ... 𝑁 ) ) = ( ♯ ‘ ( 1 ... 𝑀 ) ) ↔ ( 1 ... 𝑁 ) ≈ ( 1 ... 𝑀 ) ) |
29 |
24 28
|
sylibr |
⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = ( ♯ ‘ ( 1 ... 𝑀 ) ) ) |
30 |
5
|
simprd |
⊢ ( 𝜑 → 𝑁 ∈ ℕ ) |
31 |
30
|
nnnn0d |
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |
32 |
|
hashfz1 |
⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 ) |
33 |
31 32
|
syl |
⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 ) |
34 |
14
|
nnnn0d |
⊢ ( 𝜑 → 𝑀 ∈ ℕ0 ) |
35 |
|
hashfz1 |
⊢ ( 𝑀 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑀 ) ) = 𝑀 ) |
36 |
34 35
|
syl |
⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... 𝑀 ) ) = 𝑀 ) |
37 |
29 33 36
|
3eqtr3rd |
⊢ ( 𝜑 → 𝑀 = 𝑁 ) |
38 |
37
|
oveq2d |
⊢ ( 𝜑 → ( 1 ... 𝑀 ) = ( 1 ... 𝑁 ) ) |
39 |
38
|
f1oeq2d |
⊢ ( 𝜑 → ( ( ◡ 𝑓 ∘ 𝐾 ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) ↔ ( ◡ 𝑓 ∘ 𝐾 ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑀 ) ) ) |
40 |
21 39
|
mpbird |
⊢ ( 𝜑 → ( ◡ 𝑓 ∘ 𝐾 ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) ) |
41 |
|
fveq2 |
⊢ ( 𝑗 = 𝑚 → ( 𝑓 ‘ 𝑗 ) = ( 𝑓 ‘ 𝑚 ) ) |
42 |
41
|
csbeq1d |
⊢ ( 𝑗 = 𝑚 → ⦋ ( 𝑓 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 ) |
43 |
|
elfznn |
⊢ ( 𝑚 ∈ ( 1 ... 𝑀 ) → 𝑚 ∈ ℕ ) |
44 |
43
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) → 𝑚 ∈ ℕ ) |
45 |
|
f1of |
⊢ ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 → 𝑓 : ( 1 ... 𝑀 ) ⟶ 𝐴 ) |
46 |
6 45
|
syl |
⊢ ( 𝜑 → 𝑓 : ( 1 ... 𝑀 ) ⟶ 𝐴 ) |
47 |
46
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) → ( 𝑓 ‘ 𝑚 ) ∈ 𝐴 ) |
48 |
2
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℂ ) |
49 |
48
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℂ ) |
50 |
|
nfcsb1v |
⊢ Ⅎ 𝑘 ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 |
51 |
50
|
nfel1 |
⊢ Ⅎ 𝑘 ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 ∈ ℂ |
52 |
|
csbeq1a |
⊢ ( 𝑘 = ( 𝑓 ‘ 𝑚 ) → 𝐵 = ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 ) |
53 |
52
|
eleq1d |
⊢ ( 𝑘 = ( 𝑓 ‘ 𝑚 ) → ( 𝐵 ∈ ℂ ↔ ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 ∈ ℂ ) ) |
54 |
51 53
|
rspc |
⊢ ( ( 𝑓 ‘ 𝑚 ) ∈ 𝐴 → ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 ∈ ℂ ) ) |
55 |
47 49 54
|
sylc |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) → ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 ∈ ℂ ) |
56 |
3 42 44 55
|
fvmptd3 |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝑚 ) = ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 ) |
57 |
56 55
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝑚 ) ∈ ℂ ) |
58 |
38
|
f1oeq2d |
⊢ ( 𝜑 → ( 𝐾 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 ↔ 𝐾 : ( 1 ... 𝑁 ) –1-1-onto→ 𝐴 ) ) |
59 |
7 58
|
mpbird |
⊢ ( 𝜑 → 𝐾 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 ) |
60 |
|
f1of |
⊢ ( 𝐾 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 → 𝐾 : ( 1 ... 𝑀 ) ⟶ 𝐴 ) |
61 |
59 60
|
syl |
⊢ ( 𝜑 → 𝐾 : ( 1 ... 𝑀 ) ⟶ 𝐴 ) |
62 |
|
fvco3 |
⊢ ( ( 𝐾 : ( 1 ... 𝑀 ) ⟶ 𝐴 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) = ( ◡ 𝑓 ‘ ( 𝐾 ‘ 𝑖 ) ) ) |
63 |
61 62
|
sylan |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) = ( ◡ 𝑓 ‘ ( 𝐾 ‘ 𝑖 ) ) ) |
64 |
63
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑓 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) = ( 𝑓 ‘ ( ◡ 𝑓 ‘ ( 𝐾 ‘ 𝑖 ) ) ) ) |
65 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 ) |
66 |
61
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐾 ‘ 𝑖 ) ∈ 𝐴 ) |
67 |
|
f1ocnvfv2 |
⊢ ( ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 ∧ ( 𝐾 ‘ 𝑖 ) ∈ 𝐴 ) → ( 𝑓 ‘ ( ◡ 𝑓 ‘ ( 𝐾 ‘ 𝑖 ) ) ) = ( 𝐾 ‘ 𝑖 ) ) |
68 |
65 66 67
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑓 ‘ ( ◡ 𝑓 ‘ ( 𝐾 ‘ 𝑖 ) ) ) = ( 𝐾 ‘ 𝑖 ) ) |
69 |
64 68
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑓 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) = ( 𝐾 ‘ 𝑖 ) ) |
70 |
69
|
csbeq1d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ⦋ ( 𝑓 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝐾 ‘ 𝑖 ) / 𝑘 ⦌ 𝐵 ) |
71 |
70
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( I ‘ ⦋ ( 𝑓 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) / 𝑘 ⦌ 𝐵 ) = ( I ‘ ⦋ ( 𝐾 ‘ 𝑖 ) / 𝑘 ⦌ 𝐵 ) ) |
72 |
|
f1of |
⊢ ( ( ◡ 𝑓 ∘ 𝐾 ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) → ( ◡ 𝑓 ∘ 𝐾 ) : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) ) |
73 |
40 72
|
syl |
⊢ ( 𝜑 → ( ◡ 𝑓 ∘ 𝐾 ) : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) ) |
74 |
73
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ∈ ( 1 ... 𝑀 ) ) |
75 |
|
elfznn |
⊢ ( ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ∈ ( 1 ... 𝑀 ) → ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ∈ ℕ ) |
76 |
|
fveq2 |
⊢ ( 𝑗 = ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑓 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) ) |
77 |
76
|
csbeq1d |
⊢ ( 𝑗 = ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) → ⦋ ( 𝑓 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝑓 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) / 𝑘 ⦌ 𝐵 ) |
78 |
77 3
|
fvmpti |
⊢ ( ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ∈ ℕ → ( 𝐺 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) = ( I ‘ ⦋ ( 𝑓 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) / 𝑘 ⦌ 𝐵 ) ) |
79 |
74 75 78
|
3syl |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) = ( I ‘ ⦋ ( 𝑓 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) / 𝑘 ⦌ 𝐵 ) ) |
80 |
|
elfznn |
⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → 𝑖 ∈ ℕ ) |
81 |
80
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝑖 ∈ ℕ ) |
82 |
|
fveq2 |
⊢ ( 𝑗 = 𝑖 → ( 𝐾 ‘ 𝑗 ) = ( 𝐾 ‘ 𝑖 ) ) |
83 |
82
|
csbeq1d |
⊢ ( 𝑗 = 𝑖 → ⦋ ( 𝐾 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝐾 ‘ 𝑖 ) / 𝑘 ⦌ 𝐵 ) |
84 |
83 4
|
fvmpti |
⊢ ( 𝑖 ∈ ℕ → ( 𝐻 ‘ 𝑖 ) = ( I ‘ ⦋ ( 𝐾 ‘ 𝑖 ) / 𝑘 ⦌ 𝐵 ) ) |
85 |
81 84
|
syl |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐻 ‘ 𝑖 ) = ( I ‘ ⦋ ( 𝐾 ‘ 𝑖 ) / 𝑘 ⦌ 𝐵 ) ) |
86 |
71 79 85
|
3eqtr4rd |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐻 ‘ 𝑖 ) = ( 𝐺 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) ) |
87 |
9 11 13 16 17 40 57 86
|
seqf1o |
⊢ ( 𝜑 → ( seq 1 ( · , 𝐻 ) ‘ 𝑀 ) = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ) |
88 |
37
|
fveq2d |
⊢ ( 𝜑 → ( seq 1 ( · , 𝐻 ) ‘ 𝑀 ) = ( seq 1 ( · , 𝐻 ) ‘ 𝑁 ) ) |
89 |
87 88
|
eqtr3d |
⊢ ( 𝜑 → ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , 𝐻 ) ‘ 𝑁 ) ) |