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

Theorem stoweidlem36 42675
 Description: This lemma is used to prove the existence of a function pt as in Lemma 1 of [BrosowskiDeutsh] p. 90 (at the beginning of Lemma 1): for all t in T - U, there exists a function p in the subalgebra, such that pt ( t0 ) = 0 , pt ( t ) > 0, and 0 <= pt <= 1. Z is used for t0 , S is used for t e. T - U , h is used for pt . G is used for (ht)^2 and the final h is a normalized version of G ( divided by its norm, see the variable N ). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem36.1 𝑄
stoweidlem36.2 𝑡𝐻
stoweidlem36.3 𝑡𝐹
stoweidlem36.4 𝑡𝐺
stoweidlem36.5 𝑡𝜑
stoweidlem36.6 𝐾 = (topGen‘ran (,))
stoweidlem36.7 𝑄 = {𝐴 ∣ ((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))}
stoweidlem36.8 𝑇 = 𝐽
stoweidlem36.9 𝐺 = (𝑡𝑇 ↦ ((𝐹𝑡) · (𝐹𝑡)))
stoweidlem36.10 𝑁 = sup(ran 𝐺, ℝ, < )
stoweidlem36.11 𝐻 = (𝑡𝑇 ↦ ((𝐺𝑡) / 𝑁))
stoweidlem36.12 (𝜑𝐽 ∈ Comp)
stoweidlem36.13 (𝜑𝐴 ⊆ (𝐽 Cn 𝐾))
stoweidlem36.14 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
stoweidlem36.15 ((𝜑𝑥 ∈ ℝ) → (𝑡𝑇𝑥) ∈ 𝐴)
stoweidlem36.16 (𝜑𝑆𝑇)
stoweidlem36.17 (𝜑𝑍𝑇)
stoweidlem36.18 (𝜑𝐹𝐴)
stoweidlem36.19 (𝜑 → (𝐹𝑆) ≠ (𝐹𝑍))
stoweidlem36.20 (𝜑 → (𝐹𝑍) = 0)
Assertion
Ref Expression
stoweidlem36 (𝜑 → ∃(𝑄 ∧ 0 < (𝑆)))
Distinct variable groups:   𝑓,𝑔,𝑡,𝑇   𝐴,𝑓,𝑔   𝑓,𝐹,𝑔   𝑓,𝐺,𝑔   𝜑,𝑓,𝑔   𝑔,𝑁,𝑡   𝑡,,𝑆   𝐴,   ,𝐻   𝑇,   ,𝑍,𝑡   𝑥,𝑡,𝑁   𝑥,𝐴   𝑥,𝑇   𝜑,𝑥
Allowed substitution hints:   𝜑(𝑡,)   𝐴(𝑡)   𝑄(𝑥,𝑡,𝑓,𝑔,)   𝑆(𝑥,𝑓,𝑔)   𝐹(𝑥,𝑡,)   𝐺(𝑥,𝑡,)   𝐻(𝑥,𝑡,𝑓,𝑔)   𝐽(𝑥,𝑡,𝑓,𝑔,)   𝐾(𝑥,𝑡,𝑓,𝑔,)   𝑁(𝑓,)   𝑍(𝑥,𝑓,𝑔)

