| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | faclim.1 | . . 3
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝐴) / (1 + (𝐴 / 𝑛)))) | 
| 2 |  | seqeq3 14048 | . . 3
⊢ (𝐹 = (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝐴) / (1 + (𝐴 / 𝑛)))) → seq1( · , 𝐹) = seq1( · , (𝑛 ∈ ℕ ↦ (((1 +
(1 / 𝑛))↑𝐴) / (1 + (𝐴 / 𝑛)))))) | 
| 3 | 1, 2 | ax-mp 5 | . 2
⊢ seq1(
· , 𝐹) = seq1(
· , (𝑛 ∈
ℕ ↦ (((1 + (1 / 𝑛))↑𝐴) / (1 + (𝐴 / 𝑛))))) | 
| 4 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑎 = 0 → ((1 + (1 / 𝑛))↑𝑎) = ((1 + (1 / 𝑛))↑0)) | 
| 5 |  | oveq1 7439 | . . . . . . . 8
⊢ (𝑎 = 0 → (𝑎 / 𝑛) = (0 / 𝑛)) | 
| 6 | 5 | oveq2d 7448 | . . . . . . 7
⊢ (𝑎 = 0 → (1 + (𝑎 / 𝑛)) = (1 + (0 / 𝑛))) | 
| 7 | 4, 6 | oveq12d 7450 | . . . . . 6
⊢ (𝑎 = 0 → (((1 + (1 / 𝑛))↑𝑎) / (1 + (𝑎 / 𝑛))) = (((1 + (1 / 𝑛))↑0) / (1 + (0 / 𝑛)))) | 
| 8 | 7 | mpteq2dv 5243 | . . . . 5
⊢ (𝑎 = 0 → (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑎) / (1 + (𝑎 / 𝑛)))) = (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑0) / (1 + (0 / 𝑛))))) | 
| 9 | 8 | seqeq3d 14051 | . . . 4
⊢ (𝑎 = 0 → seq1( · ,
(𝑛 ∈ ℕ ↦
(((1 + (1 / 𝑛))↑𝑎) / (1 + (𝑎 / 𝑛))))) = seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑0) / (1 + (0 / 𝑛)))))) | 
| 10 |  | fveq2 6905 | . . . . 5
⊢ (𝑎 = 0 → (!‘𝑎) =
(!‘0)) | 
| 11 |  | fac0 14316 | . . . . 5
⊢
(!‘0) = 1 | 
| 12 | 10, 11 | eqtrdi 2792 | . . . 4
⊢ (𝑎 = 0 → (!‘𝑎) = 1) | 
| 13 | 9, 12 | breq12d 5155 | . . 3
⊢ (𝑎 = 0 → (seq1( · ,
(𝑛 ∈ ℕ ↦
(((1 + (1 / 𝑛))↑𝑎) / (1 + (𝑎 / 𝑛))))) ⇝ (!‘𝑎) ↔ seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑0) / (1 + (0 / 𝑛))))) ⇝
1)) | 
| 14 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑎 = 𝑚 → ((1 + (1 / 𝑛))↑𝑎) = ((1 + (1 / 𝑛))↑𝑚)) | 
| 15 |  | oveq1 7439 | . . . . . . . 8
⊢ (𝑎 = 𝑚 → (𝑎 / 𝑛) = (𝑚 / 𝑛)) | 
| 16 | 15 | oveq2d 7448 | . . . . . . 7
⊢ (𝑎 = 𝑚 → (1 + (𝑎 / 𝑛)) = (1 + (𝑚 / 𝑛))) | 
| 17 | 14, 16 | oveq12d 7450 | . . . . . 6
⊢ (𝑎 = 𝑚 → (((1 + (1 / 𝑛))↑𝑎) / (1 + (𝑎 / 𝑛))) = (((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛)))) | 
| 18 | 17 | mpteq2dv 5243 | . . . . 5
⊢ (𝑎 = 𝑚 → (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑎) / (1 + (𝑎 / 𝑛)))) = (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛))))) | 
| 19 | 18 | seqeq3d 14051 | . . . 4
⊢ (𝑎 = 𝑚 → seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑎) / (1 + (𝑎 / 𝑛))))) = seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛)))))) | 
| 20 |  | fveq2 6905 | . . . 4
⊢ (𝑎 = 𝑚 → (!‘𝑎) = (!‘𝑚)) | 
| 21 | 19, 20 | breq12d 5155 | . . 3
⊢ (𝑎 = 𝑚 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑎) / (1 + (𝑎 / 𝑛))))) ⇝ (!‘𝑎) ↔ seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛))))) ⇝ (!‘𝑚))) | 
| 22 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑎 = (𝑚 + 1) → ((1 + (1 / 𝑛))↑𝑎) = ((1 + (1 / 𝑛))↑(𝑚 + 1))) | 
| 23 |  | oveq1 7439 | . . . . . . . 8
⊢ (𝑎 = (𝑚 + 1) → (𝑎 / 𝑛) = ((𝑚 + 1) / 𝑛)) | 
| 24 | 23 | oveq2d 7448 | . . . . . . 7
⊢ (𝑎 = (𝑚 + 1) → (1 + (𝑎 / 𝑛)) = (1 + ((𝑚 + 1) / 𝑛))) | 
| 25 | 22, 24 | oveq12d 7450 | . . . . . 6
⊢ (𝑎 = (𝑚 + 1) → (((1 + (1 / 𝑛))↑𝑎) / (1 + (𝑎 / 𝑛))) = (((1 + (1 / 𝑛))↑(𝑚 + 1)) / (1 + ((𝑚 + 1) / 𝑛)))) | 
| 26 | 25 | mpteq2dv 5243 | . . . . 5
⊢ (𝑎 = (𝑚 + 1) → (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑎) / (1 + (𝑎 / 𝑛)))) = (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑(𝑚 + 1)) / (1 + ((𝑚 + 1) / 𝑛))))) | 
| 27 | 26 | seqeq3d 14051 | . . . 4
⊢ (𝑎 = (𝑚 + 1) → seq1( · , (𝑛 ∈ ℕ ↦ (((1 +
(1 / 𝑛))↑𝑎) / (1 + (𝑎 / 𝑛))))) = seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑(𝑚 + 1)) / (1 + ((𝑚 + 1) / 𝑛)))))) | 
| 28 |  | fveq2 6905 | . . . 4
⊢ (𝑎 = (𝑚 + 1) → (!‘𝑎) = (!‘(𝑚 + 1))) | 
| 29 | 27, 28 | breq12d 5155 | . . 3
⊢ (𝑎 = (𝑚 + 1) → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 +
(1 / 𝑛))↑𝑎) / (1 + (𝑎 / 𝑛))))) ⇝ (!‘𝑎) ↔ seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑(𝑚 + 1)) / (1 + ((𝑚 + 1) / 𝑛))))) ⇝ (!‘(𝑚 + 1)))) | 
| 30 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑎 = 𝐴 → ((1 + (1 / 𝑛))↑𝑎) = ((1 + (1 / 𝑛))↑𝐴)) | 
| 31 |  | oveq1 7439 | . . . . . . . 8
⊢ (𝑎 = 𝐴 → (𝑎 / 𝑛) = (𝐴 / 𝑛)) | 
| 32 | 31 | oveq2d 7448 | . . . . . . 7
⊢ (𝑎 = 𝐴 → (1 + (𝑎 / 𝑛)) = (1 + (𝐴 / 𝑛))) | 
| 33 | 30, 32 | oveq12d 7450 | . . . . . 6
⊢ (𝑎 = 𝐴 → (((1 + (1 / 𝑛))↑𝑎) / (1 + (𝑎 / 𝑛))) = (((1 + (1 / 𝑛))↑𝐴) / (1 + (𝐴 / 𝑛)))) | 
| 34 | 33 | mpteq2dv 5243 | . . . . 5
⊢ (𝑎 = 𝐴 → (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑎) / (1 + (𝑎 / 𝑛)))) = (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝐴) / (1 + (𝐴 / 𝑛))))) | 
| 35 | 34 | seqeq3d 14051 | . . . 4
⊢ (𝑎 = 𝐴 → seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑎) / (1 + (𝑎 / 𝑛))))) = seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝐴) / (1 + (𝐴 / 𝑛)))))) | 
| 36 |  | fveq2 6905 | . . . 4
⊢ (𝑎 = 𝐴 → (!‘𝑎) = (!‘𝐴)) | 
| 37 | 35, 36 | breq12d 5155 | . . 3
⊢ (𝑎 = 𝐴 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 +
(1 / 𝑛))↑𝑎) / (1 + (𝑎 / 𝑛))))) ⇝ (!‘𝑎) ↔ seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝐴) / (1 + (𝐴 / 𝑛))))) ⇝ (!‘𝐴))) | 
| 38 |  | 1red 11263 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 1 ∈
ℝ) | 
| 39 |  | nnrecre 12309 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (1 /
𝑛) ∈
ℝ) | 
| 40 | 38, 39 | readdcld 11291 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (1 + (1 /
𝑛)) ∈
ℝ) | 
| 41 | 40 | recnd 11290 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (1 + (1 /
𝑛)) ∈
ℂ) | 
| 42 | 41 | exp0d 14181 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ → ((1 + (1
/ 𝑛))↑0) =
1) | 
| 43 |  | nncn 12275 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) | 
| 44 |  | nnne0 12301 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0) | 
| 45 | 43, 44 | div0d 12043 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (0 /
𝑛) = 0) | 
| 46 | 45 | oveq2d 7448 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (1 + (0 /
𝑛)) = (1 +
0)) | 
| 47 |  | 1p0e1 12391 | . . . . . . . . . 10
⊢ (1 + 0) =
1 | 
| 48 | 46, 47 | eqtrdi 2792 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (1 + (0 /
𝑛)) = 1) | 
| 49 | 42, 48 | oveq12d 7450 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ → (((1 + (1
/ 𝑛))↑0) / (1 + (0 /
𝑛))) = (1 /
1)) | 
| 50 |  | 1div1e1 11959 | . . . . . . . 8
⊢ (1 / 1) =
1 | 
| 51 | 49, 50 | eqtrdi 2792 | . . . . . . 7
⊢ (𝑛 ∈ ℕ → (((1 + (1
/ 𝑛))↑0) / (1 + (0 /
𝑛))) = 1) | 
| 52 | 51 | mpteq2ia 5244 | . . . . . 6
⊢ (𝑛 ∈ ℕ ↦ (((1 +
(1 / 𝑛))↑0) / (1 + (0
/ 𝑛)))) = (𝑛 ∈ ℕ ↦
1) | 
| 53 |  | fconstmpt 5746 | . . . . . 6
⊢ (ℕ
× {1}) = (𝑛 ∈
ℕ ↦ 1) | 
| 54 | 52, 53 | eqtr4i 2767 | . . . . 5
⊢ (𝑛 ∈ ℕ ↦ (((1 +
(1 / 𝑛))↑0) / (1 + (0
/ 𝑛)))) = (ℕ ×
{1}) | 
| 55 |  | seqeq3 14048 | . . . . 5
⊢ ((𝑛 ∈ ℕ ↦ (((1 +
(1 / 𝑛))↑0) / (1 + (0
/ 𝑛)))) = (ℕ ×
{1}) → seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑0) / (1 + (0 / 𝑛))))) = seq1( · ,
(ℕ × {1}))) | 
| 56 | 54, 55 | ax-mp 5 | . . . 4
⊢ seq1(
· , (𝑛 ∈
ℕ ↦ (((1 + (1 / 𝑛))↑0) / (1 + (0 / 𝑛))))) = seq1( · , (ℕ ×
{1})) | 
| 57 |  | nnuz 12922 | . . . . . 6
⊢ ℕ =
(ℤ≥‘1) | 
| 58 |  | 1zzd 12650 | . . . . . 6
⊢ (⊤
→ 1 ∈ ℤ) | 
| 59 | 57, 58 | climprod1 16002 | . . . . 5
⊢ (⊤
→ seq1( · , (ℕ × {1})) ⇝ 1) | 
| 60 | 59 | mptru 1546 | . . . 4
⊢ seq1(
· , (ℕ × {1})) ⇝ 1 | 
| 61 | 56, 60 | eqbrtri 5163 | . . 3
⊢ seq1(
· , (𝑛 ∈
ℕ ↦ (((1 + (1 / 𝑛))↑0) / (1 + (0 / 𝑛))))) ⇝ 1 | 
| 62 |  | 1zzd 12650 | . . . . . 6
⊢ ((𝑚 ∈ ℕ0
∧ seq1( · , (𝑛
∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛))))) ⇝ (!‘𝑚)) → 1 ∈ ℤ) | 
| 63 |  | simpr 484 | . . . . . 6
⊢ ((𝑚 ∈ ℕ0
∧ seq1( · , (𝑛
∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛))))) ⇝ (!‘𝑚)) → seq1( · , (𝑛 ∈ ℕ ↦ (((1 +
(1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛))))) ⇝ (!‘𝑚)) | 
| 64 |  | seqex 14045 | . . . . . . 7
⊢ seq1(
· , (𝑛 ∈
ℕ ↦ (((1 + (1 / 𝑛))↑(𝑚 + 1)) / (1 + ((𝑚 + 1) / 𝑛))))) ∈ V | 
| 65 | 64 | a1i 11 | . . . . . 6
⊢ ((𝑚 ∈ ℕ0
∧ seq1( · , (𝑛
∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛))))) ⇝ (!‘𝑚)) → seq1( · , (𝑛 ∈ ℕ ↦ (((1 +
(1 / 𝑛))↑(𝑚 + 1)) / (1 + ((𝑚 + 1) / 𝑛))))) ∈ V) | 
| 66 |  | faclimlem2 35745 | . . . . . . 7
⊢ (𝑚 ∈ ℕ0
→ seq1( · , (𝑛
∈ ℕ ↦ (((1 + (𝑚 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑚 + 1) / 𝑛))))) ⇝ (𝑚 + 1)) | 
| 67 | 66 | adantr 480 | . . . . . 6
⊢ ((𝑚 ∈ ℕ0
∧ seq1( · , (𝑛
∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛))))) ⇝ (!‘𝑚)) → seq1( · , (𝑛 ∈ ℕ ↦ (((1 +
(𝑚 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑚 + 1) / 𝑛))))) ⇝ (𝑚 + 1)) | 
| 68 |  | elnnuz 12923 | . . . . . . . . . 10
⊢ (𝑎 ∈ ℕ ↔ 𝑎 ∈
(ℤ≥‘1)) | 
| 69 | 68 | biimpi 216 | . . . . . . . . 9
⊢ (𝑎 ∈ ℕ → 𝑎 ∈
(ℤ≥‘1)) | 
| 70 | 69 | adantl 481 | . . . . . . . 8
⊢ ((𝑚 ∈ ℕ0
∧ 𝑎 ∈ ℕ)
→ 𝑎 ∈
(ℤ≥‘1)) | 
| 71 |  | 1rp 13039 | . . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ+ | 
| 72 | 71 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ 1 ∈ ℝ+) | 
| 73 |  | nnrp 13047 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ+) | 
| 74 | 73 | rpreccld 13088 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (1 /
𝑛) ∈
ℝ+) | 
| 75 | 74 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ (1 / 𝑛) ∈
ℝ+) | 
| 76 | 72, 75 | rpaddcld 13093 | . . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ (1 + (1 / 𝑛)) ∈
ℝ+) | 
| 77 |  | nn0z 12640 | . . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℤ) | 
| 78 | 77 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ 𝑚 ∈
ℤ) | 
| 79 | 76, 78 | rpexpcld 14287 | . . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ ((1 + (1 / 𝑛))↑𝑚) ∈
ℝ+) | 
| 80 |  | 1cnd 11257 | . . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ 1 ∈ ℂ) | 
| 81 |  | nn0nndivcl 12600 | . . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ (𝑚 / 𝑛) ∈
ℝ) | 
| 82 | 81 | recnd 11290 | . . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ (𝑚 / 𝑛) ∈
ℂ) | 
| 83 | 80, 82 | addcomd 11464 | . . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ (1 + (𝑚 / 𝑛)) = ((𝑚 / 𝑛) + 1)) | 
| 84 |  | nn0ge0div 12689 | . . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ 0 ≤ (𝑚 / 𝑛)) | 
| 85 | 81, 84 | ge0p1rpd 13108 | . . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ ((𝑚 / 𝑛) + 1) ∈
ℝ+) | 
| 86 | 83, 85 | eqeltrd 2840 | . . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ (1 + (𝑚 / 𝑛)) ∈
ℝ+) | 
| 87 | 79, 86 | rpdivcld 13095 | . . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ (((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛))) ∈
ℝ+) | 
| 88 | 87 | rpcnd 13080 | . . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ (((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛))) ∈ ℂ) | 
| 89 | 88 | fmpttd 7134 | . . . . . . . . . 10
⊢ (𝑚 ∈ ℕ0
→ (𝑛 ∈ ℕ
↦ (((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛)))):ℕ⟶ℂ) | 
| 90 |  | elfznn 13594 | . . . . . . . . . 10
⊢ (𝑏 ∈ (1...𝑎) → 𝑏 ∈ ℕ) | 
| 91 |  | ffvelcdm 7100 | . . . . . . . . . 10
⊢ (((𝑛 ∈ ℕ ↦ (((1 +
(1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛)))):ℕ⟶ℂ ∧ 𝑏 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (((1 +
(1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛))))‘𝑏) ∈ ℂ) | 
| 92 | 89, 90, 91 | syl2an 596 | . . . . . . . . 9
⊢ ((𝑚 ∈ ℕ0
∧ 𝑏 ∈ (1...𝑎)) → ((𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛))))‘𝑏) ∈ ℂ) | 
| 93 | 92 | adantlr 715 | . . . . . . . 8
⊢ (((𝑚 ∈ ℕ0
∧ 𝑎 ∈ ℕ)
∧ 𝑏 ∈ (1...𝑎)) → ((𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛))))‘𝑏) ∈ ℂ) | 
| 94 |  | mulcl 11240 | . . . . . . . . 9
⊢ ((𝑏 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑏 · 𝑥) ∈ ℂ) | 
| 95 | 94 | adantl 481 | . . . . . . . 8
⊢ (((𝑚 ∈ ℕ0
∧ 𝑎 ∈ ℕ)
∧ (𝑏 ∈ ℂ
∧ 𝑥 ∈ ℂ))
→ (𝑏 · 𝑥) ∈
ℂ) | 
| 96 | 70, 93, 95 | seqcl 14064 | . . . . . . 7
⊢ ((𝑚 ∈ ℕ0
∧ 𝑎 ∈ ℕ)
→ (seq1( · , (𝑛
∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛)))))‘𝑎) ∈ ℂ) | 
| 97 | 96 | adantlr 715 | . . . . . 6
⊢ (((𝑚 ∈ ℕ0
∧ seq1( · , (𝑛
∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛))))) ⇝ (!‘𝑚)) ∧ 𝑎 ∈ ℕ) → (seq1( · ,
(𝑛 ∈ ℕ ↦
(((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛)))))‘𝑎) ∈ ℂ) | 
| 98 | 86, 76 | rpmulcld 13094 | . . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ ((1 + (𝑚 / 𝑛)) · (1 + (1 / 𝑛))) ∈
ℝ+) | 
| 99 |  | nn0p1nn 12567 | . . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ℕ0
→ (𝑚 + 1) ∈
ℕ) | 
| 100 | 99 | nnrpd 13076 | . . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ0
→ (𝑚 + 1) ∈
ℝ+) | 
| 101 |  | rpdivcl 13061 | . . . . . . . . . . . . . . 15
⊢ (((𝑚 + 1) ∈ ℝ+
∧ 𝑛 ∈
ℝ+) → ((𝑚 + 1) / 𝑛) ∈
ℝ+) | 
| 102 | 100, 73, 101 | syl2an 596 | . . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ ((𝑚 + 1) / 𝑛) ∈
ℝ+) | 
| 103 | 72, 102 | rpaddcld 13093 | . . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ (1 + ((𝑚 + 1) /
𝑛)) ∈
ℝ+) | 
| 104 | 98, 103 | rpdivcld 13095 | . . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ (((1 + (𝑚 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑚 + 1) / 𝑛))) ∈
ℝ+) | 
| 105 | 104 | rpcnd 13080 | . . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ (((1 + (𝑚 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑚 + 1) / 𝑛))) ∈ ℂ) | 
| 106 | 105 | fmpttd 7134 | . . . . . . . . . 10
⊢ (𝑚 ∈ ℕ0
→ (𝑛 ∈ ℕ
↦ (((1 + (𝑚 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑚 + 1) / 𝑛)))):ℕ⟶ℂ) | 
| 107 |  | ffvelcdm 7100 | . . . . . . . . . 10
⊢ (((𝑛 ∈ ℕ ↦ (((1 +
(𝑚 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑚 + 1) / 𝑛)))):ℕ⟶ℂ ∧ 𝑏 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (((1 +
(𝑚 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑚 + 1) / 𝑛))))‘𝑏) ∈ ℂ) | 
| 108 | 106, 90, 107 | syl2an 596 | . . . . . . . . 9
⊢ ((𝑚 ∈ ℕ0
∧ 𝑏 ∈ (1...𝑎)) → ((𝑛 ∈ ℕ ↦ (((1 + (𝑚 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑚 + 1) / 𝑛))))‘𝑏) ∈ ℂ) | 
| 109 | 108 | adantlr 715 | . . . . . . . 8
⊢ (((𝑚 ∈ ℕ0
∧ 𝑎 ∈ ℕ)
∧ 𝑏 ∈ (1...𝑎)) → ((𝑛 ∈ ℕ ↦ (((1 + (𝑚 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑚 + 1) / 𝑛))))‘𝑏) ∈ ℂ) | 
| 110 | 70, 109, 95 | seqcl 14064 | . . . . . . 7
⊢ ((𝑚 ∈ ℕ0
∧ 𝑎 ∈ ℕ)
→ (seq1( · , (𝑛
∈ ℕ ↦ (((1 + (𝑚 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑚 + 1) / 𝑛)))))‘𝑎) ∈ ℂ) | 
| 111 | 110 | adantlr 715 | . . . . . 6
⊢ (((𝑚 ∈ ℕ0
∧ seq1( · , (𝑛
∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛))))) ⇝ (!‘𝑚)) ∧ 𝑎 ∈ ℕ) → (seq1( · ,
(𝑛 ∈ ℕ ↦
(((1 + (𝑚 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑚 + 1) / 𝑛)))))‘𝑎) ∈ ℂ) | 
| 112 |  | faclimlem3 35746 | . . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ0
∧ 𝑏 ∈ ℕ)
→ (((1 + (1 / 𝑏))↑(𝑚 + 1)) / (1 + ((𝑚 + 1) / 𝑏))) = ((((1 + (1 / 𝑏))↑𝑚) / (1 + (𝑚 / 𝑏))) · (((1 + (𝑚 / 𝑏)) · (1 + (1 / 𝑏))) / (1 + ((𝑚 + 1) / 𝑏))))) | 
| 113 |  | oveq2 7440 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑏 → (1 / 𝑛) = (1 / 𝑏)) | 
| 114 | 113 | oveq2d 7448 | . . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑏 → (1 + (1 / 𝑛)) = (1 + (1 / 𝑏))) | 
| 115 | 114 | oveq1d 7447 | . . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑏 → ((1 + (1 / 𝑛))↑(𝑚 + 1)) = ((1 + (1 / 𝑏))↑(𝑚 + 1))) | 
| 116 |  | oveq2 7440 | . . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑏 → ((𝑚 + 1) / 𝑛) = ((𝑚 + 1) / 𝑏)) | 
| 117 | 116 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑏 → (1 + ((𝑚 + 1) / 𝑛)) = (1 + ((𝑚 + 1) / 𝑏))) | 
| 118 | 115, 117 | oveq12d 7450 | . . . . . . . . . . . . 13
⊢ (𝑛 = 𝑏 → (((1 + (1 / 𝑛))↑(𝑚 + 1)) / (1 + ((𝑚 + 1) / 𝑛))) = (((1 + (1 / 𝑏))↑(𝑚 + 1)) / (1 + ((𝑚 + 1) / 𝑏)))) | 
| 119 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ ↦ (((1 +
(1 / 𝑛))↑(𝑚 + 1)) / (1 + ((𝑚 + 1) / 𝑛)))) = (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑(𝑚 + 1)) / (1 + ((𝑚 + 1) / 𝑛)))) | 
| 120 |  | ovex 7465 | . . . . . . . . . . . . 13
⊢ (((1 + (1
/ 𝑏))↑(𝑚 + 1)) / (1 + ((𝑚 + 1) / 𝑏))) ∈ V | 
| 121 | 118, 119,
120 | fvmpt 7015 | . . . . . . . . . . . 12
⊢ (𝑏 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (((1 +
(1 / 𝑛))↑(𝑚 + 1)) / (1 + ((𝑚 + 1) / 𝑛))))‘𝑏) = (((1 + (1 / 𝑏))↑(𝑚 + 1)) / (1 + ((𝑚 + 1) / 𝑏)))) | 
| 122 | 121 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ0
∧ 𝑏 ∈ ℕ)
→ ((𝑛 ∈ ℕ
↦ (((1 + (1 / 𝑛))↑(𝑚 + 1)) / (1 + ((𝑚 + 1) / 𝑛))))‘𝑏) = (((1 + (1 / 𝑏))↑(𝑚 + 1)) / (1 + ((𝑚 + 1) / 𝑏)))) | 
| 123 | 114 | oveq1d 7447 | . . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑏 → ((1 + (1 / 𝑛))↑𝑚) = ((1 + (1 / 𝑏))↑𝑚)) | 
| 124 |  | oveq2 7440 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑏 → (𝑚 / 𝑛) = (𝑚 / 𝑏)) | 
| 125 | 124 | oveq2d 7448 | . . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑏 → (1 + (𝑚 / 𝑛)) = (1 + (𝑚 / 𝑏))) | 
| 126 | 123, 125 | oveq12d 7450 | . . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑏 → (((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛))) = (((1 + (1 / 𝑏))↑𝑚) / (1 + (𝑚 / 𝑏)))) | 
| 127 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ ↦ (((1 +
(1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛)))) = (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛)))) | 
| 128 |  | ovex 7465 | . . . . . . . . . . . . . 14
⊢ (((1 + (1
/ 𝑏))↑𝑚) / (1 + (𝑚 / 𝑏))) ∈ V | 
| 129 | 126, 127,
128 | fvmpt 7015 | . . . . . . . . . . . . 13
⊢ (𝑏 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (((1 +
(1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛))))‘𝑏) = (((1 + (1 / 𝑏))↑𝑚) / (1 + (𝑚 / 𝑏)))) | 
| 130 | 125, 114 | oveq12d 7450 | . . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑏 → ((1 + (𝑚 / 𝑛)) · (1 + (1 / 𝑛))) = ((1 + (𝑚 / 𝑏)) · (1 + (1 / 𝑏)))) | 
| 131 | 130, 117 | oveq12d 7450 | . . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑏 → (((1 + (𝑚 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑚 + 1) / 𝑛))) = (((1 + (𝑚 / 𝑏)) · (1 + (1 / 𝑏))) / (1 + ((𝑚 + 1) / 𝑏)))) | 
| 132 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ ↦ (((1 +
(𝑚 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑚 + 1) / 𝑛)))) = (𝑛 ∈ ℕ ↦ (((1 + (𝑚 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑚 + 1) / 𝑛)))) | 
| 133 |  | ovex 7465 | . . . . . . . . . . . . . 14
⊢ (((1 +
(𝑚 / 𝑏)) · (1 + (1 / 𝑏))) / (1 + ((𝑚 + 1) / 𝑏))) ∈ V | 
| 134 | 131, 132,
133 | fvmpt 7015 | . . . . . . . . . . . . 13
⊢ (𝑏 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (((1 +
(𝑚 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑚 + 1) / 𝑛))))‘𝑏) = (((1 + (𝑚 / 𝑏)) · (1 + (1 / 𝑏))) / (1 + ((𝑚 + 1) / 𝑏)))) | 
| 135 | 129, 134 | oveq12d 7450 | . . . . . . . . . . . 12
⊢ (𝑏 ∈ ℕ → (((𝑛 ∈ ℕ ↦ (((1 +
(1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛))))‘𝑏) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑚 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑚 + 1) / 𝑛))))‘𝑏)) = ((((1 + (1 / 𝑏))↑𝑚) / (1 + (𝑚 / 𝑏))) · (((1 + (𝑚 / 𝑏)) · (1 + (1 / 𝑏))) / (1 + ((𝑚 + 1) / 𝑏))))) | 
| 136 | 135 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ0
∧ 𝑏 ∈ ℕ)
→ (((𝑛 ∈ ℕ
↦ (((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛))))‘𝑏) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑚 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑚 + 1) / 𝑛))))‘𝑏)) = ((((1 + (1 / 𝑏))↑𝑚) / (1 + (𝑚 / 𝑏))) · (((1 + (𝑚 / 𝑏)) · (1 + (1 / 𝑏))) / (1 + ((𝑚 + 1) / 𝑏))))) | 
| 137 | 112, 122,
136 | 3eqtr4d 2786 | . . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ0
∧ 𝑏 ∈ ℕ)
→ ((𝑛 ∈ ℕ
↦ (((1 + (1 / 𝑛))↑(𝑚 + 1)) / (1 + ((𝑚 + 1) / 𝑛))))‘𝑏) = (((𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛))))‘𝑏) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑚 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑚 + 1) / 𝑛))))‘𝑏))) | 
| 138 | 90, 137 | sylan2 593 | . . . . . . . . 9
⊢ ((𝑚 ∈ ℕ0
∧ 𝑏 ∈ (1...𝑎)) → ((𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑(𝑚 + 1)) / (1 + ((𝑚 + 1) / 𝑛))))‘𝑏) = (((𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛))))‘𝑏) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑚 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑚 + 1) / 𝑛))))‘𝑏))) | 
| 139 | 138 | adantlr 715 | . . . . . . . 8
⊢ (((𝑚 ∈ ℕ0
∧ 𝑎 ∈ ℕ)
∧ 𝑏 ∈ (1...𝑎)) → ((𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑(𝑚 + 1)) / (1 + ((𝑚 + 1) / 𝑛))))‘𝑏) = (((𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛))))‘𝑏) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑚 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑚 + 1) / 𝑛))))‘𝑏))) | 
| 140 | 70, 93, 109, 139 | prodfmul 15927 | . . . . . . 7
⊢ ((𝑚 ∈ ℕ0
∧ 𝑎 ∈ ℕ)
→ (seq1( · , (𝑛
∈ ℕ ↦ (((1 + (1 / 𝑛))↑(𝑚 + 1)) / (1 + ((𝑚 + 1) / 𝑛)))))‘𝑎) = ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛)))))‘𝑎) · (seq1( · , (𝑛 ∈ ℕ ↦ (((1 +
(𝑚 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑚 + 1) / 𝑛)))))‘𝑎))) | 
| 141 | 140 | adantlr 715 | . . . . . 6
⊢ (((𝑚 ∈ ℕ0
∧ seq1( · , (𝑛
∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛))))) ⇝ (!‘𝑚)) ∧ 𝑎 ∈ ℕ) → (seq1( · ,
(𝑛 ∈ ℕ ↦
(((1 + (1 / 𝑛))↑(𝑚 + 1)) / (1 + ((𝑚 + 1) / 𝑛)))))‘𝑎) = ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛)))))‘𝑎) · (seq1( · , (𝑛 ∈ ℕ ↦ (((1 +
(𝑚 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑚 + 1) / 𝑛)))))‘𝑎))) | 
| 142 | 57, 62, 63, 65, 67, 97, 111, 141 | climmul 15670 | . . . . 5
⊢ ((𝑚 ∈ ℕ0
∧ seq1( · , (𝑛
∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛))))) ⇝ (!‘𝑚)) → seq1( · , (𝑛 ∈ ℕ ↦ (((1 +
(1 / 𝑛))↑(𝑚 + 1)) / (1 + ((𝑚 + 1) / 𝑛))))) ⇝ ((!‘𝑚) · (𝑚 + 1))) | 
| 143 |  | facp1 14318 | . . . . . 6
⊢ (𝑚 ∈ ℕ0
→ (!‘(𝑚 + 1)) =
((!‘𝑚) ·
(𝑚 + 1))) | 
| 144 | 143 | adantr 480 | . . . . 5
⊢ ((𝑚 ∈ ℕ0
∧ seq1( · , (𝑛
∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛))))) ⇝ (!‘𝑚)) → (!‘(𝑚 + 1)) = ((!‘𝑚) · (𝑚 + 1))) | 
| 145 | 142, 144 | breqtrrd 5170 | . . . 4
⊢ ((𝑚 ∈ ℕ0
∧ seq1( · , (𝑛
∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛))))) ⇝ (!‘𝑚)) → seq1( · , (𝑛 ∈ ℕ ↦ (((1 +
(1 / 𝑛))↑(𝑚 + 1)) / (1 + ((𝑚 + 1) / 𝑛))))) ⇝ (!‘(𝑚 + 1))) | 
| 146 | 145 | ex 412 | . . 3
⊢ (𝑚 ∈ ℕ0
→ (seq1( · , (𝑛
∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝑚) / (1 + (𝑚 / 𝑛))))) ⇝ (!‘𝑚) → seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑(𝑚 + 1)) / (1 + ((𝑚 + 1) / 𝑛))))) ⇝ (!‘(𝑚 + 1)))) | 
| 147 | 13, 21, 29, 37, 61, 146 | nn0ind 12715 | . 2
⊢ (𝐴 ∈ ℕ0
→ seq1( · , (𝑛
∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝐴) / (1 + (𝐴 / 𝑛))))) ⇝ (!‘𝐴)) | 
| 148 | 3, 147 | eqbrtrid 5177 | 1
⊢ (𝐴 ∈ ℕ0
→ seq1( · , 𝐹)
⇝ (!‘𝐴)) |