fmul01lt1lem2 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > fmul01lt1lem2		Structured version Visualization version GIF version

Theorem fmul01lt1lem2 39817

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

**Hypotheses**
Ref	Expression
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**
Ref	Expression
fmul01lt1lem2	⊢ (𝜑 → (𝐴‘𝑀) < 𝐸)

Distinct variable groups: 𝑖,𝐽 𝑖,𝐿 𝑖,𝑀 Allowed substitution hints: 𝜑(𝑖) 𝐴(𝑖) 𝐵(𝑖) 𝐸(𝑖)

Proof of Theorem fmul01lt1lem2 Dummy variables 𝑎 𝑏 𝑐 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fmul01lt1lem2.1	. . 3 ⊢ Ⅎ𝑖𝐵
2		fmul01lt1lem2.2	. . . 4 ⊢ Ⅎ𝑖𝜑
3		nfv 1843	. . . 4 ⊢ Ⅎ𝑖 𝐽 = 𝐿
4	2, 3	nfan 1828	. . 3 ⊢ Ⅎ𝑖(𝜑 ∧ 𝐽 = 𝐿)
5		fmul01lt1lem2.3	. . 3 ⊢ 𝐴 = seq𝐿( · , 𝐵)
6		fmul01lt1lem2.4	. . . 4 ⊢ (𝜑 → 𝐿 ∈ ℤ)
7	6	adantr 481	. . 3 ⊢ ((𝜑 ∧ 𝐽 = 𝐿) → 𝐿 ∈ ℤ)
8		fmul01lt1lem2.5	. . . 4 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘𝐿))
9	8	adantr 481	. . 3 ⊢ ((𝜑 ∧ 𝐽 = 𝐿) → 𝑀 ∈ (ℤ_≥‘𝐿))
10		fmul01lt1lem2.6	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ∈ ℝ)
11	10	adantlr 751	. . 3 ⊢ (((𝜑 ∧ 𝐽 = 𝐿) ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ∈ ℝ)
12		fmul01lt1lem2.7	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → 0 ≤ (𝐵‘𝑖))
13	12	adantlr 751	. . 3 ⊢ (((𝜑 ∧ 𝐽 = 𝐿) ∧ 𝑖 ∈ (𝐿...𝑀)) → 0 ≤ (𝐵‘𝑖))
14		fmul01lt1lem2.8	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ≤ 1)
15	14	adantlr 751	. . 3 ⊢ (((𝜑 ∧ 𝐽 = 𝐿) ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ≤ 1)
16		fmul01lt1lem2.9	. . . 4 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
17	16	adantr 481	. . 3 ⊢ ((𝜑 ∧ 𝐽 = 𝐿) → 𝐸 ∈ ℝ⁺)
18		simpr 477	. . . . 5 ⊢ ((𝜑 ∧ 𝐽 = 𝐿) → 𝐽 = 𝐿)
19	18	fveq2d 6195	. . . 4 ⊢ ((𝜑 ∧ 𝐽 = 𝐿) → (𝐵‘𝐽) = (𝐵‘𝐿))
20		fmul01lt1lem2.11	. . . . 5 ⊢ (𝜑 → (𝐵‘𝐽) < 𝐸)
21	20	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝐽 = 𝐿) → (𝐵‘𝐽) < 𝐸)
22	19, 21	eqbrtrrd 4677	. . 3 ⊢ ((𝜑 ∧ 𝐽 = 𝐿) → (𝐵‘𝐿) < 𝐸)
23	1, 4, 5, 7, 9, 11, 13, 15, 17, 22	fmul01lt1lem1 39816	. 2 ⊢ ((𝜑 ∧ 𝐽 = 𝐿) → (𝐴‘𝑀) < 𝐸)
24	5	fveq1i 6192	. . 3 ⊢ (𝐴‘𝑀) = (seq𝐿( · , 𝐵)‘𝑀)
25		nfv 1843	. . . . . . . . 9 ⊢ Ⅎ𝑖 𝑎 ∈ (𝐿...𝑀)
26	2, 25	nfan 1828	. . . . . . . 8 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑎 ∈ (𝐿...𝑀))
27		nfcv 2764	. . . . . . . . . 10 ⊢ Ⅎ𝑖𝑎
28	1, 27	nffv 6198	. . . . . . . . 9 ⊢ Ⅎ𝑖(𝐵‘𝑎)
29	28	nfel1 2779	. . . . . . . 8 ⊢ Ⅎ𝑖(𝐵‘𝑎) ∈ ℝ
30	26, 29	nfim 1825	. . . . . . 7 ⊢ Ⅎ𝑖((𝜑 ∧ 𝑎 ∈ (𝐿...𝑀)) → (𝐵‘𝑎) ∈ ℝ)
31		eleq1 2689	. . . . . . . . 9 ⊢ (𝑖 = 𝑎 → (𝑖 ∈ (𝐿...𝑀) ↔ 𝑎 ∈ (𝐿...𝑀)))
32	31	anbi2d 740	. . . . . . . 8 ⊢ (𝑖 = 𝑎 → ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) ↔ (𝜑 ∧ 𝑎 ∈ (𝐿...𝑀))))
33		fveq2 6191	. . . . . . . . 9 ⊢ (𝑖 = 𝑎 → (𝐵‘𝑖) = (𝐵‘𝑎))
34	33	eleq1d 2686	. . . . . . . 8 ⊢ (𝑖 = 𝑎 → ((𝐵‘𝑖) ∈ ℝ ↔ (𝐵‘𝑎) ∈ ℝ))
35	32, 34	imbi12d 334	. . . . . . 7 ⊢ (𝑖 = 𝑎 → (((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ∈ ℝ) ↔ ((𝜑 ∧ 𝑎 ∈ (𝐿...𝑀)) → (𝐵‘𝑎) ∈ ℝ)))
36	30, 35, 10	chvar 2262	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝐿...𝑀)) → (𝐵‘𝑎) ∈ ℝ)
37		remulcl 10021	. . . . . . 7 ⊢ ((𝑎 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑎 · 𝑗) ∈ ℝ)
38	37	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ 𝑗 ∈ ℝ)) → (𝑎 · 𝑗) ∈ ℝ)
39	8, 36, 38	seqcl 12821	. . . . 5 ⊢ (𝜑 → (seq𝐿( · , 𝐵)‘𝑀) ∈ ℝ)
40	39	adantr 481	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → (seq𝐿( · , 𝐵)‘𝑀) ∈ ℝ)
41		fmul01lt1lem2.10	. . . . . . 7 ⊢ (𝜑 → 𝐽 ∈ (𝐿...𝑀))
42		elfzuz3 12339	. . . . . . 7 ⊢ (𝐽 ∈ (𝐿...𝑀) → 𝑀 ∈ (ℤ_≥‘𝐽))
43	41, 42	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘𝐽))
44		nfv 1843	. . . . . . . . 9 ⊢ Ⅎ𝑖 𝑎 ∈ (𝐽...𝑀)
45	2, 44	nfan 1828	. . . . . . . 8 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑎 ∈ (𝐽...𝑀))
46	45, 29	nfim 1825	. . . . . . 7 ⊢ Ⅎ𝑖((𝜑 ∧ 𝑎 ∈ (𝐽...𝑀)) → (𝐵‘𝑎) ∈ ℝ)
47		eleq1 2689	. . . . . . . . 9 ⊢ (𝑖 = 𝑎 → (𝑖 ∈ (𝐽...𝑀) ↔ 𝑎 ∈ (𝐽...𝑀)))
48	47	anbi2d 740	. . . . . . . 8 ⊢ (𝑖 = 𝑎 → ((𝜑 ∧ 𝑖 ∈ (𝐽...𝑀)) ↔ (𝜑 ∧ 𝑎 ∈ (𝐽...𝑀))))
49	48, 34	imbi12d 334	. . . . . . 7 ⊢ (𝑖 = 𝑎 → (((𝜑 ∧ 𝑖 ∈ (𝐽...𝑀)) → (𝐵‘𝑖) ∈ ℝ) ↔ ((𝜑 ∧ 𝑎 ∈ (𝐽...𝑀)) → (𝐵‘𝑎) ∈ ℝ)))
50	6	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐽...𝑀)) → 𝐿 ∈ ℤ)
51		eluzelz 11697	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ (ℤ_≥‘𝐿) → 𝑀 ∈ ℤ)
52	8, 51	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℤ)
53	52	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐽...𝑀)) → 𝑀 ∈ ℤ)
54		elfzelz 12342	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (𝐽...𝑀) → 𝑖 ∈ ℤ)
55	54	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐽...𝑀)) → 𝑖 ∈ ℤ)
56	50, 53, 55	3jca 1242	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐽...𝑀)) → (𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ))
57	6	zred 11482	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐿 ∈ ℝ)
58	57	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐽...𝑀)) → 𝐿 ∈ ℝ)
59		elfzelz 12342	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ (𝐿...𝑀) → 𝐽 ∈ ℤ)
60	41, 59	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽 ∈ ℤ)
61	60	zred 11482	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ ℝ)
62	61	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐽...𝑀)) → 𝐽 ∈ ℝ)
63	54	zred 11482	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (𝐽...𝑀) → 𝑖 ∈ ℝ)
64	63	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐽...𝑀)) → 𝑖 ∈ ℝ)
65		elfzle1 12344	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ (𝐿...𝑀) → 𝐿 ≤ 𝐽)
66	41, 65	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐿 ≤ 𝐽)
67	66	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐽...𝑀)) → 𝐿 ≤ 𝐽)
68		elfzle1 12344	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (𝐽...𝑀) → 𝐽 ≤ 𝑖)
69	68	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐽...𝑀)) → 𝐽 ≤ 𝑖)
70	58, 62, 64, 67, 69	letrd 10194	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐽...𝑀)) → 𝐿 ≤ 𝑖)
71		elfzle2 12345	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (𝐽...𝑀) → 𝑖 ≤ 𝑀)
72	71	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐽...𝑀)) → 𝑖 ≤ 𝑀)
73	70, 72	jca 554	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐽...𝑀)) → (𝐿 ≤ 𝑖 ∧ 𝑖 ≤ 𝑀))
74		elfz2 12333	. . . . . . . . 9 ⊢ (𝑖 ∈ (𝐿...𝑀) ↔ ((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝐿 ≤ 𝑖 ∧ 𝑖 ≤ 𝑀)))
75	56, 73, 74	sylanbrc 698	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐽...𝑀)) → 𝑖 ∈ (𝐿...𝑀))
76	75, 10	syldan 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐽...𝑀)) → (𝐵‘𝑖) ∈ ℝ)
77	46, 49, 76	chvar 2262	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝐽...𝑀)) → (𝐵‘𝑎) ∈ ℝ)
78	43, 77, 38	seqcl 12821	. . . . 5 ⊢ (𝜑 → (seq𝐽( · , 𝐵)‘𝑀) ∈ ℝ)
79	78	adantr 481	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → (seq𝐽( · , 𝐵)‘𝑀) ∈ ℝ)
80	16	rpred 11872	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ ℝ)
81	80	adantr 481	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → 𝐸 ∈ ℝ)
82		remulcl 10021	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑎 · 𝑏) ∈ ℝ)
83	82	adantl 482	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐽 = 𝐿) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → (𝑎 · 𝑏) ∈ ℝ)
84		simp1 1061	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ) → 𝑎 ∈ ℝ)
85	84	recnd 10068	. . . . . . . . . 10 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ) → 𝑎 ∈ ℂ)
86		simp2 1062	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ) → 𝑏 ∈ ℝ)
87	86	recnd 10068	. . . . . . . . . 10 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ) → 𝑏 ∈ ℂ)
88		simp3 1063	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ) → 𝑐 ∈ ℝ)
89	88	recnd 10068	. . . . . . . . . 10 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ) → 𝑐 ∈ ℂ)
90	85, 87, 89	mulassd 10063	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ) → ((𝑎 · 𝑏) · 𝑐) = (𝑎 · (𝑏 · 𝑐)))
91	90	adantl 482	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐽 = 𝐿) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ)) → ((𝑎 · 𝑏) · 𝑐) = (𝑎 · (𝑏 · 𝑐)))
92	60	zcnd 11483	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ ℂ)
93		1cnd 10056	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℂ)
94	92, 93	npcand 10396	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐽 − 1) + 1) = 𝐽)
95	94	fveq2d 6195	. . . . . . . . . 10 ⊢ (𝜑 → (ℤ_≥‘((𝐽 − 1) + 1)) = (ℤ_≥‘𝐽))
96	43, 95	eleqtrrd 2704	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘((𝐽 − 1) + 1)))
97	96	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → 𝑀 ∈ (ℤ_≥‘((𝐽 − 1) + 1)))
98	6	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → 𝐿 ∈ ℤ)
99	60	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → 𝐽 ∈ ℤ)
100		1zzd 11408	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → 1 ∈ ℤ)
101	99, 100	zsubcld 11487	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → (𝐽 − 1) ∈ ℤ)
102		simpr 477	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → ¬ 𝐽 = 𝐿)
103		eqcom 2629	. . . . . . . . . . . 12 ⊢ (𝐽 = 𝐿 ↔ 𝐿 = 𝐽)
104	102, 103	sylnib 318	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → ¬ 𝐿 = 𝐽)
105	57, 61	leloed 10180	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 ≤ 𝐽 ↔ (𝐿 < 𝐽 ∨ 𝐿 = 𝐽)))
106	66, 105	mpbid 222	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐿 < 𝐽 ∨ 𝐿 = 𝐽))
107	106	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → (𝐿 < 𝐽 ∨ 𝐿 = 𝐽))
108		orel2 398	. . . . . . . . . . 11 ⊢ (¬ 𝐿 = 𝐽 → ((𝐿 < 𝐽 ∨ 𝐿 = 𝐽) → 𝐿 < 𝐽))
109	104, 107, 108	sylc 65	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → 𝐿 < 𝐽)
110		zltlem1 11430	. . . . . . . . . . . 12 ⊢ ((𝐿 ∈ ℤ ∧ 𝐽 ∈ ℤ) → (𝐿 < 𝐽 ↔ 𝐿 ≤ (𝐽 − 1)))
111	6, 60, 110	syl2anc 693	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐿 < 𝐽 ↔ 𝐿 ≤ (𝐽 − 1)))
112	111	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → (𝐿 < 𝐽 ↔ 𝐿 ≤ (𝐽 − 1)))
113	109, 112	mpbid 222	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → 𝐿 ≤ (𝐽 − 1))
114		eluz2 11693	. . . . . . . . 9 ⊢ ((𝐽 − 1) ∈ (ℤ_≥‘𝐿) ↔ (𝐿 ∈ ℤ ∧ (𝐽 − 1) ∈ ℤ ∧ 𝐿 ≤ (𝐽 − 1)))
115	98, 101, 113, 114	syl3anbrc 1246	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → (𝐽 − 1) ∈ (ℤ_≥‘𝐿))
116		nfv 1843	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖 ¬ 𝐽 = 𝐿
117	2, 116	nfan 1828	. . . . . . . . . . 11 ⊢ Ⅎ𝑖(𝜑 ∧ ¬ 𝐽 = 𝐿)
118	117, 25	nfan 1828	. . . . . . . . . 10 ⊢ Ⅎ𝑖((𝜑 ∧ ¬ 𝐽 = 𝐿) ∧ 𝑎 ∈ (𝐿...𝑀))
119	118, 29	nfim 1825	. . . . . . . . 9 ⊢ Ⅎ𝑖(((𝜑 ∧ ¬ 𝐽 = 𝐿) ∧ 𝑎 ∈ (𝐿...𝑀)) → (𝐵‘𝑎) ∈ ℝ)
120	31	anbi2d 740	. . . . . . . . . 10 ⊢ (𝑖 = 𝑎 → (((𝜑 ∧ ¬ 𝐽 = 𝐿) ∧ 𝑖 ∈ (𝐿...𝑀)) ↔ ((𝜑 ∧ ¬ 𝐽 = 𝐿) ∧ 𝑎 ∈ (𝐿...𝑀))))
121	120, 34	imbi12d 334	. . . . . . . . 9 ⊢ (𝑖 = 𝑎 → ((((𝜑 ∧ ¬ 𝐽 = 𝐿) ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ∈ ℝ) ↔ (((𝜑 ∧ ¬ 𝐽 = 𝐿) ∧ 𝑎 ∈ (𝐿...𝑀)) → (𝐵‘𝑎) ∈ ℝ)))
122	10	adantlr 751	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐽 = 𝐿) ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ∈ ℝ)
123	119, 121, 122	chvar 2262	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐽 = 𝐿) ∧ 𝑎 ∈ (𝐿...𝑀)) → (𝐵‘𝑎) ∈ ℝ)
124	83, 91, 97, 115, 123	seqsplit 12834	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → (seq𝐿( · , 𝐵)‘𝑀) = ((seq𝐿( · , 𝐵)‘(𝐽 − 1)) · (seq((𝐽 − 1) + 1)( · , 𝐵)‘𝑀)))
125	94	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → ((𝐽 − 1) + 1) = 𝐽)
126	125	seqeq1d 12807	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → seq((𝐽 − 1) + 1)( · , 𝐵) = seq𝐽( · , 𝐵))
127	126	fveq1d 6193	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → (seq((𝐽 − 1) + 1)( · , 𝐵)‘𝑀) = (seq𝐽( · , 𝐵)‘𝑀))
128	127	oveq2d 6666	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → ((seq𝐿( · , 𝐵)‘(𝐽 − 1)) · (seq((𝐽 − 1) + 1)( · , 𝐵)‘𝑀)) = ((seq𝐿( · , 𝐵)‘(𝐽 − 1)) · (seq𝐽( · , 𝐵)‘𝑀)))
129	124, 128	eqtrd 2656	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → (seq𝐿( · , 𝐵)‘𝑀) = ((seq𝐿( · , 𝐵)‘(𝐽 − 1)) · (seq𝐽( · , 𝐵)‘𝑀)))
130		nfv 1843	. . . . . . . . . . 11 ⊢ Ⅎ𝑖 𝑎 ∈ (𝐿...(𝐽 − 1))
131	117, 130	nfan 1828	. . . . . . . . . 10 ⊢ Ⅎ𝑖((𝜑 ∧ ¬ 𝐽 = 𝐿) ∧ 𝑎 ∈ (𝐿...(𝐽 − 1)))
132	131, 29	nfim 1825	. . . . . . . . 9 ⊢ Ⅎ𝑖(((𝜑 ∧ ¬ 𝐽 = 𝐿) ∧ 𝑎 ∈ (𝐿...(𝐽 − 1))) → (𝐵‘𝑎) ∈ ℝ)
133		eleq1 2689	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑎 → (𝑖 ∈ (𝐿...(𝐽 − 1)) ↔ 𝑎 ∈ (𝐿...(𝐽 − 1))))
134	133	anbi2d 740	. . . . . . . . . 10 ⊢ (𝑖 = 𝑎 → (((𝜑 ∧ ¬ 𝐽 = 𝐿) ∧ 𝑖 ∈ (𝐿...(𝐽 − 1))) ↔ ((𝜑 ∧ ¬ 𝐽 = 𝐿) ∧ 𝑎 ∈ (𝐿...(𝐽 − 1)))))
135	134, 34	imbi12d 334	. . . . . . . . 9 ⊢ (𝑖 = 𝑎 → ((((𝜑 ∧ ¬ 𝐽 = 𝐿) ∧ 𝑖 ∈ (𝐿...(𝐽 − 1))) → (𝐵‘𝑖) ∈ ℝ) ↔ (((𝜑 ∧ ¬ 𝐽 = 𝐿) ∧ 𝑎 ∈ (𝐿...(𝐽 − 1))) → (𝐵‘𝑎) ∈ ℝ)))
136	6	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...(𝐽 − 1))) → 𝐿 ∈ ℤ)
137	52	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...(𝐽 − 1))) → 𝑀 ∈ ℤ)
138		elfzelz 12342	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝐿...(𝐽 − 1)) → 𝑖 ∈ ℤ)
139	138	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...(𝐽 − 1))) → 𝑖 ∈ ℤ)
140	136, 137, 139	3jca 1242	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...(𝐽 − 1))) → (𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ))
141		elfzle1 12344	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝐿...(𝐽 − 1)) → 𝐿 ≤ 𝑖)
142	141	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...(𝐽 − 1))) → 𝐿 ≤ 𝑖)
143	138	zred 11482	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝐿...(𝐽 − 1)) → 𝑖 ∈ ℝ)
144	143	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...(𝐽 − 1))) → 𝑖 ∈ ℝ)
145	61	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...(𝐽 − 1))) → 𝐽 ∈ ℝ)
146	52	zred 11482	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ ℝ)
147	146	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...(𝐽 − 1))) → 𝑀 ∈ ℝ)
148		1red 10055	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ∈ ℝ)
149	61, 148	resubcld 10458	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐽 − 1) ∈ ℝ)
150	149	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...(𝐽 − 1))) → (𝐽 − 1) ∈ ℝ)
151		elfzle2 12345	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (𝐿...(𝐽 − 1)) → 𝑖 ≤ (𝐽 − 1))
152	151	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...(𝐽 − 1))) → 𝑖 ≤ (𝐽 − 1))
153	61	lem1d 10957	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐽 − 1) ≤ 𝐽)
154	153	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...(𝐽 − 1))) → (𝐽 − 1) ≤ 𝐽)
155	144, 150, 145, 152, 154	letrd 10194	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...(𝐽 − 1))) → 𝑖 ≤ 𝐽)
156		elfzle2 12345	. . . . . . . . . . . . . . . 16 ⊢ (𝐽 ∈ (𝐿...𝑀) → 𝐽 ≤ 𝑀)
157	41, 156	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐽 ≤ 𝑀)
158	157	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...(𝐽 − 1))) → 𝐽 ≤ 𝑀)
159	144, 145, 147, 155, 158	letrd 10194	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...(𝐽 − 1))) → 𝑖 ≤ 𝑀)
160	142, 159	jca 554	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...(𝐽 − 1))) → (𝐿 ≤ 𝑖 ∧ 𝑖 ≤ 𝑀))
161	140, 160, 74	sylanbrc 698	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...(𝐽 − 1))) → 𝑖 ∈ (𝐿...𝑀))
162	161, 10	syldan 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...(𝐽 − 1))) → (𝐵‘𝑖) ∈ ℝ)
163	162	adantlr 751	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐽 = 𝐿) ∧ 𝑖 ∈ (𝐿...(𝐽 − 1))) → (𝐵‘𝑖) ∈ ℝ)
164	132, 135, 163	chvar 2262	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐽 = 𝐿) ∧ 𝑎 ∈ (𝐿...(𝐽 − 1))) → (𝐵‘𝑎) ∈ ℝ)
165	37	adantl 482	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐽 = 𝐿) ∧ (𝑎 ∈ ℝ ∧ 𝑗 ∈ ℝ)) → (𝑎 · 𝑗) ∈ ℝ)
166	115, 164, 165	seqcl 12821	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → (seq𝐿( · , 𝐵)‘(𝐽 − 1)) ∈ ℝ)
167		1red 10055	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → 1 ∈ ℝ)
168		eqid 2622	. . . . . . . . 9 ⊢ seq𝐽( · , 𝐵) = seq𝐽( · , 𝐵)
169	43	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → 𝑀 ∈ (ℤ_≥‘𝐽))
170		eluzfz2 12349	. . . . . . . . . . 11 ⊢ (𝑀 ∈ (ℤ_≥‘𝐽) → 𝑀 ∈ (𝐽...𝑀))
171	43, 170	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ (𝐽...𝑀))
172	171	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → 𝑀 ∈ (𝐽...𝑀))
173	76	adantlr 751	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐽 = 𝐿) ∧ 𝑖 ∈ (𝐽...𝑀)) → (𝐵‘𝑖) ∈ ℝ)
174	75, 12	syldan 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐽...𝑀)) → 0 ≤ (𝐵‘𝑖))
175	174	adantlr 751	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐽 = 𝐿) ∧ 𝑖 ∈ (𝐽...𝑀)) → 0 ≤ (𝐵‘𝑖))
176	75, 14	syldan 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝐽...𝑀)) → (𝐵‘𝑖) ≤ 1)
177	176	adantlr 751	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐽 = 𝐿) ∧ 𝑖 ∈ (𝐽...𝑀)) → (𝐵‘𝑖) ≤ 1)
178	1, 117, 168, 99, 169, 172, 173, 175, 177	fmul01 39812	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → (0 ≤ (seq𝐽( · , 𝐵)‘𝑀) ∧ (seq𝐽( · , 𝐵)‘𝑀) ≤ 1))
179	178	simpld 475	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → 0 ≤ (seq𝐽( · , 𝐵)‘𝑀))
180		eqid 2622	. . . . . . . . 9 ⊢ seq𝐿( · , 𝐵) = seq𝐿( · , 𝐵)
181	8	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → 𝑀 ∈ (ℤ_≥‘𝐿))
182		1zzd 11408	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ∈ ℤ)
183	60, 182	zsubcld 11487	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐽 − 1) ∈ ℤ)
184	6, 52, 183	3jca 1242	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝐽 − 1) ∈ ℤ))
185	184	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → (𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝐽 − 1) ∈ ℤ))
186	149, 61, 146	3jca 1242	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐽 − 1) ∈ ℝ ∧ 𝐽 ∈ ℝ ∧ 𝑀 ∈ ℝ))
187	186	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → ((𝐽 − 1) ∈ ℝ ∧ 𝐽 ∈ ℝ ∧ 𝑀 ∈ ℝ))
188	61	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → 𝐽 ∈ ℝ)
189	188	lem1d 10957	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → (𝐽 − 1) ≤ 𝐽)
190	157	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → 𝐽 ≤ 𝑀)
191	189, 190	jca 554	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → ((𝐽 − 1) ≤ 𝐽 ∧ 𝐽 ≤ 𝑀))
192		letr 10131	. . . . . . . . . . . 12 ⊢ (((𝐽 − 1) ∈ ℝ ∧ 𝐽 ∈ ℝ ∧ 𝑀 ∈ ℝ) → (((𝐽 − 1) ≤ 𝐽 ∧ 𝐽 ≤ 𝑀) → (𝐽 − 1) ≤ 𝑀))
193	187, 191, 192	sylc 65	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → (𝐽 − 1) ≤ 𝑀)
194	113, 193	jca 554	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → (𝐿 ≤ (𝐽 − 1) ∧ (𝐽 − 1) ≤ 𝑀))
195		elfz2 12333	. . . . . . . . . 10 ⊢ ((𝐽 − 1) ∈ (𝐿...𝑀) ↔ ((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝐽 − 1) ∈ ℤ) ∧ (𝐿 ≤ (𝐽 − 1) ∧ (𝐽 − 1) ≤ 𝑀)))
196	185, 194, 195	sylanbrc 698	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → (𝐽 − 1) ∈ (𝐿...𝑀))
197	12	adantlr 751	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐽 = 𝐿) ∧ 𝑖 ∈ (𝐿...𝑀)) → 0 ≤ (𝐵‘𝑖))
198	14	adantlr 751	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐽 = 𝐿) ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ≤ 1)
199	1, 117, 180, 98, 181, 196, 122, 197, 198	fmul01 39812	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → (0 ≤ (seq𝐿( · , 𝐵)‘(𝐽 − 1)) ∧ (seq𝐿( · , 𝐵)‘(𝐽 − 1)) ≤ 1))
200	199	simprd 479	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → (seq𝐿( · , 𝐵)‘(𝐽 − 1)) ≤ 1)
201	166, 167, 79, 179, 200	lemul1ad 10963	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → ((seq𝐿( · , 𝐵)‘(𝐽 − 1)) · (seq𝐽( · , 𝐵)‘𝑀)) ≤ (1 · (seq𝐽( · , 𝐵)‘𝑀)))
202	129, 201	eqbrtrd 4675	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → (seq𝐿( · , 𝐵)‘𝑀) ≤ (1 · (seq𝐽( · , 𝐵)‘𝑀)))
203	79	recnd 10068	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → (seq𝐽( · , 𝐵)‘𝑀) ∈ ℂ)
204	203	mulid2d 10058	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → (1 · (seq𝐽( · , 𝐵)‘𝑀)) = (seq𝐽( · , 𝐵)‘𝑀))
205	202, 204	breqtrd 4679	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → (seq𝐿( · , 𝐵)‘𝑀) ≤ (seq𝐽( · , 𝐵)‘𝑀))
206	1, 2, 168, 60, 43, 76, 174, 176, 16, 20	fmul01lt1lem1 39816	. . . . 5 ⊢ (𝜑 → (seq𝐽( · , 𝐵)‘𝑀) < 𝐸)
207	206	adantr 481	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → (seq𝐽( · , 𝐵)‘𝑀) < 𝐸)
208	40, 79, 81, 205, 207	lelttrd 10195	. . 3 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → (seq𝐿( · , 𝐵)‘𝑀) < 𝐸)
209	24, 208	syl5eqbr 4688	. 2 ⊢ ((𝜑 ∧ ¬ 𝐽 = 𝐿) → (𝐴‘𝑀) < 𝐸)
210	23, 209	pm2.61dan 832	1 ⊢ (𝜑 → (𝐴‘𝑀) < 𝐸)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∨ wo 383 ∧ wa 384 ∧ w3a 1037 = wceq 1483 Ⅎwnf 1708 ∈ wcel 1990 Ⅎwnfc 2751 class class class wbr 4653 ‘cfv 5888 (class class class)co 6650 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 < clt 10074 ≤ cle 10075 − cmin 10266 ℤcz 11377 ℤ_≥cuz 11687 ℝ⁺crp 11832 ...cfz 12326 seqcseq 12801

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-n0 11293 df-z 11378 df-uz 11688 df-rp 11833 df-fz 12327 df-fzo 12466 df-seq 12802

This theorem is referenced by: fmul01lt1 39818

W3C validator