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

Theorem stoweidlem36 45424
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 2728 . . . . . . . . . . . 12 (𝐽 Cn 𝐾) = (𝐽 Cn 𝐾)
6 stoweidlem36.13 . . . . . . . . . . . . 13 (𝜑𝐴 ⊆ (𝐽 Cn 𝐾))
7 stoweidlem36.9 . . . . . . . . . . . . . 14 𝐺 = (𝑡𝑇 ↦ ((𝐹𝑡) · (𝐹𝑡)))
8 stoweidlem36.18 . . . . . . . . . . . . . . 15 (𝜑𝐹𝐴)
9 stoweidlem36.3 . . . . . . . . . . . . . . . . 17 𝑡𝐹
109nfeq2 2917 . . . . . . . . . . . . . . . 16 𝑡 𝑓 = 𝐹
119nfeq2 2917 . . . . . . . . . . . . . . . 16 𝑡 𝑔 = 𝐹
12 stoweidlem36.14 . . . . . . . . . . . . . . . 16 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
1310, 11, 12stoweidlem6 45394 . . . . . . . . . . . . . . 15 ((𝜑𝐹𝐴𝐹𝐴) → (𝑡𝑇 ↦ ((𝐹𝑡) · (𝐹𝑡))) ∈ 𝐴)
148, 8, 13mpd3an23 1460 . . . . . . . . . . . . . 14 (𝜑 → (𝑡𝑇 ↦ ((𝐹𝑡) · (𝐹𝑡))) ∈ 𝐴)
157, 14eqeltrid 2833 . . . . . . . . . . . . 13 (𝜑𝐺𝐴)
166, 15sseldd 3981 . . . . . . . . . . . 12 (𝜑𝐺 ∈ (𝐽 Cn 𝐾))
173, 4, 5, 16fcnre 44387 . . . . . . . . . . 11 (𝜑𝐺:𝑇⟶ℝ)
1817ffvelcdmda 7094 . . . . . . . . . 10 ((𝜑𝑡𝑇) → (𝐺𝑡) ∈ ℝ)
1918recnd 11273 . . . . . . . . 9 ((𝜑𝑡𝑇) → (𝐺𝑡) ∈ ℂ)
20 stoweidlem36.10 . . . . . . . . . . . 12 𝑁 = sup(ran 𝐺, ℝ, < )
21 stoweidlem36.12 . . . . . . . . . . . . . 14 (𝜑𝐽 ∈ Comp)
22 stoweidlem36.16 . . . . . . . . . . . . . . 15 (𝜑𝑆𝑇)
2322ne0d 4336 . . . . . . . . . . . . . 14 (𝜑𝑇 ≠ ∅)
244, 3, 21, 16, 23cncmpmax 44394 . . . . . . . . . . . . 13 (𝜑 → (sup(ran 𝐺, ℝ, < ) ∈ ran 𝐺 ∧ sup(ran 𝐺, ℝ, < ) ∈ ℝ ∧ ∀𝑠𝑇 (𝐺𝑠) ≤ sup(ran 𝐺, ℝ, < )))
2524simp2d 1141 . . . . . . . . . . . 12 (𝜑 → sup(ran 𝐺, ℝ, < ) ∈ ℝ)
2620, 25eqeltrid 2833 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℝ)
2726recnd 11273 . . . . . . . . . 10 (𝜑𝑁 ∈ ℂ)
2827adantr 480 . . . . . . . . 9 ((𝜑𝑡𝑇) → 𝑁 ∈ ℂ)
29 0red 11248 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ ℝ)
3017, 22ffvelcdmd 7095 . . . . . . . . . . . . 13 (𝜑 → (𝐺𝑆) ∈ ℝ)
316, 8sseldd 3981 . . . . . . . . . . . . . . . . 17 (𝜑𝐹 ∈ (𝐽 Cn 𝐾))
323, 4, 5, 31fcnre 44387 . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝑇⟶ℝ)
3332, 22ffvelcdmd 7095 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹𝑆) ∈ ℝ)
34 stoweidlem36.19 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹𝑆) ≠ (𝐹𝑍))
35 stoweidlem36.20 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹𝑍) = 0)
3634, 35neeqtrd 3007 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹𝑆) ≠ 0)
3733, 36msqgt0d 11812 . . . . . . . . . . . . . 14 (𝜑 → 0 < ((𝐹𝑆) · (𝐹𝑆)))
3833, 33remulcld 11275 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐹𝑆) · (𝐹𝑆)) ∈ ℝ)
39 nfcv 2899 . . . . . . . . . . . . . . . 16 𝑡𝑆
409, 39nffv 6907 . . . . . . . . . . . . . . . . 17 𝑡(𝐹𝑆)
41 nfcv 2899 . . . . . . . . . . . . . . . . 17 𝑡 ·
4240, 41, 40nfov 7450 . . . . . . . . . . . . . . . 16 𝑡((𝐹𝑆) · (𝐹𝑆))
43 fveq2 6897 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑆 → (𝐹𝑡) = (𝐹𝑆))
4443, 43oveq12d 7438 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑆 → ((𝐹𝑡) · (𝐹𝑡)) = ((𝐹𝑆) · (𝐹𝑆)))
4539, 42, 44, 7fvmptf 7026 . . . . . . . . . . . . . . 15 ((𝑆𝑇 ∧ ((𝐹𝑆) · (𝐹𝑆)) ∈ ℝ) → (𝐺𝑆) = ((𝐹𝑆) · (𝐹𝑆)))
4622, 38, 45syl2anc 583 . . . . . . . . . . . . . 14 (𝜑 → (𝐺𝑆) = ((𝐹𝑆) · (𝐹𝑆)))
4737, 46breqtrrd 5176 . . . . . . . . . . . . 13 (𝜑 → 0 < (𝐺𝑆))
4824simp3d 1142 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑠𝑇 (𝐺𝑠) ≤ sup(ran 𝐺, ℝ, < ))
49 fveq2 6897 . . . . . . . . . . . . . . . 16 (𝑠 = 𝑆 → (𝐺𝑠) = (𝐺𝑆))
5049breq1d 5158 . . . . . . . . . . . . . . 15 (𝑠 = 𝑆 → ((𝐺𝑠) ≤ sup(ran 𝐺, ℝ, < ) ↔ (𝐺𝑆) ≤ sup(ran 𝐺, ℝ, < )))
5150rspccva 3608 . . . . . . . . . . . . . 14 ((∀𝑠𝑇 (𝐺𝑠) ≤ sup(ran 𝐺, ℝ, < ) ∧ 𝑆𝑇) → (𝐺𝑆) ≤ sup(ran 𝐺, ℝ, < ))
5248, 22, 51syl2anc 583 . . . . . . . . . . . . 13 (𝜑 → (𝐺𝑆) ≤ sup(ran 𝐺, ℝ, < ))
5329, 30, 25, 47, 52ltletrd 11405 . . . . . . . . . . . 12 (𝜑 → 0 < sup(ran 𝐺, ℝ, < ))
5453gt0ne0d 11809 . . . . . . . . . . 11 (𝜑 → sup(ran 𝐺, ℝ, < ) ≠ 0)
5520neeq1i 3002 . . . . . . . . . . 11 (𝑁 ≠ 0 ↔ sup(ran 𝐺, ℝ, < ) ≠ 0)
5654, 55sylibr 233 . . . . . . . . . 10 (𝜑𝑁 ≠ 0)
5756adantr 480 . . . . . . . . 9 ((𝜑𝑡𝑇) → 𝑁 ≠ 0)
5819, 28, 57divrecd 12024 . . . . . . . 8 ((𝜑𝑡𝑇) → ((𝐺𝑡) / 𝑁) = ((𝐺𝑡) · (1 / 𝑁)))
59 simpr 484 . . . . . . . . . 10 ((𝜑𝑡𝑇) → 𝑡𝑇)
6026, 56rereccld 12072 . . . . . . . . . . 11 (𝜑 → (1 / 𝑁) ∈ ℝ)
6160adantr 480 . . . . . . . . . 10 ((𝜑𝑡𝑇) → (1 / 𝑁) ∈ ℝ)
62 eqid 2728 . . . . . . . . . . 11 (𝑡𝑇 ↦ (1 / 𝑁)) = (𝑡𝑇 ↦ (1 / 𝑁))
6362fvmpt2 7016 . . . . . . . . . 10 ((𝑡𝑇 ∧ (1 / 𝑁) ∈ ℝ) → ((𝑡𝑇 ↦ (1 / 𝑁))‘𝑡) = (1 / 𝑁))
6459, 61, 63syl2anc 583 . . . . . . . . 9 ((𝜑𝑡𝑇) → ((𝑡𝑇 ↦ (1 / 𝑁))‘𝑡) = (1 / 𝑁))
6564oveq2d 7436 . . . . . . . 8 ((𝜑𝑡𝑇) → ((𝐺𝑡) · ((𝑡𝑇 ↦ (1 / 𝑁))‘𝑡)) = ((𝐺𝑡) · (1 / 𝑁)))
6658, 65eqtr4d 2771 . . . . . . 7 ((𝜑𝑡𝑇) → ((𝐺𝑡) / 𝑁) = ((𝐺𝑡) · ((𝑡𝑇 ↦ (1 / 𝑁))‘𝑡)))
672, 66mpteq2da 5246 . . . . . 6 (𝜑 → (𝑡𝑇 ↦ ((𝐺𝑡) / 𝑁)) = (𝑡𝑇 ↦ ((𝐺𝑡) · ((𝑡𝑇 ↦ (1 / 𝑁))‘𝑡))))
681, 67eqtrid 2780 . . . . 5 (𝜑𝐻 = (𝑡𝑇 ↦ ((𝐺𝑡) · ((𝑡𝑇 ↦ (1 / 𝑁))‘𝑡))))
69 stoweidlem36.15 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → (𝑡𝑇𝑥) ∈ 𝐴)
7069stoweidlem4 45392 . . . . . . 7 ((𝜑 ∧ (1 / 𝑁) ∈ ℝ) → (𝑡𝑇 ↦ (1 / 𝑁)) ∈ 𝐴)
7160, 70mpdan 686 . . . . . 6 (𝜑 → (𝑡𝑇 ↦ (1 / 𝑁)) ∈ 𝐴)
72 stoweidlem36.4 . . . . . . . 8 𝑡𝐺
7372nfeq2 2917 . . . . . . 7 𝑡 𝑓 = 𝐺
74 nfmpt1 5256 . . . . . . . 8 𝑡(𝑡𝑇 ↦ (1 / 𝑁))
7574nfeq2 2917 . . . . . . 7 𝑡 𝑔 = (𝑡𝑇 ↦ (1 / 𝑁))
7673, 75, 12stoweidlem6 45394 . . . . . 6 ((𝜑𝐺𝐴 ∧ (𝑡𝑇 ↦ (1 / 𝑁)) ∈ 𝐴) → (𝑡𝑇 ↦ ((𝐺𝑡) · ((𝑡𝑇 ↦ (1 / 𝑁))‘𝑡))) ∈ 𝐴)
7715, 71, 76mpd3an23 1460 . . . . 5 (𝜑 → (𝑡𝑇 ↦ ((𝐺𝑡) · ((𝑡𝑇 ↦ (1 / 𝑁))‘𝑡))) ∈ 𝐴)
7868, 77eqeltrd 2829 . . . 4 (𝜑𝐻𝐴)
79 stoweidlem36.17 . . . . . . 7 (𝜑𝑍𝑇)
8017, 79ffvelcdmd 7095 . . . . . . . 8 (𝜑 → (𝐺𝑍) ∈ ℝ)
8180, 26, 56redivcld 12073 . . . . . . 7 (𝜑 → ((𝐺𝑍) / 𝑁) ∈ ℝ)
82 nfcv 2899 . . . . . . . 8 𝑡𝑍
8372, 82nffv 6907 . . . . . . . . 9 𝑡(𝐺𝑍)
84 nfcv 2899 . . . . . . . . 9 𝑡 /
85 nfcv 2899 . . . . . . . . 9 𝑡𝑁
8683, 84, 85nfov 7450 . . . . . . . 8 𝑡((𝐺𝑍) / 𝑁)
87 fveq2 6897 . . . . . . . . 9 (𝑡 = 𝑍 → (𝐺𝑡) = (𝐺𝑍))
8887oveq1d 7435 . . . . . . . 8 (𝑡 = 𝑍 → ((𝐺𝑡) / 𝑁) = ((𝐺𝑍) / 𝑁))
8982, 86, 88, 1fvmptf 7026 . . . . . . 7 ((𝑍𝑇 ∧ ((𝐺𝑍) / 𝑁) ∈ ℝ) → (𝐻𝑍) = ((𝐺𝑍) / 𝑁))
9079, 81, 89syl2anc 583 . . . . . 6 (𝜑 → (𝐻𝑍) = ((𝐺𝑍) / 𝑁))
91 0re 11247 . . . . . . . . . . 11 0 ∈ ℝ
9235, 91eqeltrdi 2837 . . . . . . . . . 10 (𝜑 → (𝐹𝑍) ∈ ℝ)
9392, 92remulcld 11275 . . . . . . . . 9 (𝜑 → ((𝐹𝑍) · (𝐹𝑍)) ∈ ℝ)
949, 82nffv 6907 . . . . . . . . . . 11 𝑡(𝐹𝑍)
9594, 41, 94nfov 7450 . . . . . . . . . 10 𝑡((𝐹𝑍) · (𝐹𝑍))
96 fveq2 6897 . . . . . . . . . . 11 (𝑡 = 𝑍 → (𝐹𝑡) = (𝐹𝑍))
9796, 96oveq12d 7438 . . . . . . . . . 10 (𝑡 = 𝑍 → ((𝐹𝑡) · (𝐹𝑡)) = ((𝐹𝑍) · (𝐹𝑍)))
9882, 95, 97, 7fvmptf 7026 . . . . . . . . 9 ((𝑍𝑇 ∧ ((𝐹𝑍) · (𝐹𝑍)) ∈ ℝ) → (𝐺𝑍) = ((𝐹𝑍) · (𝐹𝑍)))
9979, 93, 98syl2anc 583 . . . . . . . 8 (𝜑 → (𝐺𝑍) = ((𝐹𝑍) · (𝐹𝑍)))
10035, 35oveq12d 7438 . . . . . . . . 9 (𝜑 → ((𝐹𝑍) · (𝐹𝑍)) = (0 · 0))
101 0cn 11237 . . . . . . . . . 10 0 ∈ ℂ
102101mul02i 11434 . . . . . . . . 9 (0 · 0) = 0
103100, 102eqtrdi 2784 . . . . . . . 8 (𝜑 → ((𝐹𝑍) · (𝐹𝑍)) = 0)
10499, 103eqtrd 2768 . . . . . . 7 (𝜑 → (𝐺𝑍) = 0)
105104oveq1d 7435 . . . . . 6 (𝜑 → ((𝐺𝑍) / 𝑁) = (0 / 𝑁))
10627, 56div0d 12020 . . . . . 6 (𝜑 → (0 / 𝑁) = 0)
10790, 105, 1063eqtrd 2772 . . . . 5 (𝜑 → (𝐻𝑍) = 0)
10832ffvelcdmda 7094 . . . . . . . . . . . 12 ((𝜑𝑡𝑇) → (𝐹𝑡) ∈ ℝ)
109108msqge0d 11813 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → 0 ≤ ((𝐹𝑡) · (𝐹𝑡)))
110108, 108remulcld 11275 . . . . . . . . . . . 12 ((𝜑𝑡𝑇) → ((𝐹𝑡) · (𝐹𝑡)) ∈ ℝ)
1117fvmpt2 7016 . . . . . . . . . . . 12 ((𝑡𝑇 ∧ ((𝐹𝑡) · (𝐹𝑡)) ∈ ℝ) → (𝐺𝑡) = ((𝐹𝑡) · (𝐹𝑡)))
11259, 110, 111syl2anc 583 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → (𝐺𝑡) = ((𝐹𝑡) · (𝐹𝑡)))
113109, 112breqtrrd 5176 . . . . . . . . . 10 ((𝜑𝑡𝑇) → 0 ≤ (𝐺𝑡))
11426adantr 480 . . . . . . . . . 10 ((𝜑𝑡𝑇) → 𝑁 ∈ ℝ)
11553, 20breqtrrdi 5190 . . . . . . . . . . 11 (𝜑 → 0 < 𝑁)
116115adantr 480 . . . . . . . . . 10 ((𝜑𝑡𝑇) → 0 < 𝑁)
117 divge0 12114 . . . . . . . . . 10 ((((𝐺𝑡) ∈ ℝ ∧ 0 ≤ (𝐺𝑡)) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → 0 ≤ ((𝐺𝑡) / 𝑁))
11818, 113, 114, 116, 117syl22anc 838 . . . . . . . . 9 ((𝜑𝑡𝑇) → 0 ≤ ((𝐺𝑡) / 𝑁))
11918, 114, 57redivcld 12073 . . . . . . . . . 10 ((𝜑𝑡𝑇) → ((𝐺𝑡) / 𝑁) ∈ ℝ)
1201fvmpt2 7016 . . . . . . . . . 10 ((𝑡𝑇 ∧ ((𝐺𝑡) / 𝑁) ∈ ℝ) → (𝐻𝑡) = ((𝐺𝑡) / 𝑁))
12159, 119, 120syl2anc 583 . . . . . . . . 9 ((𝜑𝑡𝑇) → (𝐻𝑡) = ((𝐺𝑡) / 𝑁))
122118, 121breqtrrd 5176 . . . . . . . 8 ((𝜑𝑡𝑇) → 0 ≤ (𝐻𝑡))
12319div1d 12013 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → ((𝐺𝑡) / 1) = (𝐺𝑡))
124 fveq2 6897 . . . . . . . . . . . . . . 15 (𝑠 = 𝑡 → (𝐺𝑠) = (𝐺𝑡))
125124breq1d 5158 . . . . . . . . . . . . . 14 (𝑠 = 𝑡 → ((𝐺𝑠) ≤ sup(ran 𝐺, ℝ, < ) ↔ (𝐺𝑡) ≤ sup(ran 𝐺, ℝ, < )))
126125rspccva 3608 . . . . . . . . . . . . 13 ((∀𝑠𝑇 (𝐺𝑠) ≤ sup(ran 𝐺, ℝ, < ) ∧ 𝑡𝑇) → (𝐺𝑡) ≤ sup(ran 𝐺, ℝ, < ))
12748, 126sylan 579 . . . . . . . . . . . 12 ((𝜑𝑡𝑇) → (𝐺𝑡) ≤ sup(ran 𝐺, ℝ, < ))
128127, 20breqtrrdi 5190 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → (𝐺𝑡) ≤ 𝑁)
129123, 128eqbrtrd 5170 . . . . . . . . . 10 ((𝜑𝑡𝑇) → ((𝐺𝑡) / 1) ≤ 𝑁)
130 1red 11246 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → 1 ∈ ℝ)
131 0lt1 11767 . . . . . . . . . . . 12 0 < 1
132131a1i 11 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → 0 < 1)
133 lediv23 12137 . . . . . . . . . . 11 (((𝐺𝑡) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁) ∧ (1 ∈ ℝ ∧ 0 < 1)) → (((𝐺𝑡) / 𝑁) ≤ 1 ↔ ((𝐺𝑡) / 1) ≤ 𝑁))
13418, 114, 116, 130, 132, 133syl122anc 1377 . . . . . . . . . 10 ((𝜑𝑡𝑇) → (((𝐺𝑡) / 𝑁) ≤ 1 ↔ ((𝐺𝑡) / 1) ≤ 𝑁))
135129, 134mpbird 257 . . . . . . . . 9 ((𝜑𝑡𝑇) → ((𝐺𝑡) / 𝑁) ≤ 1)
136121, 135eqbrtrd 5170 . . . . . . . 8 ((𝜑𝑡𝑇) → (𝐻𝑡) ≤ 1)
137122, 136jca 511 . . . . . . 7 ((𝜑𝑡𝑇) → (0 ≤ (𝐻𝑡) ∧ (𝐻𝑡) ≤ 1))
138137ex 412 . . . . . 6 (𝜑 → (𝑡𝑇 → (0 ≤ (𝐻𝑡) ∧ (𝐻𝑡) ≤ 1)))
1392, 138ralrimi 3251 . . . . 5 (𝜑 → ∀𝑡𝑇 (0 ≤ (𝐻𝑡) ∧ (𝐻𝑡) ≤ 1))
140107, 139jca 511 . . . 4 (𝜑 → ((𝐻𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝐻𝑡) ∧ (𝐻𝑡) ≤ 1)))
141 fveq1 6896 . . . . . . 7 ( = 𝐻 → (𝑍) = (𝐻𝑍))
142141eqeq1d 2730 . . . . . 6 ( = 𝐻 → ((𝑍) = 0 ↔ (𝐻𝑍) = 0))
143 stoweidlem36.2 . . . . . . . 8 𝑡𝐻
144143nfeq2 2917 . . . . . . 7 𝑡 = 𝐻
145 fveq1 6896 . . . . . . . . 9 ( = 𝐻 → (𝑡) = (𝐻𝑡))
146145breq2d 5160 . . . . . . . 8 ( = 𝐻 → (0 ≤ (𝑡) ↔ 0 ≤ (𝐻𝑡)))
147145breq1d 5158 . . . . . . . 8 ( = 𝐻 → ((𝑡) ≤ 1 ↔ (𝐻𝑡) ≤ 1))
148146, 147anbi12d 631 . . . . . . 7 ( = 𝐻 → ((0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ↔ (0 ≤ (𝐻𝑡) ∧ (𝐻𝑡) ≤ 1)))
149144, 148ralbid 3267 . . . . . 6 ( = 𝐻 → (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ (𝐻𝑡) ∧ (𝐻𝑡) ≤ 1)))
150142, 149anbi12d 631 . . . . 5 ( = 𝐻 → (((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)) ↔ ((𝐻𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝐻𝑡) ∧ (𝐻𝑡) ≤ 1))))
151150elrab 3682 . . . 4 (𝐻 ∈ {𝐴 ∣ ((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))} ↔ (𝐻𝐴 ∧ ((𝐻𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝐻𝑡) ∧ (𝐻𝑡) ≤ 1))))
15278, 140, 151sylanbrc 582 . . 3 (𝜑𝐻 ∈ {𝐴 ∣ ((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))})
153 stoweidlem36.7 . . 3 𝑄 = {𝐴 ∣ ((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))}
154152, 153eleqtrrdi 2840 . 2 (𝜑𝐻𝑄)
15530, 26, 47, 115divgt0d 12180 . . 3 (𝜑 → 0 < ((𝐺𝑆) / 𝑁))
15630, 26, 56redivcld 12073 . . . 4 (𝜑 → ((𝐺𝑆) / 𝑁) ∈ ℝ)
15772, 39nffv 6907 . . . . . 6 𝑡(𝐺𝑆)
158157, 84, 85nfov 7450 . . . . 5 𝑡((𝐺𝑆) / 𝑁)
159 fveq2 6897 . . . . . 6 (𝑡 = 𝑆 → (𝐺𝑡) = (𝐺𝑆))
160159oveq1d 7435 . . . . 5 (𝑡 = 𝑆 → ((𝐺𝑡) / 𝑁) = ((𝐺𝑆) / 𝑁))
16139, 158, 160, 1fvmptf 7026 . . . 4 ((𝑆𝑇 ∧ ((𝐺𝑆) / 𝑁) ∈ ℝ) → (𝐻𝑆) = ((𝐺𝑆) / 𝑁))
16222, 156, 161syl2anc 583 . . 3 (𝜑 → (𝐻𝑆) = ((𝐺𝑆) / 𝑁))
163155, 162breqtrrd 5176 . 2 (𝜑 → 0 < (𝐻𝑆))
164 nfcv 2899 . . . 4 𝐻
165 stoweidlem36.1 . . . . . 6 𝑄
166165nfel2 2918 . . . . 5 𝐻𝑄
167 nfv 1910 . . . . 5 0 < (𝐻𝑆)
168166, 167nfan 1895 . . . 4 (𝐻𝑄 ∧ 0 < (𝐻𝑆))
169 eleq1 2817 . . . . 5 ( = 𝐻 → (𝑄𝐻𝑄))
170 fveq1 6896 . . . . . 6 ( = 𝐻 → (𝑆) = (𝐻𝑆))
171170breq2d 5160 . . . . 5 ( = 𝐻 → (0 < (𝑆) ↔ 0 < (𝐻𝑆)))
172169, 171anbi12d 631 . . . 4 ( = 𝐻 → ((𝑄 ∧ 0 < (𝑆)) ↔ (𝐻𝑄 ∧ 0 < (𝐻𝑆))))
173164, 168, 172spcegf 3579 . . 3 (𝐻𝑄 → ((𝐻𝑄 ∧ 0 < (𝐻𝑆)) → ∃(𝑄 ∧ 0 < (𝑆))))
174173anabsi5 668 . 2 ((𝐻𝑄 ∧ 0 < (𝐻𝑆)) → ∃(𝑄 ∧ 0 < (𝑆)))
175154, 163, 174syl2anc 583 1 (𝜑 → ∃(𝑄 ∧ 0 < (𝑆)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3a 1085   = wceq 1534  wex 1774  wnf 1778  wcel 2099  wnfc 2879  wne 2937  wral 3058  {crab 3429  wss 3947   cuni 4908   class class class wbr 5148  cmpt 5231  ran crn 5679  cfv 6548  (class class class)co 7420  supcsup 9464  cc 11137  cr 11138  0cc0 11139  1c1 11140   · cmul 11144   < clt 11279  cle 11280   / cdiv 11902  (,)cioo 13357  topGenctg 17419   Cn ccn 23141  Compccmp 23303
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740  ax-cnex 11195  ax-resscn 11196  ax-1cn 11197  ax-icn 11198  ax-addcl 11199  ax-addrcl 11200  ax-mulcl 11201  ax-mulrcl 11202  ax-mulcom 11203  ax-addass 11204  ax-mulass 11205  ax-distr 11206  ax-i2m1 11207  ax-1ne0 11208  ax-1rid 11209  ax-rnegex 11210  ax-rrecex 11211  ax-cnre 11212  ax-pre-lttri 11213  ax-pre-lttrn 11214  ax-pre-ltadd 11215  ax-pre-mulgt0 11216  ax-pre-sup 11217
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3373  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4909  df-int 4950  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6305  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-isom 6557  df-riota 7376  df-ov 7423  df-oprab 7424  df-mpo 7425  df-of 7685  df-om 7871  df-1st 7993  df-2nd 7994  df-supp 8166  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-2o 8488  df-er 8725  df-map 8847  df-ixp 8917  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-fsupp 9387  df-fi 9435  df-sup 9466  df-inf 9467  df-oi 9534  df-card 9963  df-pnf 11281  df-mnf 11282  df-xr 11283  df-ltxr 11284  df-le 11285  df-sub 11477  df-neg 11478  df-div 11903  df-nn 12244  df-2 12306  df-3 12307  df-4 12308  df-5 12309  df-6 12310  df-7 12311  df-8 12312  df-9 12313  df-n0 12504  df-z 12590  df-dec 12709  df-uz 12854  df-q 12964  df-rp 13008  df-xneg 13125  df-xadd 13126  df-xmul 13127  df-ioo 13361  df-icc 13364  df-fz 13518  df-fzo 13661  df-seq 14000  df-exp 14060  df-hash 14323  df-cj 15079  df-re 15080  df-im 15081  df-sqrt 15215  df-abs 15216  df-struct 17116  df-sets 17133  df-slot 17151  df-ndx 17163  df-base 17181  df-ress 17210  df-plusg 17246  df-mulr 17247  df-starv 17248  df-sca 17249  df-vsca 17250  df-ip 17251  df-tset 17252  df-ple 17253  df-ds 17255  df-unif 17256  df-hom 17257  df-cco 17258  df-rest 17404  df-topn 17405  df-0g 17423  df-gsum 17424  df-topgen 17425  df-pt 17426  df-prds 17429  df-xrs 17484  df-qtop 17489  df-imas 17490  df-xps 17492  df-mre 17566  df-mrc 17567  df-acs 17569  df-mgm 18600  df-sgrp 18679  df-mnd 18695  df-submnd 18741  df-mulg 19024  df-cntz 19268  df-cmn 19737  df-psmet 21271  df-xmet 21272  df-met 21273  df-bl 21274  df-mopn 21275  df-cnfld 21280  df-top 22809  df-topon 22826  df-topsp 22848  df-bases 22862  df-cn 23144  df-cnp 23145  df-cmp 23304  df-tx 23479  df-hmeo 23672  df-xms 24239  df-ms 24240  df-tms 24241
This theorem is referenced by:  stoweidlem43  45431
  Copyright terms: Public domain W3C validator