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

Theorem stoweidlem51 38944
 Description: There exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91. Here 𝐷 is used to represent 𝐴 in the paper, because here 𝐴 is used for the subalgebra of functions. 𝐸 is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem51.1 𝑖𝜑
stoweidlem51.2 𝑡𝜑
stoweidlem51.3 𝑤𝜑
stoweidlem51.4 𝑤𝑉
stoweidlem51.5 𝑌 = {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)}
stoweidlem51.6 𝑃 = (𝑓𝑌, 𝑔𝑌 ↦ (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))))
stoweidlem51.7 𝑋 = (seq1(𝑃, 𝑈)‘𝑀)
stoweidlem51.8 𝐹 = (𝑡𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
stoweidlem51.9 𝑍 = (𝑡𝑇 ↦ (seq1( · , (𝐹𝑡))‘𝑀))
stoweidlem51.10 (𝜑𝑀 ∈ ℕ)
stoweidlem51.11 (𝜑𝑊:(1...𝑀)⟶𝑉)
stoweidlem51.12 (𝜑𝑈:(1...𝑀)⟶𝑌)
stoweidlem51.13 ((𝜑𝑤𝑉) → 𝑤𝑇)
stoweidlem51.14 (𝜑𝐷 ran 𝑊)
stoweidlem51.15 (𝜑𝐷𝑇)
stoweidlem51.16 (𝜑𝐵𝑇)
stoweidlem51.17 ((𝜑𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ (𝑊𝑖)((𝑈𝑖)‘𝑡) < (𝐸 / 𝑀))
stoweidlem51.18 ((𝜑𝑖 ∈ (1...𝑀)) → ∀𝑡𝐵 (1 − (𝐸 / 𝑀)) < ((𝑈𝑖)‘𝑡))
stoweidlem51.19 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
stoweidlem51.20 ((𝜑𝑓𝐴) → 𝑓:𝑇⟶ℝ)
stoweidlem51.21 (𝜑𝑇 ∈ V)
stoweidlem51.22 (𝜑𝐸 ∈ ℝ+)
stoweidlem51.23 (𝜑𝐸 < (1 / 3))
Assertion
Ref Expression
stoweidlem51 (𝜑 → ∃𝑥(𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡𝐷 (𝑥𝑡) < 𝐸 ∧ ∀𝑡𝐵 (1 − 𝐸) < (𝑥𝑡))))
Distinct variable groups:   𝑓,𝑔,,𝑡,𝐴   𝑓,𝑖,𝑀,,𝑡   𝑓,𝐹,𝑔   𝑇,𝑓,𝑔,,𝑡   𝑈,𝑓,𝑔,,𝑡   𝑓,𝑌,𝑔   𝜑,𝑓,𝑔   𝑔,𝑀   𝑤,𝑖,𝑇   𝐵,𝑖   𝐷,𝑖   𝑖,𝐸   𝑈,𝑖   𝑖,𝑊,𝑤   𝑥,𝑡,𝐴   𝑥,𝐵   𝑥,𝐷   𝑥,𝐸   𝑥,𝑇   𝑥,𝑋
Allowed substitution hints:   𝜑(𝑥,𝑤,𝑡,,𝑖)   𝐴(𝑤,𝑖)   𝐵(𝑤,𝑡,𝑓,𝑔,)   𝐷(𝑤,𝑡,𝑓,𝑔,)   𝑃(𝑥,𝑤,𝑡,𝑓,𝑔,,𝑖)   𝑈(𝑥,𝑤)   𝐸(𝑤,𝑡,𝑓,𝑔,)   𝐹(𝑥,𝑤,𝑡,,𝑖)   𝑀(𝑥,𝑤)   𝑉(𝑥,𝑤,𝑡,𝑓,𝑔,,𝑖)   𝑊(𝑥,𝑡,𝑓,𝑔,)   𝑋(𝑤,𝑡,𝑓,𝑔,,𝑖)   𝑌(𝑥,𝑤,𝑡,,𝑖)   𝑍(𝑥,𝑤,𝑡,𝑓,𝑔,,𝑖)

Proof of Theorem stoweidlem51
StepHypRef Expression
1 stoweidlem51.5 . . . 4 𝑌 = {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)}
2 ssrab2 3650 . . . 4 {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)} ⊆ 𝐴
31, 2eqsstri 3598 . . 3 𝑌𝐴
4 stoweidlem51.6 . . . 4 𝑃 = (𝑓𝑌, 𝑔𝑌 ↦ (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))))
5 stoweidlem51.7 . . . 4 𝑋 = (seq1(𝑃, 𝑈)‘𝑀)
6 1zzd 11285 . . . . . 6 (𝜑 → 1 ∈ ℤ)
7 stoweidlem51.10 . . . . . . 7 (𝜑𝑀 ∈ ℕ)
87nnzd 11357 . . . . . 6 (𝜑𝑀 ∈ ℤ)
96, 8, 83jca 1235 . . . . 5 (𝜑 → (1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑀 ∈ ℤ))
107nnge1d 10940 . . . . . 6 (𝜑 → 1 ≤ 𝑀)
117nnred 10912 . . . . . . 7 (𝜑𝑀 ∈ ℝ)
1211leidd 10473 . . . . . 6 (𝜑𝑀𝑀)
1310, 12jca 553 . . . . 5 (𝜑 → (1 ≤ 𝑀𝑀𝑀))
14 elfz2 12204 . . . . 5 (𝑀 ∈ (1...𝑀) ↔ ((1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (1 ≤ 𝑀𝑀𝑀)))
159, 13, 14sylanbrc 695 . . . 4 (𝜑𝑀 ∈ (1...𝑀))
16 stoweidlem51.12 . . . 4 (𝜑𝑈:(1...𝑀)⟶𝑌)
17 stoweidlem51.2 . . . . 5 𝑡𝜑
18 eqid 2610 . . . . 5 (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) = (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡)))
19 stoweidlem51.20 . . . . 5 ((𝜑𝑓𝐴) → 𝑓:𝑇⟶ℝ)
20 stoweidlem51.19 . . . . 5 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
2117, 1, 18, 19, 20stoweidlem16 38909 . . . 4 ((𝜑𝑓𝑌𝑔𝑌) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝑌)
22 stoweidlem51.21 . . . 4 (𝜑𝑇 ∈ V)
234, 5, 15, 16, 21, 22fmulcl 38648 . . 3 (𝜑𝑋𝑌)
243, 23sseldi 3566 . 2 (𝜑𝑋𝐴)
251eleq2i 2680 . . . . . . 7 (𝑋𝑌𝑋 ∈ {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)})
26 nfcv 2751 . . . . . . . . . . 11 1
27 nfrab1 3099 . . . . . . . . . . . . . 14 {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)}
281, 27nfcxfr 2749 . . . . . . . . . . . . 13 𝑌
29 nfcv 2751 . . . . . . . . . . . . 13 (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡)))
3028, 28, 29nfmpt2 6622 . . . . . . . . . . . 12 (𝑓𝑌, 𝑔𝑌 ↦ (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))))
314, 30nfcxfr 2749 . . . . . . . . . . 11 𝑃
32 nfcv 2751 . . . . . . . . . . 11 𝑈
3326, 31, 32nfseq 12673 . . . . . . . . . 10 seq1(𝑃, 𝑈)
34 nfcv 2751 . . . . . . . . . 10 𝑀
3533, 34nffv 6110 . . . . . . . . 9 (seq1(𝑃, 𝑈)‘𝑀)
365, 35nfcxfr 2749 . . . . . . . 8 𝑋
37 nfcv 2751 . . . . . . . 8 𝐴
38 nfcv 2751 . . . . . . . . 9 𝑇
39 nfcv 2751 . . . . . . . . . . 11 0
40 nfcv 2751 . . . . . . . . . . 11
41 nfcv 2751 . . . . . . . . . . . 12 𝑡
4236, 41nffv 6110 . . . . . . . . . . 11 (𝑋𝑡)
4339, 40, 42nfbr 4629 . . . . . . . . . 10 0 ≤ (𝑋𝑡)
4442, 40, 26nfbr 4629 . . . . . . . . . 10 (𝑋𝑡) ≤ 1
4543, 44nfan 1816 . . . . . . . . 9 (0 ≤ (𝑋𝑡) ∧ (𝑋𝑡) ≤ 1)
4638, 45nfral 2929 . . . . . . . 8 𝑡𝑇 (0 ≤ (𝑋𝑡) ∧ (𝑋𝑡) ≤ 1)
47 nfcv 2751 . . . . . . . . . . . . 13 𝑡1
48 nfra1 2925 . . . . . . . . . . . . . . . . 17 𝑡𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)
49 nfcv 2751 . . . . . . . . . . . . . . . . 17 𝑡𝐴
5048, 49nfrab 3100 . . . . . . . . . . . . . . . 16 𝑡{𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)}
511, 50nfcxfr 2749 . . . . . . . . . . . . . . 15 𝑡𝑌
52 nfmpt1 4675 . . . . . . . . . . . . . . 15 𝑡(𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡)))
5351, 51, 52nfmpt2 6622 . . . . . . . . . . . . . 14 𝑡(𝑓𝑌, 𝑔𝑌 ↦ (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))))
544, 53nfcxfr 2749 . . . . . . . . . . . . 13 𝑡𝑃
55 nfcv 2751 . . . . . . . . . . . . 13 𝑡𝑈
5647, 54, 55nfseq 12673 . . . . . . . . . . . 12 𝑡seq1(𝑃, 𝑈)
57 nfcv 2751 . . . . . . . . . . . 12 𝑡𝑀
5856, 57nffv 6110 . . . . . . . . . . 11 𝑡(seq1(𝑃, 𝑈)‘𝑀)
595, 58nfcxfr 2749 . . . . . . . . . 10 𝑡𝑋
6059nfeq2 2766 . . . . . . . . 9 𝑡 = 𝑋
61 fveq1 6102 . . . . . . . . . . 11 ( = 𝑋 → (𝑡) = (𝑋𝑡))
6261breq2d 4595 . . . . . . . . . 10 ( = 𝑋 → (0 ≤ (𝑡) ↔ 0 ≤ (𝑋𝑡)))
6361breq1d 4593 . . . . . . . . . 10 ( = 𝑋 → ((𝑡) ≤ 1 ↔ (𝑋𝑡) ≤ 1))
6462, 63anbi12d 743 . . . . . . . . 9 ( = 𝑋 → ((0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ↔ (0 ≤ (𝑋𝑡) ∧ (𝑋𝑡) ≤ 1)))
6560, 64ralbid 2966 . . . . . . . 8 ( = 𝑋 → (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ (𝑋𝑡) ∧ (𝑋𝑡) ≤ 1)))
6636, 37, 46, 65elrabf 3329 . . . . . . 7 (𝑋 ∈ {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)} ↔ (𝑋𝐴 ∧ ∀𝑡𝑇 (0 ≤ (𝑋𝑡) ∧ (𝑋𝑡) ≤ 1)))
6725, 66bitri 263 . . . . . 6 (𝑋𝑌 ↔ (𝑋𝐴 ∧ ∀𝑡𝑇 (0 ≤ (𝑋𝑡) ∧ (𝑋𝑡) ≤ 1)))
6823, 67sylib 207 . . . . 5 (𝜑 → (𝑋𝐴 ∧ ∀𝑡𝑇 (0 ≤ (𝑋𝑡) ∧ (𝑋𝑡) ≤ 1)))
6968simprd 478 . . . 4 (𝜑 → ∀𝑡𝑇 (0 ≤ (𝑋𝑡) ∧ (𝑋𝑡) ≤ 1))
70 stoweidlem51.1 . . . . 5 𝑖𝜑
71 stoweidlem51.8 . . . . 5 𝐹 = (𝑡𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
72 stoweidlem51.9 . . . . 5 𝑍 = (𝑡𝑇 ↦ (seq1( · , (𝐹𝑡))‘𝑀))
73 stoweidlem51.11 . . . . 5 (𝜑𝑊:(1...𝑀)⟶𝑉)
74 stoweidlem51.14 . . . . 5 (𝜑𝐷 ran 𝑊)
75 stoweidlem51.15 . . . . 5 (𝜑𝐷𝑇)
76 nfv 1830 . . . . . . 7 𝑡 𝑖 ∈ (1...𝑀)
7717, 76nfan 1816 . . . . . 6 𝑡(𝜑𝑖 ∈ (1...𝑀))
7816fnvinran 38196 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑈𝑖) ∈ 𝑌)
79 fveq1 6102 . . . . . . . . . . . . . . . . 17 ( = (𝑈𝑖) → (𝑡) = ((𝑈𝑖)‘𝑡))
8079breq2d 4595 . . . . . . . . . . . . . . . 16 ( = (𝑈𝑖) → (0 ≤ (𝑡) ↔ 0 ≤ ((𝑈𝑖)‘𝑡)))
8179breq1d 4593 . . . . . . . . . . . . . . . 16 ( = (𝑈𝑖) → ((𝑡) ≤ 1 ↔ ((𝑈𝑖)‘𝑡) ≤ 1))
8280, 81anbi12d 743 . . . . . . . . . . . . . . 15 ( = (𝑈𝑖) → ((0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ↔ (0 ≤ ((𝑈𝑖)‘𝑡) ∧ ((𝑈𝑖)‘𝑡) ≤ 1)))
8382ralbidv 2969 . . . . . . . . . . . . . 14 ( = (𝑈𝑖) → (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ ((𝑈𝑖)‘𝑡) ∧ ((𝑈𝑖)‘𝑡) ≤ 1)))
8483, 1elrab2 3333 . . . . . . . . . . . . 13 ((𝑈𝑖) ∈ 𝑌 ↔ ((𝑈𝑖) ∈ 𝐴 ∧ ∀𝑡𝑇 (0 ≤ ((𝑈𝑖)‘𝑡) ∧ ((𝑈𝑖)‘𝑡) ≤ 1)))
8584simplbi 475 . . . . . . . . . . . 12 ((𝑈𝑖) ∈ 𝑌 → (𝑈𝑖) ∈ 𝐴)
8678, 85syl 17 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑈𝑖) ∈ 𝐴)
87 eleq1 2676 . . . . . . . . . . . . . . 15 (𝑓 = (𝑈𝑖) → (𝑓𝐴 ↔ (𝑈𝑖) ∈ 𝐴))
8887anbi2d 736 . . . . . . . . . . . . . 14 (𝑓 = (𝑈𝑖) → ((𝜑𝑓𝐴) ↔ (𝜑 ∧ (𝑈𝑖) ∈ 𝐴)))
89 feq1 5939 . . . . . . . . . . . . . 14 (𝑓 = (𝑈𝑖) → (𝑓:𝑇⟶ℝ ↔ (𝑈𝑖):𝑇⟶ℝ))
9088, 89imbi12d 333 . . . . . . . . . . . . 13 (𝑓 = (𝑈𝑖) → (((𝜑𝑓𝐴) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ (𝑈𝑖) ∈ 𝐴) → (𝑈𝑖):𝑇⟶ℝ)))
9119a1i 11 . . . . . . . . . . . . 13 (𝑓𝐴 → ((𝜑𝑓𝐴) → 𝑓:𝑇⟶ℝ))
9290, 91vtoclga 3245 . . . . . . . . . . . 12 ((𝑈𝑖) ∈ 𝐴 → ((𝜑 ∧ (𝑈𝑖) ∈ 𝐴) → (𝑈𝑖):𝑇⟶ℝ))
9392anabsi7 856 . . . . . . . . . . 11 ((𝜑 ∧ (𝑈𝑖) ∈ 𝐴) → (𝑈𝑖):𝑇⟶ℝ)
9486, 93syldan 486 . . . . . . . . . 10 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑈𝑖):𝑇⟶ℝ)
9594adantr 480 . . . . . . . . 9 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊𝑖)) → (𝑈𝑖):𝑇⟶ℝ)
9673fnvinran 38196 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑊𝑖) ∈ 𝑉)
97 simpl 472 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → 𝜑)
9897, 96jca 553 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → (𝜑 ∧ (𝑊𝑖) ∈ 𝑉))
99 stoweidlem51.3 . . . . . . . . . . . . . 14 𝑤𝜑
100 stoweidlem51.4 . . . . . . . . . . . . . . 15 𝑤𝑉
101100nfel2 2767 . . . . . . . . . . . . . 14 𝑤(𝑊𝑖) ∈ 𝑉
10299, 101nfan 1816 . . . . . . . . . . . . 13 𝑤(𝜑 ∧ (𝑊𝑖) ∈ 𝑉)
103 nfv 1830 . . . . . . . . . . . . 13 𝑤(𝑊𝑖) ⊆ 𝑇
104102, 103nfim 1813 . . . . . . . . . . . 12 𝑤((𝜑 ∧ (𝑊𝑖) ∈ 𝑉) → (𝑊𝑖) ⊆ 𝑇)
105 eleq1 2676 . . . . . . . . . . . . . 14 (𝑤 = (𝑊𝑖) → (𝑤𝑉 ↔ (𝑊𝑖) ∈ 𝑉))
106105anbi2d 736 . . . . . . . . . . . . 13 (𝑤 = (𝑊𝑖) → ((𝜑𝑤𝑉) ↔ (𝜑 ∧ (𝑊𝑖) ∈ 𝑉)))
107 sseq1 3589 . . . . . . . . . . . . 13 (𝑤 = (𝑊𝑖) → (𝑤𝑇 ↔ (𝑊𝑖) ⊆ 𝑇))
108106, 107imbi12d 333 . . . . . . . . . . . 12 (𝑤 = (𝑊𝑖) → (((𝜑𝑤𝑉) → 𝑤𝑇) ↔ ((𝜑 ∧ (𝑊𝑖) ∈ 𝑉) → (𝑊𝑖) ⊆ 𝑇)))
109 stoweidlem51.13 . . . . . . . . . . . 12 ((𝜑𝑤𝑉) → 𝑤𝑇)
110104, 108, 109vtoclg1f 3238 . . . . . . . . . . 11 ((𝑊𝑖) ∈ 𝑉 → ((𝜑 ∧ (𝑊𝑖) ∈ 𝑉) → (𝑊𝑖) ⊆ 𝑇))
11196, 98, 110sylc 63 . . . . . . . . . 10 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑊𝑖) ⊆ 𝑇)
112111sselda 3568 . . . . . . . . 9 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊𝑖)) → 𝑡𝑇)
11395, 112ffvelrnd 6268 . . . . . . . 8 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊𝑖)) → ((𝑈𝑖)‘𝑡) ∈ ℝ)
114 stoweidlem51.22 . . . . . . . . . . 11 (𝜑𝐸 ∈ ℝ+)
115114rpred 11748 . . . . . . . . . 10 (𝜑𝐸 ∈ ℝ)
116115ad2antrr 758 . . . . . . . . 9 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊𝑖)) → 𝐸 ∈ ℝ)
11711ad2antrr 758 . . . . . . . . 9 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊𝑖)) → 𝑀 ∈ ℝ)
1187nnne0d 10942 . . . . . . . . . 10 (𝜑𝑀 ≠ 0)
119118ad2antrr 758 . . . . . . . . 9 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊𝑖)) → 𝑀 ≠ 0)
120116, 117, 119redivcld 10732 . . . . . . . 8 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊𝑖)) → (𝐸 / 𝑀) ∈ ℝ)
121 stoweidlem51.17 . . . . . . . . 9 ((𝜑𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ (𝑊𝑖)((𝑈𝑖)‘𝑡) < (𝐸 / 𝑀))
122121r19.21bi 2916 . . . . . . . 8 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊𝑖)) → ((𝑈𝑖)‘𝑡) < (𝐸 / 𝑀))
123 1red 9934 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℝ)
124 0lt1 10429 . . . . . . . . . . . . 13 0 < 1
125124a1i 11 . . . . . . . . . . . 12 (𝜑 → 0 < 1)
1267nngt0d 10941 . . . . . . . . . . . 12 (𝜑 → 0 < 𝑀)
127114rpregt0d 11754 . . . . . . . . . . . 12 (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
128 lediv2 10792 . . . . . . . . . . . 12 (((1 ∈ ℝ ∧ 0 < 1) ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀) ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (1 ≤ 𝑀 ↔ (𝐸 / 𝑀) ≤ (𝐸 / 1)))
129123, 125, 11, 126, 127, 128syl221anc 1329 . . . . . . . . . . 11 (𝜑 → (1 ≤ 𝑀 ↔ (𝐸 / 𝑀) ≤ (𝐸 / 1)))
13010, 129mpbid 221 . . . . . . . . . 10 (𝜑 → (𝐸 / 𝑀) ≤ (𝐸 / 1))
131114rpcnd 11750 . . . . . . . . . . 11 (𝜑𝐸 ∈ ℂ)
132131div1d 10672 . . . . . . . . . 10 (𝜑 → (𝐸 / 1) = 𝐸)
133130, 132breqtrd 4609 . . . . . . . . 9 (𝜑 → (𝐸 / 𝑀) ≤ 𝐸)
134133ad2antrr 758 . . . . . . . 8 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊𝑖)) → (𝐸 / 𝑀) ≤ 𝐸)
135113, 120, 116, 122, 134ltletrd 10076 . . . . . . 7 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ (𝑊𝑖)) → ((𝑈𝑖)‘𝑡) < 𝐸)
136135ex 449 . . . . . 6 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑡 ∈ (𝑊𝑖) → ((𝑈𝑖)‘𝑡) < 𝐸))
13777, 136ralrimi 2940 . . . . 5 ((𝜑𝑖 ∈ (1...𝑀)) → ∀𝑡 ∈ (𝑊𝑖)((𝑈𝑖)‘𝑡) < 𝐸)
13870, 17, 1, 4, 5, 71, 72, 7, 73, 16, 74, 75, 137, 22, 19, 20, 114stoweidlem48 38941 . . . 4 (𝜑 → ∀𝑡𝐷 (𝑋𝑡) < 𝐸)
139 stoweidlem51.18 . . . . 5 ((𝜑𝑖 ∈ (1...𝑀)) → ∀𝑡𝐵 (1 − (𝐸 / 𝑀)) < ((𝑈𝑖)‘𝑡))
140 stoweidlem51.23 . . . . 5 (𝜑𝐸 < (1 / 3))
1413sseli 3564 . . . . . 6 (𝑓𝑌𝑓𝐴)
142141, 19sylan2 490 . . . . 5 ((𝜑𝑓𝑌) → 𝑓:𝑇⟶ℝ)
143 stoweidlem51.16 . . . . 5 (𝜑𝐵𝑇)
14470, 17, 51, 4, 5, 71, 72, 7, 16, 139, 114, 140, 142, 21, 22, 143stoweidlem42 38935 . . . 4 (𝜑 → ∀𝑡𝐵 (1 − 𝐸) < (𝑋𝑡))
14569, 138, 1443jca 1235 . . 3 (𝜑 → (∀𝑡𝑇 (0 ≤ (𝑋𝑡) ∧ (𝑋𝑡) ≤ 1) ∧ ∀𝑡𝐷 (𝑋𝑡) < 𝐸 ∧ ∀𝑡𝐵 (1 − 𝐸) < (𝑋𝑡)))
14624, 145jca 553 . 2 (𝜑 → (𝑋𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑋𝑡) ∧ (𝑋𝑡) ≤ 1) ∧ ∀𝑡𝐷 (𝑋𝑡) < 𝐸 ∧ ∀𝑡𝐵 (1 − 𝐸) < (𝑋𝑡))))
147 eleq1 2676 . . . 4 (𝑥 = 𝑋 → (𝑥𝐴𝑋𝐴))
14859nfeq2 2766 . . . . . 6 𝑡 𝑥 = 𝑋
149 fveq1 6102 . . . . . . . 8 (𝑥 = 𝑋 → (𝑥𝑡) = (𝑋𝑡))
150149breq2d 4595 . . . . . . 7 (𝑥 = 𝑋 → (0 ≤ (𝑥𝑡) ↔ 0 ≤ (𝑋𝑡)))
151149breq1d 4593 . . . . . . 7 (𝑥 = 𝑋 → ((𝑥𝑡) ≤ 1 ↔ (𝑋𝑡) ≤ 1))
152150, 151anbi12d 743 . . . . . 6 (𝑥 = 𝑋 → ((0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ↔ (0 ≤ (𝑋𝑡) ∧ (𝑋𝑡) ≤ 1)))
153148, 152ralbid 2966 . . . . 5 (𝑥 = 𝑋 → (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ (𝑋𝑡) ∧ (𝑋𝑡) ≤ 1)))
154149breq1d 4593 . . . . . 6 (𝑥 = 𝑋 → ((𝑥𝑡) < 𝐸 ↔ (𝑋𝑡) < 𝐸))
155148, 154ralbid 2966 . . . . 5 (𝑥 = 𝑋 → (∀𝑡𝐷 (𝑥𝑡) < 𝐸 ↔ ∀𝑡𝐷 (𝑋𝑡) < 𝐸))
156149breq2d 4595 . . . . . 6 (𝑥 = 𝑋 → ((1 − 𝐸) < (𝑥𝑡) ↔ (1 − 𝐸) < (𝑋𝑡)))
157148, 156ralbid 2966 . . . . 5 (𝑥 = 𝑋 → (∀𝑡𝐵 (1 − 𝐸) < (𝑥𝑡) ↔ ∀𝑡𝐵 (1 − 𝐸) < (𝑋𝑡)))
158153, 155, 1573anbi123d 1391 . . . 4 (𝑥 = 𝑋 → ((∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡𝐷 (𝑥𝑡) < 𝐸 ∧ ∀𝑡𝐵 (1 − 𝐸) < (𝑥𝑡)) ↔ (∀𝑡𝑇 (0 ≤ (𝑋𝑡) ∧ (𝑋𝑡) ≤ 1) ∧ ∀𝑡𝐷 (𝑋𝑡) < 𝐸 ∧ ∀𝑡𝐵 (1 − 𝐸) < (𝑋𝑡))))
159147, 158anbi12d 743 . . 3 (𝑥 = 𝑋 → ((𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡𝐷 (𝑥𝑡) < 𝐸 ∧ ∀𝑡𝐵 (1 − 𝐸) < (𝑥𝑡))) ↔ (𝑋𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑋𝑡) ∧ (𝑋𝑡) ≤ 1) ∧ ∀𝑡𝐷 (𝑋𝑡) < 𝐸 ∧ ∀𝑡𝐵 (1 − 𝐸) < (𝑋𝑡)))))
160159spcegv 3267 . 2 (𝑋𝐴 → ((𝑋𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑋𝑡) ∧ (𝑋𝑡) ≤ 1) ∧ ∀𝑡𝐷 (𝑋𝑡) < 𝐸 ∧ ∀𝑡𝐵 (1 − 𝐸) < (𝑋𝑡))) → ∃𝑥(𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡𝐷 (𝑥𝑡) < 𝐸 ∧ ∀𝑡𝐵 (1 − 𝐸) < (𝑥𝑡)))))
16124, 146, 160sylc 63 1 (𝜑 → ∃𝑥(𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡𝐷 (𝑥𝑡) < 𝐸 ∧ ∀𝑡𝐵 (1 − 𝐸) < (𝑥𝑡))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695  Ⅎwnf 1699   ∈ wcel 1977  Ⅎwnfc 2738   ≠ wne 2780  ∀wral 2896  {crab 2900  Vcvv 3173   ⊆ wss 3540  ∪ cuni 4372   class class class wbr 4583   ↦ cmpt 4643  ran crn 5039  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  ℝcr 9814  0cc0 9815  1c1 9816   · cmul 9820   < clt 9953   ≤ cle 9954   − cmin 10145   / cdiv 10563  ℕcn 10897  3c3 10948  ℤcz 11254  ℝ+crp 11708  ...cfz 12197  seqcseq 12663 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-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  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  ax-pre-mulgt0 9892 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-rmo 2904  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-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  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-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  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-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  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-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-rp 11709  df-fz 12198  df-fzo 12335  df-seq 12664  df-exp 12723 This theorem is referenced by:  stoweidlem54  38947
 Copyright terms: Public domain W3C validator