Theorem fmul01lt1lem2

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