Proof of Theorem nmoleub2lem
Step | Hyp | Ref
| Expression |
1 | | nmoleub2lem.7 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝜓 → (𝐿‘𝑥) ≤ 𝑅)) |
2 | 1 | adantlr 751 |
. . . 4
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ 𝑥 ∈ 𝑉) → (𝜓 → (𝐿‘𝑥) ≤ 𝑅)) |
3 | | inss1 3833 |
. . . . . . . . . . . 12
⊢ (NrmMod
∩ ℂMod) ⊆ NrmMod |
4 | | nmoleub2.t |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ∈ (NrmMod ∩
ℂMod)) |
5 | 3, 4 | sseldi 3601 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈ NrmMod) |
6 | | nlmngp 22481 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ NrmMod → 𝑇 ∈ NrmGrp) |
7 | 5, 6 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 ∈ NrmGrp) |
8 | 7 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → 𝑇 ∈ NrmGrp) |
9 | | nmoleub2.f |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇)) |
10 | | nmoleub2.v |
. . . . . . . . . . . . 13
⊢ 𝑉 = (Base‘𝑆) |
11 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑇) =
(Base‘𝑇) |
12 | 10, 11 | lmhmf 19034 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹:𝑉⟶(Base‘𝑇)) |
13 | 9, 12 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝑉⟶(Base‘𝑇)) |
14 | 13 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → 𝐹:𝑉⟶(Base‘𝑇)) |
15 | | simprl 794 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → 𝑥 ∈ 𝑉) |
16 | 14, 15 | ffvelrnd 6360 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (𝐹‘𝑥) ∈ (Base‘𝑇)) |
17 | | nmoleub2.m |
. . . . . . . . . 10
⊢ 𝑀 = (norm‘𝑇) |
18 | 11, 17 | nmcl 22420 |
. . . . . . . . 9
⊢ ((𝑇 ∈ NrmGrp ∧ (𝐹‘𝑥) ∈ (Base‘𝑇)) → (𝑀‘(𝐹‘𝑥)) ∈ ℝ) |
19 | 8, 16, 18 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (𝑀‘(𝐹‘𝑥)) ∈ ℝ) |
20 | | nmoleub2.r |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
21 | 20 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → 𝑅 ∈
ℝ+) |
22 | 19, 21 | rerpdivcld 11903 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ∈ ℝ) |
23 | 22 | rexrd 10089 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ∈
ℝ*) |
24 | | nmoleub2.s |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ (NrmMod ∩
ℂMod)) |
25 | 3, 24 | sseldi 3601 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ NrmMod) |
26 | | nlmngp 22481 |
. . . . . . . . 9
⊢ (𝑆 ∈ NrmMod → 𝑆 ∈ NrmGrp) |
27 | 25, 26 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ NrmGrp) |
28 | | lmghm 19031 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
29 | 9, 28 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
30 | | nmoleub2.n |
. . . . . . . . 9
⊢ 𝑁 = (𝑆 normOp 𝑇) |
31 | 30 | nmocl 22524 |
. . . . . . . 8
⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → (𝑁‘𝐹) ∈
ℝ*) |
32 | 27, 7, 29, 31 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜑 → (𝑁‘𝐹) ∈
ℝ*) |
33 | 32 | ad2antrr 762 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (𝑁‘𝐹) ∈
ℝ*) |
34 | | nmoleub2.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
35 | 34 | ad2antrr 762 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → 𝐴 ∈
ℝ*) |
36 | 21 | rpred 11872 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → 𝑅 ∈ ℝ) |
37 | | rexmul 12101 |
. . . . . . . . . 10
⊢ ((((𝑀‘(𝐹‘𝑥)) / 𝑅) ∈ ℝ ∧ 𝑅 ∈ ℝ) → (((𝑀‘(𝐹‘𝑥)) / 𝑅) ·e 𝑅) = (((𝑀‘(𝐹‘𝑥)) / 𝑅) · 𝑅)) |
38 | 22, 36, 37 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (((𝑀‘(𝐹‘𝑥)) / 𝑅) ·e 𝑅) = (((𝑀‘(𝐹‘𝑥)) / 𝑅) · 𝑅)) |
39 | 19 | recnd 10068 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (𝑀‘(𝐹‘𝑥)) ∈ ℂ) |
40 | 36 | recnd 10068 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → 𝑅 ∈ ℂ) |
41 | 21 | rpne0d 11877 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → 𝑅 ≠ 0) |
42 | 39, 40, 41 | divcan1d 10802 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (((𝑀‘(𝐹‘𝑥)) / 𝑅) · 𝑅) = (𝑀‘(𝐹‘𝑥))) |
43 | 38, 42 | eqtrd 2656 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (((𝑀‘(𝐹‘𝑥)) / 𝑅) ·e 𝑅) = (𝑀‘(𝐹‘𝑥))) |
44 | 19 | rexrd 10089 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (𝑀‘(𝐹‘𝑥)) ∈
ℝ*) |
45 | 27 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → 𝑆 ∈ NrmGrp) |
46 | | nmoleub2.l |
. . . . . . . . . . . . 13
⊢ 𝐿 = (norm‘𝑆) |
47 | 10, 46 | nmcl 22420 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ NrmGrp ∧ 𝑥 ∈ 𝑉) → (𝐿‘𝑥) ∈ ℝ) |
48 | 45, 15, 47 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (𝐿‘𝑥) ∈ ℝ) |
49 | 48 | rexrd 10089 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (𝐿‘𝑥) ∈
ℝ*) |
50 | 33, 49 | xmulcld 12132 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → ((𝑁‘𝐹) ·e (𝐿‘𝑥)) ∈
ℝ*) |
51 | 21 | rpxrd 11873 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → 𝑅 ∈
ℝ*) |
52 | 33, 51 | xmulcld 12132 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → ((𝑁‘𝐹) ·e 𝑅) ∈
ℝ*) |
53 | 29 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
54 | 30, 10, 46, 17 | nmoix 22533 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑥 ∈ 𝑉) → (𝑀‘(𝐹‘𝑥)) ≤ ((𝑁‘𝐹) ·e (𝐿‘𝑥))) |
55 | 45, 8, 53, 15, 54 | syl31anc 1329 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (𝑀‘(𝐹‘𝑥)) ≤ ((𝑁‘𝐹) ·e (𝐿‘𝑥))) |
56 | 30 | nmoge0 22525 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → 0 ≤ (𝑁‘𝐹)) |
57 | 27, 7, 29, 56 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ (𝑁‘𝐹)) |
58 | 32, 57 | jca 554 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁‘𝐹) ∈ ℝ* ∧ 0 ≤
(𝑁‘𝐹))) |
59 | 58 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → ((𝑁‘𝐹) ∈ ℝ* ∧ 0 ≤
(𝑁‘𝐹))) |
60 | | simprr 796 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (𝐿‘𝑥) ≤ 𝑅) |
61 | | xlemul2a 12119 |
. . . . . . . . . 10
⊢ ((((𝐿‘𝑥) ∈ ℝ* ∧ 𝑅 ∈ ℝ*
∧ ((𝑁‘𝐹) ∈ ℝ*
∧ 0 ≤ (𝑁‘𝐹))) ∧ (𝐿‘𝑥) ≤ 𝑅) → ((𝑁‘𝐹) ·e (𝐿‘𝑥)) ≤ ((𝑁‘𝐹) ·e 𝑅)) |
62 | 49, 51, 59, 60, 61 | syl31anc 1329 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → ((𝑁‘𝐹) ·e (𝐿‘𝑥)) ≤ ((𝑁‘𝐹) ·e 𝑅)) |
63 | 44, 50, 52, 55, 62 | xrletrd 11993 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (𝑀‘(𝐹‘𝑥)) ≤ ((𝑁‘𝐹) ·e 𝑅)) |
64 | 43, 63 | eqbrtrd 4675 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (((𝑀‘(𝐹‘𝑥)) / 𝑅) ·e 𝑅) ≤ ((𝑁‘𝐹) ·e 𝑅)) |
65 | | xlemul1 12120 |
. . . . . . . 8
⊢ ((((𝑀‘(𝐹‘𝑥)) / 𝑅) ∈ ℝ* ∧ (𝑁‘𝐹) ∈ ℝ* ∧ 𝑅 ∈ ℝ+)
→ (((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ (𝑁‘𝐹) ↔ (((𝑀‘(𝐹‘𝑥)) / 𝑅) ·e 𝑅) ≤ ((𝑁‘𝐹) ·e 𝑅))) |
66 | 23, 33, 21, 65 | syl3anc 1326 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ (𝑁‘𝐹) ↔ (((𝑀‘(𝐹‘𝑥)) / 𝑅) ·e 𝑅) ≤ ((𝑁‘𝐹) ·e 𝑅))) |
67 | 64, 66 | mpbird 247 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ (𝑁‘𝐹)) |
68 | | simplr 792 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (𝑁‘𝐹) ≤ 𝐴) |
69 | 23, 33, 35, 67, 68 | xrletrd 11993 |
. . . . 5
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴) |
70 | 69 | expr 643 |
. . . 4
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ 𝑥 ∈ 𝑉) → ((𝐿‘𝑥) ≤ 𝑅 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) |
71 | 2, 70 | syld 47 |
. . 3
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ 𝑥 ∈ 𝑉) → (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) |
72 | 71 | ralrimiva 2966 |
. 2
⊢ ((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) → ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) |
73 | | eqid 2622 |
. . . 4
⊢
(0g‘𝑆) = (0g‘𝑆) |
74 | 27 | ad2antrr 762 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) ∧ 𝐴 ∈ ℝ) → 𝑆 ∈ NrmGrp) |
75 | 7 | ad2antrr 762 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) ∧ 𝐴 ∈ ℝ) → 𝑇 ∈ NrmGrp) |
76 | 29 | ad2antrr 762 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) ∧ 𝐴 ∈ ℝ) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
77 | | simpr 477 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) ∧ 𝐴 ∈ ℝ) → 𝐴 ∈ ℝ) |
78 | | nmoleub2lem.5 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) → 0 ≤ 𝐴) |
79 | 78 | adantr 481 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) ∧ 𝐴 ∈ ℝ) → 0 ≤ 𝐴) |
80 | | nmoleub2lem.6 |
. . . 4
⊢ ((((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) ∧ 𝐴 ∈ ℝ) ∧ (𝑦 ∈ 𝑉 ∧ 𝑦 ≠ (0g‘𝑆))) → (𝑀‘(𝐹‘𝑦)) ≤ (𝐴 · (𝐿‘𝑦))) |
81 | 30, 10, 46, 17, 73, 74, 75, 76, 77, 79, 80 | nmolb2d 22522 |
. . 3
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) ∧ 𝐴 ∈ ℝ) → (𝑁‘𝐹) ≤ 𝐴) |
82 | 32 | ad2antrr 762 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) ∧ 𝐴 = +∞) → (𝑁‘𝐹) ∈
ℝ*) |
83 | | pnfge 11964 |
. . . . 5
⊢ ((𝑁‘𝐹) ∈ ℝ* → (𝑁‘𝐹) ≤ +∞) |
84 | 82, 83 | syl 17 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) ∧ 𝐴 = +∞) → (𝑁‘𝐹) ≤ +∞) |
85 | | simpr 477 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) ∧ 𝐴 = +∞) → 𝐴 = +∞) |
86 | 84, 85 | breqtrrd 4681 |
. . 3
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) ∧ 𝐴 = +∞) → (𝑁‘𝐹) ≤ 𝐴) |
87 | 34 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) → 𝐴 ∈
ℝ*) |
88 | | ge0nemnf 12004 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 0 ≤ 𝐴) →
𝐴 ≠
-∞) |
89 | 87, 78, 88 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) → 𝐴 ≠ -∞) |
90 | 87, 89 | jca 554 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) → (𝐴 ∈ ℝ* ∧ 𝐴 ≠
-∞)) |
91 | | xrnemnf 11951 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
↔ (𝐴 ∈ ℝ
∨ 𝐴 =
+∞)) |
92 | 90, 91 | sylib 208 |
. . 3
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) → (𝐴 ∈ ℝ ∨ 𝐴 = +∞)) |
93 | 81, 86, 92 | mpjaodan 827 |
. 2
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) → (𝑁‘𝐹) ≤ 𝐴) |
94 | 72, 93 | impbida 877 |
1
⊢ (𝜑 → ((𝑁‘𝐹) ≤ 𝐴 ↔ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴))) |