Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stoweidlem19 Structured version   Visualization version   GIF version

Theorem stoweidlem19 38716
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.)
Hypotheses
Ref Expression
stoweidlem19.1 𝑡𝐹
stoweidlem19.2 𝑡𝜑
stoweidlem19.3 ((𝜑𝑓𝐴) → 𝑓:𝑇⟶ℝ)
stoweidlem19.4 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
stoweidlem19.5 ((𝜑𝑥 ∈ ℝ) → (𝑡𝑇𝑥) ∈ 𝐴)
stoweidlem19.6 (𝜑𝐹𝐴)
stoweidlem19.7 (𝜑𝑁 ∈ ℕ0)
Assertion
Ref Expression
stoweidlem19 (𝜑 → (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑁)) ∈ 𝐴)
Distinct variable groups:   𝑓,𝑔,𝑡,𝐴   𝑓,𝐹,𝑔   𝑇,𝑓,𝑔,𝑡   𝜑,𝑓,𝑔   𝑡,𝑁   𝑥,𝑡,𝐴   𝑥,𝑇   𝜑,𝑥
Allowed substitution hints:   𝜑(𝑡)   𝐹(𝑥,𝑡)   𝑁(𝑥,𝑓,𝑔)

Proof of Theorem stoweidlem19
Dummy variables 𝑚 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 stoweidlem19.7 . 2 (𝜑𝑁 ∈ ℕ0)
2 oveq2 6535 . . . . . 6 (𝑛 = 0 → ((𝐹𝑡)↑𝑛) = ((𝐹𝑡)↑0))
32mpteq2dv 4667 . . . . 5 (𝑛 = 0 → (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑛)) = (𝑡𝑇 ↦ ((𝐹𝑡)↑0)))
43eleq1d 2671 . . . 4 (𝑛 = 0 → ((𝑡𝑇 ↦ ((𝐹𝑡)↑𝑛)) ∈ 𝐴 ↔ (𝑡𝑇 ↦ ((𝐹𝑡)↑0)) ∈ 𝐴))
54imbi2d 328 . . 3 (𝑛 = 0 → ((𝜑 → (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑛)) ∈ 𝐴) ↔ (𝜑 → (𝑡𝑇 ↦ ((𝐹𝑡)↑0)) ∈ 𝐴)))
6 oveq2 6535 . . . . . 6 (𝑛 = 𝑚 → ((𝐹𝑡)↑𝑛) = ((𝐹𝑡)↑𝑚))
76mpteq2dv 4667 . . . . 5 (𝑛 = 𝑚 → (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑛)) = (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)))
87eleq1d 2671 . . . 4 (𝑛 = 𝑚 → ((𝑡𝑇 ↦ ((𝐹𝑡)↑𝑛)) ∈ 𝐴 ↔ (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)) ∈ 𝐴))
98imbi2d 328 . . 3 (𝑛 = 𝑚 → ((𝜑 → (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑛)) ∈ 𝐴) ↔ (𝜑 → (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)) ∈ 𝐴)))
10 oveq2 6535 . . . . . 6 (𝑛 = (𝑚 + 1) → ((𝐹𝑡)↑𝑛) = ((𝐹𝑡)↑(𝑚 + 1)))
1110mpteq2dv 4667 . . . . 5 (𝑛 = (𝑚 + 1) → (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑛)) = (𝑡𝑇 ↦ ((𝐹𝑡)↑(𝑚 + 1))))
1211eleq1d 2671 . . . 4 (𝑛 = (𝑚 + 1) → ((𝑡𝑇 ↦ ((𝐹𝑡)↑𝑛)) ∈ 𝐴 ↔ (𝑡𝑇 ↦ ((𝐹𝑡)↑(𝑚 + 1))) ∈ 𝐴))
1312imbi2d 328 . . 3 (𝑛 = (𝑚 + 1) → ((𝜑 → (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑛)) ∈ 𝐴) ↔ (𝜑 → (𝑡𝑇 ↦ ((𝐹𝑡)↑(𝑚 + 1))) ∈ 𝐴)))
14 oveq2 6535 . . . . . 6 (𝑛 = 𝑁 → ((𝐹𝑡)↑𝑛) = ((𝐹𝑡)↑𝑁))
1514mpteq2dv 4667 . . . . 5 (𝑛 = 𝑁 → (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑛)) = (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑁)))
1615eleq1d 2671 . . . 4 (𝑛 = 𝑁 → ((𝑡𝑇 ↦ ((𝐹𝑡)↑𝑛)) ∈ 𝐴 ↔ (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑁)) ∈ 𝐴))
1716imbi2d 328 . . 3 (𝑛 = 𝑁 → ((𝜑 → (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑛)) ∈ 𝐴) ↔ (𝜑 → (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑁)) ∈ 𝐴)))
18 stoweidlem19.2 . . . . 5 𝑡𝜑
19 stoweidlem19.6 . . . . . . . . 9 (𝜑𝐹𝐴)
2019ancli 571 . . . . . . . . 9 (𝜑 → (𝜑𝐹𝐴))
21 eleq1 2675 . . . . . . . . . . . 12 (𝑓 = 𝐹 → (𝑓𝐴𝐹𝐴))
2221anbi2d 735 . . . . . . . . . . 11 (𝑓 = 𝐹 → ((𝜑𝑓𝐴) ↔ (𝜑𝐹𝐴)))
23 feq1 5925 . . . . . . . . . . 11 (𝑓 = 𝐹 → (𝑓:𝑇⟶ℝ ↔ 𝐹:𝑇⟶ℝ))
2422, 23imbi12d 332 . . . . . . . . . 10 (𝑓 = 𝐹 → (((𝜑𝑓𝐴) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑𝐹𝐴) → 𝐹:𝑇⟶ℝ)))
25 stoweidlem19.3 . . . . . . . . . 10 ((𝜑𝑓𝐴) → 𝑓:𝑇⟶ℝ)
2624, 25vtoclg 3238 . . . . . . . . 9 (𝐹𝐴 → ((𝜑𝐹𝐴) → 𝐹:𝑇⟶ℝ))
2719, 20, 26sylc 62 . . . . . . . 8 (𝜑𝐹:𝑇⟶ℝ)
2827fnvinran 37999 . . . . . . 7 ((𝜑𝑡𝑇) → (𝐹𝑡) ∈ ℝ)
29 recn 9882 . . . . . . 7 ((𝐹𝑡) ∈ ℝ → (𝐹𝑡) ∈ ℂ)
30 exp0 12681 . . . . . . 7 ((𝐹𝑡) ∈ ℂ → ((𝐹𝑡)↑0) = 1)
3128, 29, 303syl 18 . . . . . 6 ((𝜑𝑡𝑇) → ((𝐹𝑡)↑0) = 1)
3231eqcomd 2615 . . . . 5 ((𝜑𝑡𝑇) → 1 = ((𝐹𝑡)↑0))
3318, 32mpteq2da 4665 . . . 4 (𝜑 → (𝑡𝑇 ↦ 1) = (𝑡𝑇 ↦ ((𝐹𝑡)↑0)))
34 1re 9895 . . . . 5 1 ∈ ℝ
35 stoweidlem19.5 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → (𝑡𝑇𝑥) ∈ 𝐴)
3635stoweidlem4 38701 . . . . 5 ((𝜑 ∧ 1 ∈ ℝ) → (𝑡𝑇 ↦ 1) ∈ 𝐴)
3734, 36mpan2 702 . . . 4 (𝜑 → (𝑡𝑇 ↦ 1) ∈ 𝐴)
3833, 37eqeltrrd 2688 . . 3 (𝜑 → (𝑡𝑇 ↦ ((𝐹𝑡)↑0)) ∈ 𝐴)
39 simpr 475 . . . . 5 (((𝑚 ∈ ℕ0 ∧ (𝜑 → (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)) ∈ 𝐴)) ∧ 𝜑) → 𝜑)
40 simpll 785 . . . . 5 (((𝑚 ∈ ℕ0 ∧ (𝜑 → (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)) ∈ 𝐴)) ∧ 𝜑) → 𝑚 ∈ ℕ0)
41 simplr 787 . . . . . 6 (((𝑚 ∈ ℕ0 ∧ (𝜑 → (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)) ∈ 𝐴)) ∧ 𝜑) → (𝜑 → (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)) ∈ 𝐴))
4239, 41mpd 15 . . . . 5 (((𝑚 ∈ ℕ0 ∧ (𝜑 → (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)) ∈ 𝐴)) ∧ 𝜑) → (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)) ∈ 𝐴)
43 nfv 1829 . . . . . . . 8 𝑡 𝑚 ∈ ℕ0
44 nfmpt1 4669 . . . . . . . . 9 𝑡(𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚))
4544nfel1 2764 . . . . . . . 8 𝑡(𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)) ∈ 𝐴
4618, 43, 45nf3an 1818 . . . . . . 7 𝑡(𝜑𝑚 ∈ ℕ0 ∧ (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)) ∈ 𝐴)
47 simpl1 1056 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ0 ∧ (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)) ∈ 𝐴) ∧ 𝑡𝑇) → 𝜑)
48 simpr 475 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ0 ∧ (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)) ∈ 𝐴) ∧ 𝑡𝑇) → 𝑡𝑇)
4928recnd 9924 . . . . . . . . 9 ((𝜑𝑡𝑇) → (𝐹𝑡) ∈ ℂ)
5047, 48, 49syl2anc 690 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ0 ∧ (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)) ∈ 𝐴) ∧ 𝑡𝑇) → (𝐹𝑡) ∈ ℂ)
51 simpl2 1057 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ0 ∧ (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)) ∈ 𝐴) ∧ 𝑡𝑇) → 𝑚 ∈ ℕ0)
5250, 51expp1d 12826 . . . . . . 7 (((𝜑𝑚 ∈ ℕ0 ∧ (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)) ∈ 𝐴) ∧ 𝑡𝑇) → ((𝐹𝑡)↑(𝑚 + 1)) = (((𝐹𝑡)↑𝑚) · (𝐹𝑡)))
5346, 52mpteq2da 4665 . . . . . 6 ((𝜑𝑚 ∈ ℕ0 ∧ (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)) ∈ 𝐴) → (𝑡𝑇 ↦ ((𝐹𝑡)↑(𝑚 + 1))) = (𝑡𝑇 ↦ (((𝐹𝑡)↑𝑚) · (𝐹𝑡))))
54283adant2 1072 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ0𝑡𝑇) → (𝐹𝑡) ∈ ℝ)
55 simp2 1054 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ0𝑡𝑇) → 𝑚 ∈ ℕ0)
5654, 55reexpcld 12842 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ0𝑡𝑇) → ((𝐹𝑡)↑𝑚) ∈ ℝ)
5747, 51, 48, 56syl3anc 1317 . . . . . . . . . 10 (((𝜑𝑚 ∈ ℕ0 ∧ (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)) ∈ 𝐴) ∧ 𝑡𝑇) → ((𝐹𝑡)↑𝑚) ∈ ℝ)
58 eqid 2609 . . . . . . . . . . . 12 (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)) = (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚))
5958fvmpt2 6185 . . . . . . . . . . 11 ((𝑡𝑇 ∧ ((𝐹𝑡)↑𝑚) ∈ ℝ) → ((𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚))‘𝑡) = ((𝐹𝑡)↑𝑚))
6059eqcomd 2615 . . . . . . . . . 10 ((𝑡𝑇 ∧ ((𝐹𝑡)↑𝑚) ∈ ℝ) → ((𝐹𝑡)↑𝑚) = ((𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚))‘𝑡))
6148, 57, 60syl2anc 690 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ0 ∧ (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)) ∈ 𝐴) ∧ 𝑡𝑇) → ((𝐹𝑡)↑𝑚) = ((𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚))‘𝑡))
6261oveq1d 6542 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ0 ∧ (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)) ∈ 𝐴) ∧ 𝑡𝑇) → (((𝐹𝑡)↑𝑚) · (𝐹𝑡)) = (((𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚))‘𝑡) · (𝐹𝑡)))
6346, 62mpteq2da 4665 . . . . . . 7 ((𝜑𝑚 ∈ ℕ0 ∧ (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)) ∈ 𝐴) → (𝑡𝑇 ↦ (((𝐹𝑡)↑𝑚) · (𝐹𝑡))) = (𝑡𝑇 ↦ (((𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚))‘𝑡) · (𝐹𝑡))))
6419adantr 479 . . . . . . . . 9 ((𝜑 ∧ (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)) ∈ 𝐴) → 𝐹𝐴)
6544nfeq2 2765 . . . . . . . . . 10 𝑡 𝑓 = (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚))
66 stoweidlem19.1 . . . . . . . . . . 11 𝑡𝐹
6766nfeq2 2765 . . . . . . . . . 10 𝑡 𝑔 = 𝐹
68 stoweidlem19.4 . . . . . . . . . 10 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
6965, 67, 68stoweidlem6 38703 . . . . . . . . 9 ((𝜑 ∧ (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)) ∈ 𝐴𝐹𝐴) → (𝑡𝑇 ↦ (((𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚))‘𝑡) · (𝐹𝑡))) ∈ 𝐴)
7064, 69mpd3an3 1416 . . . . . . . 8 ((𝜑 ∧ (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)) ∈ 𝐴) → (𝑡𝑇 ↦ (((𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚))‘𝑡) · (𝐹𝑡))) ∈ 𝐴)
71703adant2 1072 . . . . . . 7 ((𝜑𝑚 ∈ ℕ0 ∧ (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)) ∈ 𝐴) → (𝑡𝑇 ↦ (((𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚))‘𝑡) · (𝐹𝑡))) ∈ 𝐴)
7263, 71eqeltrd 2687 . . . . . 6 ((𝜑𝑚 ∈ ℕ0 ∧ (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)) ∈ 𝐴) → (𝑡𝑇 ↦ (((𝐹𝑡)↑𝑚) · (𝐹𝑡))) ∈ 𝐴)
7353, 72eqeltrd 2687 . . . . 5 ((𝜑𝑚 ∈ ℕ0 ∧ (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)) ∈ 𝐴) → (𝑡𝑇 ↦ ((𝐹𝑡)↑(𝑚 + 1))) ∈ 𝐴)
7439, 40, 42, 73syl3anc 1317 . . . 4 (((𝑚 ∈ ℕ0 ∧ (𝜑 → (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)) ∈ 𝐴)) ∧ 𝜑) → (𝑡𝑇 ↦ ((𝐹𝑡)↑(𝑚 + 1))) ∈ 𝐴)
7574exp31 627 . . 3 (𝑚 ∈ ℕ0 → ((𝜑 → (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑚)) ∈ 𝐴) → (𝜑 → (𝑡𝑇 ↦ ((𝐹𝑡)↑(𝑚 + 1))) ∈ 𝐴)))
765, 9, 13, 17, 38, 75nn0ind 11304 . 2 (𝑁 ∈ ℕ0 → (𝜑 → (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑁)) ∈ 𝐴))
771, 76mpcom 37 1 (𝜑 → (𝑡𝑇 ↦ ((𝐹𝑡)↑𝑁)) ∈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030   = wceq 1474  wnf 1698  wcel 1976  wnfc 2737  cmpt 4637  wf 5786  cfv 5790  (class class class)co 6527  cc 9790  cr 9791  0cc0 9792  1c1 9793   + caddc 9795   · cmul 9797  0cn0 11139  cexp 12677
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6935  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-er 7606  df-en 7819  df-dom 7820  df-sdom 7821  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-nn 10868  df-n0 11140  df-z 11211  df-uz 11520  df-seq 12619  df-exp 12678
This theorem is referenced by:  stoweidlem40  38737
  Copyright terms: Public domain W3C validator