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

Theorem stoweidlem41 43265
Description: This lemma is used to prove that there exists x as in Lemma 1 of [BrosowskiDeutsh] p. 90: 0 <= x(t) <= 1 for all t in T, x(t) < epsilon for all t in V, x(t) > 1 - epsilon for all t in T \ U. Here we prove the very last step of the proof of Lemma 1: "The result follows from taking x = 1 - qn";. Here 𝐸 is used to represent ε in the paper, and 𝑦 to represent qn in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem41.1 𝑡𝜑
stoweidlem41.2 𝑋 = (𝑡𝑇 ↦ (1 − (𝑦𝑡)))
stoweidlem41.3 𝐹 = (𝑡𝑇 ↦ 1)
stoweidlem41.4 𝑉𝑇
stoweidlem41.5 (𝜑𝑦𝐴)
stoweidlem41.6 (𝜑𝑦:𝑇⟶ℝ)
stoweidlem41.7 ((𝜑𝑓𝐴) → 𝑓:𝑇⟶ℝ)
stoweidlem41.8 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) + (𝑔𝑡))) ∈ 𝐴)
stoweidlem41.9 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
stoweidlem41.10 ((𝜑𝑤 ∈ ℝ) → (𝑡𝑇𝑤) ∈ 𝐴)
stoweidlem41.11 (𝜑𝐸 ∈ ℝ+)
stoweidlem41.12 (𝜑 → ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1))
stoweidlem41.13 (𝜑 → ∀𝑡𝑉 (1 − 𝐸) < (𝑦𝑡))
stoweidlem41.14 (𝜑 → ∀𝑡 ∈ (𝑇𝑈)(𝑦𝑡) < 𝐸)
Assertion
Ref Expression
stoweidlem41 (𝜑 → ∃𝑥𝐴 (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡𝑉 (𝑥𝑡) < 𝐸 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝐸) < (𝑥𝑡)))
Distinct variable groups:   𝑓,𝑔,𝑡,𝑦   𝐴,𝑓,𝑔,𝑡   𝑓,𝐹,𝑔   𝑇,𝑓,𝑔,𝑡   𝜑,𝑓,𝑔   𝑤,𝑡,𝐴   𝑥,𝑡,𝐴   𝑤,𝑇   𝜑,𝑤   𝑥,𝐸   𝑥,𝑇   𝑥,𝑈   𝑥,𝑉   𝑥,𝑋
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑡)   𝐴(𝑦)   𝑇(𝑦)   𝑈(𝑦,𝑤,𝑡,𝑓,𝑔)   𝐸(𝑦,𝑤,𝑡,𝑓,𝑔)   𝐹(𝑥,𝑦,𝑤,𝑡)   𝑉(𝑦,𝑤,𝑡,𝑓,𝑔)   𝑋(𝑦,𝑤,𝑡,𝑓,𝑔)

