Proof of Theorem nrginvrcnlem
| Step | Hyp | Ref
| Expression |
| 1 | | nrginvrcn.t |
. . 3
⊢ 𝑇 = (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) · ((𝑁‘𝐴) / 2)) |
| 2 | | 1rp 13038 |
. . . . 5
⊢ 1 ∈
ℝ+ |
| 3 | | nrginvrcn.r |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ NrmRing) |
| 4 | | nrgngp 24683 |
. . . . . . . 8
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp) |
| 5 | 3, 4 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ NrmGrp) |
| 6 | | nrginvrcn.x |
. . . . . . . . 9
⊢ 𝑋 = (Base‘𝑅) |
| 7 | | nrginvrcn.u |
. . . . . . . . 9
⊢ 𝑈 = (Unit‘𝑅) |
| 8 | 6, 7 | unitss 20376 |
. . . . . . . 8
⊢ 𝑈 ⊆ 𝑋 |
| 9 | | nrginvrcn.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑈) |
| 10 | 8, 9 | sselid 3981 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
| 11 | | nrginvrcn.z |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ NzRing) |
| 12 | | eqid 2737 |
. . . . . . . . 9
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 13 | 7, 12 | nzrunit 20524 |
. . . . . . . 8
⊢ ((𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈) → 𝐴 ≠ (0g‘𝑅)) |
| 14 | 11, 9, 13 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ≠ (0g‘𝑅)) |
| 15 | | nrginvrcn.n |
. . . . . . . 8
⊢ 𝑁 = (norm‘𝑅) |
| 16 | 6, 15, 12 | nmrpcl 24633 |
. . . . . . 7
⊢ ((𝑅 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ (0g‘𝑅)) → (𝑁‘𝐴) ∈
ℝ+) |
| 17 | 5, 10, 14, 16 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → (𝑁‘𝐴) ∈
ℝ+) |
| 18 | | nrginvrcn.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
| 19 | 17, 18 | rpmulcld 13093 |
. . . . 5
⊢ (𝜑 → ((𝑁‘𝐴) · 𝐵) ∈
ℝ+) |
| 20 | | ifcl 4571 |
. . . . 5
⊢ ((1
∈ ℝ+ ∧ ((𝑁‘𝐴) · 𝐵) ∈ ℝ+) → if(1
≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ∈
ℝ+) |
| 21 | 2, 19, 20 | sylancr 587 |
. . . 4
⊢ (𝜑 → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ∈
ℝ+) |
| 22 | 17 | rphalfcld 13089 |
. . . 4
⊢ (𝜑 → ((𝑁‘𝐴) / 2) ∈
ℝ+) |
| 23 | 21, 22 | rpmulcld 13093 |
. . 3
⊢ (𝜑 → (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) · ((𝑁‘𝐴) / 2)) ∈
ℝ+) |
| 24 | 1, 23 | eqeltrid 2845 |
. 2
⊢ (𝜑 → 𝑇 ∈
ℝ+) |
| 25 | 5 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑅 ∈ NrmGrp) |
| 26 | 9 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝐴 ∈ 𝑈) |
| 27 | 6, 7 | unitcl 20375 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑈 → 𝐴 ∈ 𝑋) |
| 28 | 26, 27 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝐴 ∈ 𝑋) |
| 29 | 6, 15 | nmcl 24629 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ ℝ) |
| 30 | 25, 28, 29 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝐴) ∈ ℝ) |
| 31 | 30 | recnd 11289 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝐴) ∈ ℂ) |
| 32 | | simprl 771 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑦 ∈ 𝑈) |
| 33 | 8, 32 | sselid 3981 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑦 ∈ 𝑋) |
| 34 | 6, 15 | nmcl 24629 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ NrmGrp ∧ 𝑦 ∈ 𝑋) → (𝑁‘𝑦) ∈ ℝ) |
| 35 | 25, 33, 34 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝑦) ∈ ℝ) |
| 36 | 35 | recnd 11289 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝑦) ∈ ℂ) |
| 37 | | ngpgrp 24612 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ NrmGrp → 𝑅 ∈ Grp) |
| 38 | 25, 37 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑅 ∈ Grp) |
| 39 | | nrgring 24684 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ Ring) |
| 40 | 3, 39 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 41 | 40 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑅 ∈ Ring) |
| 42 | | nrginvrcn.i |
. . . . . . . . . . . . . 14
⊢ 𝐼 = (invr‘𝑅) |
| 43 | 7, 42, 6 | ringinvcl 20392 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈) → (𝐼‘𝐴) ∈ 𝑋) |
| 44 | 41, 26, 43 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐼‘𝐴) ∈ 𝑋) |
| 45 | 7, 42, 6 | ringinvcl 20392 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝑈) → (𝐼‘𝑦) ∈ 𝑋) |
| 46 | 41, 32, 45 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐼‘𝑦) ∈ 𝑋) |
| 47 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(-g‘𝑅) = (-g‘𝑅) |
| 48 | 6, 47 | grpsubcl 19038 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Grp ∧ (𝐼‘𝐴) ∈ 𝑋 ∧ (𝐼‘𝑦) ∈ 𝑋) → ((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)) ∈ 𝑋) |
| 49 | 38, 44, 46, 48 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)) ∈ 𝑋) |
| 50 | 6, 15 | nmcl 24629 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ NrmGrp ∧ ((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)) ∈ 𝑋) → (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) ∈ ℝ) |
| 51 | 25, 49, 50 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) ∈ ℝ) |
| 52 | 51 | recnd 11289 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) ∈ ℂ) |
| 53 | 31, 36, 52 | mul32d 11471 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · (𝑁‘𝑦)) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = (((𝑁‘𝐴) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦))) |
| 54 | 3 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑅 ∈ NrmRing) |
| 55 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 56 | 6, 15, 55 | nmmul 24685 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ NrmRing ∧ 𝐴 ∈ 𝑋 ∧ ((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)) ∈ 𝑋) → (𝑁‘(𝐴(.r‘𝑅)((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = ((𝑁‘𝐴) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))))) |
| 57 | 54, 28, 49, 56 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(𝐴(.r‘𝑅)((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = ((𝑁‘𝐴) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))))) |
| 58 | 6, 55, 47, 41, 28, 44, 46 | ringsubdi 20304 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) = ((𝐴(.r‘𝑅)(𝐼‘𝐴))(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))) |
| 59 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(1r‘𝑅) = (1r‘𝑅) |
| 60 | 7, 42, 55, 59 | unitrinv 20394 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈) → (𝐴(.r‘𝑅)(𝐼‘𝐴)) = (1r‘𝑅)) |
| 61 | 41, 26, 60 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)(𝐼‘𝐴)) = (1r‘𝑅)) |
| 62 | 61 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐴(.r‘𝑅)(𝐼‘𝐴))(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))) = ((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))) |
| 63 | 58, 62 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) = ((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))) |
| 64 | 63 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(𝐴(.r‘𝑅)((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = (𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))))) |
| 65 | 57, 64 | eqtr3d 2779 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = (𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))))) |
| 66 | 65 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦)) = ((𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦))) |
| 67 | 6, 59 | ringidcl 20262 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ 𝑋) |
| 68 | 41, 67 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (1r‘𝑅) ∈ 𝑋) |
| 69 | 6, 55 | ringcl 20247 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑋 ∧ (𝐼‘𝑦) ∈ 𝑋) → (𝐴(.r‘𝑅)(𝐼‘𝑦)) ∈ 𝑋) |
| 70 | 41, 28, 46, 69 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)(𝐼‘𝑦)) ∈ 𝑋) |
| 71 | 6, 47 | grpsubcl 19038 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Grp ∧
(1r‘𝑅)
∈ 𝑋 ∧ (𝐴(.r‘𝑅)(𝐼‘𝑦)) ∈ 𝑋) → ((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))) ∈ 𝑋) |
| 72 | 38, 68, 70, 71 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))) ∈ 𝑋) |
| 73 | 6, 15, 55 | nmmul 24685 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ NrmRing ∧
((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦))) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑁‘(((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))(.r‘𝑅)𝑦)) = ((𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦))) |
| 74 | 54, 72, 33, 73 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))(.r‘𝑅)𝑦)) = ((𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦))) |
| 75 | 6, 55, 47, 41, 68, 70, 33 | ringsubdir 20305 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))(.r‘𝑅)𝑦) = (((1r‘𝑅)(.r‘𝑅)𝑦)(-g‘𝑅)((𝐴(.r‘𝑅)(𝐼‘𝑦))(.r‘𝑅)𝑦))) |
| 76 | 6, 55, 59 | ringlidm 20266 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝑋) → ((1r‘𝑅)(.r‘𝑅)𝑦) = 𝑦) |
| 77 | 41, 33, 76 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((1r‘𝑅)(.r‘𝑅)𝑦) = 𝑦) |
| 78 | 6, 55 | ringass 20250 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ (𝐴 ∈ 𝑋 ∧ (𝐼‘𝑦) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐴(.r‘𝑅)(𝐼‘𝑦))(.r‘𝑅)𝑦) = (𝐴(.r‘𝑅)((𝐼‘𝑦)(.r‘𝑅)𝑦))) |
| 79 | 41, 28, 46, 33, 78 | syl13anc 1374 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐴(.r‘𝑅)(𝐼‘𝑦))(.r‘𝑅)𝑦) = (𝐴(.r‘𝑅)((𝐼‘𝑦)(.r‘𝑅)𝑦))) |
| 80 | 7, 42, 55, 59 | unitlinv 20393 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝑈) → ((𝐼‘𝑦)(.r‘𝑅)𝑦) = (1r‘𝑅)) |
| 81 | 41, 32, 80 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐼‘𝑦)(.r‘𝑅)𝑦) = (1r‘𝑅)) |
| 82 | 81 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)((𝐼‘𝑦)(.r‘𝑅)𝑦)) = (𝐴(.r‘𝑅)(1r‘𝑅))) |
| 83 | 6, 55, 59 | ringridm 20267 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑋) → (𝐴(.r‘𝑅)(1r‘𝑅)) = 𝐴) |
| 84 | 41, 28, 83 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴(.r‘𝑅)(1r‘𝑅)) = 𝐴) |
| 85 | 79, 82, 84 | 3eqtrd 2781 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐴(.r‘𝑅)(𝐼‘𝑦))(.r‘𝑅)𝑦) = 𝐴) |
| 86 | 77, 85 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((1r‘𝑅)(.r‘𝑅)𝑦)(-g‘𝑅)((𝐴(.r‘𝑅)(𝐼‘𝑦))(.r‘𝑅)𝑦)) = (𝑦(-g‘𝑅)𝐴)) |
| 87 | 75, 86 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))(.r‘𝑅)𝑦) = (𝑦(-g‘𝑅)𝐴)) |
| 88 | 87 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))(.r‘𝑅)𝑦)) = (𝑁‘(𝑦(-g‘𝑅)𝐴))) |
| 89 | 74, 88 | eqtr3d 2779 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘((1r‘𝑅)(-g‘𝑅)(𝐴(.r‘𝑅)(𝐼‘𝑦)))) · (𝑁‘𝑦)) = (𝑁‘(𝑦(-g‘𝑅)𝐴))) |
| 90 | 53, 66, 89 | 3eqtrd 2781 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · (𝑁‘𝑦)) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = (𝑁‘(𝑦(-g‘𝑅)𝐴))) |
| 91 | 6, 47 | grpsubcl 19038 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Grp ∧ 𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝑦(-g‘𝑅)𝐴) ∈ 𝑋) |
| 92 | 38, 33, 28, 91 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑦(-g‘𝑅)𝐴) ∈ 𝑋) |
| 93 | 6, 15 | nmcl 24629 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ NrmGrp ∧ (𝑦(-g‘𝑅)𝐴) ∈ 𝑋) → (𝑁‘(𝑦(-g‘𝑅)𝐴)) ∈ ℝ) |
| 94 | 25, 92, 93 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(𝑦(-g‘𝑅)𝐴)) ∈ ℝ) |
| 95 | 94 | recnd 11289 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘(𝑦(-g‘𝑅)𝐴)) ∈ ℂ) |
| 96 | 17 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝐴) ∈
ℝ+) |
| 97 | 11 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑅 ∈ NzRing) |
| 98 | 7, 12 | nzrunit 20524 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ NzRing ∧ 𝑦 ∈ 𝑈) → 𝑦 ≠ (0g‘𝑅)) |
| 99 | 97, 32, 98 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑦 ≠ (0g‘𝑅)) |
| 100 | 6, 15, 12 | nmrpcl 24633 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ NrmGrp ∧ 𝑦 ∈ 𝑋 ∧ 𝑦 ≠ (0g‘𝑅)) → (𝑁‘𝑦) ∈
ℝ+) |
| 101 | 25, 33, 99, 100 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝑦) ∈
ℝ+) |
| 102 | 96, 101 | rpmulcld 13093 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · (𝑁‘𝑦)) ∈
ℝ+) |
| 103 | 102 | rpred 13077 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · (𝑁‘𝑦)) ∈ ℝ) |
| 104 | 103 | recnd 11289 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · (𝑁‘𝑦)) ∈ ℂ) |
| 105 | 102 | rpne0d 13082 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · (𝑁‘𝑦)) ≠ 0) |
| 106 | 95, 104, 52, 105 | divmuld 12065 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘(𝑦(-g‘𝑅)𝐴)) / ((𝑁‘𝐴) · (𝑁‘𝑦))) = (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦))) ↔ (((𝑁‘𝐴) · (𝑁‘𝑦)) · (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) = (𝑁‘(𝑦(-g‘𝑅)𝐴)))) |
| 107 | 90, 106 | mpbird 257 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘(𝑦(-g‘𝑅)𝐴)) / ((𝑁‘𝐴) · (𝑁‘𝑦))) = (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) |
| 108 | | nrginvrcn.d |
. . . . . . . . 9
⊢ 𝐷 = (dist‘𝑅) |
| 109 | 15, 6, 47, 108 | ngpdsr 24618 |
. . . . . . . 8
⊢ ((𝑅 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝐷𝑦) = (𝑁‘(𝑦(-g‘𝑅)𝐴))) |
| 110 | 25, 28, 33, 109 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) = (𝑁‘(𝑦(-g‘𝑅)𝐴))) |
| 111 | 110 | oveq1d 7446 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐴𝐷𝑦) / ((𝑁‘𝐴) · (𝑁‘𝑦))) = ((𝑁‘(𝑦(-g‘𝑅)𝐴)) / ((𝑁‘𝐴) · (𝑁‘𝑦)))) |
| 112 | 15, 6, 47, 108 | ngpds 24617 |
. . . . . . 7
⊢ ((𝑅 ∈ NrmGrp ∧ (𝐼‘𝐴) ∈ 𝑋 ∧ (𝐼‘𝑦) ∈ 𝑋) → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) = (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) |
| 113 | 25, 44, 46, 112 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) = (𝑁‘((𝐼‘𝐴)(-g‘𝑅)(𝐼‘𝑦)))) |
| 114 | 107, 111,
113 | 3eqtr4rd 2788 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) = ((𝐴𝐷𝑦) / ((𝑁‘𝐴) · (𝑁‘𝑦)))) |
| 115 | 110, 94 | eqeltrd 2841 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) ∈ ℝ) |
| 116 | 24 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 ∈
ℝ+) |
| 117 | 116 | rpred 13077 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 ∈ ℝ) |
| 118 | 18 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝐵 ∈
ℝ+) |
| 119 | 118 | rpred 13077 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝐵 ∈ ℝ) |
| 120 | 103, 119 | remulcld 11291 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵) ∈ ℝ) |
| 121 | | simprr 773 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) < 𝑇) |
| 122 | 19 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · 𝐵) ∈
ℝ+) |
| 123 | 96 | rphalfcld 13089 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) / 2) ∈
ℝ+) |
| 124 | 122, 123 | rpmulcld 13093 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2)) ∈
ℝ+) |
| 125 | 124 | rpred 13077 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2)) ∈ ℝ) |
| 126 | | 1re 11261 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
| 127 | 122 | rpred 13077 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) · 𝐵) ∈ ℝ) |
| 128 | | min2 13232 |
. . . . . . . . . . 11
⊢ ((1
∈ ℝ ∧ ((𝑁‘𝐴) · 𝐵) ∈ ℝ) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ≤ ((𝑁‘𝐴) · 𝐵)) |
| 129 | 126, 127,
128 | sylancr 587 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ≤ ((𝑁‘𝐴) · 𝐵)) |
| 130 | 21 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ∈
ℝ+) |
| 131 | 130 | rpred 13077 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ∈ ℝ) |
| 132 | 131, 127,
123 | lemul1d 13120 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ≤ ((𝑁‘𝐴) · 𝐵) ↔ (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) · ((𝑁‘𝐴) / 2)) ≤ (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2)))) |
| 133 | 129, 132 | mpbid 232 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) · ((𝑁‘𝐴) / 2)) ≤ (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2))) |
| 134 | 1, 133 | eqbrtrid 5178 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 ≤ (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2))) |
| 135 | 123 | rpred 13077 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) / 2) ∈ ℝ) |
| 136 | 31 | 2halvesd 12512 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) / 2) + ((𝑁‘𝐴) / 2)) = (𝑁‘𝐴)) |
| 137 | 30, 35 | resubcld 11691 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) − (𝑁‘𝑦)) ∈ ℝ) |
| 138 | 6, 15, 47 | nm2dif 24638 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑁‘𝐴) − (𝑁‘𝑦)) ≤ (𝑁‘(𝐴(-g‘𝑅)𝑦))) |
| 139 | 25, 28, 33, 138 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) − (𝑁‘𝑦)) ≤ (𝑁‘(𝐴(-g‘𝑅)𝑦))) |
| 140 | 15, 6, 47, 108 | ngpds 24617 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝐷𝑦) = (𝑁‘(𝐴(-g‘𝑅)𝑦))) |
| 141 | 25, 28, 33, 140 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) = (𝑁‘(𝐴(-g‘𝑅)𝑦))) |
| 142 | 139, 141 | breqtrrd 5171 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) − (𝑁‘𝑦)) ≤ (𝐴𝐷𝑦)) |
| 143 | | min1 13231 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℝ ∧ ((𝑁‘𝐴) · 𝐵) ∈ ℝ) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ≤ 1) |
| 144 | 126, 127,
143 | sylancr 587 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ≤ 1) |
| 145 | | 1red 11262 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 1 ∈ ℝ) |
| 146 | 131, 145,
123 | lemul1d 13120 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) ≤ 1 ↔ (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) · ((𝑁‘𝐴) / 2)) ≤ (1 · ((𝑁‘𝐴) / 2)))) |
| 147 | 144, 146 | mpbid 232 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (if(1 ≤ ((𝑁‘𝐴) · 𝐵), 1, ((𝑁‘𝐴) · 𝐵)) · ((𝑁‘𝐴) / 2)) ≤ (1 · ((𝑁‘𝐴) / 2))) |
| 148 | 1, 147 | eqbrtrid 5178 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 ≤ (1 · ((𝑁‘𝐴) / 2))) |
| 149 | 135 | recnd 11289 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) / 2) ∈ ℂ) |
| 150 | 149 | mullidd 11279 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (1 · ((𝑁‘𝐴) / 2)) = ((𝑁‘𝐴) / 2)) |
| 151 | 148, 150 | breqtrd 5169 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 ≤ ((𝑁‘𝐴) / 2)) |
| 152 | 115, 117,
135, 121, 151 | ltletrd 11421 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) < ((𝑁‘𝐴) / 2)) |
| 153 | 137, 115,
135, 142, 152 | lelttrd 11419 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) − (𝑁‘𝑦)) < ((𝑁‘𝐴) / 2)) |
| 154 | 30, 35, 135 | ltsubadd2d 11861 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) − (𝑁‘𝑦)) < ((𝑁‘𝐴) / 2) ↔ (𝑁‘𝐴) < ((𝑁‘𝑦) + ((𝑁‘𝐴) / 2)))) |
| 155 | 153, 154 | mpbid 232 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝑁‘𝐴) < ((𝑁‘𝑦) + ((𝑁‘𝐴) / 2))) |
| 156 | 136, 155 | eqbrtrd 5165 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) / 2) + ((𝑁‘𝐴) / 2)) < ((𝑁‘𝑦) + ((𝑁‘𝐴) / 2))) |
| 157 | 135, 35, 135 | ltadd1d 11856 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) / 2) < (𝑁‘𝑦) ↔ (((𝑁‘𝐴) / 2) + ((𝑁‘𝐴) / 2)) < ((𝑁‘𝑦) + ((𝑁‘𝐴) / 2)))) |
| 158 | 156, 157 | mpbird 257 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝑁‘𝐴) / 2) < (𝑁‘𝑦)) |
| 159 | 135, 35, 122, 158 | ltmul2dd 13133 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2)) < (((𝑁‘𝐴) · 𝐵) · (𝑁‘𝑦))) |
| 160 | 119 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝐵 ∈ ℂ) |
| 161 | 31, 36, 160 | mul32d 11471 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵) = (((𝑁‘𝐴) · 𝐵) · (𝑁‘𝑦))) |
| 162 | 159, 161 | breqtrrd 5171 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝑁‘𝐴) · 𝐵) · ((𝑁‘𝐴) / 2)) < (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵)) |
| 163 | 117, 125,
120, 134, 162 | lelttrd 11419 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → 𝑇 < (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵)) |
| 164 | 115, 117,
120, 121, 163 | lttrd 11422 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (𝐴𝐷𝑦) < (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵)) |
| 165 | 115, 119,
102 | ltdivmuld 13128 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → (((𝐴𝐷𝑦) / ((𝑁‘𝐴) · (𝑁‘𝑦))) < 𝐵 ↔ (𝐴𝐷𝑦) < (((𝑁‘𝐴) · (𝑁‘𝑦)) · 𝐵))) |
| 166 | 164, 165 | mpbird 257 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐴𝐷𝑦) / ((𝑁‘𝐴) · (𝑁‘𝑦))) < 𝐵) |
| 167 | 114, 166 | eqbrtrd 5165 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑈 ∧ (𝐴𝐷𝑦) < 𝑇)) → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵) |
| 168 | 167 | expr 456 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑈) → ((𝐴𝐷𝑦) < 𝑇 → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵)) |
| 169 | 168 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ 𝑈 ((𝐴𝐷𝑦) < 𝑇 → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵)) |
| 170 | | breq2 5147 |
. . 3
⊢ (𝑥 = 𝑇 → ((𝐴𝐷𝑦) < 𝑥 ↔ (𝐴𝐷𝑦) < 𝑇)) |
| 171 | 170 | rspceaimv 3628 |
. 2
⊢ ((𝑇 ∈ ℝ+
∧ ∀𝑦 ∈
𝑈 ((𝐴𝐷𝑦) < 𝑇 → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵)) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝑈 ((𝐴𝐷𝑦) < 𝑥 → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵)) |
| 172 | 24, 169, 171 | syl2anc 584 |
1
⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝑈 ((𝐴𝐷𝑦) < 𝑥 → ((𝐼‘𝐴)𝐷(𝐼‘𝑦)) < 𝐵)) |