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

Theorem stoweidlem42 42681
Description: This lemma is used to prove that 𝑥 built as in Lemma 2 of [BrosowskiDeutsh] p. 91, is such that x > 1 - ε on B. Here 𝑋 is used to represent 𝑥 in the paper, and E is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem42.1 𝑖𝜑
stoweidlem42.2 𝑡𝜑
stoweidlem42.3 𝑡𝑌
stoweidlem42.4 𝑃 = (𝑓𝑌, 𝑔𝑌 ↦ (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))))
stoweidlem42.5 𝑋 = (seq1(𝑃, 𝑈)‘𝑀)
stoweidlem42.6 𝐹 = (𝑡𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
stoweidlem42.7 𝑍 = (𝑡𝑇 ↦ (seq1( · , (𝐹𝑡))‘𝑀))
stoweidlem42.8 (𝜑𝑀 ∈ ℕ)
stoweidlem42.9 (𝜑𝑈:(1...𝑀)⟶𝑌)
stoweidlem42.10 ((𝜑𝑖 ∈ (1...𝑀)) → ∀𝑡𝐵 (1 − (𝐸 / 𝑀)) < ((𝑈𝑖)‘𝑡))
stoweidlem42.11 (𝜑𝐸 ∈ ℝ+)
stoweidlem42.12 (𝜑𝐸 < (1 / 3))
stoweidlem42.13 ((𝜑𝑓𝑌) → 𝑓:𝑇⟶ℝ)
stoweidlem42.14 ((𝜑𝑓𝑌𝑔𝑌) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝑌)
stoweidlem42.15 (𝜑𝑇 ∈ V)
stoweidlem42.16 (𝜑𝐵𝑇)
Assertion
Ref Expression
stoweidlem42 (𝜑 → ∀𝑡𝐵 (1 − 𝐸) < (𝑋𝑡))
Distinct variable groups:   𝑡,𝑖   𝐵,𝑖   𝑖,𝑀   𝑓,𝑔,𝑡,𝑇   𝑓,𝑖,𝑇   𝑓,𝐹,𝑔   𝑓,𝑀,𝑔   𝑈,𝑓,𝑔,𝑡   𝑓,𝑌,𝑔   𝜑,𝑓,𝑔   𝑖,𝐸   𝑈,𝑖
Allowed substitution hints:   𝜑(𝑡,𝑖)   𝐵(𝑡,𝑓,𝑔)   𝑃(𝑡,𝑓,𝑔,𝑖)   𝐸(𝑡,𝑓,𝑔)   𝐹(𝑡,𝑖)   𝑀(𝑡)   𝑋(𝑡,𝑓,𝑔,𝑖)   𝑌(𝑡,𝑖)   𝑍(𝑡,𝑓,𝑔,𝑖)

Proof of Theorem stoweidlem42
Dummy variables 𝑎 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 stoweidlem42.2 . 2 𝑡𝜑
2 1red 10635 . . . . . . . 8 (𝜑 → 1 ∈ ℝ)
3 stoweidlem42.11 . . . . . . . . 9 (𝜑𝐸 ∈ ℝ+)
43rpred 12423 . . . . . . . 8 (𝜑𝐸 ∈ ℝ)
52, 4resubcld 11061 . . . . . . 7 (𝜑 → (1 − 𝐸) ∈ ℝ)
65adantr 484 . . . . . 6 ((𝜑𝑡𝐵) → (1 − 𝐸) ∈ ℝ)
7 stoweidlem42.8 . . . . . . . . . 10 (𝜑𝑀 ∈ ℕ)
84, 7nndivred 11683 . . . . . . . . 9 (𝜑 → (𝐸 / 𝑀) ∈ ℝ)
92, 8resubcld 11061 . . . . . . . 8 (𝜑 → (1 − (𝐸 / 𝑀)) ∈ ℝ)
109adantr 484 . . . . . . 7 ((𝜑𝑡𝐵) → (1 − (𝐸 / 𝑀)) ∈ ℝ)
117nnnn0d 11947 . . . . . . . 8 (𝜑𝑀 ∈ ℕ0)
1211adantr 484 . . . . . . 7 ((𝜑𝑡𝐵) → 𝑀 ∈ ℕ0)
1310, 12reexpcld 13527 . . . . . 6 ((𝜑𝑡𝐵) → ((1 − (𝐸 / 𝑀))↑𝑀) ∈ ℝ)
14 elnnuz 12274 . . . . . . . . 9 (𝑀 ∈ ℕ ↔ 𝑀 ∈ (ℤ‘1))
157, 14sylib 221 . . . . . . . 8 (𝜑𝑀 ∈ (ℤ‘1))
1615adantr 484 . . . . . . 7 ((𝜑𝑡𝐵) → 𝑀 ∈ (ℤ‘1))
17 stoweidlem42.1 . . . . . . . . . . 11 𝑖𝜑
18 nfv 1915 . . . . . . . . . . 11 𝑖 𝑡𝐵
1917, 18nfan 1900 . . . . . . . . . 10 𝑖(𝜑𝑡𝐵)
20 nfv 1915 . . . . . . . . . 10 𝑖 𝑎 ∈ (1...𝑀)
2119, 20nfan 1900 . . . . . . . . 9 𝑖((𝜑𝑡𝐵) ∧ 𝑎 ∈ (1...𝑀))
22 stoweidlem42.6 . . . . . . . . . . . . 13 𝐹 = (𝑡𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
23 nfcv 2958 . . . . . . . . . . . . . 14 𝑖𝑇
24 nfmpt1 5131 . . . . . . . . . . . . . 14 𝑖(𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))
2523, 24nfmpt 5130 . . . . . . . . . . . . 13 𝑖(𝑡𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
2622, 25nfcxfr 2956 . . . . . . . . . . . 12 𝑖𝐹
27 nfcv 2958 . . . . . . . . . . . 12 𝑖𝑡
2826, 27nffv 6659 . . . . . . . . . . 11 𝑖(𝐹𝑡)
29 nfcv 2958 . . . . . . . . . . 11 𝑖𝑎
3028, 29nffv 6659 . . . . . . . . . 10 𝑖((𝐹𝑡)‘𝑎)
3130nfel1 2974 . . . . . . . . 9 𝑖((𝐹𝑡)‘𝑎) ∈ ℝ
3221, 31nfim 1897 . . . . . . . 8 𝑖(((𝜑𝑡𝐵) ∧ 𝑎 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑎) ∈ ℝ)
33 eleq1 2880 . . . . . . . . . 10 (𝑖 = 𝑎 → (𝑖 ∈ (1...𝑀) ↔ 𝑎 ∈ (1...𝑀)))
3433anbi2d 631 . . . . . . . . 9 (𝑖 = 𝑎 → (((𝜑𝑡𝐵) ∧ 𝑖 ∈ (1...𝑀)) ↔ ((𝜑𝑡𝐵) ∧ 𝑎 ∈ (1...𝑀))))
35 fveq2 6649 . . . . . . . . . 10 (𝑖 = 𝑎 → ((𝐹𝑡)‘𝑖) = ((𝐹𝑡)‘𝑎))
3635eleq1d 2877 . . . . . . . . 9 (𝑖 = 𝑎 → (((𝐹𝑡)‘𝑖) ∈ ℝ ↔ ((𝐹𝑡)‘𝑎) ∈ ℝ))
3734, 36imbi12d 348 . . . . . . . 8 (𝑖 = 𝑎 → ((((𝜑𝑡𝐵) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑖) ∈ ℝ) ↔ (((𝜑𝑡𝐵) ∧ 𝑎 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑎) ∈ ℝ)))
38 stoweidlem42.16 . . . . . . . . . . . 12 (𝜑𝐵𝑇)
3938sselda 3918 . . . . . . . . . . 11 ((𝜑𝑡𝐵) → 𝑡𝑇)
40 ovex 7172 . . . . . . . . . . . 12 (1...𝑀) ∈ V
41 mptexg 6965 . . . . . . . . . . . 12 ((1...𝑀) ∈ V → (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)) ∈ V)
4240, 41mp1i 13 . . . . . . . . . . 11 ((𝜑𝑡𝐵) → (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)) ∈ V)
4322fvmpt2 6760 . . . . . . . . . . 11 ((𝑡𝑇 ∧ (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)) ∈ V) → (𝐹𝑡) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
4439, 42, 43syl2anc 587 . . . . . . . . . 10 ((𝜑𝑡𝐵) → (𝐹𝑡) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
45 stoweidlem42.9 . . . . . . . . . . . . . 14 (𝜑𝑈:(1...𝑀)⟶𝑌)
4645ffvelrnda 6832 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑈𝑖) ∈ 𝑌)
47 simpl 486 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → 𝜑)
4847, 46jca 515 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → (𝜑 ∧ (𝑈𝑖) ∈ 𝑌))
49 eleq1 2880 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑈𝑖) → (𝑓𝑌 ↔ (𝑈𝑖) ∈ 𝑌))
5049anbi2d 631 . . . . . . . . . . . . . . 15 (𝑓 = (𝑈𝑖) → ((𝜑𝑓𝑌) ↔ (𝜑 ∧ (𝑈𝑖) ∈ 𝑌)))
51 feq1 6472 . . . . . . . . . . . . . . 15 (𝑓 = (𝑈𝑖) → (𝑓:𝑇⟶ℝ ↔ (𝑈𝑖):𝑇⟶ℝ))
5250, 51imbi12d 348 . . . . . . . . . . . . . 14 (𝑓 = (𝑈𝑖) → (((𝜑𝑓𝑌) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ (𝑈𝑖) ∈ 𝑌) → (𝑈𝑖):𝑇⟶ℝ)))
53 stoweidlem42.13 . . . . . . . . . . . . . 14 ((𝜑𝑓𝑌) → 𝑓:𝑇⟶ℝ)
5452, 53vtoclg 3518 . . . . . . . . . . . . 13 ((𝑈𝑖) ∈ 𝑌 → ((𝜑 ∧ (𝑈𝑖) ∈ 𝑌) → (𝑈𝑖):𝑇⟶ℝ))
5546, 48, 54sylc 65 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑈𝑖):𝑇⟶ℝ)
5655adantlr 714 . . . . . . . . . . 11 (((𝜑𝑡𝐵) ∧ 𝑖 ∈ (1...𝑀)) → (𝑈𝑖):𝑇⟶ℝ)
5739adantr 484 . . . . . . . . . . 11 (((𝜑𝑡𝐵) ∧ 𝑖 ∈ (1...𝑀)) → 𝑡𝑇)
5856, 57ffvelrnd 6833 . . . . . . . . . 10 (((𝜑𝑡𝐵) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑈𝑖)‘𝑡) ∈ ℝ)
5944, 58fvmpt2d 6762 . . . . . . . . 9 (((𝜑𝑡𝐵) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑖) = ((𝑈𝑖)‘𝑡))
6059, 58eqeltrd 2893 . . . . . . . 8 (((𝜑𝑡𝐵) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑖) ∈ ℝ)
6132, 37, 60chvarfv 2241 . . . . . . 7 (((𝜑𝑡𝐵) ∧ 𝑎 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑎) ∈ ℝ)
62 remulcl 10615 . . . . . . . 8 ((𝑎 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑎 · 𝑗) ∈ ℝ)
6362adantl 485 . . . . . . 7 (((𝜑𝑡𝐵) ∧ (𝑎 ∈ ℝ ∧ 𝑗 ∈ ℝ)) → (𝑎 · 𝑗) ∈ ℝ)
6416, 61, 63seqcl 13390 . . . . . 6 ((𝜑𝑡𝐵) → (seq1( · , (𝐹𝑡))‘𝑀) ∈ ℝ)
653rpcnd 12425 . . . . . . . . . . . 12 (𝜑𝐸 ∈ ℂ)
667nncnd 11645 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℂ)
677nnne0d 11679 . . . . . . . . . . . 12 (𝜑𝑀 ≠ 0)
6865, 66, 67divcan1d 11410 . . . . . . . . . . 11 (𝜑 → ((𝐸 / 𝑀) · 𝑀) = 𝐸)
6968eqcomd 2807 . . . . . . . . . 10 (𝜑𝐸 = ((𝐸 / 𝑀) · 𝑀))
7069oveq2d 7155 . . . . . . . . 9 (𝜑 → (1 − 𝐸) = (1 − ((𝐸 / 𝑀) · 𝑀)))
71 1cnd 10629 . . . . . . . . . 10 (𝜑 → 1 ∈ ℂ)
7265, 66, 67divcld 11409 . . . . . . . . . . 11 (𝜑 → (𝐸 / 𝑀) ∈ ℂ)
7372, 66mulcld 10654 . . . . . . . . . 10 (𝜑 → ((𝐸 / 𝑀) · 𝑀) ∈ ℂ)
7471, 73negsubd 10996 . . . . . . . . 9 (𝜑 → (1 + -((𝐸 / 𝑀) · 𝑀)) = (1 − ((𝐸 / 𝑀) · 𝑀)))
7572, 66mulneg1d 11086 . . . . . . . . . . 11 (𝜑 → (-(𝐸 / 𝑀) · 𝑀) = -((𝐸 / 𝑀) · 𝑀))
7675eqcomd 2807 . . . . . . . . . 10 (𝜑 → -((𝐸 / 𝑀) · 𝑀) = (-(𝐸 / 𝑀) · 𝑀))
7776oveq2d 7155 . . . . . . . . 9 (𝜑 → (1 + -((𝐸 / 𝑀) · 𝑀)) = (1 + (-(𝐸 / 𝑀) · 𝑀)))
7870, 74, 773eqtr2d 2842 . . . . . . . 8 (𝜑 → (1 − 𝐸) = (1 + (-(𝐸 / 𝑀) · 𝑀)))
798renegcld 11060 . . . . . . . . . 10 (𝜑 → -(𝐸 / 𝑀) ∈ ℝ)
807nnred 11644 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ ℝ)
81 3re 11709 . . . . . . . . . . . . . . . . . 18 3 ∈ ℝ
8281a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 3 ∈ ℝ)
83 3ne0 11735 . . . . . . . . . . . . . . . . . 18 3 ≠ 0
8483a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 3 ≠ 0)
8582, 84rereccld 11460 . . . . . . . . . . . . . . . 16 (𝜑 → (1 / 3) ∈ ℝ)
86 stoweidlem42.12 . . . . . . . . . . . . . . . 16 (𝜑𝐸 < (1 / 3))
87 1lt3 11802 . . . . . . . . . . . . . . . . . . 19 1 < 3
8887a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → 1 < 3)
89 0lt1 11155 . . . . . . . . . . . . . . . . . . . 20 0 < 1
9089a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 < 1)
91 3pos 11734 . . . . . . . . . . . . . . . . . . . 20 0 < 3
9291a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 < 3)
93 ltdiv2 11519 . . . . . . . . . . . . . . . . . . 19 (((1 ∈ ℝ ∧ 0 < 1) ∧ (3 ∈ ℝ ∧ 0 < 3) ∧ (1 ∈ ℝ ∧ 0 < 1)) → (1 < 3 ↔ (1 / 3) < (1 / 1)))
942, 90, 82, 92, 2, 90, 93syl222anc 1383 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1 < 3 ↔ (1 / 3) < (1 / 1)))
9588, 94mpbid 235 . . . . . . . . . . . . . . . . 17 (𝜑 → (1 / 3) < (1 / 1))
96 1div1e1 11323 . . . . . . . . . . . . . . . . 17 (1 / 1) = 1
9795, 96breqtrdi 5074 . . . . . . . . . . . . . . . 16 (𝜑 → (1 / 3) < 1)
984, 85, 2, 86, 97lttrd 10794 . . . . . . . . . . . . . . 15 (𝜑𝐸 < 1)
997nnge1d 11677 . . . . . . . . . . . . . . 15 (𝜑 → 1 ≤ 𝑀)
1004, 2, 80, 98, 99ltletrd 10793 . . . . . . . . . . . . . 14 (𝜑𝐸 < 𝑀)
1014, 80, 100ltled 10781 . . . . . . . . . . . . 13 (𝜑𝐸𝑀)
1023rpregt0d 12429 . . . . . . . . . . . . . 14 (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
1037nngt0d 11678 . . . . . . . . . . . . . 14 (𝜑 → 0 < 𝑀)
104 lediv2 11523 . . . . . . . . . . . . . 14 (((𝐸 ∈ ℝ ∧ 0 < 𝐸) ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀) ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (𝐸𝑀 ↔ (𝐸 / 𝑀) ≤ (𝐸 / 𝐸)))
105102, 80, 103, 102, 104syl121anc 1372 . . . . . . . . . . . . 13 (𝜑 → (𝐸𝑀 ↔ (𝐸 / 𝑀) ≤ (𝐸 / 𝐸)))
106101, 105mpbid 235 . . . . . . . . . . . 12 (𝜑 → (𝐸 / 𝑀) ≤ (𝐸 / 𝐸))
1073rpcnne0d 12432 . . . . . . . . . . . . 13 (𝜑 → (𝐸 ∈ ℂ ∧ 𝐸 ≠ 0))
108 divid 11320 . . . . . . . . . . . . 13 ((𝐸 ∈ ℂ ∧ 𝐸 ≠ 0) → (𝐸 / 𝐸) = 1)
109107, 108syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐸 / 𝐸) = 1)
110106, 109breqtrd 5059 . . . . . . . . . . 11 (𝜑 → (𝐸 / 𝑀) ≤ 1)
1118, 2lenegd 11212 . . . . . . . . . . 11 (𝜑 → ((𝐸 / 𝑀) ≤ 1 ↔ -1 ≤ -(𝐸 / 𝑀)))
112110, 111mpbid 235 . . . . . . . . . 10 (𝜑 → -1 ≤ -(𝐸 / 𝑀))
113 bernneq 13590 . . . . . . . . . 10 ((-(𝐸 / 𝑀) ∈ ℝ ∧ 𝑀 ∈ ℕ0 ∧ -1 ≤ -(𝐸 / 𝑀)) → (1 + (-(𝐸 / 𝑀) · 𝑀)) ≤ ((1 + -(𝐸 / 𝑀))↑𝑀))
11479, 11, 112, 113syl3anc 1368 . . . . . . . . 9 (𝜑 → (1 + (-(𝐸 / 𝑀) · 𝑀)) ≤ ((1 + -(𝐸 / 𝑀))↑𝑀))
11571, 72negsubd 10996 . . . . . . . . . 10 (𝜑 → (1 + -(𝐸 / 𝑀)) = (1 − (𝐸 / 𝑀)))
116115oveq1d 7154 . . . . . . . . 9 (𝜑 → ((1 + -(𝐸 / 𝑀))↑𝑀) = ((1 − (𝐸 / 𝑀))↑𝑀))
117114, 116breqtrd 5059 . . . . . . . 8 (𝜑 → (1 + (-(𝐸 / 𝑀) · 𝑀)) ≤ ((1 − (𝐸 / 𝑀))↑𝑀))
11878, 117eqbrtrd 5055 . . . . . . 7 (𝜑 → (1 − 𝐸) ≤ ((1 − (𝐸 / 𝑀))↑𝑀))
119118adantr 484 . . . . . 6 ((𝜑𝑡𝐵) → (1 − 𝐸) ≤ ((1 − (𝐸 / 𝑀))↑𝑀))
120 eqid 2801 . . . . . . 7 seq1( · , (𝐹𝑡)) = seq1( · , (𝐹𝑡))
1217adantr 484 . . . . . . 7 ((𝜑𝑡𝐵) → 𝑀 ∈ ℕ)
122 eqid 2801 . . . . . . . . 9 (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))
12319, 58, 122fmptdf 6862 . . . . . . . 8 ((𝜑𝑡𝐵) → (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)):(1...𝑀)⟶ℝ)
12444feq1d 6476 . . . . . . . 8 ((𝜑𝑡𝐵) → ((𝐹𝑡):(1...𝑀)⟶ℝ ↔ (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)):(1...𝑀)⟶ℝ))
125123, 124mpbird 260 . . . . . . 7 ((𝜑𝑡𝐵) → (𝐹𝑡):(1...𝑀)⟶ℝ)
126 stoweidlem42.10 . . . . . . . . . 10 ((𝜑𝑖 ∈ (1...𝑀)) → ∀𝑡𝐵 (1 − (𝐸 / 𝑀)) < ((𝑈𝑖)‘𝑡))
127126r19.21bi 3176 . . . . . . . . 9 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑡𝐵) → (1 − (𝐸 / 𝑀)) < ((𝑈𝑖)‘𝑡))
128127an32s 651 . . . . . . . 8 (((𝜑𝑡𝐵) ∧ 𝑖 ∈ (1...𝑀)) → (1 − (𝐸 / 𝑀)) < ((𝑈𝑖)‘𝑡))
129128, 59breqtrrd 5061 . . . . . . 7 (((𝜑𝑡𝐵) ∧ 𝑖 ∈ (1...𝑀)) → (1 − (𝐸 / 𝑀)) < ((𝐹𝑡)‘𝑖))
13072addid2d 10834 . . . . . . . . . . 11 (𝜑 → (0 + (𝐸 / 𝑀)) = (𝐸 / 𝑀))
131 lediv2 11523 . . . . . . . . . . . . . . 15 (((1 ∈ ℝ ∧ 0 < 1) ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀) ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (1 ≤ 𝑀 ↔ (𝐸 / 𝑀) ≤ (𝐸 / 1)))
1322, 90, 80, 103, 102, 131syl221anc 1378 . . . . . . . . . . . . . 14 (𝜑 → (1 ≤ 𝑀 ↔ (𝐸 / 𝑀) ≤ (𝐸 / 1)))
13399, 132mpbid 235 . . . . . . . . . . . . 13 (𝜑 → (𝐸 / 𝑀) ≤ (𝐸 / 1))
13465div1d 11401 . . . . . . . . . . . . 13 (𝜑 → (𝐸 / 1) = 𝐸)
135133, 134breqtrd 5059 . . . . . . . . . . . 12 (𝜑 → (𝐸 / 𝑀) ≤ 𝐸)
1368, 4, 2, 135, 98lelttrd 10791 . . . . . . . . . . 11 (𝜑 → (𝐸 / 𝑀) < 1)
137130, 136eqbrtrd 5055 . . . . . . . . . 10 (𝜑 → (0 + (𝐸 / 𝑀)) < 1)
138 0red 10637 . . . . . . . . . . 11 (𝜑 → 0 ∈ ℝ)
139138, 8, 2ltaddsubd 11233 . . . . . . . . . 10 (𝜑 → ((0 + (𝐸 / 𝑀)) < 1 ↔ 0 < (1 − (𝐸 / 𝑀))))
140137, 139mpbid 235 . . . . . . . . 9 (𝜑 → 0 < (1 − (𝐸 / 𝑀)))
1419, 140elrpd 12420 . . . . . . . 8 (𝜑 → (1 − (𝐸 / 𝑀)) ∈ ℝ+)
142141adantr 484 . . . . . . 7 ((𝜑𝑡𝐵) → (1 − (𝐸 / 𝑀)) ∈ ℝ+)
14328, 19, 120, 121, 125, 129, 142stoweidlem3 42642 . . . . . 6 ((𝜑𝑡𝐵) → ((1 − (𝐸 / 𝑀))↑𝑀) < (seq1( · , (𝐹𝑡))‘𝑀))
1446, 13, 64, 119, 143lelttrd 10791 . . . . 5 ((𝜑𝑡𝐵) → (1 − 𝐸) < (seq1( · , (𝐹𝑡))‘𝑀))
145 stoweidlem42.7 . . . . . . 7 𝑍 = (𝑡𝑇 ↦ (seq1( · , (𝐹𝑡))‘𝑀))
146145fvmpt2 6760 . . . . . 6 ((𝑡𝑇 ∧ (seq1( · , (𝐹𝑡))‘𝑀) ∈ ℝ) → (𝑍𝑡) = (seq1( · , (𝐹𝑡))‘𝑀))
14739, 64, 146syl2anc 587 . . . . 5 ((𝜑𝑡𝐵) → (𝑍𝑡) = (seq1( · , (𝐹𝑡))‘𝑀))
148144, 147breqtrrd 5061 . . . 4 ((𝜑𝑡𝐵) → (1 − 𝐸) < (𝑍𝑡))
149 simpl 486 . . . . 5 ((𝜑𝑡𝐵) → 𝜑)
150 stoweidlem42.3 . . . . . 6 𝑡𝑌
151 stoweidlem42.4 . . . . . 6 𝑃 = (𝑓𝑌, 𝑔𝑌 ↦ (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))))
152 stoweidlem42.5 . . . . . 6 𝑋 = (seq1(𝑃, 𝑈)‘𝑀)
153 stoweidlem42.15 . . . . . 6 (𝜑𝑇 ∈ V)
154 stoweidlem42.14 . . . . . 6 ((𝜑𝑓𝑌𝑔𝑌) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝑌)
15517, 150, 151, 152, 22, 145, 153, 7, 45, 53, 154fmuldfeq 42222 . . . . 5 ((𝜑𝑡𝑇) → (𝑋𝑡) = (𝑍𝑡))
156149, 39, 155syl2anc 587 . . . 4 ((𝜑𝑡𝐵) → (𝑋𝑡) = (𝑍𝑡))
157148, 156breqtrrd 5061 . . 3 ((𝜑𝑡𝐵) → (1 − 𝐸) < (𝑋𝑡))
158157ex 416 . 2 (𝜑 → (𝑡𝐵 → (1 − 𝐸) < (𝑋𝑡)))
1591, 158ralrimi 3183 1 (𝜑 → ∀𝑡𝐵 (1 − 𝐸) < (𝑋𝑡))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wnf 1785  wcel 2112  wnfc 2939  wne 2990  wral 3109  Vcvv 3444  wss 3884   class class class wbr 5033  cmpt 5113  wf 6324  cfv 6328  (class class class)co 7139  cmpo 7141  cc 10528  cr 10529  0cc0 10530  1c1 10531   + caddc 10533   · cmul 10535   < clt 10668  cle 10669  cmin 10863  -cneg 10864   / cdiv 11290  cn 11629  3c3 11685  0cn0 11889  cuz 12235  +crp 12381  ...cfz 12889  seqcseq 13368  cexp 13429
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
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-iun 4886  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-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-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  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-n0 11890  df-z 11974  df-uz 12236  df-rp 12382  df-fz 12890  df-fzo 13033  df-seq 13369  df-exp 13430
This theorem is referenced by:  stoweidlem51  42690
  Copyright terms: Public domain W3C validator