Proof of Theorem stoweidlem36
Dummy variable 𝑠 is distinct from all other variables.
StepHypRef Expression
1 stoweidlem36.11 . . . . . 6 𝐻 = (𝑡𝑇 ↦ ((𝐺𝑡) / 𝑁))
2 stoweidlem36.5 . . . . . . 7 𝑡𝜑
3 stoweidlem36.6 . . . . . . . . . . . 12 𝐾 = (topGen‘ran (,))
4 stoweidlem36.8 . . . . . . . . . . . 12 𝑇 = 𝐽
5 eqid 2801 . . . . . . . . . . . 12 (𝐽 Cn 𝐾) = (𝐽 Cn 𝐾)
6 stoweidlem36.13 . . . . . . . . . . . . 13 (𝜑𝐴 ⊆ (𝐽 Cn 𝐾))
7 stoweidlem36.9 . . . . . . . . . . . . . 14 𝐺 = (𝑡𝑇 ↦ ((𝐹𝑡) · (𝐹𝑡)))
8 stoweidlem36.18 . . . . . . . . . . . . . . 15 (𝜑𝐹𝐴)
9 stoweidlem36.3 . . . . . . . . . . . . . . . . 17 𝑡𝐹
109nfeq2 2975 . . . . . . . . . . . . . . . 16 𝑡 𝑓 = 𝐹
119nfeq2 2975 . . . . . . . . . . . . . . . 16 𝑡 𝑔 = 𝐹
12 stoweidlem36.14 . . . . . . . . . . . . . . . 16 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
1310, 11, 12stoweidlem6 42645 . . . . . . . . . . . . . . 15 ((𝜑𝐹𝐴𝐹𝐴) → (𝑡𝑇 ↦ ((𝐹𝑡) · (𝐹𝑡))) ∈ 𝐴)
148, 8, 13mpd3an23 1460 . . . . . . . . . . . . . 14 (𝜑 → (𝑡𝑇 ↦ ((𝐹𝑡) · (𝐹𝑡))) ∈ 𝐴)
157, 14eqeltrid 2897 . . . . . . . . . . . . 13 (𝜑𝐺𝐴)
166, 15sseldd 3919 . . . . . . . . . . . 12 (𝜑𝐺 ∈ (𝐽 Cn 𝐾))
173, 4, 5, 16fcnre 41651 . . . . . . . . . . 11 (𝜑𝐺:𝑇⟶ℝ)
1817ffvelrnda 6832 . . . . . . . . . 10 ((𝜑𝑡𝑇) → (𝐺𝑡) ∈ ℝ)
1918recnd 10662 . . . . . . . . 9 ((𝜑𝑡𝑇) → (𝐺𝑡) ∈ ℂ)
20 stoweidlem36.10 . . . . . . . . . . . 12 𝑁 = sup(ran 𝐺, ℝ, < )
21 stoweidlem36.12 . . . . . . . . . . . . . 14 (𝜑𝐽 ∈ Comp)
22 stoweidlem36.16 . . . . . . . . . . . . . . 15 (𝜑𝑆𝑇)
2322ne0d 4254 . . . . . . . . . . . . . 14 (𝜑𝑇 ≠ ∅)
244, 3, 21, 16, 23cncmpmax 41658 . . . . . . . . . . . . 13 (𝜑 → (sup(ran 𝐺, ℝ, < ) ∈ ran 𝐺 ∧ sup(ran 𝐺, ℝ, < ) ∈ ℝ ∧ ∀𝑠𝑇 (𝐺𝑠) ≤ sup(ran 𝐺, ℝ, < )))
2524simp2d 1140 . . . . . . . . . . . 12 (𝜑 → sup(ran 𝐺, ℝ, < ) ∈ ℝ)
2620, 25eqeltrid 2897 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℝ)
2726recnd 10662 . . . . . . . . . 10 (𝜑𝑁 ∈ ℂ)
2827adantr 484 . . . . . . . . 9 ((𝜑𝑡𝑇) → 𝑁 ∈ ℂ)
29 0red 10637 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ ℝ)
3017, 22ffvelrnd 6833 . . . . . . . . . . . . 13 (𝜑 → (𝐺𝑆) ∈ ℝ)
316, 8sseldd 3919 . . . . . . . . . . . . . . . . 17 (𝜑𝐹 ∈ (𝐽 Cn 𝐾))
323, 4, 5, 31fcnre 41651 . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝑇⟶ℝ)
3332, 22ffvelrnd 6833 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹𝑆) ∈ ℝ)
34 stoweidlem36.19 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹𝑆) ≠ (𝐹𝑍))
35 stoweidlem36.20 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹𝑍) = 0)
3634, 35neeqtrd 3059 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹𝑆) ≠ 0)
3733, 36msqgt0d 11200 . . . . . . . . . . . . . 14 (𝜑 → 0 < ((𝐹𝑆) · (𝐹𝑆)))
3833, 33remulcld 10664 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐹𝑆) · (𝐹𝑆)) ∈ ℝ)
39 nfcv 2958 . . . . . . . . . . . . . . . 16 𝑡𝑆
409, 39nffv 6659 . . . . . . . . . . . . . . . . 17 𝑡(𝐹𝑆)
41 nfcv 2958 . . . . . . . . . . . . . . . . 17 𝑡 ·
4240, 41, 40nfov 7169 . . . . . . . . . . . . . . . 16 𝑡((𝐹𝑆) · (𝐹𝑆))
43 fveq2 6649 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑆 → (𝐹𝑡) = (𝐹𝑆))
4443, 43oveq12d 7157 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑆 → ((𝐹𝑡) · (𝐹𝑡)) = ((𝐹𝑆) · (𝐹𝑆)))
4539, 42, 44, 7fvmptf 6770 . . . . . . . . . . . . . . 15 ((𝑆𝑇 ∧ ((𝐹𝑆) · (𝐹𝑆)) ∈ ℝ) → (𝐺𝑆) = ((𝐹𝑆) · (𝐹𝑆)))
4622, 38, 45syl2anc 587 . . . . . . . . . . . . . 14 (𝜑 → (𝐺𝑆) = ((𝐹𝑆) · (𝐹𝑆)))
4737, 46breqtrrd 5061 . . . . . . . . . . . . 13 (𝜑 → 0 < (𝐺𝑆))
4824simp3d 1141 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑠𝑇 (𝐺𝑠) ≤ sup(ran 𝐺, ℝ, < ))
49 fveq2 6649 . . . . . . . . . . . . . . . 16 (𝑠 = 𝑆 → (𝐺𝑠) = (𝐺𝑆))
5049breq1d 5043 . . . . . . . . . . . . . . 15 (𝑠 = 𝑆 → ((𝐺𝑠) ≤ sup(ran 𝐺, ℝ, < ) ↔ (𝐺𝑆) ≤ sup(ran 𝐺, ℝ, < )))
5150rspccva 3573 . . . . . . . . . . . . . 14 ((∀𝑠𝑇 (𝐺𝑠) ≤ sup(ran 𝐺, ℝ, < ) ∧ 𝑆𝑇) → (𝐺𝑆) ≤ sup(ran 𝐺, ℝ, < ))
5248, 22, 51syl2anc 587 . . . . . . . . . . . . 13 (𝜑 → (𝐺𝑆) ≤ sup(ran 𝐺, ℝ, < ))
5329, 30, 25, 47, 52ltletrd 10793 . . . . . . . . . . . 12 (𝜑 → 0 < sup(ran 𝐺, ℝ, < ))
5453gt0ne0d 11197 . . . . . . . . . . 11 (𝜑 → sup(ran 𝐺, ℝ, < ) ≠ 0)
5520neeq1i 3054 . . . . . . . . . . 11 (𝑁 ≠ 0 ↔ sup(ran 𝐺, ℝ, < ) ≠ 0)
5654, 55sylibr 237 . . . . . . . . . 10 (𝜑𝑁 ≠ 0)
5756adantr 484 . . . . . . . . 9 ((𝜑𝑡𝑇) → 𝑁 ≠ 0)
5819, 28, 57divrecd 11412 . . . . . . . 8 ((𝜑𝑡𝑇) → ((𝐺𝑡) / 𝑁) = ((𝐺𝑡) · (1 / 𝑁)))
59 simpr 488 . . . . . . . . . 10 ((𝜑𝑡𝑇) → 𝑡𝑇)
6026, 56rereccld 11460 . . . . . . . . . . 11 (𝜑 → (1 / 𝑁) ∈ ℝ)
6160adantr 484 . . . . . . . . . 10 ((𝜑𝑡𝑇) → (1 / 𝑁) ∈ ℝ)
62 eqid 2801 . . . . . . . . . . 11 (𝑡𝑇 ↦ (1 / 𝑁)) = (𝑡𝑇 ↦ (1 / 𝑁))
6362fvmpt2 6760 . . . . . . . . . 10 ((𝑡𝑇 ∧ (1 / 𝑁) ∈ ℝ) → ((𝑡𝑇 ↦ (1 / 𝑁))‘𝑡) = (1 / 𝑁))
6459, 61, 63syl2anc 587 . . . . . . . . 9 ((𝜑𝑡𝑇) → ((𝑡𝑇 ↦ (1 / 𝑁))‘𝑡) = (1 / 𝑁))
6564oveq2d 7155 . . . . . . . 8 ((𝜑𝑡𝑇) → ((𝐺𝑡) · ((𝑡𝑇 ↦ (1 / 𝑁))‘𝑡)) = ((𝐺𝑡) · (1 / 𝑁)))
6658, 65eqtr4d 2839 . . . . . . 7 ((𝜑𝑡𝑇) → ((𝐺𝑡) / 𝑁) = ((𝐺𝑡) · ((𝑡𝑇 ↦ (1 / 𝑁))‘𝑡)))
672, 66mpteq2da 5127 . . . . . 6 (𝜑 → (𝑡𝑇 ↦ ((𝐺𝑡) / 𝑁)) = (𝑡𝑇 ↦ ((𝐺𝑡) · ((𝑡𝑇 ↦ (1 / 𝑁))‘𝑡))))
681, 67syl5eq 2848 . . . . 5 (𝜑𝐻 = (𝑡𝑇 ↦ ((𝐺𝑡) · ((𝑡𝑇 ↦ (1 / 𝑁))‘𝑡))))
69 stoweidlem36.15 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → (𝑡𝑇𝑥) ∈ 𝐴)
7069stoweidlem4 42643 . . . . . . 7 ((𝜑 ∧ (1 / 𝑁) ∈ ℝ) → (𝑡𝑇 ↦ (1 / 𝑁)) ∈ 𝐴)
7160, 70mpdan 686 . . . . . 6 (𝜑 → (𝑡𝑇 ↦ (1 / 𝑁)) ∈ 𝐴)
72 stoweidlem36.4 . . . . . . . 8 𝑡𝐺
7372nfeq2 2975 . . . . . . 7 𝑡 𝑓 = 𝐺
74 nfmpt1 5131 . . . . . . . 8 𝑡(𝑡𝑇 ↦ (1 / 𝑁))
7574nfeq2 2975 . . . . . . 7 𝑡 𝑔 = (𝑡𝑇 ↦ (1 / 𝑁))
7673, 75, 12stoweidlem6 42645 . . . . . 6 ((𝜑𝐺𝐴 ∧ (𝑡𝑇 ↦ (1 / 𝑁)) ∈ 𝐴) → (𝑡𝑇 ↦ ((𝐺𝑡) · ((𝑡𝑇 ↦ (1 / 𝑁))‘𝑡))) ∈ 𝐴)
7715, 71, 76mpd3an23 1460 . . . . 5 (𝜑 → (𝑡𝑇 ↦ ((𝐺𝑡) · ((𝑡𝑇 ↦ (1 / 𝑁))‘𝑡))) ∈ 𝐴)
7868, 77eqeltrd 2893 . . . 4 (𝜑𝐻𝐴)
79 stoweidlem36.17 . . . . . . 7 (𝜑𝑍𝑇)
8017, 79ffvelrnd 6833 . . . . . . . 8 (𝜑 → (𝐺𝑍) ∈ ℝ)
8180, 26, 56redivcld 11461 . . . . . . 7 (𝜑 → ((𝐺𝑍) / 𝑁) ∈ ℝ)
82 nfcv 2958 . . . . . . . 8 𝑡𝑍
8372, 82nffv 6659 . . . . . . . . 9 𝑡(𝐺𝑍)
84 nfcv 2958 . . . . . . . . 9 𝑡 /
85 nfcv 2958 . . . . . . . . 9 𝑡𝑁
8683, 84, 85nfov 7169 . . . . . . . 8 𝑡((𝐺𝑍) / 𝑁)
87 fveq2 6649 . . . . . . . . 9 (𝑡 = 𝑍 → (𝐺𝑡) = (𝐺𝑍))
8887oveq1d 7154 . . . . . . . 8 (𝑡 = 𝑍 → ((𝐺𝑡) / 𝑁) = ((𝐺𝑍) / 𝑁))
8982, 86, 88, 1fvmptf 6770 . . . . . . 7 ((𝑍𝑇 ∧ ((𝐺𝑍) / 𝑁) ∈ ℝ) → (𝐻𝑍) = ((𝐺𝑍) / 𝑁))
9079, 81, 89syl2anc 587 . . . . . 6 (𝜑 → (𝐻𝑍) = ((𝐺𝑍) / 𝑁))
91 0re 10636 . . . . . . . . . . 11 0 ∈ ℝ
9235, 91eqeltrdi 2901 . . . . . . . . . 10 (𝜑 → (𝐹𝑍) ∈ ℝ)
9392, 92remulcld 10664 . . . . . . . . 9 (𝜑 → ((𝐹𝑍) · (𝐹𝑍)) ∈ ℝ)
949, 82nffv 6659 . . . . . . . . . . 11 𝑡(𝐹𝑍)
9594, 41, 94nfov 7169 . . . . . . . . . 10 𝑡((𝐹𝑍) · (𝐹𝑍))
96 fveq2 6649 . . . . . . . . . . 11 (𝑡 = 𝑍 → (𝐹𝑡) = (𝐹𝑍))
9796, 96oveq12d 7157 . . . . . . . . . 10 (𝑡 = 𝑍 → ((𝐹𝑡) · (𝐹𝑡)) = ((𝐹𝑍) · (𝐹𝑍)))
9882, 95, 97, 7fvmptf 6770 . . . . . . . . 9 ((𝑍𝑇 ∧ ((𝐹𝑍) · (𝐹𝑍)) ∈ ℝ) → (𝐺𝑍) = ((𝐹𝑍) · (𝐹𝑍)))
9979, 93, 98syl2anc 587 . . . . . . . 8 (𝜑 → (𝐺𝑍) = ((𝐹𝑍) · (𝐹𝑍)))
10035, 35oveq12d 7157 . . . . . . . . 9 (𝜑 → ((𝐹𝑍) · (𝐹𝑍)) = (0 · 0))
101 0cn 10626 . . . . . . . . . 10 0 ∈ ℂ
102101mul02i 10822 . . . . . . . . 9 (0 · 0) = 0
103100, 102eqtrdi 2852 . . . . . . . 8 (𝜑 → ((𝐹𝑍) · (𝐹𝑍)) = 0)
10499, 103eqtrd 2836 . . . . . . 7 (𝜑 → (𝐺𝑍) = 0)
105104oveq1d 7154 . . . . . 6 (𝜑 → ((𝐺𝑍) / 𝑁) = (0 / 𝑁))
10627, 56div0d 11408 . . . . . 6 (𝜑 → (0 / 𝑁) = 0)
10790, 105, 1063eqtrd 2840 . . . . 5 (𝜑 → (𝐻𝑍) = 0)
10832ffvelrnda 6832 . . . . . . . . . . . 12 ((𝜑𝑡𝑇) → (𝐹𝑡) ∈ ℝ)
109108msqge0d 11201 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → 0 ≤ ((𝐹𝑡) · (𝐹𝑡)))
110108, 108remulcld 10664 . . . . . . . . . . . 12 ((𝜑𝑡𝑇) → ((𝐹𝑡) · (𝐹𝑡)) ∈ ℝ)
1117fvmpt2 6760 . . . . . . . . . . . 12 ((𝑡𝑇 ∧ ((𝐹𝑡) · (𝐹𝑡)) ∈ ℝ) → (𝐺𝑡) = ((𝐹𝑡) · (𝐹𝑡)))
11259, 110, 111syl2anc 587 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → (𝐺𝑡) = ((𝐹𝑡) · (𝐹𝑡)))
113109, 112breqtrrd 5061 . . . . . . . . . 10 ((𝜑𝑡𝑇) → 0 ≤ (𝐺𝑡))
11426adantr 484 . . . . . . . . . 10 ((𝜑𝑡𝑇) → 𝑁 ∈ ℝ)
11553, 20breqtrrdi 5075 . . . . . . . . . . 11 (𝜑 → 0 < 𝑁)
116115adantr 484 . . . . . . . . . 10 ((𝜑𝑡𝑇) → 0 < 𝑁)
117 divge0 11502 . . . . . . . . . 10 ((((𝐺𝑡) ∈ ℝ ∧ 0 ≤ (𝐺𝑡)) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → 0 ≤ ((𝐺𝑡) / 𝑁))
11818, 113, 114, 116, 117syl22anc 837 . . . . . . . . 9 ((𝜑𝑡𝑇) → 0 ≤ ((𝐺𝑡) / 𝑁))
11918, 114, 57redivcld 11461 . . . . . . . . . 10 ((𝜑𝑡𝑇) → ((𝐺𝑡) / 𝑁) ∈ ℝ)
1201fvmpt2 6760 . . . . . . . . . 10 ((𝑡𝑇 ∧ ((𝐺𝑡) / 𝑁) ∈ ℝ) → (𝐻𝑡) = ((𝐺𝑡) / 𝑁))
12159, 119, 120syl2anc 587 . . . . . . . . 9 ((𝜑𝑡𝑇) → (𝐻𝑡) = ((𝐺𝑡) / 𝑁))
122118, 121breqtrrd 5061 . . . . . . . 8 ((𝜑𝑡𝑇) → 0 ≤ (𝐻𝑡))
12319div1d 11401 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → ((𝐺𝑡) / 1) = (𝐺𝑡))
124 fveq2 6649 . . . . . . . . . . . . . . 15 (𝑠 = 𝑡 → (𝐺𝑠) = (𝐺𝑡))
125124breq1d 5043 . . . . . . . . . . . . . 14 (𝑠 = 𝑡 → ((𝐺𝑠) ≤ sup(ran 𝐺, ℝ, < ) ↔ (𝐺𝑡) ≤ sup(ran 𝐺, ℝ, < )))
126125rspccva 3573 . . . . . . . . . . . . 13 ((∀𝑠𝑇 (𝐺𝑠) ≤ sup(ran 𝐺, ℝ, < ) ∧ 𝑡𝑇) → (𝐺𝑡) ≤ sup(ran 𝐺, ℝ, < ))
12748, 126sylan 583 . . . . . . . . . . . 12 ((𝜑𝑡𝑇) → (𝐺𝑡) ≤ sup(ran 𝐺, ℝ, < ))
128127, 20breqtrrdi 5075 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → (𝐺𝑡) ≤ 𝑁)
129123, 128eqbrtrd 5055 . . . . . . . . . 10 ((𝜑𝑡𝑇) → ((𝐺𝑡) / 1) ≤ 𝑁)
130 1red 10635 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → 1 ∈ ℝ)
131 0lt1 11155 . . . . . . . . . . . 12 0 < 1
132131a1i 11 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → 0 < 1)
133 lediv23 11525 . . . . . . . . . . 11 (((𝐺𝑡) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁) ∧ (1 ∈ ℝ ∧ 0 < 1)) → (((𝐺𝑡) / 𝑁) ≤ 1 ↔ ((𝐺𝑡) / 1) ≤ 𝑁))
13418, 114, 116, 130, 132, 133syl122anc 1376 . . . . . . . . . 10 ((𝜑𝑡𝑇) → (((𝐺𝑡) / 𝑁) ≤ 1 ↔ ((𝐺𝑡) / 1) ≤ 𝑁))
135129, 134mpbird 260 . . . . . . . . 9 ((𝜑𝑡𝑇) → ((𝐺𝑡) / 𝑁) ≤ 1)
136121, 135eqbrtrd 5055 . . . . . . . 8 ((𝜑𝑡𝑇) → (𝐻𝑡) ≤ 1)
137122, 136jca 515 . . . . . . 7 ((𝜑𝑡𝑇) → (0 ≤ (𝐻𝑡) ∧ (𝐻𝑡) ≤ 1))
138137ex 416 . . . . . 6 (𝜑 → (𝑡𝑇 → (0 ≤ (𝐻𝑡) ∧ (𝐻𝑡) ≤ 1)))
1392, 138ralrimi 3183 . . . . 5 (𝜑 → ∀𝑡𝑇 (0 ≤ (𝐻𝑡) ∧ (𝐻𝑡) ≤ 1))
140107, 139jca 515 . . . 4 (𝜑 → ((𝐻𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝐻𝑡) ∧ (𝐻𝑡) ≤ 1)))
141 fveq1 6648 . . . . . . 7 ( = 𝐻 → (𝑍) = (𝐻𝑍))
142141eqeq1d 2803 . . . . . 6 ( = 𝐻 → ((𝑍) = 0 ↔ (𝐻𝑍) = 0))
143 stoweidlem36.2 . . . . . . . 8 𝑡𝐻
144143nfeq2 2975 . . . . . . 7 𝑡 = 𝐻
145 fveq1 6648 . . . . . . . . 9 ( = 𝐻 → (𝑡) = (𝐻𝑡))
146145breq2d 5045 . . . . . . . 8 ( = 𝐻 → (0 ≤ (𝑡) ↔ 0 ≤ (𝐻𝑡)))
147145breq1d 5043 . . . . . . . 8 ( = 𝐻 → ((𝑡) ≤ 1 ↔ (𝐻𝑡) ≤ 1))
148146, 147anbi12d 633 . . . . . . 7 ( = 𝐻 → ((0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ↔ (0 ≤ (𝐻𝑡) ∧ (𝐻𝑡) ≤ 1)))
149144, 148ralbid 3198 . . . . . 6 ( = 𝐻 → (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ (𝐻𝑡) ∧ (𝐻𝑡) ≤ 1)))
150142, 149anbi12d 633 . . . . 5 ( = 𝐻 → (((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)) ↔ ((𝐻𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝐻𝑡) ∧ (𝐻𝑡) ≤ 1))))
151150elrab 3631 . . . 4 (𝐻 ∈ {𝐴 ∣ ((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))} ↔ (𝐻𝐴 ∧ ((𝐻𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝐻𝑡) ∧ (𝐻𝑡) ≤ 1))))
15278, 140, 151sylanbrc 586 . . 3 (𝜑𝐻 ∈ {𝐴 ∣ ((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))})
153 stoweidlem36.7 . . 3 𝑄 = {𝐴 ∣ ((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))}
154152, 153eleqtrrdi 2904 . 2 (𝜑𝐻𝑄)
15530, 26, 47, 115divgt0d 11568 . . 3 (𝜑 → 0 < ((𝐺𝑆) / 𝑁))
15630, 26, 56redivcld 11461 . . . 4 (𝜑 → ((𝐺𝑆) / 𝑁) ∈ ℝ)
15772, 39nffv 6659 . . . . . 6 𝑡(𝐺𝑆)
158157, 84, 85nfov 7169 . . . . 5 𝑡((𝐺𝑆) / 𝑁)
159 fveq2 6649 . . . . . 6 (𝑡 = 𝑆 → (𝐺𝑡) = (𝐺𝑆))
160159oveq1d 7154 . . . . 5 (𝑡 = 𝑆 → ((𝐺𝑡) / 𝑁) = ((𝐺𝑆) / 𝑁))
16139, 158, 160, 1fvmptf 6770 . . . 4 ((𝑆𝑇 ∧ ((𝐺𝑆) / 𝑁) ∈ ℝ) → (𝐻𝑆) = ((𝐺𝑆) / 𝑁))
16222, 156, 161syl2anc 587 . . 3 (𝜑 → (𝐻𝑆) = ((𝐺𝑆) / 𝑁))
163155, 162breqtrrd 5061 . 2 (𝜑 → 0 < (𝐻𝑆))
164 nfcv 2958 . . . 4 𝐻
165 stoweidlem36.1 . . . . . 6 𝑄
166165nfel2 2976 . . . . 5 𝐻𝑄
167 nfv 1915 . . . . 5 0 < (𝐻𝑆)
168166, 167nfan 1900 . . . 4 (𝐻𝑄 ∧ 0 < (𝐻𝑆))
169 eleq1 2880 . . . . 5 ( = 𝐻 → (𝑄𝐻𝑄))
170 fveq1 6648 . . . . . 6 ( = 𝐻 → (𝑆) = (𝐻𝑆))
171170breq2d 5045 . . . . 5 ( = 𝐻 → (0 < (𝑆) ↔ 0 < (𝐻𝑆)))
172169, 171anbi12d 633 . . . 4 ( = 𝐻 → ((𝑄 ∧ 0 < (𝑆)) ↔ (𝐻𝑄 ∧ 0 < (𝐻𝑆))))
173164, 168, 172spcegf 3542 . . 3 (𝐻𝑄 → ((𝐻𝑄 ∧ 0 < (𝐻𝑆)) → ∃(𝑄 ∧ 0 < (𝑆))))
174173anabsi5 668 . 2 ((𝐻𝑄 ∧ 0 < (𝐻𝑆)) → ∃(𝑄 ∧ 0 < (𝑆)))
175154, 163, 174syl2anc 587 1 (𝜑 → ∃(𝑄 ∧ 0 < (𝑆)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ∃wex 1781  Ⅎwnf 1785   ∈ wcel 2112  Ⅎwnfc 2939   ≠ wne 2990  ∀wral 3109  {crab 3113   ⊆ wss 3884  ∪ cuni 4803   class class class wbr 5033   ↦ cmpt 5113  ran crn 5524  ‘cfv 6328  (class class class)co 7139  supcsup 8892  ℂcc 10528  ℝcr 10529  0cc0 10530  1c1 10531   · cmul 10535   < clt 10668   ≤ cle 10669   / cdiv 11290  (,)cioo 12730  topGenctg 16707   Cn ccn 21833  Compccmp 21995 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607  ax-pre-sup 10608  ax-mulf 10610 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-of 7393  df-om 7565  df-1st 7675  df-2nd 7676  df-supp 7818  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-2o 8090  df-oadd 8093  df-er 8276  df-map 8395  df-ixp 8449  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fsupp 8822  df-fi 8863  df-sup 8894  df-inf 8895  df-oi 8962  df-card 9356  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-div 11291  df-nn 11630  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-q 12341  df-rp 12382  df-xneg 12499  df-xadd 12500  df-xmul 12501  df-ioo 12734  df-icc 12737  df-fz 12890  df-fzo 13033  df-seq 13369  df-exp 13430  df-hash 13691  df-cj 14454  df-re 14455  df-im 14456  df-sqrt 14590  df-abs 14591  df-struct 16481  df-ndx 16482  df-slot 16483  df-base 16485  df-sets 16486  df-ress 16487  df-plusg 16574  df-mulr 16575  df-starv 16576  df-sca 16577  df-vsca 16578  df-ip 16579  df-tset 16580  df-ple 16581  df-ds 16583  df-unif 16584  df-hom 16585  df-cco 16586  df-rest 16692  df-topn 16693  df-0g 16711  df-gsum 16712  df-topgen 16713  df-pt 16714  df-prds 16717  df-xrs 16771  df-qtop 16776  df-imas 16777  df-xps 16779  df-mre 16853  df-mrc 16854  df-acs 16856  df-mgm 17848  df-sgrp 17897  df-mnd 17908  df-submnd 17953  df-mulg 18221  df-cntz 18443  df-cmn 18904  df-psmet 20087  df-xmet 20088  df-met 20089  df-bl 20090  df-mopn 20091  df-cnfld 20096  df-top 21503  df-topon 21520  df-topsp 21542  df-bases 21555  df-cn 21836  df-cnp 21837  df-cmp 21996  df-tx 22171  df-hmeo 22364  df-xms 22931  df-ms 22932  df-tms 22933 This theorem is referenced by:  stoweidlem43  42682
 Copyright terms: Public domain W3C validator