Metamath Proof Explorer

Theorem stoweidlem42

Description: This lemma is used to prove that x built as in Lemma 2 of BrosowskiDeutsh p. 91, is such that x > 1 - ε on B. Here X is used to represent x in the paper, and E is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem42.1 ⊢ Ⅎ 𝑖 𝜑
stoweidlem42.2 ⊢ Ⅎ 𝑡 𝜑
stoweidlem42.3 ⊢ Ⅎ 𝑡 𝑌
stoweidlem42.4 ⊢ 𝑃 = ( 𝑓 ∈ 𝑌 , 𝑔 ∈ 𝑌 ↦ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) )
stoweidlem42.5 ⊢ 𝑋 = ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑀 )
stoweidlem42.6 ⊢ 𝐹 = ( 𝑡 ∈ 𝑇 ↦ ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ) )
stoweidlem42.7 ⊢ 𝑍 = ( 𝑡 ∈ 𝑇 ↦ ( seq 1 ( · , ( 𝐹 ‘ 𝑡 ) ) ‘ 𝑀 ) )
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 stoweidlem42 ( 𝜑 → ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑋 ‘ 𝑡 ) )

Proof

Step Hyp Ref Expression
1 stoweidlem42.1 ⊢ Ⅎ 𝑖 𝜑
2 stoweidlem42.2 ⊢ Ⅎ 𝑡 𝜑
3 stoweidlem42.3 ⊢ Ⅎ 𝑡 𝑌
4 stoweidlem42.4 ⊢ 𝑃 = ( 𝑓 ∈ 𝑌 , 𝑔 ∈ 𝑌 ↦ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) )
5 stoweidlem42.5 ⊢ 𝑋 = ( seq 1 ( 𝑃 , 𝑈 ) ‘ 𝑀 )
6 stoweidlem42.6 ⊢ 𝐹 = ( 𝑡 ∈ 𝑇 ↦ ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ) )
7 stoweidlem42.7 ⊢ 𝑍 = ( 𝑡 ∈ 𝑇 ↦ ( seq 1 ( · , ( 𝐹 ‘ 𝑡 ) ) ‘ 𝑀 ) )
8 stoweidlem42.8 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
9 stoweidlem42.9 ⊢ ( 𝜑 → 𝑈 : ( 1 ... 𝑀 ) ⟶ 𝑌 )
10 stoweidlem42.10 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) )
11 stoweidlem42.11 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
12 stoweidlem42.12 ⊢ ( 𝜑 → 𝐸 < ( 1 / 3 ) )
13 stoweidlem42.13 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ) → 𝑓 : 𝑇 ⟶ ℝ )
14 stoweidlem42.14 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ∧ 𝑔 ∈ 𝑌 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝑌 )
15 stoweidlem42.15 ⊢ ( 𝜑 → 𝑇 ∈ V )
16 stoweidlem42.16 ⊢ ( 𝜑 → 𝐵 ⊆ 𝑇 )
17 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
18 11 rpred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
19 17 18 resubcld ⊢ ( 𝜑 → ( 1 − 𝐸 ) ∈ ℝ )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → ( 1 − 𝐸 ) ∈ ℝ )
21 18 8 nndivred ⊢ ( 𝜑 → ( 𝐸 / 𝑀 ) ∈ ℝ )
22 17 21 resubcld ⊢ ( 𝜑 → ( 1 − ( 𝐸 / 𝑀 ) ) ∈ ℝ )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → ( 1 − ( 𝐸 / 𝑀 ) ) ∈ ℝ )
24 8 nnnn0d ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
25 24 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → 𝑀 ∈ ℕ0 )
26 23 25 reexpcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → ( ( 1 − ( 𝐸 / 𝑀 ) ) ↑ 𝑀 ) ∈ ℝ )
27 elnnuz ⊢ ( 𝑀 ∈ ℕ ↔ 𝑀 ∈ ( ℤ≥ ‘ 1 ) )
28 8 27 sylib ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 1 ) )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → 𝑀 ∈ ( ℤ≥ ‘ 1 ) )
30 nfv ⊢ Ⅎ 𝑖 𝑡 ∈ 𝐵
31 1 30 nfan ⊢ Ⅎ 𝑖 ( 𝜑 ∧ 𝑡 ∈ 𝐵 )
32 nfv ⊢ Ⅎ 𝑖 𝑎 ∈ ( 1 ... 𝑀 )
33 31 32 nfan ⊢ Ⅎ 𝑖 ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 1 ... 𝑀 ) )
34 nfcv ⊢ Ⅎ 𝑖 𝑇
35 nfmpt1 ⊢ Ⅎ 𝑖 ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) )
36 34 35 nfmpt ⊢ Ⅎ 𝑖 ( 𝑡 ∈ 𝑇 ↦ ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ) )
37 6 36 nfcxfr ⊢ Ⅎ 𝑖 𝐹
38 nfcv ⊢ Ⅎ 𝑖 𝑡
39 37 38 nffv ⊢ Ⅎ 𝑖 ( 𝐹 ‘ 𝑡 )
40 nfcv ⊢ Ⅎ 𝑖 𝑎
41 39 40 nffv ⊢ Ⅎ 𝑖 ( ( 𝐹 ‘ 𝑡 ) ‘ 𝑎 )
42 41 nfel1 ⊢ Ⅎ 𝑖 ( ( 𝐹 ‘ 𝑡 ) ‘ 𝑎 ) ∈ ℝ
43 33 42 nfim ⊢ Ⅎ 𝑖 ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐹 ‘ 𝑡 ) ‘ 𝑎 ) ∈ ℝ )
44 eleq1 ⊢ ( 𝑖 = 𝑎 → ( 𝑖 ∈ ( 1 ... 𝑀 ) ↔ 𝑎 ∈ ( 1 ... 𝑀 ) ) )
45 44 anbi2d ⊢ ( 𝑖 = 𝑎 → ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ↔ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 1 ... 𝑀 ) ) ) )
46 fveq2 ⊢ ( 𝑖 = 𝑎 → ( ( 𝐹 ‘ 𝑡 ) ‘ 𝑖 ) = ( ( 𝐹 ‘ 𝑡 ) ‘ 𝑎 ) )
47 46 eleq1d ⊢ ( 𝑖 = 𝑎 → ( ( ( 𝐹 ‘ 𝑡 ) ‘ 𝑖 ) ∈ ℝ ↔ ( ( 𝐹 ‘ 𝑡 ) ‘ 𝑎 ) ∈ ℝ ) )
48 45 47 imbi12d ⊢ ( 𝑖 = 𝑎 → ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐹 ‘ 𝑡 ) ‘ 𝑖 ) ∈ ℝ ) ↔ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐹 ‘ 𝑡 ) ‘ 𝑎 ) ∈ ℝ ) ) )
49 16 sselda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → 𝑡 ∈ 𝑇 )
50 ovex ⊢ ( 1 ... 𝑀 ) ∈ V
51 mptexg ⊢ ( ( 1 ... 𝑀 ) ∈ V → ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ V )
52 50 51 mp1i ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ V )
53 6 fvmpt2 ⊢ ( ( 𝑡 ∈ 𝑇 ∧ ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ V ) → ( 𝐹 ‘ 𝑡 ) = ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ) )
54 49 52 53 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑡 ) = ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ) )
55 9 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑈 ‘ 𝑖 ) ∈ 𝑌 )
56 simpl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝜑 )
57 56 55 jca ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝜑 ∧ ( 𝑈 ‘ 𝑖 ) ∈ 𝑌 ) )
58 eleq1 ⊢ ( 𝑓 = ( 𝑈 ‘ 𝑖 ) → ( 𝑓 ∈ 𝑌 ↔ ( 𝑈 ‘ 𝑖 ) ∈ 𝑌 ) )
59 58 anbi2d ⊢ ( 𝑓 = ( 𝑈 ‘ 𝑖 ) → ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ) ↔ ( 𝜑 ∧ ( 𝑈 ‘ 𝑖 ) ∈ 𝑌 ) ) )
60 feq1 ⊢ ( 𝑓 = ( 𝑈 ‘ 𝑖 ) → ( 𝑓 : 𝑇 ⟶ ℝ ↔ ( 𝑈 ‘ 𝑖 ) : 𝑇 ⟶ ℝ ) )
61 59 60 imbi12d ⊢ ( 𝑓 = ( 𝑈 ‘ 𝑖 ) → ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑌 ) → 𝑓 : 𝑇 ⟶ ℝ ) ↔ ( ( 𝜑 ∧ ( 𝑈 ‘ 𝑖 ) ∈ 𝑌 ) → ( 𝑈 ‘ 𝑖 ) : 𝑇 ⟶ ℝ ) ) )
62 61 13 vtoclg ⊢ ( ( 𝑈 ‘ 𝑖 ) ∈ 𝑌 → ( ( 𝜑 ∧ ( 𝑈 ‘ 𝑖 ) ∈ 𝑌 ) → ( 𝑈 ‘ 𝑖 ) : 𝑇 ⟶ ℝ ) )
63 55 57 62 sylc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑈 ‘ 𝑖 ) : 𝑇 ⟶ ℝ )
64 63 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑈 ‘ 𝑖 ) : 𝑇 ⟶ ℝ )
65 49 adantr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝑡 ∈ 𝑇 )
66 64 65 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ )
67 54 66 fvmpt2d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐹 ‘ 𝑡 ) ‘ 𝑖 ) = ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) )
68 67 66 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐹 ‘ 𝑡 ) ‘ 𝑖 ) ∈ ℝ )
69 43 48 68 chvarfv ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐹 ‘ 𝑡 ) ‘ 𝑎 ) ∈ ℝ )
70 remulcl ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑗 ∈ ℝ ) → ( 𝑎 · 𝑗 ) ∈ ℝ )
71 70 adantl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) → ( 𝑎 · 𝑗 ) ∈ ℝ )
72 29 69 71 seqcl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → ( seq 1 ( · , ( 𝐹 ‘ 𝑡 ) ) ‘ 𝑀 ) ∈ ℝ )
73 11 rpcnd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
74 8 nncnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
75 8 nnne0d ⊢ ( 𝜑 → 𝑀 ≠ 0 )
76 73 74 75 divcan1d ⊢ ( 𝜑 → ( ( 𝐸 / 𝑀 ) · 𝑀 ) = 𝐸 )
77 76 eqcomd ⊢ ( 𝜑 → 𝐸 = ( ( 𝐸 / 𝑀 ) · 𝑀 ) )
78 77 oveq2d ⊢ ( 𝜑 → ( 1 − 𝐸 ) = ( 1 − ( ( 𝐸 / 𝑀 ) · 𝑀 ) ) )
79 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
80 73 74 75 divcld ⊢ ( 𝜑 → ( 𝐸 / 𝑀 ) ∈ ℂ )
81 80 74 mulcld ⊢ ( 𝜑 → ( ( 𝐸 / 𝑀 ) · 𝑀 ) ∈ ℂ )
82 79 81 negsubd ⊢ ( 𝜑 → ( 1 + - ( ( 𝐸 / 𝑀 ) · 𝑀 ) ) = ( 1 − ( ( 𝐸 / 𝑀 ) · 𝑀 ) ) )
83 80 74 mulneg1d ⊢ ( 𝜑 → ( - ( 𝐸 / 𝑀 ) · 𝑀 ) = - ( ( 𝐸 / 𝑀 ) · 𝑀 ) )
84 83 eqcomd ⊢ ( 𝜑 → - ( ( 𝐸 / 𝑀 ) · 𝑀 ) = ( - ( 𝐸 / 𝑀 ) · 𝑀 ) )
85 84 oveq2d ⊢ ( 𝜑 → ( 1 + - ( ( 𝐸 / 𝑀 ) · 𝑀 ) ) = ( 1 + ( - ( 𝐸 / 𝑀 ) · 𝑀 ) ) )
86 78 82 85 3eqtr2d ⊢ ( 𝜑 → ( 1 − 𝐸 ) = ( 1 + ( - ( 𝐸 / 𝑀 ) · 𝑀 ) ) )
87 21 renegcld ⊢ ( 𝜑 → - ( 𝐸 / 𝑀 ) ∈ ℝ )
88 8 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
89 3re ⊢ 3 ∈ ℝ
90 89 a1i ⊢ ( 𝜑 → 3 ∈ ℝ )
91 3ne0 ⊢ 3 ≠ 0
92 91 a1i ⊢ ( 𝜑 → 3 ≠ 0 )
93 90 92 rereccld ⊢ ( 𝜑 → ( 1 / 3 ) ∈ ℝ )
94 1lt3 ⊢ 1 < 3
95 94 a1i ⊢ ( 𝜑 → 1 < 3 )
96 0lt1 ⊢ 0 < 1
97 96 a1i ⊢ ( 𝜑 → 0 < 1 )
98 3pos ⊢ 0 < 3
99 98 a1i ⊢ ( 𝜑 → 0 < 3 )
100 ltdiv2 ⊢ ( ( ( 1 ∈ ℝ ∧ 0 < 1 ) ∧ ( 3 ∈ ℝ ∧ 0 < 3 ) ∧ ( 1 ∈ ℝ ∧ 0 < 1 ) ) → ( 1 < 3 ↔ ( 1 / 3 ) < ( 1 / 1 ) ) )
101 17 97 90 99 17 97 100 syl222anc ⊢ ( 𝜑 → ( 1 < 3 ↔ ( 1 / 3 ) < ( 1 / 1 ) ) )
102 95 101 mpbid ⊢ ( 𝜑 → ( 1 / 3 ) < ( 1 / 1 ) )
103 1div1e1 ⊢ ( 1 / 1 ) = 1
104 102 103 breqtrdi ⊢ ( 𝜑 → ( 1 / 3 ) < 1 )
105 18 93 17 12 104 lttrd ⊢ ( 𝜑 → 𝐸 < 1 )
106 8 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝑀 )
107 18 17 88 105 106 ltletrd ⊢ ( 𝜑 → 𝐸 < 𝑀 )
108 18 88 107 ltled ⊢ ( 𝜑 → 𝐸 ≤ 𝑀 )
109 11 rpregt0d ⊢ ( 𝜑 → ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) )
110 8 nngt0d ⊢ ( 𝜑 → 0 < 𝑀 )
111 lediv2 ⊢ ( ( ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) ∧ ( 𝑀 ∈ ℝ ∧ 0 < 𝑀 ) ∧ ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) ) → ( 𝐸 ≤ 𝑀 ↔ ( 𝐸 / 𝑀 ) ≤ ( 𝐸 / 𝐸 ) ) )
112 109 88 110 109 111 syl121anc ⊢ ( 𝜑 → ( 𝐸 ≤ 𝑀 ↔ ( 𝐸 / 𝑀 ) ≤ ( 𝐸 / 𝐸 ) ) )
113 108 112 mpbid ⊢ ( 𝜑 → ( 𝐸 / 𝑀 ) ≤ ( 𝐸 / 𝐸 ) )
114 11 rpcnne0d ⊢ ( 𝜑 → ( 𝐸 ∈ ℂ ∧ 𝐸 ≠ 0 ) )
115 divid ⊢ ( ( 𝐸 ∈ ℂ ∧ 𝐸 ≠ 0 ) → ( 𝐸 / 𝐸 ) = 1 )
116 114 115 syl ⊢ ( 𝜑 → ( 𝐸 / 𝐸 ) = 1 )
117 113 116 breqtrd ⊢ ( 𝜑 → ( 𝐸 / 𝑀 ) ≤ 1 )
118 21 17 lenegd ⊢ ( 𝜑 → ( ( 𝐸 / 𝑀 ) ≤ 1 ↔ - 1 ≤ - ( 𝐸 / 𝑀 ) ) )
119 117 118 mpbid ⊢ ( 𝜑 → - 1 ≤ - ( 𝐸 / 𝑀 ) )
120 bernneq ⊢ ( ( - ( 𝐸 / 𝑀 ) ∈ ℝ ∧ 𝑀 ∈ ℕ0 ∧ - 1 ≤ - ( 𝐸 / 𝑀 ) ) → ( 1 + ( - ( 𝐸 / 𝑀 ) · 𝑀 ) ) ≤ ( ( 1 + - ( 𝐸 / 𝑀 ) ) ↑ 𝑀 ) )
121 87 24 119 120 syl3anc ⊢ ( 𝜑 → ( 1 + ( - ( 𝐸 / 𝑀 ) · 𝑀 ) ) ≤ ( ( 1 + - ( 𝐸 / 𝑀 ) ) ↑ 𝑀 ) )
122 79 80 negsubd ⊢ ( 𝜑 → ( 1 + - ( 𝐸 / 𝑀 ) ) = ( 1 − ( 𝐸 / 𝑀 ) ) )
123 122 oveq1d ⊢ ( 𝜑 → ( ( 1 + - ( 𝐸 / 𝑀 ) ) ↑ 𝑀 ) = ( ( 1 − ( 𝐸 / 𝑀 ) ) ↑ 𝑀 ) )
124 121 123 breqtrd ⊢ ( 𝜑 → ( 1 + ( - ( 𝐸 / 𝑀 ) · 𝑀 ) ) ≤ ( ( 1 − ( 𝐸 / 𝑀 ) ) ↑ 𝑀 ) )
125 86 124 eqbrtrd ⊢ ( 𝜑 → ( 1 − 𝐸 ) ≤ ( ( 1 − ( 𝐸 / 𝑀 ) ) ↑ 𝑀 ) )
126 125 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → ( 1 − 𝐸 ) ≤ ( ( 1 − ( 𝐸 / 𝑀 ) ) ↑ 𝑀 ) )
127 eqid ⊢ seq 1 ( · , ( 𝐹 ‘ 𝑡 ) ) = seq 1 ( · , ( 𝐹 ‘ 𝑡 ) )
128 8 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → 𝑀 ∈ ℕ )
129 eqid ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ) = ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) )
130 31 66 129 fmptdf ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ) : ( 1 ... 𝑀 ) ⟶ ℝ )
131 54 feq1d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑡 ) : ( 1 ... 𝑀 ) ⟶ ℝ ↔ ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) ) : ( 1 ... 𝑀 ) ⟶ ℝ ) )
132 130 131 mpbird ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑡 ) : ( 1 ... 𝑀 ) ⟶ ℝ )
133 10 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑡 ∈ 𝐵 ) → ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) )
134 133 an32s ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑈 ‘ 𝑖 ) ‘ 𝑡 ) )
135 134 67 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝐹 ‘ 𝑡 ) ‘ 𝑖 ) )
136 80 addid2d ⊢ ( 𝜑 → ( 0 + ( 𝐸 / 𝑀 ) ) = ( 𝐸 / 𝑀 ) )
137 lediv2 ⊢ ( ( ( 1 ∈ ℝ ∧ 0 < 1 ) ∧ ( 𝑀 ∈ ℝ ∧ 0 < 𝑀 ) ∧ ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) ) → ( 1 ≤ 𝑀 ↔ ( 𝐸 / 𝑀 ) ≤ ( 𝐸 / 1 ) ) )
138 17 97 88 110 109 137 syl221anc ⊢ ( 𝜑 → ( 1 ≤ 𝑀 ↔ ( 𝐸 / 𝑀 ) ≤ ( 𝐸 / 1 ) ) )
139 106 138 mpbid ⊢ ( 𝜑 → ( 𝐸 / 𝑀 ) ≤ ( 𝐸 / 1 ) )
140 73 div1d ⊢ ( 𝜑 → ( 𝐸 / 1 ) = 𝐸 )
141 139 140 breqtrd ⊢ ( 𝜑 → ( 𝐸 / 𝑀 ) ≤ 𝐸 )
142 21 18 17 141 105 lelttrd ⊢ ( 𝜑 → ( 𝐸 / 𝑀 ) < 1 )
143 136 142 eqbrtrd ⊢ ( 𝜑 → ( 0 + ( 𝐸 / 𝑀 ) ) < 1 )
144 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
145 144 21 17 ltaddsubd ⊢ ( 𝜑 → ( ( 0 + ( 𝐸 / 𝑀 ) ) < 1 ↔ 0 < ( 1 − ( 𝐸 / 𝑀 ) ) ) )
146 143 145 mpbid ⊢ ( 𝜑 → 0 < ( 1 − ( 𝐸 / 𝑀 ) ) )
147 22 146 elrpd ⊢ ( 𝜑 → ( 1 − ( 𝐸 / 𝑀 ) ) ∈ ℝ+ )
148 147 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → ( 1 − ( 𝐸 / 𝑀 ) ) ∈ ℝ+ )
149 39 31 127 128 132 135 148 stoweidlem3 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → ( ( 1 − ( 𝐸 / 𝑀 ) ) ↑ 𝑀 ) < ( seq 1 ( · , ( 𝐹 ‘ 𝑡 ) ) ‘ 𝑀 ) )
150 20 26 72 126 149 lelttrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → ( 1 − 𝐸 ) < ( seq 1 ( · , ( 𝐹 ‘ 𝑡 ) ) ‘ 𝑀 ) )
151 7 fvmpt2 ⊢ ( ( 𝑡 ∈ 𝑇 ∧ ( seq 1 ( · , ( 𝐹 ‘ 𝑡 ) ) ‘ 𝑀 ) ∈ ℝ ) → ( 𝑍 ‘ 𝑡 ) = ( seq 1 ( · , ( 𝐹 ‘ 𝑡 ) ) ‘ 𝑀 ) )
152 49 72 151 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → ( 𝑍 ‘ 𝑡 ) = ( seq 1 ( · , ( 𝐹 ‘ 𝑡 ) ) ‘ 𝑀 ) )
153 150 152 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → ( 1 − 𝐸 ) < ( 𝑍 ‘ 𝑡 ) )
154 simpl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → 𝜑 )
155 1 3 4 5 6 7 15 8 9 13 14 fmuldfeq ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑋 ‘ 𝑡 ) = ( 𝑍 ‘ 𝑡 ) )
156 154 49 155 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → ( 𝑋 ‘ 𝑡 ) = ( 𝑍 ‘ 𝑡 ) )
157 153 156 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → ( 1 − 𝐸 ) < ( 𝑋 ‘ 𝑡 ) )
158 157 ex ⊢ ( 𝜑 → ( 𝑡 ∈ 𝐵 → ( 1 − 𝐸 ) < ( 𝑋 ‘ 𝑡 ) ) )
159 2 158 ralrimi ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝐵 ( 1 − 𝐸 ) < ( 𝑋 ‘ 𝑡 ) )