Step |
Hyp |
Ref |
Expression |
1 |
|
climdivf.1 |
⊢ Ⅎ 𝑘 𝜑 |
2 |
|
climdivf.2 |
⊢ Ⅎ 𝑘 𝐹 |
3 |
|
climdivf.3 |
⊢ Ⅎ 𝑘 𝐺 |
4 |
|
climdivf.4 |
⊢ Ⅎ 𝑘 𝐻 |
5 |
|
climdivf.5 |
⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) |
6 |
|
climdivf.6 |
⊢ ( 𝜑 → 𝑀 ∈ ℤ ) |
7 |
|
climdivf.7 |
⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 ) |
8 |
|
climdivf.8 |
⊢ ( 𝜑 → 𝐻 ∈ 𝑋 ) |
9 |
|
climdivf.9 |
⊢ ( 𝜑 → 𝐺 ⇝ 𝐵 ) |
10 |
|
climdivf.10 |
⊢ ( 𝜑 → 𝐵 ≠ 0 ) |
11 |
|
climdivf.11 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) |
12 |
|
climdivf.12 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ( ℂ ∖ { 0 } ) ) |
13 |
|
climdivf.13 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) / ( 𝐺 ‘ 𝑘 ) ) ) |
14 |
|
nfmpt1 |
⊢ Ⅎ 𝑘 ( 𝑘 ∈ 𝑍 ↦ ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) |
15 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ 𝑍 ) |
16 |
12
|
eldifad |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ ) |
17 |
|
eldifsni |
⊢ ( ( 𝐺 ‘ 𝑘 ) ∈ ( ℂ ∖ { 0 } ) → ( 𝐺 ‘ 𝑘 ) ≠ 0 ) |
18 |
12 17
|
syl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ≠ 0 ) |
19 |
16 18
|
reccld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 1 / ( 𝐺 ‘ 𝑘 ) ) ∈ ℂ ) |
20 |
|
eqid |
⊢ ( 𝑘 ∈ 𝑍 ↦ ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 𝑍 ↦ ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) |
21 |
20
|
fvmpt2 |
⊢ ( ( 𝑘 ∈ 𝑍 ∧ ( 1 / ( 𝐺 ‘ 𝑘 ) ) ∈ ℂ ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) ‘ 𝑘 ) = ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) |
22 |
15 19 21
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) ‘ 𝑘 ) = ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) |
23 |
5
|
fvexi |
⊢ 𝑍 ∈ V |
24 |
23
|
mptex |
⊢ ( 𝑘 ∈ 𝑍 ↦ ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) ∈ V |
25 |
24
|
a1i |
⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) ∈ V ) |
26 |
1 3 14 5 6 9 10 12 22 25
|
climrecf |
⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) ⇝ ( 1 / 𝐵 ) ) |
27 |
22 19
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) ‘ 𝑘 ) ∈ ℂ ) |
28 |
11 16 18
|
divrecd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑘 ) / ( 𝐺 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑘 ) · ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) ) |
29 |
22
|
eqcomd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 1 / ( 𝐺 ‘ 𝑘 ) ) = ( ( 𝑘 ∈ 𝑍 ↦ ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) ‘ 𝑘 ) ) |
30 |
29
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑘 ) · ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) = ( ( 𝐹 ‘ 𝑘 ) · ( ( 𝑘 ∈ 𝑍 ↦ ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) ‘ 𝑘 ) ) ) |
31 |
13 28 30
|
3eqtrd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) · ( ( 𝑘 ∈ 𝑍 ↦ ( 1 / ( 𝐺 ‘ 𝑘 ) ) ) ‘ 𝑘 ) ) ) |
32 |
1 2 14 4 5 6 7 8 26 11 27 31
|
climmulf |
⊢ ( 𝜑 → 𝐻 ⇝ ( 𝐴 · ( 1 / 𝐵 ) ) ) |
33 |
|
climcl |
⊢ ( 𝐹 ⇝ 𝐴 → 𝐴 ∈ ℂ ) |
34 |
7 33
|
syl |
⊢ ( 𝜑 → 𝐴 ∈ ℂ ) |
35 |
|
climcl |
⊢ ( 𝐺 ⇝ 𝐵 → 𝐵 ∈ ℂ ) |
36 |
9 35
|
syl |
⊢ ( 𝜑 → 𝐵 ∈ ℂ ) |
37 |
34 36 10
|
divrecd |
⊢ ( 𝜑 → ( 𝐴 / 𝐵 ) = ( 𝐴 · ( 1 / 𝐵 ) ) ) |
38 |
32 37
|
breqtrrd |
⊢ ( 𝜑 → 𝐻 ⇝ ( 𝐴 / 𝐵 ) ) |