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	$⊢ \underline{Ⅎ} i B$
	fmul01lt1lem2.2	$⊢ Ⅎ i φ$
	fmul01lt1lem2.3	$⊢ A = seq L (\times B)$
	fmul01lt1lem2.4	$⊢ φ \to L \in ℤ$
	fmul01lt1lem2.5	$⊢ φ \to M \in ℤ_{\geq L}$
	fmul01lt1lem2.6	$⊢ (φ \land i \in (L \dots M)) \to B (i) \in ℝ$
	fmul01lt1lem2.7	$⊢ (φ \land i \in (L \dots M)) \to 0 \leq B (i)$
	fmul01lt1lem2.8	$⊢ (φ \land i \in (L \dots M)) \to B (i) \leq 1$
	fmul01lt1lem2.9	$⊢ φ \to E \in ℝ^{+}$
	fmul01lt1lem2.10	$⊢ φ \to J \in (L \dots M)$
	fmul01lt1lem2.11	$⊢ φ \to B (J) < E$
Assertion	fmul01lt1lem2	$⊢ φ \to A (M) < E$

Proof

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

Metamath Proof Explorer

Theorem fmul01lt1lem2

Proof