Proof of Theorem nmoleub2lem
Step | Hyp | Ref
| Expression |
1 | | nmoleub2lem.7 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝜓 → (𝐿‘𝑥) ≤ 𝑅)) |
2 | 1 | adantlr 715 |
. . . 4
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ 𝑥 ∈ 𝑉) → (𝜓 → (𝐿‘𝑥) ≤ 𝑅)) |
3 | | nmoleub2.t |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ∈ (NrmMod ∩
ℂMod)) |
4 | 3 | elin1d 4112 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈ NrmMod) |
5 | | nlmngp 23575 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ NrmMod → 𝑇 ∈ NrmGrp) |
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 ∈ NrmGrp) |
7 | 6 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → 𝑇 ∈ NrmGrp) |
8 | | nmoleub2.f |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇)) |
9 | | nmoleub2.v |
. . . . . . . . . . . . 13
⊢ 𝑉 = (Base‘𝑆) |
10 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑇) =
(Base‘𝑇) |
11 | 9, 10 | lmhmf 20071 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹:𝑉⟶(Base‘𝑇)) |
12 | 8, 11 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝑉⟶(Base‘𝑇)) |
13 | 12 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → 𝐹:𝑉⟶(Base‘𝑇)) |
14 | | simprl 771 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → 𝑥 ∈ 𝑉) |
15 | 13, 14 | ffvelrnd 6905 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (𝐹‘𝑥) ∈ (Base‘𝑇)) |
16 | | nmoleub2.m |
. . . . . . . . . 10
⊢ 𝑀 = (norm‘𝑇) |
17 | 10, 16 | nmcl 23514 |
. . . . . . . . 9
⊢ ((𝑇 ∈ NrmGrp ∧ (𝐹‘𝑥) ∈ (Base‘𝑇)) → (𝑀‘(𝐹‘𝑥)) ∈ ℝ) |
18 | 7, 15, 17 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (𝑀‘(𝐹‘𝑥)) ∈ ℝ) |
19 | | nmoleub2.r |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
20 | 19 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → 𝑅 ∈
ℝ+) |
21 | 18, 20 | rerpdivcld 12659 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ∈ ℝ) |
22 | 21 | rexrd 10883 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ∈
ℝ*) |
23 | | nmoleub2.s |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ (NrmMod ∩
ℂMod)) |
24 | 23 | elin1d 4112 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ NrmMod) |
25 | | nlmngp 23575 |
. . . . . . . . 9
⊢ (𝑆 ∈ NrmMod → 𝑆 ∈ NrmGrp) |
26 | 24, 25 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ NrmGrp) |
27 | | lmghm 20068 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
28 | 8, 27 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
29 | | nmoleub2.n |
. . . . . . . . 9
⊢ 𝑁 = (𝑆 normOp 𝑇) |
30 | 29 | nmocl 23618 |
. . . . . . . 8
⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → (𝑁‘𝐹) ∈
ℝ*) |
31 | 26, 6, 28, 30 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → (𝑁‘𝐹) ∈
ℝ*) |
32 | 31 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (𝑁‘𝐹) ∈
ℝ*) |
33 | | nmoleub2.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
34 | 33 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → 𝐴 ∈
ℝ*) |
35 | 20 | rpred 12628 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → 𝑅 ∈ ℝ) |
36 | | rexmul 12861 |
. . . . . . . . . 10
⊢ ((((𝑀‘(𝐹‘𝑥)) / 𝑅) ∈ ℝ ∧ 𝑅 ∈ ℝ) → (((𝑀‘(𝐹‘𝑥)) / 𝑅) ·e 𝑅) = (((𝑀‘(𝐹‘𝑥)) / 𝑅) · 𝑅)) |
37 | 21, 35, 36 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (((𝑀‘(𝐹‘𝑥)) / 𝑅) ·e 𝑅) = (((𝑀‘(𝐹‘𝑥)) / 𝑅) · 𝑅)) |
38 | 18 | recnd 10861 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (𝑀‘(𝐹‘𝑥)) ∈ ℂ) |
39 | 35 | recnd 10861 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → 𝑅 ∈ ℂ) |
40 | 20 | rpne0d 12633 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → 𝑅 ≠ 0) |
41 | 38, 39, 40 | divcan1d 11609 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (((𝑀‘(𝐹‘𝑥)) / 𝑅) · 𝑅) = (𝑀‘(𝐹‘𝑥))) |
42 | 37, 41 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (((𝑀‘(𝐹‘𝑥)) / 𝑅) ·e 𝑅) = (𝑀‘(𝐹‘𝑥))) |
43 | 18 | rexrd 10883 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (𝑀‘(𝐹‘𝑥)) ∈
ℝ*) |
44 | 26 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → 𝑆 ∈ NrmGrp) |
45 | | nmoleub2.l |
. . . . . . . . . . . . 13
⊢ 𝐿 = (norm‘𝑆) |
46 | 9, 45 | nmcl 23514 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ NrmGrp ∧ 𝑥 ∈ 𝑉) → (𝐿‘𝑥) ∈ ℝ) |
47 | 44, 14, 46 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (𝐿‘𝑥) ∈ ℝ) |
48 | 47 | rexrd 10883 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (𝐿‘𝑥) ∈
ℝ*) |
49 | 32, 48 | xmulcld 12892 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → ((𝑁‘𝐹) ·e (𝐿‘𝑥)) ∈
ℝ*) |
50 | 20 | rpxrd 12629 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → 𝑅 ∈
ℝ*) |
51 | 32, 50 | xmulcld 12892 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → ((𝑁‘𝐹) ·e 𝑅) ∈
ℝ*) |
52 | 28 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
53 | 29, 9, 45, 16 | nmoix 23627 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑥 ∈ 𝑉) → (𝑀‘(𝐹‘𝑥)) ≤ ((𝑁‘𝐹) ·e (𝐿‘𝑥))) |
54 | 44, 7, 52, 14, 53 | syl31anc 1375 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (𝑀‘(𝐹‘𝑥)) ≤ ((𝑁‘𝐹) ·e (𝐿‘𝑥))) |
55 | 29 | nmoge0 23619 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → 0 ≤ (𝑁‘𝐹)) |
56 | 26, 6, 28, 55 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ (𝑁‘𝐹)) |
57 | 31, 56 | jca 515 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁‘𝐹) ∈ ℝ* ∧ 0 ≤
(𝑁‘𝐹))) |
58 | 57 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → ((𝑁‘𝐹) ∈ ℝ* ∧ 0 ≤
(𝑁‘𝐹))) |
59 | | simprr 773 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (𝐿‘𝑥) ≤ 𝑅) |
60 | | xlemul2a 12879 |
. . . . . . . . . 10
⊢ ((((𝐿‘𝑥) ∈ ℝ* ∧ 𝑅 ∈ ℝ*
∧ ((𝑁‘𝐹) ∈ ℝ*
∧ 0 ≤ (𝑁‘𝐹))) ∧ (𝐿‘𝑥) ≤ 𝑅) → ((𝑁‘𝐹) ·e (𝐿‘𝑥)) ≤ ((𝑁‘𝐹) ·e 𝑅)) |
61 | 48, 50, 58, 59, 60 | syl31anc 1375 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → ((𝑁‘𝐹) ·e (𝐿‘𝑥)) ≤ ((𝑁‘𝐹) ·e 𝑅)) |
62 | 43, 49, 51, 54, 61 | xrletrd 12752 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (𝑀‘(𝐹‘𝑥)) ≤ ((𝑁‘𝐹) ·e 𝑅)) |
63 | 42, 62 | eqbrtrd 5075 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (((𝑀‘(𝐹‘𝑥)) / 𝑅) ·e 𝑅) ≤ ((𝑁‘𝐹) ·e 𝑅)) |
64 | | xlemul1 12880 |
. . . . . . . 8
⊢ ((((𝑀‘(𝐹‘𝑥)) / 𝑅) ∈ ℝ* ∧ (𝑁‘𝐹) ∈ ℝ* ∧ 𝑅 ∈ ℝ+)
→ (((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ (𝑁‘𝐹) ↔ (((𝑀‘(𝐹‘𝑥)) / 𝑅) ·e 𝑅) ≤ ((𝑁‘𝐹) ·e 𝑅))) |
65 | 22, 32, 20, 64 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ (𝑁‘𝐹) ↔ (((𝑀‘(𝐹‘𝑥)) / 𝑅) ·e 𝑅) ≤ ((𝑁‘𝐹) ·e 𝑅))) |
66 | 63, 65 | mpbird 260 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ (𝑁‘𝐹)) |
67 | | simplr 769 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → (𝑁‘𝐹) ≤ 𝐴) |
68 | 22, 32, 34, 66, 67 | xrletrd 12752 |
. . . . 5
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ (𝑥 ∈ 𝑉 ∧ (𝐿‘𝑥) ≤ 𝑅)) → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴) |
69 | 68 | expr 460 |
. . . 4
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ 𝑥 ∈ 𝑉) → ((𝐿‘𝑥) ≤ 𝑅 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) |
70 | 2, 69 | syld 47 |
. . 3
⊢ (((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) ∧ 𝑥 ∈ 𝑉) → (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) |
71 | 70 | ralrimiva 3105 |
. 2
⊢ ((𝜑 ∧ (𝑁‘𝐹) ≤ 𝐴) → ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) |
72 | | eqid 2737 |
. . . 4
⊢
(0g‘𝑆) = (0g‘𝑆) |
73 | 26 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) ∧ 𝐴 ∈ ℝ) → 𝑆 ∈ NrmGrp) |
74 | 6 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) ∧ 𝐴 ∈ ℝ) → 𝑇 ∈ NrmGrp) |
75 | 28 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) ∧ 𝐴 ∈ ℝ) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
76 | | simpr 488 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) ∧ 𝐴 ∈ ℝ) → 𝐴 ∈ ℝ) |
77 | | nmoleub2lem.5 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) → 0 ≤ 𝐴) |
78 | 77 | adantr 484 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) ∧ 𝐴 ∈ ℝ) → 0 ≤ 𝐴) |
79 | | nmoleub2lem.6 |
. . . 4
⊢ ((((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) ∧ 𝐴 ∈ ℝ) ∧ (𝑦 ∈ 𝑉 ∧ 𝑦 ≠ (0g‘𝑆))) → (𝑀‘(𝐹‘𝑦)) ≤ (𝐴 · (𝐿‘𝑦))) |
80 | 29, 9, 45, 16, 72, 73, 74, 75, 76, 78, 79 | nmolb2d 23616 |
. . 3
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) ∧ 𝐴 ∈ ℝ) → (𝑁‘𝐹) ≤ 𝐴) |
81 | 31 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) ∧ 𝐴 = +∞) → (𝑁‘𝐹) ∈
ℝ*) |
82 | | pnfge 12722 |
. . . . 5
⊢ ((𝑁‘𝐹) ∈ ℝ* → (𝑁‘𝐹) ≤ +∞) |
83 | 81, 82 | syl 17 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) ∧ 𝐴 = +∞) → (𝑁‘𝐹) ≤ +∞) |
84 | | simpr 488 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) ∧ 𝐴 = +∞) → 𝐴 = +∞) |
85 | 83, 84 | breqtrrd 5081 |
. . 3
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) ∧ 𝐴 = +∞) → (𝑁‘𝐹) ≤ 𝐴) |
86 | 33 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) → 𝐴 ∈
ℝ*) |
87 | | ge0nemnf 12763 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 0 ≤ 𝐴) →
𝐴 ≠
-∞) |
88 | 86, 77, 87 | syl2anc 587 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) → 𝐴 ≠ -∞) |
89 | 86, 88 | jca 515 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) → (𝐴 ∈ ℝ* ∧ 𝐴 ≠
-∞)) |
90 | | xrnemnf 12709 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
↔ (𝐴 ∈ ℝ
∨ 𝐴 =
+∞)) |
91 | 89, 90 | sylib 221 |
. . 3
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) → (𝐴 ∈ ℝ ∨ 𝐴 = +∞)) |
92 | 80, 85, 91 | mpjaodan 959 |
. 2
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴)) → (𝑁‘𝐹) ≤ 𝐴) |
93 | 71, 92 | impbida 801 |
1
⊢ (𝜑 → ((𝑁‘𝐹) ≤ 𝐴 ↔ ∀𝑥 ∈ 𝑉 (𝜓 → ((𝑀‘(𝐹‘𝑥)) / 𝑅) ≤ 𝐴))) |