stoweidlem40

Description: This lemma proves that q_n is in the subalgebra, as in the proof of Lemma 1 in BrosowskiDeutsh p. 90. Q is used to represent q_n in the paper, N is used to represent n in the paper, and M is used to represent k^n in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem40.1	$⊢ \underline{Ⅎ} t P$
	stoweidlem40.2	$⊢ Ⅎ t φ$
	stoweidlem40.3	$⊢ Q = (t \in T ⟼ {(1 - {P (t)}^{N})}^{M})$
	stoweidlem40.4	$⊢ F = (t \in T ⟼ 1 - {P (t)}^{N})$
	stoweidlem40.5	$⊢ G = (t \in T ⟼ 1)$
	stoweidlem40.6	$⊢ H = (t \in T ⟼ {P (t)}^{N})$
	stoweidlem40.7	$⊢ φ \to P \in A$
	stoweidlem40.8	$⊢ φ \to P : T ⟶ ℝ$
	stoweidlem40.9	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
	stoweidlem40.10	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
	stoweidlem40.11	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
	stoweidlem40.12	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
	stoweidlem40.13	$⊢ φ \to N \in ℕ$
	stoweidlem40.14	$⊢ φ \to M \in ℕ$
Assertion	stoweidlem40	$⊢ φ \to Q \in A$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem40.1	$⊢ \underline{Ⅎ} t P$
2		stoweidlem40.2	$⊢ Ⅎ t φ$
3		stoweidlem40.3	$⊢ Q = (t \in T ⟼ {(1 - {P (t)}^{N})}^{M})$
4		stoweidlem40.4	$⊢ F = (t \in T ⟼ 1 - {P (t)}^{N})$
5		stoweidlem40.5	$⊢ G = (t \in T ⟼ 1)$
6		stoweidlem40.6	$⊢ H = (t \in T ⟼ {P (t)}^{N})$
7		stoweidlem40.7	$⊢ φ \to P \in A$
8		stoweidlem40.8	$⊢ φ \to P : T ⟶ ℝ$
9		stoweidlem40.9	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
10		stoweidlem40.10	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
11		stoweidlem40.11	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
12		stoweidlem40.12	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
13		stoweidlem40.13	$⊢ φ \to N \in ℕ$
14		stoweidlem40.14	$⊢ φ \to M \in ℕ$
15		simpr	$⊢ (φ \land t \in T) \to t \in T$
16		1red	$⊢ (φ \land t \in T) \to 1 \in ℝ$
17	8	ffvelrnda	$⊢ (φ \land t \in T) \to P (t) \in ℝ$
18	13	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
19	18	adantr	$⊢ (φ \land t \in T) \to N \in ℕ_{0}$
20	17 19	reexpcld	$⊢ (φ \land t \in T) \to {P (t)}^{N} \in ℝ$
21	16 20	resubcld	$⊢ (φ \land t \in T) \to 1 - {P (t)}^{N} \in ℝ$
22	4	fvmpt2	$⊢ (t \in T \land 1 - {P (t)}^{N} \in ℝ) \to F (t) = 1 - {P (t)}^{N}$
23	15 21 22	syl2anc	$⊢ (φ \land t \in T) \to F (t) = 1 - {P (t)}^{N}$
24	23	eqcomd	$⊢ (φ \land t \in T) \to 1 - {P (t)}^{N} = F (t)$
25	24	oveq1d	$⊢ (φ \land t \in T) \to {(1 - {P (t)}^{N})}^{M} = {F (t)}^{M}$
26	2 25	mpteq2da	$⊢ φ \to (t \in T ⟼ {(1 - {P (t)}^{N})}^{M}) = (t \in T ⟼ {F (t)}^{M})$
27	3 26	syl5eq	$⊢ φ \to Q = (t \in T ⟼ {F (t)}^{M})$
28		nfmpt1	$⊢ \underline{Ⅎ} t (t \in T ⟼ 1 - {P (t)}^{N})$
29	4 28	nfcxfr	$⊢ \underline{Ⅎ} t F$
30		1re	$⊢ 1 \in ℝ$
31	5	fvmpt2	$⊢ (t \in T \land 1 \in ℝ) \to G (t) = 1$
32	30 31	mpan2	$⊢ t \in T \to G (t) = 1$
33	32	eqcomd	$⊢ t \in T \to 1 = G (t)$
34	33	adantl	$⊢ (φ \land t \in T) \to 1 = G (t)$
35	6	fvmpt2	$⊢ (t \in T \land {P (t)}^{N} \in ℝ) \to H (t) = {P (t)}^{N}$
36	15 20 35	syl2anc	$⊢ (φ \land t \in T) \to H (t) = {P (t)}^{N}$
37	36	eqcomd	$⊢ (φ \land t \in T) \to {P (t)}^{N} = H (t)$
38	34 37	oveq12d	$⊢ (φ \land t \in T) \to 1 - {P (t)}^{N} = G (t) - H (t)$
39	2 38	mpteq2da	$⊢ φ \to (t \in T ⟼ 1 - {P (t)}^{N}) = (t \in T ⟼ G (t) - H (t))$
40	4 39	syl5eq	$⊢ φ \to F = (t \in T ⟼ G (t) - H (t))$
41	12	stoweidlem4	$⊢ (φ \land 1 \in ℝ) \to (t \in T ⟼ 1) \in A$
42	30 41	mpan2	$⊢ φ \to (t \in T ⟼ 1) \in A$
43	5 42	eqeltrid	$⊢ φ \to G \in A$
44	1 2 9 11 12 7 18	stoweidlem19	$⊢ φ \to (t \in T ⟼ {P (t)}^{N}) \in A$
45	6 44	eqeltrid	$⊢ φ \to H \in A$
46		nfmpt1	$⊢ \underline{Ⅎ} t (t \in T ⟼ 1)$
47	5 46	nfcxfr	$⊢ \underline{Ⅎ} t G$
48		nfmpt1	$⊢ \underline{Ⅎ} t (t \in T ⟼ {P (t)}^{N})$
49	6 48	nfcxfr	$⊢ \underline{Ⅎ} t H$
50	47 49 2 9 10 11 12	stoweidlem33	$⊢ (φ \land G \in A \land H \in A) \to (t \in T ⟼ G (t) - H (t)) \in A$
51	43 45 50	mpd3an23	$⊢ φ \to (t \in T ⟼ G (t) - H (t)) \in A$
52	40 51	eqeltrd	$⊢ φ \to F \in A$
53	14	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
54	29 2 9 11 12 52 53	stoweidlem19	$⊢ φ \to (t \in T ⟼ {F (t)}^{M}) \in A$
55	27 54	eqeltrd	$⊢ φ \to Q \in A$

Metamath Proof Explorer

Theorem stoweidlem40

Proof