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 44273
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 11156 . . . . . . . 8 (𝜑 → 1 ∈ ℝ)
3 stoweidlem42.11 . . . . . . . . 9 (𝜑𝐸 ∈ ℝ+)
43rpred 12957 . . . . . . . 8 (𝜑𝐸 ∈ ℝ)
52, 4resubcld 11583 . . . . . . 7 (𝜑 → (1 − 𝐸) ∈ ℝ)
65adantr 481 . . . . . 6 ((𝜑𝑡𝐵) → (1 − 𝐸) ∈ ℝ)
7 stoweidlem42.8 . . . . . . . . . 10 (𝜑𝑀 ∈ ℕ)
84, 7nndivred 12207 . . . . . . . . 9 (𝜑 → (𝐸 / 𝑀) ∈ ℝ)
92, 8resubcld 11583 . . . . . . . 8 (𝜑 → (1 − (𝐸 / 𝑀)) ∈ ℝ)
109adantr 481 . . . . . . 7 ((𝜑𝑡𝐵) → (1 − (𝐸 / 𝑀)) ∈ ℝ)
117nnnn0d 12473 . . . . . . . 8 (𝜑𝑀 ∈ ℕ0)
1211adantr 481 . . . . . . 7 ((𝜑𝑡𝐵) → 𝑀 ∈ ℕ0)
1310, 12reexpcld 14068 . . . . . 6 ((𝜑𝑡𝐵) → ((1 − (𝐸 / 𝑀))↑𝑀) ∈ ℝ)
14 elnnuz 12807 . . . . . . . . 9 (𝑀 ∈ ℕ ↔ 𝑀 ∈ (ℤ‘1))
157, 14sylib 217 . . . . . . . 8 (𝜑𝑀 ∈ (ℤ‘1))
1615adantr 481 . . . . . . 7 ((𝜑𝑡𝐵) → 𝑀 ∈ (ℤ‘1))
17 stoweidlem42.1 . . . . . . . . . . 11 𝑖𝜑
18 nfv 1917 . . . . . . . . . . 11 𝑖 𝑡𝐵
1917, 18nfan 1902 . . . . . . . . . 10 𝑖(𝜑𝑡𝐵)
20 nfv 1917 . . . . . . . . . 10 𝑖 𝑎 ∈ (1...𝑀)
2119, 20nfan 1902 . . . . . . . . 9 𝑖((𝜑𝑡𝐵) ∧ 𝑎 ∈ (1...𝑀))
22 stoweidlem42.6 . . . . . . . . . . . . 13 𝐹 = (𝑡𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
23 nfcv 2907 . . . . . . . . . . . . . 14 𝑖𝑇
24 nfmpt1 5213 . . . . . . . . . . . . . 14 𝑖(𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))
2523, 24nfmpt 5212 . . . . . . . . . . . . 13 𝑖(𝑡𝑇 ↦ (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
2622, 25nfcxfr 2905 . . . . . . . . . . . 12 𝑖𝐹
27 nfcv 2907 . . . . . . . . . . . 12 𝑖𝑡
2826, 27nffv 6852 . . . . . . . . . . 11 𝑖(𝐹𝑡)
29 nfcv 2907 . . . . . . . . . . 11 𝑖𝑎
3028, 29nffv 6852 . . . . . . . . . 10 𝑖((𝐹𝑡)‘𝑎)
3130nfel1 2923 . . . . . . . . 9 𝑖((𝐹𝑡)‘𝑎) ∈ ℝ
3221, 31nfim 1899 . . . . . . . 8 𝑖(((𝜑𝑡𝐵) ∧ 𝑎 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑎) ∈ ℝ)
33 eleq1 2825 . . . . . . . . . 10 (𝑖 = 𝑎 → (𝑖 ∈ (1...𝑀) ↔ 𝑎 ∈ (1...𝑀)))
3433anbi2d 629 . . . . . . . . 9 (𝑖 = 𝑎 → (((𝜑𝑡𝐵) ∧ 𝑖 ∈ (1...𝑀)) ↔ ((𝜑𝑡𝐵) ∧ 𝑎 ∈ (1...𝑀))))
35 fveq2 6842 . . . . . . . . . 10 (𝑖 = 𝑎 → ((𝐹𝑡)‘𝑖) = ((𝐹𝑡)‘𝑎))
3635eleq1d 2822 . . . . . . . . 9 (𝑖 = 𝑎 → (((𝐹𝑡)‘𝑖) ∈ ℝ ↔ ((𝐹𝑡)‘𝑎) ∈ ℝ))
3734, 36imbi12d 344 . . . . . . . 8 (𝑖 = 𝑎 → ((((𝜑𝑡𝐵) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑖) ∈ ℝ) ↔ (((𝜑𝑡𝐵) ∧ 𝑎 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑎) ∈ ℝ)))
38 stoweidlem42.16 . . . . . . . . . . . 12 (𝜑𝐵𝑇)
3938sselda 3944 . . . . . . . . . . 11 ((𝜑𝑡𝐵) → 𝑡𝑇)
40 ovex 7390 . . . . . . . . . . . 12 (1...𝑀) ∈ V
41 mptexg 7171 . . . . . . . . . . . 12 ((1...𝑀) ∈ V → (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)) ∈ V)
4240, 41mp1i 13 . . . . . . . . . . 11 ((𝜑𝑡𝐵) → (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)) ∈ V)
4322fvmpt2 6959 . . . . . . . . . . 11 ((𝑡𝑇 ∧ (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)) ∈ V) → (𝐹𝑡) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
4439, 42, 43syl2anc 584 . . . . . . . . . 10 ((𝜑𝑡𝐵) → (𝐹𝑡) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)))
45 stoweidlem42.9 . . . . . . . . . . . . . 14 (𝜑𝑈:(1...𝑀)⟶𝑌)
4645ffvelcdmda 7035 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑈𝑖) ∈ 𝑌)
47 simpl 483 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → 𝜑)
4847, 46jca 512 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → (𝜑 ∧ (𝑈𝑖) ∈ 𝑌))
49 eleq1 2825 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑈𝑖) → (𝑓𝑌 ↔ (𝑈𝑖) ∈ 𝑌))
5049anbi2d 629 . . . . . . . . . . . . . . 15 (𝑓 = (𝑈𝑖) → ((𝜑𝑓𝑌) ↔ (𝜑 ∧ (𝑈𝑖) ∈ 𝑌)))
51 feq1 6649 . . . . . . . . . . . . . . 15 (𝑓 = (𝑈𝑖) → (𝑓:𝑇⟶ℝ ↔ (𝑈𝑖):𝑇⟶ℝ))
5250, 51imbi12d 344 . . . . . . . . . . . . . 14 (𝑓 = (𝑈𝑖) → (((𝜑𝑓𝑌) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ (𝑈𝑖) ∈ 𝑌) → (𝑈𝑖):𝑇⟶ℝ)))
53 stoweidlem42.13 . . . . . . . . . . . . . 14 ((𝜑𝑓𝑌) → 𝑓:𝑇⟶ℝ)
5452, 53vtoclg 3525 . . . . . . . . . . . . 13 ((𝑈𝑖) ∈ 𝑌 → ((𝜑 ∧ (𝑈𝑖) ∈ 𝑌) → (𝑈𝑖):𝑇⟶ℝ))
5546, 48, 54sylc 65 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑈𝑖):𝑇⟶ℝ)
5655adantlr 713 . . . . . . . . . . 11 (((𝜑𝑡𝐵) ∧ 𝑖 ∈ (1...𝑀)) → (𝑈𝑖):𝑇⟶ℝ)
5739adantr 481 . . . . . . . . . . 11 (((𝜑𝑡𝐵) ∧ 𝑖 ∈ (1...𝑀)) → 𝑡𝑇)
5856, 57ffvelcdmd 7036 . . . . . . . . . 10 (((𝜑𝑡𝐵) ∧ 𝑖 ∈ (1...𝑀)) → ((𝑈𝑖)‘𝑡) ∈ ℝ)
5944, 58fvmpt2d 6961 . . . . . . . . 9 (((𝜑𝑡𝐵) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑖) = ((𝑈𝑖)‘𝑡))
6059, 58eqeltrd 2838 . . . . . . . 8 (((𝜑𝑡𝐵) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑖) ∈ ℝ)
6132, 37, 60chvarfv 2233 . . . . . . 7 (((𝜑𝑡𝐵) ∧ 𝑎 ∈ (1...𝑀)) → ((𝐹𝑡)‘𝑎) ∈ ℝ)
62 remulcl 11136 . . . . . . . 8 ((𝑎 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑎 · 𝑗) ∈ ℝ)
6362adantl 482 . . . . . . 7 (((𝜑𝑡𝐵) ∧ (𝑎 ∈ ℝ ∧ 𝑗 ∈ ℝ)) → (𝑎 · 𝑗) ∈ ℝ)
6416, 61, 63seqcl 13928 . . . . . 6 ((𝜑𝑡𝐵) → (seq1( · , (𝐹𝑡))‘𝑀) ∈ ℝ)
653rpcnd 12959 . . . . . . . . . . . 12 (𝜑𝐸 ∈ ℂ)
667nncnd 12169 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℂ)
677nnne0d 12203 . . . . . . . . . . . 12 (𝜑𝑀 ≠ 0)
6865, 66, 67divcan1d 11932 . . . . . . . . . . 11 (𝜑 → ((𝐸 / 𝑀) · 𝑀) = 𝐸)
6968eqcomd 2742 . . . . . . . . . 10 (𝜑𝐸 = ((𝐸 / 𝑀) · 𝑀))
7069oveq2d 7373 . . . . . . . . 9 (𝜑 → (1 − 𝐸) = (1 − ((𝐸 / 𝑀) · 𝑀)))
71 1cnd 11150 . . . . . . . . . 10 (𝜑 → 1 ∈ ℂ)
7265, 66, 67divcld 11931 . . . . . . . . . . 11 (𝜑 → (𝐸 / 𝑀) ∈ ℂ)
7372, 66mulcld 11175 . . . . . . . . . 10 (𝜑 → ((𝐸 / 𝑀) · 𝑀) ∈ ℂ)
7471, 73negsubd 11518 . . . . . . . . 9 (𝜑 → (1 + -((𝐸 / 𝑀) · 𝑀)) = (1 − ((𝐸 / 𝑀) · 𝑀)))
7572, 66mulneg1d 11608 . . . . . . . . . . 11 (𝜑 → (-(𝐸 / 𝑀) · 𝑀) = -((𝐸 / 𝑀) · 𝑀))
7675eqcomd 2742 . . . . . . . . . 10 (𝜑 → -((𝐸 / 𝑀) · 𝑀) = (-(𝐸 / 𝑀) · 𝑀))
7776oveq2d 7373 . . . . . . . . 9 (𝜑 → (1 + -((𝐸 / 𝑀) · 𝑀)) = (1 + (-(𝐸 / 𝑀) · 𝑀)))
7870, 74, 773eqtr2d 2782 . . . . . . . 8 (𝜑 → (1 − 𝐸) = (1 + (-(𝐸 / 𝑀) · 𝑀)))
798renegcld 11582 . . . . . . . . . 10 (𝜑 → -(𝐸 / 𝑀) ∈ ℝ)
807nnred 12168 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ ℝ)
81 3re 12233 . . . . . . . . . . . . . . . . . 18 3 ∈ ℝ
8281a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 3 ∈ ℝ)
83 3ne0 12259 . . . . . . . . . . . . . . . . . 18 3 ≠ 0
8483a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 3 ≠ 0)
8582, 84rereccld 11982 . . . . . . . . . . . . . . . 16 (𝜑 → (1 / 3) ∈ ℝ)
86 stoweidlem42.12 . . . . . . . . . . . . . . . 16 (𝜑𝐸 < (1 / 3))
87 1lt3 12326 . . . . . . . . . . . . . . . . . . 19 1 < 3
8887a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → 1 < 3)
89 0lt1 11677 . . . . . . . . . . . . . . . . . . . 20 0 < 1
9089a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 < 1)
91 3pos 12258 . . . . . . . . . . . . . . . . . . . 20 0 < 3
9291a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 < 3)
93 ltdiv2 12041 . . . . . . . . . . . . . . . . . . 19 (((1 ∈ ℝ ∧ 0 < 1) ∧ (3 ∈ ℝ ∧ 0 < 3) ∧ (1 ∈ ℝ ∧ 0 < 1)) → (1 < 3 ↔ (1 / 3) < (1 / 1)))
942, 90, 82, 92, 2, 90, 93syl222anc 1386 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1 < 3 ↔ (1 / 3) < (1 / 1)))
9588, 94mpbid 231 . . . . . . . . . . . . . . . . 17 (𝜑 → (1 / 3) < (1 / 1))
96 1div1e1 11845 . . . . . . . . . . . . . . . . 17 (1 / 1) = 1
9795, 96breqtrdi 5146 . . . . . . . . . . . . . . . 16 (𝜑 → (1 / 3) < 1)
984, 85, 2, 86, 97lttrd 11316 . . . . . . . . . . . . . . 15 (𝜑𝐸 < 1)
997nnge1d 12201 . . . . . . . . . . . . . . 15 (𝜑 → 1 ≤ 𝑀)
1004, 2, 80, 98, 99ltletrd 11315 . . . . . . . . . . . . . 14 (𝜑𝐸 < 𝑀)
1014, 80, 100ltled 11303 . . . . . . . . . . . . 13 (𝜑𝐸𝑀)
1023rpregt0d 12963 . . . . . . . . . . . . . 14 (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
1037nngt0d 12202 . . . . . . . . . . . . . 14 (𝜑 → 0 < 𝑀)
104 lediv2 12045 . . . . . . . . . . . . . 14 (((𝐸 ∈ ℝ ∧ 0 < 𝐸) ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀) ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (𝐸𝑀 ↔ (𝐸 / 𝑀) ≤ (𝐸 / 𝐸)))
105102, 80, 103, 102, 104syl121anc 1375 . . . . . . . . . . . . 13 (𝜑 → (𝐸𝑀 ↔ (𝐸 / 𝑀) ≤ (𝐸 / 𝐸)))
106101, 105mpbid 231 . . . . . . . . . . . 12 (𝜑 → (𝐸 / 𝑀) ≤ (𝐸 / 𝐸))
1073rpcnne0d 12966 . . . . . . . . . . . . 13 (𝜑 → (𝐸 ∈ ℂ ∧ 𝐸 ≠ 0))
108 divid 11842 . . . . . . . . . . . . 13 ((𝐸 ∈ ℂ ∧ 𝐸 ≠ 0) → (𝐸 / 𝐸) = 1)
109107, 108syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐸 / 𝐸) = 1)
110106, 109breqtrd 5131 . . . . . . . . . . 11 (𝜑 → (𝐸 / 𝑀) ≤ 1)
1118, 2lenegd 11734 . . . . . . . . . . 11 (𝜑 → ((𝐸 / 𝑀) ≤ 1 ↔ -1 ≤ -(𝐸 / 𝑀)))
112110, 111mpbid 231 . . . . . . . . . 10 (𝜑 → -1 ≤ -(𝐸 / 𝑀))
113 bernneq 14132 . . . . . . . . . 10 ((-(𝐸 / 𝑀) ∈ ℝ ∧ 𝑀 ∈ ℕ0 ∧ -1 ≤ -(𝐸 / 𝑀)) → (1 + (-(𝐸 / 𝑀) · 𝑀)) ≤ ((1 + -(𝐸 / 𝑀))↑𝑀))
11479, 11, 112, 113syl3anc 1371 . . . . . . . . 9 (𝜑 → (1 + (-(𝐸 / 𝑀) · 𝑀)) ≤ ((1 + -(𝐸 / 𝑀))↑𝑀))
11571, 72negsubd 11518 . . . . . . . . . 10 (𝜑 → (1 + -(𝐸 / 𝑀)) = (1 − (𝐸 / 𝑀)))
116115oveq1d 7372 . . . . . . . . 9 (𝜑 → ((1 + -(𝐸 / 𝑀))↑𝑀) = ((1 − (𝐸 / 𝑀))↑𝑀))
117114, 116breqtrd 5131 . . . . . . . 8 (𝜑 → (1 + (-(𝐸 / 𝑀) · 𝑀)) ≤ ((1 − (𝐸 / 𝑀))↑𝑀))
11878, 117eqbrtrd 5127 . . . . . . 7 (𝜑 → (1 − 𝐸) ≤ ((1 − (𝐸 / 𝑀))↑𝑀))
119118adantr 481 . . . . . 6 ((𝜑𝑡𝐵) → (1 − 𝐸) ≤ ((1 − (𝐸 / 𝑀))↑𝑀))
120 eqid 2736 . . . . . . 7 seq1( · , (𝐹𝑡)) = seq1( · , (𝐹𝑡))
1217adantr 481 . . . . . . 7 ((𝜑𝑡𝐵) → 𝑀 ∈ ℕ)
122 eqid 2736 . . . . . . . . 9 (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)) = (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡))
12319, 58, 122fmptdf 7065 . . . . . . . 8 ((𝜑𝑡𝐵) → (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)):(1...𝑀)⟶ℝ)
12444feq1d 6653 . . . . . . . 8 ((𝜑𝑡𝐵) → ((𝐹𝑡):(1...𝑀)⟶ℝ ↔ (𝑖 ∈ (1...𝑀) ↦ ((𝑈𝑖)‘𝑡)):(1...𝑀)⟶ℝ))
125123, 124mpbird 256 . . . . . . 7 ((𝜑𝑡𝐵) → (𝐹𝑡):(1...𝑀)⟶ℝ)
126 stoweidlem42.10 . . . . . . . . . 10 ((𝜑𝑖 ∈ (1...𝑀)) → ∀𝑡𝐵 (1 − (𝐸 / 𝑀)) < ((𝑈𝑖)‘𝑡))
127126r19.21bi 3234 . . . . . . . . 9 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑡𝐵) → (1 − (𝐸 / 𝑀)) < ((𝑈𝑖)‘𝑡))
128127an32s 650 . . . . . . . 8 (((𝜑𝑡𝐵) ∧ 𝑖 ∈ (1...𝑀)) → (1 − (𝐸 / 𝑀)) < ((𝑈𝑖)‘𝑡))
129128, 59breqtrrd 5133 . . . . . . 7 (((𝜑𝑡𝐵) ∧ 𝑖 ∈ (1...𝑀)) → (1 − (𝐸 / 𝑀)) < ((𝐹𝑡)‘𝑖))
13072addid2d 11356 . . . . . . . . . . 11 (𝜑 → (0 + (𝐸 / 𝑀)) = (𝐸 / 𝑀))
131 lediv2 12045 . . . . . . . . . . . . . . 15 (((1 ∈ ℝ ∧ 0 < 1) ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀) ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (1 ≤ 𝑀 ↔ (𝐸 / 𝑀) ≤ (𝐸 / 1)))
1322, 90, 80, 103, 102, 131syl221anc 1381 . . . . . . . . . . . . . 14 (𝜑 → (1 ≤ 𝑀 ↔ (𝐸 / 𝑀) ≤ (𝐸 / 1)))
13399, 132mpbid 231 . . . . . . . . . . . . 13 (𝜑 → (𝐸 / 𝑀) ≤ (𝐸 / 1))
13465div1d 11923 . . . . . . . . . . . . 13 (𝜑 → (𝐸 / 1) = 𝐸)
135133, 134breqtrd 5131 . . . . . . . . . . . 12 (𝜑 → (𝐸 / 𝑀) ≤ 𝐸)
1368, 4, 2, 135, 98lelttrd 11313 . . . . . . . . . . 11 (𝜑 → (𝐸 / 𝑀) < 1)
137130, 136eqbrtrd 5127 . . . . . . . . . 10 (𝜑 → (0 + (𝐸 / 𝑀)) < 1)
138 0red 11158 . . . . . . . . . . 11 (𝜑 → 0 ∈ ℝ)
139138, 8, 2ltaddsubd 11755 . . . . . . . . . 10 (𝜑 → ((0 + (𝐸 / 𝑀)) < 1 ↔ 0 < (1 − (𝐸 / 𝑀))))
140137, 139mpbid 231 . . . . . . . . 9 (𝜑 → 0 < (1 − (𝐸 / 𝑀)))
1419, 140elrpd 12954 . . . . . . . 8 (𝜑 → (1 − (𝐸 / 𝑀)) ∈ ℝ+)
142141adantr 481 . . . . . . 7 ((𝜑𝑡𝐵) → (1 − (𝐸 / 𝑀)) ∈ ℝ+)
14328, 19, 120, 121, 125, 129, 142stoweidlem3 44234 . . . . . 6 ((𝜑𝑡𝐵) → ((1 − (𝐸 / 𝑀))↑𝑀) < (seq1( · , (𝐹𝑡))‘𝑀))
1446, 13, 64, 119, 143lelttrd 11313 . . . . 5 ((𝜑𝑡𝐵) → (1 − 𝐸) < (seq1( · , (𝐹𝑡))‘𝑀))
145 stoweidlem42.7 . . . . . . 7 𝑍 = (𝑡𝑇 ↦ (seq1( · , (𝐹𝑡))‘𝑀))
146145fvmpt2 6959 . . . . . 6 ((𝑡𝑇 ∧ (seq1( · , (𝐹𝑡))‘𝑀) ∈ ℝ) → (𝑍𝑡) = (seq1( · , (𝐹𝑡))‘𝑀))
14739, 64, 146syl2anc 584 . . . . 5 ((𝜑𝑡𝐵) → (𝑍𝑡) = (seq1( · , (𝐹𝑡))‘𝑀))
148144, 147breqtrrd 5133 . . . 4 ((𝜑𝑡𝐵) → (1 − 𝐸) < (𝑍𝑡))
149 simpl 483 . . . . 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 43814 . . . . 5 ((𝜑𝑡𝑇) → (𝑋𝑡) = (𝑍𝑡))
156149, 39, 155syl2anc 584 . . . 4 ((𝜑𝑡𝐵) → (𝑋𝑡) = (𝑍𝑡))
157148, 156breqtrrd 5133 . . 3 ((𝜑𝑡𝐵) → (1 − 𝐸) < (𝑋𝑡))
158157ex 413 . 2 (𝜑 → (𝑡𝐵 → (1 − 𝐸) < (𝑋𝑡)))
1591, 158ralrimi 3240 1 (𝜑 → ∀𝑡𝐵 (1 − 𝐸) < (𝑋𝑡))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wnf 1785  wcel 2106  wnfc 2887  wne 2943  wral 3064  Vcvv 3445  wss 3910   class class class wbr 5105  cmpt 5188  wf 6492  cfv 6496  (class class class)co 7357  cmpo 7359  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056   < clt 11189  cle 11190  cmin 11385  -cneg 11386   / cdiv 11812  cn 12153  3c3 12209  0cn0 12413  cuz 12763  +crp 12915  ...cfz 13424  seqcseq 13906  cexp 13967
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-n0 12414  df-z 12500  df-uz 12764  df-rp 12916  df-fz 13425  df-fzo 13568  df-seq 13907  df-exp 13968
This theorem is referenced by:  stoweidlem51  44282
  Copyright terms: Public domain W3C validator