Theorem fmul01lt1lem2

Description: Given a finite multiplication of values between 0 and 1, a value E larger than any multiplicand, is larger than the whole multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	fmul01lt1lem2.1	⊢ Ⅎ 𝑖 𝐵
	fmul01lt1lem2.2	⊢ Ⅎ 𝑖 𝜑
	fmul01lt1lem2.3	⊢ 𝐴 = seq 𝐿 ( · , 𝐵 )
	fmul01lt1lem2.4	⊢ ( 𝜑 → 𝐿 ∈ ℤ )
	fmul01lt1lem2.5	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝐿 ) )
	fmul01lt1lem2.6	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ )
	fmul01lt1lem2.7	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → 0 ≤ ( 𝐵 ‘ 𝑖 ) )
	fmul01lt1lem2.8	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ≤ 1 )
	fmul01lt1lem2.9	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
	fmul01lt1lem2.10	⊢ ( 𝜑 → 𝐽 ∈ ( 𝐿 ... 𝑀 ) )
	fmul01lt1lem2.11	⊢ ( 𝜑 → ( 𝐵 ‘ 𝐽 ) < 𝐸 )
Assertion	fmul01lt1lem2	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑀 ) < 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		fmul01lt1lem2.1	⊢ Ⅎ 𝑖 𝐵
2		fmul01lt1lem2.2	⊢ Ⅎ 𝑖 𝜑
3		fmul01lt1lem2.3	⊢ 𝐴 = seq 𝐿 ( · , 𝐵 )
4		fmul01lt1lem2.4	⊢ ( 𝜑 → 𝐿 ∈ ℤ )
5		fmul01lt1lem2.5	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝐿 ) )
6		fmul01lt1lem2.6	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ )
7		fmul01lt1lem2.7	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → 0 ≤ ( 𝐵 ‘ 𝑖 ) )
8		fmul01lt1lem2.8	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ≤ 1 )
9		fmul01lt1lem2.9	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
10		fmul01lt1lem2.10	⊢ ( 𝜑 → 𝐽 ∈ ( 𝐿 ... 𝑀 ) )
11		fmul01lt1lem2.11	⊢ ( 𝜑 → ( 𝐵 ‘ 𝐽 ) < 𝐸 )
12		nfv	⊢ Ⅎ 𝑖 𝐽 = 𝐿
13	2 12	nfan	⊢ Ⅎ 𝑖 ( 𝜑 ∧ 𝐽 = 𝐿 )
14	4	adantr	⊢ ( ( 𝜑 ∧ 𝐽 = 𝐿 ) → 𝐿 ∈ ℤ )
15	5	adantr	⊢ ( ( 𝜑 ∧ 𝐽 = 𝐿 ) → 𝑀 ∈ ( ℤ≥ ‘ 𝐿 ) )
16	6	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐽 = 𝐿 ) ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ )
17	7	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐽 = 𝐿 ) ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → 0 ≤ ( 𝐵 ‘ 𝑖 ) )
18	8	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐽 = 𝐿 ) ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ≤ 1 )
19	9	adantr	⊢ ( ( 𝜑 ∧ 𝐽 = 𝐿 ) → 𝐸 ∈ ℝ+ )
20		simpr	⊢ ( ( 𝜑 ∧ 𝐽 = 𝐿 ) → 𝐽 = 𝐿 )
21	20	fveq2d	⊢ ( ( 𝜑 ∧ 𝐽 = 𝐿 ) → ( 𝐵 ‘ 𝐽 ) = ( 𝐵 ‘ 𝐿 ) )
22	11	adantr	⊢ ( ( 𝜑 ∧ 𝐽 = 𝐿 ) → ( 𝐵 ‘ 𝐽 ) < 𝐸 )
23	21 22	eqbrtrrd	⊢ ( ( 𝜑 ∧ 𝐽 = 𝐿 ) → ( 𝐵 ‘ 𝐿 ) < 𝐸 )
24	1 13 3 14 15 16 17 18 19 23	fmul01lt1lem1	⊢ ( ( 𝜑 ∧ 𝐽 = 𝐿 ) → ( 𝐴 ‘ 𝑀 ) < 𝐸 )
25	3	fveq1i	⊢ ( 𝐴 ‘ 𝑀 ) = ( seq 𝐿 ( · , 𝐵 ) ‘ 𝑀 )
26		nfv	⊢ Ⅎ 𝑖 𝑎 ∈ ( 𝐿 ... 𝑀 )
27	2 26	nfan	⊢ Ⅎ 𝑖 ( 𝜑 ∧ 𝑎 ∈ ( 𝐿 ... 𝑀 ) )
28		nfcv	⊢ Ⅎ 𝑖 𝑎
29	1 28	nffv	⊢ Ⅎ 𝑖 ( 𝐵 ‘ 𝑎 )
30	29	nfel1	⊢ Ⅎ 𝑖 ( 𝐵 ‘ 𝑎 ) ∈ ℝ
31	27 30	nfim	⊢ Ⅎ 𝑖 ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑎 ) ∈ ℝ )
32		eleq1w	⊢ ( 𝑖 = 𝑎 → ( 𝑖 ∈ ( 𝐿 ... 𝑀 ) ↔ 𝑎 ∈ ( 𝐿 ... 𝑀 ) ) )
33	32	anbi2d	⊢ ( 𝑖 = 𝑎 → ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) ↔ ( 𝜑 ∧ 𝑎 ∈ ( 𝐿 ... 𝑀 ) ) ) )
34		fveq2	⊢ ( 𝑖 = 𝑎 → ( 𝐵 ‘ 𝑖 ) = ( 𝐵 ‘ 𝑎 ) )
35	34	eleq1d	⊢ ( 𝑖 = 𝑎 → ( ( 𝐵 ‘ 𝑖 ) ∈ ℝ ↔ ( 𝐵 ‘ 𝑎 ) ∈ ℝ ) )
36	33 35	imbi12d	⊢ ( 𝑖 = 𝑎 → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ ) ↔ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑎 ) ∈ ℝ ) ) )
37	31 36 6	chvarfv	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑎 ) ∈ ℝ )
38		remulcl	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑗 ∈ ℝ ) → ( 𝑎 · 𝑗 ) ∈ ℝ )
39	38	adantl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) → ( 𝑎 · 𝑗 ) ∈ ℝ )
40	5 37 39	seqcl	⊢ ( 𝜑 → ( seq 𝐿 ( · , 𝐵 ) ‘ 𝑀 ) ∈ ℝ )
41	40	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( seq 𝐿 ( · , 𝐵 ) ‘ 𝑀 ) ∈ ℝ )
42		elfzuz3	⊢ ( 𝐽 ∈ ( 𝐿 ... 𝑀 ) → 𝑀 ∈ ( ℤ≥ ‘ 𝐽 ) )
43	10 42	syl	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝐽 ) )
44		nfv	⊢ Ⅎ 𝑖 𝑎 ∈ ( 𝐽 ... 𝑀 )
45	2 44	nfan	⊢ Ⅎ 𝑖 ( 𝜑 ∧ 𝑎 ∈ ( 𝐽 ... 𝑀 ) )
46	45 30	nfim	⊢ Ⅎ 𝑖 ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐽 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑎 ) ∈ ℝ )
47		eleq1w	⊢ ( 𝑖 = 𝑎 → ( 𝑖 ∈ ( 𝐽 ... 𝑀 ) ↔ 𝑎 ∈ ( 𝐽 ... 𝑀 ) ) )
48	47	anbi2d	⊢ ( 𝑖 = 𝑎 → ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐽 ... 𝑀 ) ) ↔ ( 𝜑 ∧ 𝑎 ∈ ( 𝐽 ... 𝑀 ) ) ) )
49	48 35	imbi12d	⊢ ( 𝑖 = 𝑎 → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐽 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ ) ↔ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐽 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑎 ) ∈ ℝ ) ) )
50	4	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐽 ... 𝑀 ) ) → 𝐿 ∈ ℤ )
51		eluzelz	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝐿 ) → 𝑀 ∈ ℤ )
52	5 51	syl	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
53	52	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐽 ... 𝑀 ) ) → 𝑀 ∈ ℤ )
54		elfzelz	⊢ ( 𝑖 ∈ ( 𝐽 ... 𝑀 ) → 𝑖 ∈ ℤ )
55	54	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐽 ... 𝑀 ) ) → 𝑖 ∈ ℤ )
56	4	zred	⊢ ( 𝜑 → 𝐿 ∈ ℝ )
57	56	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐽 ... 𝑀 ) ) → 𝐿 ∈ ℝ )
58		elfzelz	⊢ ( 𝐽 ∈ ( 𝐿 ... 𝑀 ) → 𝐽 ∈ ℤ )
59	10 58	syl	⊢ ( 𝜑 → 𝐽 ∈ ℤ )
60	59	zred	⊢ ( 𝜑 → 𝐽 ∈ ℝ )
61	60	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐽 ... 𝑀 ) ) → 𝐽 ∈ ℝ )
62	54	zred	⊢ ( 𝑖 ∈ ( 𝐽 ... 𝑀 ) → 𝑖 ∈ ℝ )
63	62	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐽 ... 𝑀 ) ) → 𝑖 ∈ ℝ )
64		elfzle1	⊢ ( 𝐽 ∈ ( 𝐿 ... 𝑀 ) → 𝐿 ≤ 𝐽 )
65	10 64	syl	⊢ ( 𝜑 → 𝐿 ≤ 𝐽 )
66	65	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐽 ... 𝑀 ) ) → 𝐿 ≤ 𝐽 )
67		elfzle1	⊢ ( 𝑖 ∈ ( 𝐽 ... 𝑀 ) → 𝐽 ≤ 𝑖 )
68	67	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐽 ... 𝑀 ) ) → 𝐽 ≤ 𝑖 )
69	57 61 63 66 68	letrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐽 ... 𝑀 ) ) → 𝐿 ≤ 𝑖 )
70		elfzle2	⊢ ( 𝑖 ∈ ( 𝐽 ... 𝑀 ) → 𝑖 ≤ 𝑀 )
71	70	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐽 ... 𝑀 ) ) → 𝑖 ≤ 𝑀 )
72	50 53 55 69 71	elfzd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐽 ... 𝑀 ) ) → 𝑖 ∈ ( 𝐿 ... 𝑀 ) )
73	72 6	syldan	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐽 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ )
74	46 49 73	chvarfv	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐽 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑎 ) ∈ ℝ )
75	43 74 39	seqcl	⊢ ( 𝜑 → ( seq 𝐽 ( · , 𝐵 ) ‘ 𝑀 ) ∈ ℝ )
76	75	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( seq 𝐽 ( · , 𝐵 ) ‘ 𝑀 ) ∈ ℝ )
77	9	rpred	⊢ ( 𝜑 → 𝐸 ∈ ℝ )
78	77	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → 𝐸 ∈ ℝ )
79		remulcl	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( 𝑎 · 𝑏 ) ∈ ℝ )
80	79	adantl	⊢ ( ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ) → ( 𝑎 · 𝑏 ) ∈ ℝ )
81		simp1	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ ) → 𝑎 ∈ ℝ )
82	81	recnd	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ ) → 𝑎 ∈ ℂ )
83		simp2	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ ) → 𝑏 ∈ ℝ )
84	83	recnd	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ ) → 𝑏 ∈ ℂ )
85		simp3	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ ) → 𝑐 ∈ ℝ )
86	85	recnd	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ ) → 𝑐 ∈ ℂ )
87	82 84 86	mulassd	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ ) → ( ( 𝑎 · 𝑏 ) · 𝑐 ) = ( 𝑎 · ( 𝑏 · 𝑐 ) ) )
88	87	adantl	⊢ ( ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ ) ) → ( ( 𝑎 · 𝑏 ) · 𝑐 ) = ( 𝑎 · ( 𝑏 · 𝑐 ) ) )
89	59	zcnd	⊢ ( 𝜑 → 𝐽 ∈ ℂ )
90		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
91	89 90	npcand	⊢ ( 𝜑 → ( ( 𝐽 − 1 ) + 1 ) = 𝐽 )
92	91	fveq2d	⊢ ( 𝜑 → ( ℤ≥ ‘ ( ( 𝐽 − 1 ) + 1 ) ) = ( ℤ≥ ‘ 𝐽 ) )
93	43 92	eleqtrrd	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ ( ( 𝐽 − 1 ) + 1 ) ) )
94	93	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → 𝑀 ∈ ( ℤ≥ ‘ ( ( 𝐽 − 1 ) + 1 ) ) )
95	4	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → 𝐿 ∈ ℤ )
96	59	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → 𝐽 ∈ ℤ )
97		1zzd	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → 1 ∈ ℤ )
98	96 97	zsubcld	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( 𝐽 − 1 ) ∈ ℤ )
99		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ¬ 𝐽 = 𝐿 )
100		eqcom	⊢ ( 𝐽 = 𝐿 ↔ 𝐿 = 𝐽 )
101	99 100	sylnib	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ¬ 𝐿 = 𝐽 )
102	56 60	leloed	⊢ ( 𝜑 → ( 𝐿 ≤ 𝐽 ↔ ( 𝐿 < 𝐽 ∨ 𝐿 = 𝐽 ) ) )
103	65 102	mpbid	⊢ ( 𝜑 → ( 𝐿 < 𝐽 ∨ 𝐿 = 𝐽 ) )
104	103	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( 𝐿 < 𝐽 ∨ 𝐿 = 𝐽 ) )
105		orel2	⊢ ( ¬ 𝐿 = 𝐽 → ( ( 𝐿 < 𝐽 ∨ 𝐿 = 𝐽 ) → 𝐿 < 𝐽 ) )
106	101 104 105	sylc	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → 𝐿 < 𝐽 )
107		zltlem1	⊢ ( ( 𝐿 ∈ ℤ ∧ 𝐽 ∈ ℤ ) → ( 𝐿 < 𝐽 ↔ 𝐿 ≤ ( 𝐽 − 1 ) ) )
108	4 59 107	syl2anc	⊢ ( 𝜑 → ( 𝐿 < 𝐽 ↔ 𝐿 ≤ ( 𝐽 − 1 ) ) )
109	108	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( 𝐿 < 𝐽 ↔ 𝐿 ≤ ( 𝐽 − 1 ) ) )
110	106 109	mpbid	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → 𝐿 ≤ ( 𝐽 − 1 ) )
111		eluz2	⊢ ( ( 𝐽 − 1 ) ∈ ( ℤ≥ ‘ 𝐿 ) ↔ ( 𝐿 ∈ ℤ ∧ ( 𝐽 − 1 ) ∈ ℤ ∧ 𝐿 ≤ ( 𝐽 − 1 ) ) )
112	95 98 110 111	syl3anbrc	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( 𝐽 − 1 ) ∈ ( ℤ≥ ‘ 𝐿 ) )
113		nfv	⊢ Ⅎ 𝑖 ¬ 𝐽 = 𝐿
114	2 113	nfan	⊢ Ⅎ 𝑖 ( 𝜑 ∧ ¬ 𝐽 = 𝐿 )
115	114 26	nfan	⊢ Ⅎ 𝑖 ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) ∧ 𝑎 ∈ ( 𝐿 ... 𝑀 ) )
116	115 30	nfim	⊢ Ⅎ 𝑖 ( ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) ∧ 𝑎 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑎 ) ∈ ℝ )
117	32	anbi2d	⊢ ( 𝑖 = 𝑎 → ( ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) ↔ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) ∧ 𝑎 ∈ ( 𝐿 ... 𝑀 ) ) ) )
118	117 35	imbi12d	⊢ ( 𝑖 = 𝑎 → ( ( ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ ) ↔ ( ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) ∧ 𝑎 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑎 ) ∈ ℝ ) ) )
119	6	adantlr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ )
120	116 118 119	chvarfv	⊢ ( ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) ∧ 𝑎 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑎 ) ∈ ℝ )
121	80 88 94 112 120	seqsplit	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( seq 𝐿 ( · , 𝐵 ) ‘ 𝑀 ) = ( ( seq 𝐿 ( · , 𝐵 ) ‘ ( 𝐽 − 1 ) ) · ( seq ( ( 𝐽 − 1 ) + 1 ) ( · , 𝐵 ) ‘ 𝑀 ) ) )
122	91	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( ( 𝐽 − 1 ) + 1 ) = 𝐽 )
123	122	seqeq1d	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → seq ( ( 𝐽 − 1 ) + 1 ) ( · , 𝐵 ) = seq 𝐽 ( · , 𝐵 ) )
124	123	fveq1d	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( seq ( ( 𝐽 − 1 ) + 1 ) ( · , 𝐵 ) ‘ 𝑀 ) = ( seq 𝐽 ( · , 𝐵 ) ‘ 𝑀 ) )
125	124	oveq2d	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( ( seq 𝐿 ( · , 𝐵 ) ‘ ( 𝐽 − 1 ) ) · ( seq ( ( 𝐽 − 1 ) + 1 ) ( · , 𝐵 ) ‘ 𝑀 ) ) = ( ( seq 𝐿 ( · , 𝐵 ) ‘ ( 𝐽 − 1 ) ) · ( seq 𝐽 ( · , 𝐵 ) ‘ 𝑀 ) ) )
126	121 125	eqtrd	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( seq 𝐿 ( · , 𝐵 ) ‘ 𝑀 ) = ( ( seq 𝐿 ( · , 𝐵 ) ‘ ( 𝐽 − 1 ) ) · ( seq 𝐽 ( · , 𝐵 ) ‘ 𝑀 ) ) )
127		nfv	⊢ Ⅎ 𝑖 𝑎 ∈ ( 𝐿 ... ( 𝐽 − 1 ) )
128	114 127	nfan	⊢ Ⅎ 𝑖 ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) ∧ 𝑎 ∈ ( 𝐿 ... ( 𝐽 − 1 ) ) )
129	128 30	nfim	⊢ Ⅎ 𝑖 ( ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) ∧ 𝑎 ∈ ( 𝐿 ... ( 𝐽 − 1 ) ) ) → ( 𝐵 ‘ 𝑎 ) ∈ ℝ )
130		eleq1w	⊢ ( 𝑖 = 𝑎 → ( 𝑖 ∈ ( 𝐿 ... ( 𝐽 − 1 ) ) ↔ 𝑎 ∈ ( 𝐿 ... ( 𝐽 − 1 ) ) ) )
131	130	anbi2d	⊢ ( 𝑖 = 𝑎 → ( ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) ∧ 𝑖 ∈ ( 𝐿 ... ( 𝐽 − 1 ) ) ) ↔ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) ∧ 𝑎 ∈ ( 𝐿 ... ( 𝐽 − 1 ) ) ) ) )
132	131 35	imbi12d	⊢ ( 𝑖 = 𝑎 → ( ( ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) ∧ 𝑖 ∈ ( 𝐿 ... ( 𝐽 − 1 ) ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ ) ↔ ( ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) ∧ 𝑎 ∈ ( 𝐿 ... ( 𝐽 − 1 ) ) ) → ( 𝐵 ‘ 𝑎 ) ∈ ℝ ) ) )
133	4	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... ( 𝐽 − 1 ) ) ) → 𝐿 ∈ ℤ )
134	52	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... ( 𝐽 − 1 ) ) ) → 𝑀 ∈ ℤ )
135		elfzelz	⊢ ( 𝑖 ∈ ( 𝐿 ... ( 𝐽 − 1 ) ) → 𝑖 ∈ ℤ )
136	135	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... ( 𝐽 − 1 ) ) ) → 𝑖 ∈ ℤ )
137		elfzle1	⊢ ( 𝑖 ∈ ( 𝐿 ... ( 𝐽 − 1 ) ) → 𝐿 ≤ 𝑖 )
138	137	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... ( 𝐽 − 1 ) ) ) → 𝐿 ≤ 𝑖 )
139	135	zred	⊢ ( 𝑖 ∈ ( 𝐿 ... ( 𝐽 − 1 ) ) → 𝑖 ∈ ℝ )
140	139	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... ( 𝐽 − 1 ) ) ) → 𝑖 ∈ ℝ )
141	60	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... ( 𝐽 − 1 ) ) ) → 𝐽 ∈ ℝ )
142	52	zred	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
143	142	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... ( 𝐽 − 1 ) ) ) → 𝑀 ∈ ℝ )
144		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
145	60 144	resubcld	⊢ ( 𝜑 → ( 𝐽 − 1 ) ∈ ℝ )
146	145	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... ( 𝐽 − 1 ) ) ) → ( 𝐽 − 1 ) ∈ ℝ )
147		elfzle2	⊢ ( 𝑖 ∈ ( 𝐿 ... ( 𝐽 − 1 ) ) → 𝑖 ≤ ( 𝐽 − 1 ) )
148	147	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... ( 𝐽 − 1 ) ) ) → 𝑖 ≤ ( 𝐽 − 1 ) )
149	60	lem1d	⊢ ( 𝜑 → ( 𝐽 − 1 ) ≤ 𝐽 )
150	149	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... ( 𝐽 − 1 ) ) ) → ( 𝐽 − 1 ) ≤ 𝐽 )
151	140 146 141 148 150	letrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... ( 𝐽 − 1 ) ) ) → 𝑖 ≤ 𝐽 )
152		elfzle2	⊢ ( 𝐽 ∈ ( 𝐿 ... 𝑀 ) → 𝐽 ≤ 𝑀 )
153	10 152	syl	⊢ ( 𝜑 → 𝐽 ≤ 𝑀 )
154	153	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... ( 𝐽 − 1 ) ) ) → 𝐽 ≤ 𝑀 )
155	140 141 143 151 154	letrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... ( 𝐽 − 1 ) ) ) → 𝑖 ≤ 𝑀 )
156	133 134 136 138 155	elfzd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... ( 𝐽 − 1 ) ) ) → 𝑖 ∈ ( 𝐿 ... 𝑀 ) )
157	156 6	syldan	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... ( 𝐽 − 1 ) ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ )
158	157	adantlr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) ∧ 𝑖 ∈ ( 𝐿 ... ( 𝐽 − 1 ) ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ )
159	129 132 158	chvarfv	⊢ ( ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) ∧ 𝑎 ∈ ( 𝐿 ... ( 𝐽 − 1 ) ) ) → ( 𝐵 ‘ 𝑎 ) ∈ ℝ )
160	38	adantl	⊢ ( ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑗 ∈ ℝ ) ) → ( 𝑎 · 𝑗 ) ∈ ℝ )
161	112 159 160	seqcl	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( seq 𝐿 ( · , 𝐵 ) ‘ ( 𝐽 − 1 ) ) ∈ ℝ )
162		1red	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → 1 ∈ ℝ )
163		eqid	⊢ seq 𝐽 ( · , 𝐵 ) = seq 𝐽 ( · , 𝐵 )
164	43	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → 𝑀 ∈ ( ℤ≥ ‘ 𝐽 ) )
165		eluzfz2	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝐽 ) → 𝑀 ∈ ( 𝐽 ... 𝑀 ) )
166	43 165	syl	⊢ ( 𝜑 → 𝑀 ∈ ( 𝐽 ... 𝑀 ) )
167	166	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → 𝑀 ∈ ( 𝐽 ... 𝑀 ) )
168	73	adantlr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) ∧ 𝑖 ∈ ( 𝐽 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ )
169	72 7	syldan	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐽 ... 𝑀 ) ) → 0 ≤ ( 𝐵 ‘ 𝑖 ) )
170	169	adantlr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) ∧ 𝑖 ∈ ( 𝐽 ... 𝑀 ) ) → 0 ≤ ( 𝐵 ‘ 𝑖 ) )
171	72 8	syldan	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐽 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ≤ 1 )
172	171	adantlr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) ∧ 𝑖 ∈ ( 𝐽 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ≤ 1 )
173	1 114 163 96 164 167 168 170 172	fmul01	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( 0 ≤ ( seq 𝐽 ( · , 𝐵 ) ‘ 𝑀 ) ∧ ( seq 𝐽 ( · , 𝐵 ) ‘ 𝑀 ) ≤ 1 ) )
174	173	simpld	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → 0 ≤ ( seq 𝐽 ( · , 𝐵 ) ‘ 𝑀 ) )
175		eqid	⊢ seq 𝐿 ( · , 𝐵 ) = seq 𝐿 ( · , 𝐵 )
176	5	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → 𝑀 ∈ ( ℤ≥ ‘ 𝐿 ) )
177		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
178	59 177	zsubcld	⊢ ( 𝜑 → ( 𝐽 − 1 ) ∈ ℤ )
179	4 52 178	3jca	⊢ ( 𝜑 → ( 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( 𝐽 − 1 ) ∈ ℤ ) )
180	179	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( 𝐽 − 1 ) ∈ ℤ ) )
181	145 60 142	3jca	⊢ ( 𝜑 → ( ( 𝐽 − 1 ) ∈ ℝ ∧ 𝐽 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
182	181	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( ( 𝐽 − 1 ) ∈ ℝ ∧ 𝐽 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
183	60	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → 𝐽 ∈ ℝ )
184	183	lem1d	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( 𝐽 − 1 ) ≤ 𝐽 )
185	153	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → 𝐽 ≤ 𝑀 )
186	184 185	jca	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( ( 𝐽 − 1 ) ≤ 𝐽 ∧ 𝐽 ≤ 𝑀 ) )
187		letr	⊢ ( ( ( 𝐽 − 1 ) ∈ ℝ ∧ 𝐽 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( ( ( 𝐽 − 1 ) ≤ 𝐽 ∧ 𝐽 ≤ 𝑀 ) → ( 𝐽 − 1 ) ≤ 𝑀 ) )
188	182 186 187	sylc	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( 𝐽 − 1 ) ≤ 𝑀 )
189	110 188	jca	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( 𝐿 ≤ ( 𝐽 − 1 ) ∧ ( 𝐽 − 1 ) ≤ 𝑀 ) )
190		elfz2	⊢ ( ( 𝐽 − 1 ) ∈ ( 𝐿 ... 𝑀 ) ↔ ( ( 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( 𝐽 − 1 ) ∈ ℤ ) ∧ ( 𝐿 ≤ ( 𝐽 − 1 ) ∧ ( 𝐽 − 1 ) ≤ 𝑀 ) ) )
191	180 189 190	sylanbrc	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( 𝐽 − 1 ) ∈ ( 𝐿 ... 𝑀 ) )
192	7	adantlr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → 0 ≤ ( 𝐵 ‘ 𝑖 ) )
193	8	adantlr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ≤ 1 )
194	1 114 175 95 176 191 119 192 193	fmul01	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( 0 ≤ ( seq 𝐿 ( · , 𝐵 ) ‘ ( 𝐽 − 1 ) ) ∧ ( seq 𝐿 ( · , 𝐵 ) ‘ ( 𝐽 − 1 ) ) ≤ 1 ) )
195	194	simprd	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( seq 𝐿 ( · , 𝐵 ) ‘ ( 𝐽 − 1 ) ) ≤ 1 )
196	161 162 76 174 195	lemul1ad	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( ( seq 𝐿 ( · , 𝐵 ) ‘ ( 𝐽 − 1 ) ) · ( seq 𝐽 ( · , 𝐵 ) ‘ 𝑀 ) ) ≤ ( 1 · ( seq 𝐽 ( · , 𝐵 ) ‘ 𝑀 ) ) )
197	126 196	eqbrtrd	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( seq 𝐿 ( · , 𝐵 ) ‘ 𝑀 ) ≤ ( 1 · ( seq 𝐽 ( · , 𝐵 ) ‘ 𝑀 ) ) )
198	76	recnd	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( seq 𝐽 ( · , 𝐵 ) ‘ 𝑀 ) ∈ ℂ )
199	198	mullidd	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( 1 · ( seq 𝐽 ( · , 𝐵 ) ‘ 𝑀 ) ) = ( seq 𝐽 ( · , 𝐵 ) ‘ 𝑀 ) )
200	197 199	breqtrd	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( seq 𝐿 ( · , 𝐵 ) ‘ 𝑀 ) ≤ ( seq 𝐽 ( · , 𝐵 ) ‘ 𝑀 ) )
201	1 2 163 59 43 73 169 171 9 11	fmul01lt1lem1	⊢ ( 𝜑 → ( seq 𝐽 ( · , 𝐵 ) ‘ 𝑀 ) < 𝐸 )
202	201	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( seq 𝐽 ( · , 𝐵 ) ‘ 𝑀 ) < 𝐸 )
203	41 76 78 200 202	lelttrd	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( seq 𝐿 ( · , 𝐵 ) ‘ 𝑀 ) < 𝐸 )
204	25 203	eqbrtrid	⊢ ( ( 𝜑 ∧ ¬ 𝐽 = 𝐿 ) → ( 𝐴 ‘ 𝑀 ) < 𝐸 )
205	24 204	pm2.61dan	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑀 ) < 𝐸 )