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

Theorem stoweidlem41 38934
 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 9918 . . . . . . . 8 1 ∈ ℝ
3 stoweidlem41.3 . . . . . . . . 9 𝐹 = (𝑡𝑇 ↦ 1)
43fvmpt2 6200 . . . . . . . 8 ((𝑡𝑇 ∧ 1 ∈ ℝ) → (𝐹𝑡) = 1)
52, 4mpan2 703 . . . . . . 7 (𝑡𝑇 → (𝐹𝑡) = 1)
65adantl 481 . . . . . 6 ((𝜑𝑡𝑇) → (𝐹𝑡) = 1)
76oveq1d 6564 . . . . 5 ((𝜑𝑡𝑇) → ((𝐹𝑡) − (𝑦𝑡)) = (1 − (𝑦𝑡)))
81, 7mpteq2da 4671 . . . 4 (𝜑 → (𝑡𝑇 ↦ ((𝐹𝑡) − (𝑦𝑡))) = (𝑡𝑇 ↦ (1 − (𝑦𝑡))))
9 stoweidlem41.2 . . . 4 𝑋 = (𝑡𝑇 ↦ (1 − (𝑦𝑡)))
108, 9syl6eqr 2662 . . 3 (𝜑 → (𝑡𝑇 ↦ ((𝐹𝑡) − (𝑦𝑡))) = 𝑋)
11 stoweidlem41.10 . . . . . . 7 ((𝜑𝑤 ∈ ℝ) → (𝑡𝑇𝑤) ∈ 𝐴)
1211stoweidlem4 38897 . . . . . 6 ((𝜑 ∧ 1 ∈ ℝ) → (𝑡𝑇 ↦ 1) ∈ 𝐴)
132, 12mpan2 703 . . . . 5 (𝜑 → (𝑡𝑇 ↦ 1) ∈ 𝐴)
143, 13syl5eqel 2692 . . . 4 (𝜑𝐹𝐴)
15 stoweidlem41.5 . . . 4 (𝜑𝑦𝐴)
16 nfmpt1 4675 . . . . . 6 𝑡(𝑡𝑇 ↦ 1)
173, 16nfcxfr 2749 . . . . 5 𝑡𝐹
18 nfcv 2751 . . . . 5 𝑡𝑦
19 stoweidlem41.7 . . . . 5 ((𝜑𝑓𝐴) → 𝑓:𝑇⟶ℝ)
20 stoweidlem41.8 . . . . 5 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) + (𝑔𝑡))) ∈ 𝐴)
21 stoweidlem41.9 . . . . 5 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
2217, 18, 1, 19, 20, 21, 11stoweidlem33 38926 . . . 4 ((𝜑𝐹𝐴𝑦𝐴) → (𝑡𝑇 ↦ ((𝐹𝑡) − (𝑦𝑡))) ∈ 𝐴)
2314, 15, 22mpd3an23 1418 . . 3 (𝜑 → (𝑡𝑇 ↦ ((𝐹𝑡) − (𝑦𝑡))) ∈ 𝐴)
2410, 23eqeltrrd 2689 . 2 (𝜑𝑋𝐴)
25 stoweidlem41.6 . . . . . . . 8 (𝜑𝑦:𝑇⟶ℝ)
2625fnvinran 38196 . . . . . . 7 ((𝜑𝑡𝑇) → (𝑦𝑡) ∈ ℝ)
27 1red 9934 . . . . . . 7 ((𝜑𝑡𝑇) → 1 ∈ ℝ)
28 0red 9920 . . . . . . 7 ((𝜑𝑡𝑇) → 0 ∈ ℝ)
29 stoweidlem41.12 . . . . . . . . . 10 (𝜑 → ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1))
3029r19.21bi 2916 . . . . . . . . 9 ((𝜑𝑡𝑇) → (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1))
3130simprd 478 . . . . . . . 8 ((𝜑𝑡𝑇) → (𝑦𝑡) ≤ 1)
32 1m0e1 11008 . . . . . . . 8 (1 − 0) = 1
3331, 32syl6breqr 4625 . . . . . . 7 ((𝜑𝑡𝑇) → (𝑦𝑡) ≤ (1 − 0))
3426, 27, 28, 33lesubd 10510 . . . . . 6 ((𝜑𝑡𝑇) → 0 ≤ (1 − (𝑦𝑡)))
35 simpr 476 . . . . . . 7 ((𝜑𝑡𝑇) → 𝑡𝑇)
3627, 26resubcld 10337 . . . . . . 7 ((𝜑𝑡𝑇) → (1 − (𝑦𝑡)) ∈ ℝ)
379fvmpt2 6200 . . . . . . 7 ((𝑡𝑇 ∧ (1 − (𝑦𝑡)) ∈ ℝ) → (𝑋𝑡) = (1 − (𝑦𝑡)))
3835, 36, 37syl2anc 691 . . . . . 6 ((𝜑𝑡𝑇) → (𝑋𝑡) = (1 − (𝑦𝑡)))
3934, 38breqtrrd 4611 . . . . 5 ((𝜑𝑡𝑇) → 0 ≤ (𝑋𝑡))
4030simpld 474 . . . . . . . 8 ((𝜑𝑡𝑇) → 0 ≤ (𝑦𝑡))
4128, 26, 27, 40lesub2dd 10523 . . . . . . 7 ((𝜑𝑡𝑇) → (1 − (𝑦𝑡)) ≤ (1 − 0))
4241, 32syl6breq 4624 . . . . . 6 ((𝜑𝑡𝑇) → (1 − (𝑦𝑡)) ≤ 1)
4338, 42eqbrtrd 4605 . . . . 5 ((𝜑𝑡𝑇) → (𝑋𝑡) ≤ 1)
4439, 43jca 553 . . . 4 ((𝜑𝑡𝑇) → (0 ≤ (𝑋𝑡) ∧ (𝑋𝑡) ≤ 1))
4544ex 449 . . 3 (𝜑 → (𝑡𝑇 → (0 ≤ (𝑋𝑡) ∧ (𝑋𝑡) ≤ 1)))
461, 45ralrimi 2940 . 2 (𝜑 → ∀𝑡𝑇 (0 ≤ (𝑋𝑡) ∧ (𝑋𝑡) ≤ 1))
47 stoweidlem41.4 . . . . . . 7 𝑉𝑇
4847sseli 3564 . . . . . 6 (𝑡𝑉𝑡𝑇)
4948, 38sylan2 490 . . . . 5 ((𝜑𝑡𝑉) → (𝑋𝑡) = (1 − (𝑦𝑡)))
50 1red 9934 . . . . . 6 ((𝜑𝑡𝑉) → 1 ∈ ℝ)
51 stoweidlem41.11 . . . . . . . 8 (𝜑𝐸 ∈ ℝ+)
5251rpred 11748 . . . . . . 7 (𝜑𝐸 ∈ ℝ)
5352adantr 480 . . . . . 6 ((𝜑𝑡𝑉) → 𝐸 ∈ ℝ)
5448, 26sylan2 490 . . . . . 6 ((𝜑𝑡𝑉) → (𝑦𝑡) ∈ ℝ)
55 stoweidlem41.13 . . . . . . 7 (𝜑 → ∀𝑡𝑉 (1 − 𝐸) < (𝑦𝑡))
5655r19.21bi 2916 . . . . . 6 ((𝜑𝑡𝑉) → (1 − 𝐸) < (𝑦𝑡))
5750, 53, 54, 56ltsub23d 10511 . . . . 5 ((𝜑𝑡𝑉) → (1 − (𝑦𝑡)) < 𝐸)
5849, 57eqbrtrd 4605 . . . 4 ((𝜑𝑡𝑉) → (𝑋𝑡) < 𝐸)
5958ex 449 . . 3 (𝜑 → (𝑡𝑉 → (𝑋𝑡) < 𝐸))
601, 59ralrimi 2940 . 2 (𝜑 → ∀𝑡𝑉 (𝑋𝑡) < 𝐸)
61 eldifi 3694 . . . . . . 7 (𝑡 ∈ (𝑇𝑈) → 𝑡𝑇)
6261, 26sylan2 490 . . . . . 6 ((𝜑𝑡 ∈ (𝑇𝑈)) → (𝑦𝑡) ∈ ℝ)
6352adantr 480 . . . . . 6 ((𝜑𝑡 ∈ (𝑇𝑈)) → 𝐸 ∈ ℝ)
64 1red 9934 . . . . . 6 ((𝜑𝑡 ∈ (𝑇𝑈)) → 1 ∈ ℝ)
65 stoweidlem41.14 . . . . . . 7 (𝜑 → ∀𝑡 ∈ (𝑇𝑈)(𝑦𝑡) < 𝐸)
6665r19.21bi 2916 . . . . . 6 ((𝜑𝑡 ∈ (𝑇𝑈)) → (𝑦𝑡) < 𝐸)
6762, 63, 64, 66ltsub2dd 10519 . . . . 5 ((𝜑𝑡 ∈ (𝑇𝑈)) → (1 − 𝐸) < (1 − (𝑦𝑡)))
6861, 38sylan2 490 . . . . 5 ((𝜑𝑡 ∈ (𝑇𝑈)) → (𝑋𝑡) = (1 − (𝑦𝑡)))
6967, 68breqtrrd 4611 . . . 4 ((𝜑𝑡 ∈ (𝑇𝑈)) → (1 − 𝐸) < (𝑋𝑡))
7069ex 449 . . 3 (𝜑 → (𝑡 ∈ (𝑇𝑈) → (1 − 𝐸) < (𝑋𝑡)))
711, 70ralrimi 2940 . 2 (𝜑 → ∀𝑡 ∈ (𝑇𝑈)(1 − 𝐸) < (𝑋𝑡))
72 nfmpt1 4675 . . . . . . 7 𝑡(𝑡𝑇 ↦ (1 − (𝑦𝑡)))
739, 72nfcxfr 2749 . . . . . 6 𝑡𝑋
7473nfeq2 2766 . . . . 5 𝑡 𝑥 = 𝑋
75 fveq1 6102 . . . . . . 7 (𝑥 = 𝑋 → (𝑥𝑡) = (𝑋𝑡))
7675breq2d 4595 . . . . . 6 (𝑥 = 𝑋 → (0 ≤ (𝑥𝑡) ↔ 0 ≤ (𝑋𝑡)))
7775breq1d 4593 . . . . . 6 (𝑥 = 𝑋 → ((𝑥𝑡) ≤ 1 ↔ (𝑋𝑡) ≤ 1))
7876, 77anbi12d 743 . . . . 5 (𝑥 = 𝑋 → ((0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ↔ (0 ≤ (𝑋𝑡) ∧ (𝑋𝑡) ≤ 1)))
7974, 78ralbid 2966 . . . 4 (𝑥 = 𝑋 → (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ (𝑋𝑡) ∧ (𝑋𝑡) ≤ 1)))
8075breq1d 4593 . . . . 5 (𝑥 = 𝑋 → ((𝑥𝑡) < 𝐸 ↔ (𝑋𝑡) < 𝐸))
8174, 80ralbid 2966 . . . 4 (𝑥 = 𝑋 → (∀𝑡𝑉 (𝑥𝑡) < 𝐸 ↔ ∀𝑡𝑉 (𝑋𝑡) < 𝐸))
8275breq2d 4595 . . . . 5 (𝑥 = 𝑋 → ((1 − 𝐸) < (𝑥𝑡) ↔ (1 − 𝐸) < (𝑋𝑡)))
8374, 82ralbid 2966 . . . 4 (𝑥 = 𝑋 → (∀𝑡 ∈ (𝑇𝑈)(1 − 𝐸) < (𝑥𝑡) ↔ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝐸) < (𝑋𝑡)))
8479, 81, 833anbi123d 1391 . . 3 (𝑥 = 𝑋 → ((∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡𝑉 (𝑥𝑡) < 𝐸 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝐸) < (𝑥𝑡)) ↔ (∀𝑡𝑇 (0 ≤ (𝑋𝑡) ∧ (𝑋𝑡) ≤ 1) ∧ ∀𝑡𝑉 (𝑋𝑡) < 𝐸 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝐸) < (𝑋𝑡))))
8584rspcev 3282 . 2 ((𝑋𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑋𝑡) ∧ (𝑋𝑡) ≤ 1) ∧ ∀𝑡𝑉 (𝑋𝑡) < 𝐸 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝐸) < (𝑋𝑡))) → ∃𝑥𝐴 (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡𝑉 (𝑥𝑡) < 𝐸 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝐸) < (𝑥𝑡)))
8624, 46, 60, 71, 85syl13anc 1320 1 (𝜑 → ∃𝑥𝐴 (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡𝑉 (𝑥𝑡) < 𝐸 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝐸) < (𝑥𝑡)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475  Ⅎwnf 1699   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897   ∖ cdif 3537   ⊆ wss 3540   class class class wbr 4583   ↦ cmpt 4643  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820   < clt 9953   ≤ cle 9954   − cmin 10145  ℝ+crp 11708 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-po 4959  df-so 4960  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-rp 11709 This theorem is referenced by:  stoweidlem52  38945
 Copyright terms: Public domain W3C validator