Proof of Theorem stoweidlem41
StepHypRef Expression
1 stoweidlem41.1 . . . . 5 𝑡𝜑
2 1re 10838 . . . . . . . 8 1 ∈ ℝ
3 stoweidlem41.3 . . . . . . . . 9 𝐹 = (𝑡𝑇 ↦ 1)
43fvmpt2 6834 . . . . . . . 8 ((𝑡𝑇 ∧ 1 ∈ ℝ) → (𝐹𝑡) = 1)
52, 4mpan2 691 . . . . . . 7 (𝑡𝑇 → (𝐹𝑡) = 1)
65adantl 485 . . . . . 6 ((𝜑𝑡𝑇) → (𝐹𝑡) = 1)
76oveq1d 7233 . . . . 5 ((𝜑𝑡𝑇) → ((𝐹𝑡) − (𝑦𝑡)) = (1 − (𝑦𝑡)))
81, 7mpteq2da 5154 . . . 4 (𝜑 → (𝑡𝑇 ↦ ((𝐹𝑡) − (𝑦𝑡))) = (𝑡𝑇 ↦ (1 − (𝑦𝑡))))
9 stoweidlem41.2 . . . 4 𝑋 = (𝑡𝑇 ↦ (1 − (𝑦𝑡)))
108, 9eqtr4di 2796 . . 3 (𝜑 → (𝑡𝑇 ↦ ((𝐹𝑡) − (𝑦𝑡))) = 𝑋)
11 stoweidlem41.10 . . . . . . 7 ((𝜑𝑤 ∈ ℝ) → (𝑡𝑇𝑤) ∈ 𝐴)
1211stoweidlem4 43228 . . . . . 6 ((𝜑 ∧ 1 ∈ ℝ) → (𝑡𝑇 ↦ 1) ∈ 𝐴)
132, 12mpan2 691 . . . . 5 (𝜑 → (𝑡𝑇 ↦ 1) ∈ 𝐴)
143, 13eqeltrid 2842 . . . 4 (𝜑𝐹𝐴)
15 stoweidlem41.5 . . . 4 (𝜑𝑦𝐴)
16 nfmpt1 5158 . . . . . 6 𝑡(𝑡𝑇 ↦ 1)
173, 16nfcxfr 2902 . . . . 5 𝑡𝐹
18 nfcv 2904 . . . . 5 𝑡𝑦
19 stoweidlem41.7 . . . . 5 ((𝜑𝑓𝐴) → 𝑓:𝑇⟶ℝ)
20 stoweidlem41.8 . . . . 5 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) + (𝑔𝑡))) ∈ 𝐴)
21 stoweidlem41.9 . . . . 5 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
2217, 18, 1, 19, 20, 21, 11stoweidlem33 43257 . . . 4 ((𝜑𝐹𝐴𝑦𝐴) → (𝑡𝑇 ↦ ((𝐹𝑡) − (𝑦𝑡))) ∈ 𝐴)
2314, 15, 22mpd3an23 1465 . . 3 (𝜑 → (𝑡𝑇 ↦ ((𝐹𝑡) − (𝑦𝑡))) ∈ 𝐴)
2410, 23eqeltrrd 2839 . 2 (𝜑𝑋𝐴)
25 stoweidlem41.6 . . . . . . . 8 (𝜑𝑦:𝑇⟶ℝ)
2625ffvelrnda 6909 . . . . . . 7 ((𝜑𝑡𝑇) → (𝑦𝑡) ∈ ℝ)
27 1red 10839 . . . . . . 7 ((𝜑𝑡𝑇) → 1 ∈ ℝ)
28 0red 10841 . . . . . . 7 ((𝜑𝑡𝑇) → 0 ∈ ℝ)
29 stoweidlem41.12 . . . . . . . . . 10 (𝜑 → ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1))
3029r19.21bi 3130 . . . . . . . . 9 ((𝜑𝑡𝑇) → (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1))
3130simprd 499 . . . . . . . 8 ((𝜑𝑡𝑇) → (𝑦𝑡) ≤ 1)
32 1m0e1 11956 . . . . . . . 8 (1 − 0) = 1
3331, 32breqtrrdi 5100 . . . . . . 7 ((𝜑𝑡𝑇) → (𝑦𝑡) ≤ (1 − 0))
3426, 27, 28, 33lesubd 11441 . . . . . 6 ((𝜑𝑡𝑇) → 0 ≤ (1 − (𝑦𝑡)))
35 simpr 488 . . . . . . 7 ((𝜑𝑡𝑇) → 𝑡𝑇)
3627, 26resubcld 11265 . . . . . . 7 ((𝜑𝑡𝑇) → (1 − (𝑦𝑡)) ∈ ℝ)
379fvmpt2 6834 . . . . . . 7 ((𝑡𝑇 ∧ (1 − (𝑦𝑡)) ∈ ℝ) → (𝑋𝑡) = (1 − (𝑦𝑡)))
3835, 36, 37syl2anc 587 . . . . . 6 ((𝜑𝑡𝑇) → (𝑋𝑡) = (1 − (𝑦𝑡)))
3934, 38breqtrrd 5086 . . . . 5 ((𝜑𝑡𝑇) → 0 ≤ (𝑋𝑡))
4030simpld 498 . . . . . . . 8 ((𝜑𝑡𝑇) → 0 ≤ (𝑦𝑡))
4128, 26, 27, 40lesub2dd 11454 . . . . . . 7 ((𝜑𝑡𝑇) → (1 − (𝑦𝑡)) ≤ (1 − 0))
4241, 32breqtrdi 5099 . . . . . 6 ((𝜑𝑡𝑇) → (1 − (𝑦𝑡)) ≤ 1)
4338, 42eqbrtrd 5080 . . . . 5 ((𝜑𝑡𝑇) → (𝑋𝑡) ≤ 1)
4439, 43jca 515 . . . 4 ((𝜑𝑡𝑇) → (0 ≤ (𝑋𝑡) ∧ (𝑋𝑡) ≤ 1))
4544ex 416 . . 3 (𝜑 → (𝑡𝑇 → (0 ≤ (𝑋𝑡) ∧ (𝑋𝑡) ≤ 1)))
461, 45ralrimi 3137 . 2 (𝜑 → ∀𝑡𝑇 (0 ≤ (𝑋𝑡) ∧ (𝑋𝑡) ≤ 1))
47 stoweidlem41.4 . . . . . . 7 𝑉𝑇
4847sseli 3901 . . . . . 6 (𝑡𝑉𝑡𝑇)
4948, 38sylan2 596 . . . . 5 ((𝜑𝑡𝑉) → (𝑋𝑡) = (1 − (𝑦𝑡)))
50 1red 10839 . . . . . 6 ((𝜑𝑡𝑉) → 1 ∈ ℝ)
51 stoweidlem41.11 . . . . . . . 8 (𝜑𝐸 ∈ ℝ+)
5251rpred 12633 . . . . . . 7 (𝜑𝐸 ∈ ℝ)
5352adantr 484 . . . . . 6 ((𝜑𝑡𝑉) → 𝐸 ∈ ℝ)
5448, 26sylan2 596 . . . . . 6 ((𝜑𝑡𝑉) → (𝑦𝑡) ∈ ℝ)
55 stoweidlem41.13 . . . . . . 7 (𝜑 → ∀𝑡𝑉 (1 − 𝐸) < (𝑦𝑡))
5655r19.21bi 3130 . . . . . 6 ((𝜑𝑡𝑉) → (1 − 𝐸) < (𝑦𝑡))
5750, 53, 54, 56ltsub23d 11442 . . . . 5 ((𝜑𝑡𝑉) → (1 − (𝑦𝑡)) < 𝐸)
5849, 57eqbrtrd 5080 . . . 4 ((𝜑𝑡𝑉) → (𝑋𝑡) < 𝐸)
5958ex 416 . . 3 (𝜑 → (𝑡𝑉 → (𝑋𝑡) < 𝐸))
601, 59ralrimi 3137 . 2 (𝜑 → ∀𝑡𝑉 (𝑋𝑡) < 𝐸)
61 eldifi 4046 . . . . . . 7 (𝑡 ∈ (𝑇𝑈) → 𝑡𝑇)
6261, 26sylan2 596 . . . . . 6 ((𝜑𝑡 ∈ (𝑇𝑈)) → (𝑦𝑡) ∈ ℝ)
6352adantr 484 . . . . . 6 ((𝜑𝑡 ∈ (𝑇𝑈)) → 𝐸 ∈ ℝ)
64 1red 10839 . . . . . 6 ((𝜑𝑡 ∈ (𝑇𝑈)) → 1 ∈ ℝ)
65 stoweidlem41.14 . . . . . . 7 (𝜑 → ∀𝑡 ∈ (𝑇𝑈)(𝑦𝑡) < 𝐸)
6665r19.21bi 3130 . . . . . 6 ((𝜑𝑡 ∈ (𝑇𝑈)) → (𝑦𝑡) < 𝐸)
6762, 63, 64, 66ltsub2dd 11450 . . . . 5 ((𝜑𝑡 ∈ (𝑇𝑈)) → (1 − 𝐸) < (1 − (𝑦𝑡)))
6861, 38sylan2 596 . . . . 5 ((𝜑𝑡 ∈ (𝑇𝑈)) → (𝑋𝑡) = (1 − (𝑦𝑡)))
6967, 68breqtrrd 5086 . . . 4 ((𝜑𝑡 ∈ (𝑇𝑈)) → (1 − 𝐸) < (𝑋𝑡))
7069ex 416 . . 3 (𝜑 → (𝑡 ∈ (𝑇𝑈) → (1 − 𝐸) < (𝑋𝑡)))
711, 70ralrimi 3137 . 2 (𝜑 → ∀𝑡 ∈ (𝑇𝑈)(1 − 𝐸) < (𝑋𝑡))
72 nfmpt1 5158 . . . . . . 7 𝑡(𝑡𝑇 ↦ (1 − (𝑦𝑡)))
739, 72nfcxfr 2902 . . . . . 6 𝑡𝑋
7473nfeq2 2921 . . . . 5 𝑡 𝑥 = 𝑋
75 fveq1 6721 . . . . . . 7 (𝑥 = 𝑋 → (𝑥𝑡) = (𝑋𝑡))
7675breq2d 5070 . . . . . 6 (𝑥 = 𝑋 → (0 ≤ (𝑥𝑡) ↔ 0 ≤ (𝑋𝑡)))
7775breq1d 5068 . . . . . 6 (𝑥 = 𝑋 → ((𝑥𝑡) ≤ 1 ↔ (𝑋𝑡) ≤ 1))
7876, 77anbi12d 634 . . . . 5 (𝑥 = 𝑋 → ((0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ↔ (0 ≤ (𝑋𝑡) ∧ (𝑋𝑡) ≤ 1)))
7974, 78ralbid 3156 . . . 4 (𝑥 = 𝑋 → (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ (𝑋𝑡) ∧ (𝑋𝑡) ≤ 1)))
8075breq1d 5068 . . . . 5 (𝑥 = 𝑋 → ((𝑥𝑡) < 𝐸 ↔ (𝑋𝑡) < 𝐸))
8174, 80ralbid 3156 . . . 4 (𝑥 = 𝑋 → (∀𝑡𝑉 (𝑥𝑡) < 𝐸 ↔ ∀𝑡𝑉 (𝑋𝑡) < 𝐸))
8275breq2d 5070 . . . . 5 (𝑥 = 𝑋 → ((1 − 𝐸) < (𝑥𝑡) ↔ (1 − 𝐸) < (𝑋𝑡)))
8374, 82ralbid 3156 . . . 4 (𝑥 = 𝑋 → (∀𝑡 ∈ (𝑇𝑈)(1 − 𝐸) < (𝑥𝑡) ↔ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝐸) < (𝑋𝑡)))
8479, 81, 833anbi123d 1438 . . 3 (𝑥 = 𝑋 → ((∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡𝑉 (𝑥𝑡) < 𝐸 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝐸) < (𝑥𝑡)) ↔ (∀𝑡𝑇 (0 ≤ (𝑋𝑡) ∧ (𝑋𝑡) ≤ 1) ∧ ∀𝑡𝑉 (𝑋𝑡) < 𝐸 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝐸) < (𝑋𝑡))))
8584rspcev 3542 . 2 ((𝑋𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑋𝑡) ∧ (𝑋𝑡) ≤ 1) ∧ ∀𝑡𝑉 (𝑋𝑡) < 𝐸 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝐸) < (𝑋𝑡))) → ∃𝑥𝐴 (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡𝑉 (𝑥𝑡) < 𝐸 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝐸) < (𝑥𝑡)))
8624, 46, 60, 71, 85syl13anc 1374 1 (𝜑 → ∃𝑥𝐴 (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡𝑉 (𝑥𝑡) < 𝐸 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝐸) < (𝑥𝑡)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1089   = wceq 1543  wnf 1791  wcel 2110  wral 3061  wrex 3062  cdif 3868  wss 3871   class class class wbr 5058  cmpt 5140  wf 6381  cfv 6385  (class class class)co 7218  cr 10733  0cc0 10734  1c1 10735   + caddc 10737   · cmul 10739   < clt 10872  cle 10873  cmin 11067  +crp 12591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5197  ax-nul 5204  ax-pow 5263  ax-pr 5327  ax-un 7528  ax-resscn 10791  ax-1cn 10792  ax-icn 10793  ax-addcl 10794  ax-addrcl 10795  ax-mulcl 10796  ax-mulrcl 10797  ax-mulcom 10798  ax-addass 10799  ax-mulass 10800  ax-distr 10801  ax-i2m1 10802  ax-1ne0 10803  ax-1rid 10804  ax-rnegex 10805  ax-rrecex 10806  ax-cnre 10807  ax-pre-lttri 10808  ax-pre-lttrn 10809  ax-pre-ltadd 10810
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3415  df-sbc 3700  df-csb 3817  df-dif 3874  df-un 3876  df-in 3878  df-ss 3888  df-nul 4243  df-if 4445  df-pw 4520  df-sn 4547  df-pr 4549  df-op 4553  df-uni 4825  df-br 5059  df-opab 5121  df-mpt 5141  df-id 5460  df-po 5473  df-so 5474  df-xp 5562  df-rel 5563  df-cnv 5564  df-co 5565  df-dm 5566  df-rn 5567  df-res 5568  df-ima 5569  df-iota 6343  df-fun 6387  df-fn 6388  df-f 6389  df-f1 6390  df-fo 6391  df-f1o 6392  df-fv 6393  df-riota 7175  df-ov 7221  df-oprab 7222  df-mpo 7223  df-er 8396  df-en 8632  df-dom 8633  df-sdom 8634  df-pnf 10874  df-mnf 10875  df-xr 10876  df-ltxr 10877  df-le 10878  df-sub 11069  df-neg 11070  df-rp 12592
This theorem is referenced by:  stoweidlem52  43276
  Copyright terms: Public domain W3C validator