Metamath Proof Explorer

Theorem expcnOLD

Description: Obsolete version of expcn as of 6-Apr-2025. (Contributed by Mario Carneiro, 5-May-2014) (Revised by Mario Carneiro, 23-Aug-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis expcnOLD.j ⊢ J = TopOpen ⁡ ℂ fld
Assertion expcnOLD ⊢ N ∈ ℕ 0 → x ∈ ℂ ⟼ x N ∈ J Cn J

Proof

Step Hyp Ref Expression
1 expcnOLD.j ⊢ J = TopOpen ⁡ ℂ fld
2 oveq2 ⊢ n = 0 → x n = x 0
3 2 mpteq2dv ⊢ n = 0 → x ∈ ℂ ⟼ x n = x ∈ ℂ ⟼ x 0
4 3 eleq1d ⊢ n = 0 → x ∈ ℂ ⟼ x n ∈ J Cn J ↔ x ∈ ℂ ⟼ x 0 ∈ J Cn J
5 oveq2 ⊢ n = k → x n = x k
6 5 mpteq2dv ⊢ n = k → x ∈ ℂ ⟼ x n = x ∈ ℂ ⟼ x k
7 6 eleq1d ⊢ n = k → x ∈ ℂ ⟼ x n ∈ J Cn J ↔ x ∈ ℂ ⟼ x k ∈ J Cn J
8 oveq2 ⊢ n = k + 1 → x n = x k + 1
9 8 mpteq2dv ⊢ n = k + 1 → x ∈ ℂ ⟼ x n = x ∈ ℂ ⟼ x k + 1
10 9 eleq1d ⊢ n = k + 1 → x ∈ ℂ ⟼ x n ∈ J Cn J ↔ x ∈ ℂ ⟼ x k + 1 ∈ J Cn J
11 oveq2 ⊢ n = N → x n = x N
12 11 mpteq2dv ⊢ n = N → x ∈ ℂ ⟼ x n = x ∈ ℂ ⟼ x N
13 12 eleq1d ⊢ n = N → x ∈ ℂ ⟼ x n ∈ J Cn J ↔ x ∈ ℂ ⟼ x N ∈ J Cn J
14 exp0 ⊢ x ∈ ℂ → x 0 = 1
15 14 mpteq2ia ⊢ x ∈ ℂ ⟼ x 0 = x ∈ ℂ ⟼ 1
16 1 cnfldtopon ⊢ J ∈ TopOn ⁡ ℂ
17 16 a1i ⊢ ⊤ → J ∈ TopOn ⁡ ℂ
18 1cnd ⊢ ⊤ → 1 ∈ ℂ
19 17 17 18 cnmptc ⊢ ⊤ → x ∈ ℂ ⟼ 1 ∈ J Cn J
20 19 mptru ⊢ x ∈ ℂ ⟼ 1 ∈ J Cn J
21 15 20 eqeltri ⊢ x ∈ ℂ ⟼ x 0 ∈ J Cn J
22 oveq1 ⊢ x = n → x k + 1 = n k + 1
23 22 cbvmptv ⊢ x ∈ ℂ ⟼ x k + 1 = n ∈ ℂ ⟼ n k + 1
24 id ⊢ n ∈ ℂ → n ∈ ℂ
25 simpl ⊢ k ∈ ℕ 0 ∧ x ∈ ℂ ⟼ x k ∈ J Cn J → k ∈ ℕ 0
26 expp1 ⊢ n ∈ ℂ ∧ k ∈ ℕ 0 → n k + 1 = n k ⁢ n
27 24 25 26 syl2anr ⊢ k ∈ ℕ 0 ∧ x ∈ ℂ ⟼ x k ∈ J Cn J ∧ n ∈ ℂ → n k + 1 = n k ⁢ n
28 27 mpteq2dva ⊢ k ∈ ℕ 0 ∧ x ∈ ℂ ⟼ x k ∈ J Cn J → n ∈ ℂ ⟼ n k + 1 = n ∈ ℂ ⟼ n k ⁢ n
29 23 28 eqtrid ⊢ k ∈ ℕ 0 ∧ x ∈ ℂ ⟼ x k ∈ J Cn J → x ∈ ℂ ⟼ x k + 1 = n ∈ ℂ ⟼ n k ⁢ n
30 16 a1i ⊢ k ∈ ℕ 0 ∧ x ∈ ℂ ⟼ x k ∈ J Cn J → J ∈ TopOn ⁡ ℂ
31 oveq1 ⊢ x = n → x k = n k
32 31 cbvmptv ⊢ x ∈ ℂ ⟼ x k = n ∈ ℂ ⟼ n k
33 simpr ⊢ k ∈ ℕ 0 ∧ x ∈ ℂ ⟼ x k ∈ J Cn J → x ∈ ℂ ⟼ x k ∈ J Cn J
34 32 33 eqeltrrid ⊢ k ∈ ℕ 0 ∧ x ∈ ℂ ⟼ x k ∈ J Cn J → n ∈ ℂ ⟼ n k ∈ J Cn J
35 30 cnmptid ⊢ k ∈ ℕ 0 ∧ x ∈ ℂ ⟼ x k ∈ J Cn J → n ∈ ℂ ⟼ n ∈ J Cn J
36 1 mulcn ⊢ × ∈ J × t J Cn J
37 36 a1i ⊢ k ∈ ℕ 0 ∧ x ∈ ℂ ⟼ x k ∈ J Cn J → × ∈ J × t J Cn J
38 30 34 35 37 cnmpt12f ⊢ k ∈ ℕ 0 ∧ x ∈ ℂ ⟼ x k ∈ J Cn J → n ∈ ℂ ⟼ n k ⁢ n ∈ J Cn J
39 29 38 eqeltrd ⊢ k ∈ ℕ 0 ∧ x ∈ ℂ ⟼ x k ∈ J Cn J → x ∈ ℂ ⟼ x k + 1 ∈ J Cn J
40 39 ex ⊢ k ∈ ℕ 0 → x ∈ ℂ ⟼ x k ∈ J Cn J → x ∈ ℂ ⟼ x k + 1 ∈ J Cn J
41 4 7 10 13 21 40 nn0ind ⊢ N ∈ ℕ 0 → x ∈ ℂ ⟼ x N ∈ J Cn J