stoweidlem19

Description: If a set of real functions is closed under multiplication and it contains constants, then it is closed under finite exponentiation. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem19.1	$⊢ \underline{Ⅎ} t F$
	stoweidlem19.2	$⊢ Ⅎ t φ$
	stoweidlem19.3	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
	stoweidlem19.4	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
	stoweidlem19.5	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
	stoweidlem19.6	$⊢ φ \to F \in A$
	stoweidlem19.7	$⊢ φ \to N \in ℕ_{0}$
Assertion	stoweidlem19	$⊢ φ \to (t \in T ⟼ {F (t)}^{N}) \in A$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem19.1	$⊢ \underline{Ⅎ} t F$
2		stoweidlem19.2	$⊢ Ⅎ t φ$
3		stoweidlem19.3	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
4		stoweidlem19.4	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
5		stoweidlem19.5	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
6		stoweidlem19.6	$⊢ φ \to F \in A$
7		stoweidlem19.7	$⊢ φ \to N \in ℕ_{0}$
8		oveq2	$⊢ n = 0 \to {F (t)}^{n} = {F (t)}^{0}$
9	8	mpteq2dv	$⊢ n = 0 \to (t \in T ⟼ {F (t)}^{n}) = (t \in T ⟼ {F (t)}^{0})$
10	9	eleq1d	$⊢ n = 0 \to ((t \in T ⟼ {F (t)}^{n}) \in A \leftrightarrow (t \in T ⟼ {F (t)}^{0}) \in A)$
11	10	imbi2d	$⊢ n = 0 \to ((φ \to (t \in T ⟼ {F (t)}^{n}) \in A) \leftrightarrow (φ \to (t \in T ⟼ {F (t)}^{0}) \in A))$
12		oveq2	$⊢ n = m \to {F (t)}^{n} = {F (t)}^{m}$
13	12	mpteq2dv	$⊢ n = m \to (t \in T ⟼ {F (t)}^{n}) = (t \in T ⟼ {F (t)}^{m})$
14	13	eleq1d	$⊢ n = m \to ((t \in T ⟼ {F (t)}^{n}) \in A \leftrightarrow (t \in T ⟼ {F (t)}^{m}) \in A)$
15	14	imbi2d	$⊢ n = m \to ((φ \to (t \in T ⟼ {F (t)}^{n}) \in A) \leftrightarrow (φ \to (t \in T ⟼ {F (t)}^{m}) \in A))$
16		oveq2	$⊢ n = m + 1 \to {F (t)}^{n} = {F (t)}^{m + 1}$
17	16	mpteq2dv	$⊢ n = m + 1 \to (t \in T ⟼ {F (t)}^{n}) = (t \in T ⟼ {F (t)}^{m + 1})$
18	17	eleq1d	$⊢ n = m + 1 \to ((t \in T ⟼ {F (t)}^{n}) \in A \leftrightarrow (t \in T ⟼ {F (t)}^{m + 1}) \in A)$
19	18	imbi2d	$⊢ n = m + 1 \to ((φ \to (t \in T ⟼ {F (t)}^{n}) \in A) \leftrightarrow (φ \to (t \in T ⟼ {F (t)}^{m + 1}) \in A))$
20		oveq2	$⊢ n = N \to {F (t)}^{n} = {F (t)}^{N}$
21	20	mpteq2dv	$⊢ n = N \to (t \in T ⟼ {F (t)}^{n}) = (t \in T ⟼ {F (t)}^{N})$
22	21	eleq1d	$⊢ n = N \to ((t \in T ⟼ {F (t)}^{n}) \in A \leftrightarrow (t \in T ⟼ {F (t)}^{N}) \in A)$
23	22	imbi2d	$⊢ n = N \to ((φ \to (t \in T ⟼ {F (t)}^{n}) \in A) \leftrightarrow (φ \to (t \in T ⟼ {F (t)}^{N}) \in A))$
24	6	ancli	$⊢ φ \to (φ \land F \in A)$
25		eleq1	$⊢ f = F \to (f \in A \leftrightarrow F \in A)$
26	25	anbi2d	$⊢ f = F \to ((φ \land f \in A) \leftrightarrow (φ \land F \in A))$
27		feq1	$⊢ f = F \to (f : T ⟶ ℝ \leftrightarrow F : T ⟶ ℝ)$
28	26 27	imbi12d	$⊢ f = F \to (((φ \land f \in A) \to f : T ⟶ ℝ) \leftrightarrow ((φ \land F \in A) \to F : T ⟶ ℝ))$
29	28 3	vtoclg	$⊢ F \in A \to ((φ \land F \in A) \to F : T ⟶ ℝ)$
30	6 24 29	sylc	$⊢ φ \to F : T ⟶ ℝ$
31	30	ffvelrnda	$⊢ (φ \land t \in T) \to F (t) \in ℝ$
32		recn	$⊢ F (t) \in ℝ \to F (t) \in ℂ$
33		exp0	$⊢ F (t) \in ℂ \to {F (t)}^{0} = 1$
34	31 32 33	3syl	$⊢ (φ \land t \in T) \to {F (t)}^{0} = 1$
35	34	eqcomd	$⊢ (φ \land t \in T) \to 1 = {F (t)}^{0}$
36	2 35	mpteq2da	$⊢ φ \to (t \in T ⟼ 1) = (t \in T ⟼ {F (t)}^{0})$
37		1re	$⊢ 1 \in ℝ$
38	5	stoweidlem4	$⊢ (φ \land 1 \in ℝ) \to (t \in T ⟼ 1) \in A$
39	37 38	mpan2	$⊢ φ \to (t \in T ⟼ 1) \in A$
40	36 39	eqeltrrd	$⊢ φ \to (t \in T ⟼ {F (t)}^{0}) \in A$
41		simpr	$⊢ ((m \in ℕ_{0} \land (φ \to (t \in T ⟼ {F (t)}^{m}) \in A)) \land φ) \to φ$
42		simpll	$⊢ ((m \in ℕ_{0} \land (φ \to (t \in T ⟼ {F (t)}^{m}) \in A)) \land φ) \to m \in ℕ_{0}$
43		simplr	$⊢ ((m \in ℕ_{0} \land (φ \to (t \in T ⟼ {F (t)}^{m}) \in A)) \land φ) \to (φ \to (t \in T ⟼ {F (t)}^{m}) \in A)$
44	41 43	mpd	$⊢ ((m \in ℕ_{0} \land (φ \to (t \in T ⟼ {F (t)}^{m}) \in A)) \land φ) \to (t \in T ⟼ {F (t)}^{m}) \in A$
45		nfv	$⊢ Ⅎ t m \in ℕ_{0}$
46		nfmpt1	$⊢ \underline{Ⅎ} t (t \in T ⟼ {F (t)}^{m})$
47	46	nfel1	$⊢ Ⅎ t (t \in T ⟼ {F (t)}^{m}) \in A$
48	2 45 47	nf3an	$⊢ Ⅎ t (φ \land m \in ℕ_{0} \land (t \in T ⟼ {F (t)}^{m}) \in A)$
49		simpl1	$⊢ ((φ \land m \in ℕ_{0} \land (t \in T ⟼ {F (t)}^{m}) \in A) \land t \in T) \to φ$
50		simpr	$⊢ ((φ \land m \in ℕ_{0} \land (t \in T ⟼ {F (t)}^{m}) \in A) \land t \in T) \to t \in T$
51	31	recnd	$⊢ (φ \land t \in T) \to F (t) \in ℂ$
52	49 50 51	syl2anc	$⊢ ((φ \land m \in ℕ_{0} \land (t \in T ⟼ {F (t)}^{m}) \in A) \land t \in T) \to F (t) \in ℂ$
53		simpl2	$⊢ ((φ \land m \in ℕ_{0} \land (t \in T ⟼ {F (t)}^{m}) \in A) \land t \in T) \to m \in ℕ_{0}$
54	52 53	expp1d	$⊢ ((φ \land m \in ℕ_{0} \land (t \in T ⟼ {F (t)}^{m}) \in A) \land t \in T) \to {F (t)}^{m + 1} = {F (t)}^{m} F (t)$
55	48 54	mpteq2da	$⊢ (φ \land m \in ℕ_{0} \land (t \in T ⟼ {F (t)}^{m}) \in A) \to (t \in T ⟼ {F (t)}^{m + 1}) = (t \in T ⟼ {F (t)}^{m} F (t))$
56	31	3adant2	$⊢ (φ \land m \in ℕ_{0} \land t \in T) \to F (t) \in ℝ$
57		simp2	$⊢ (φ \land m \in ℕ_{0} \land t \in T) \to m \in ℕ_{0}$
58	56 57	reexpcld	$⊢ (φ \land m \in ℕ_{0} \land t \in T) \to {F (t)}^{m} \in ℝ$
59	49 53 50 58	syl3anc	$⊢ ((φ \land m \in ℕ_{0} \land (t \in T ⟼ {F (t)}^{m}) \in A) \land t \in T) \to {F (t)}^{m} \in ℝ$
60		eqid	$⊢ (t \in T ⟼ {F (t)}^{m}) = (t \in T ⟼ {F (t)}^{m})$
61	60	fvmpt2	$⊢ (t \in T \land {F (t)}^{m} \in ℝ) \to (t \in T ⟼ {F (t)}^{m}) (t) = {F (t)}^{m}$
62	61	eqcomd	$⊢ (t \in T \land {F (t)}^{m} \in ℝ) \to {F (t)}^{m} = (t \in T ⟼ {F (t)}^{m}) (t)$
63	50 59 62	syl2anc	$⊢ ((φ \land m \in ℕ_{0} \land (t \in T ⟼ {F (t)}^{m}) \in A) \land t \in T) \to {F (t)}^{m} = (t \in T ⟼ {F (t)}^{m}) (t)$
64	63	oveq1d	$⊢ ((φ \land m \in ℕ_{0} \land (t \in T ⟼ {F (t)}^{m}) \in A) \land t \in T) \to {F (t)}^{m} F (t) = (t \in T ⟼ {F (t)}^{m}) (t) F (t)$
65	48 64	mpteq2da	$⊢ (φ \land m \in ℕ_{0} \land (t \in T ⟼ {F (t)}^{m}) \in A) \to (t \in T ⟼ {F (t)}^{m} F (t)) = (t \in T ⟼ (t \in T ⟼ {F (t)}^{m}) (t) F (t))$
66	6	adantr	$⊢ (φ \land (t \in T ⟼ {F (t)}^{m}) \in A) \to F \in A$
67	46	nfeq2	$⊢ Ⅎ t f = (t \in T ⟼ {F (t)}^{m})$
68	1	nfeq2	$⊢ Ⅎ t g = F$
69	67 68 4	stoweidlem6	$⊢ (φ \land (t \in T ⟼ {F (t)}^{m}) \in A \land F \in A) \to (t \in T ⟼ (t \in T ⟼ {F (t)}^{m}) (t) F (t)) \in A$
70	66 69	mpd3an3	$⊢ (φ \land (t \in T ⟼ {F (t)}^{m}) \in A) \to (t \in T ⟼ (t \in T ⟼ {F (t)}^{m}) (t) F (t)) \in A$
71	70	3adant2	$⊢ (φ \land m \in ℕ_{0} \land (t \in T ⟼ {F (t)}^{m}) \in A) \to (t \in T ⟼ (t \in T ⟼ {F (t)}^{m}) (t) F (t)) \in A$
72	65 71	eqeltrd	$⊢ (φ \land m \in ℕ_{0} \land (t \in T ⟼ {F (t)}^{m}) \in A) \to (t \in T ⟼ {F (t)}^{m} F (t)) \in A$
73	55 72	eqeltrd	$⊢ (φ \land m \in ℕ_{0} \land (t \in T ⟼ {F (t)}^{m}) \in A) \to (t \in T ⟼ {F (t)}^{m + 1}) \in A$
74	41 42 44 73	syl3anc	$⊢ ((m \in ℕ_{0} \land (φ \to (t \in T ⟼ {F (t)}^{m}) \in A)) \land φ) \to (t \in T ⟼ {F (t)}^{m + 1}) \in A$
75	74	exp31	$⊢ m \in ℕ_{0} \to ((φ \to (t \in T ⟼ {F (t)}^{m}) \in A) \to (φ \to (t \in T ⟼ {F (t)}^{m + 1}) \in A))$
76	11 15 19 23 40 75	nn0ind	$⊢ N \in ℕ_{0} \to (φ \to (t \in T ⟼ {F (t)}^{N}) \in A)$
77	7 76	mpcom	$⊢ φ \to (t \in T ⟼ {F (t)}^{N}) \in A$

Metamath Proof Explorer

Theorem stoweidlem19

Proof