| Step | Hyp | Ref
| Expression |
| 1 | | nnrecgt0 12309 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 0 < (1
/ 𝑛)) |
| 2 | 1 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 < (1 / 𝑛)) |
| 3 | | nnrecre 12308 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (1 /
𝑛) ∈
ℝ) |
| 4 | 3 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈
ℝ) |
| 5 | | minveco.s |
. . . . . . . . . . . . . 14
⊢ 𝑆 = inf(𝑅, ℝ, < ) |
| 6 | | minveco.x |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑋 = (BaseSet‘𝑈) |
| 7 | | minveco.m |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑀 = ( −𝑣
‘𝑈) |
| 8 | | minveco.n |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑁 =
(normCV‘𝑈) |
| 9 | | minveco.y |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑌 = (BaseSet‘𝑊) |
| 10 | | minveco.u |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑈 ∈
CPreHilOLD) |
| 11 | | minveco.w |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan)) |
| 12 | | minveco.a |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
| 13 | | minveco.d |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐷 = (IndMet‘𝑈) |
| 14 | | minveco.j |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐽 = (MetOpen‘𝐷) |
| 15 | | minveco.r |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) |
| 16 | 6, 7, 8, 9, 10, 11, 12, 13, 14, 15 | minvecolem1 30893 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) |
| 17 | 16 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) |
| 18 | 17 | simp1d 1143 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑅 ⊆ ℝ) |
| 19 | 17 | simp2d 1144 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑅 ≠ ∅) |
| 20 | | 0re 11263 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ |
| 21 | 17 | simp3d 1145 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) |
| 22 | | breq1 5146 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 0 → (𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤)) |
| 23 | 22 | ralbidv 3178 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 0 → (∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) |
| 24 | 23 | rspcev 3622 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℝ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) |
| 25 | 20, 21, 24 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) |
| 26 | | infrecl 12250 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) → inf(𝑅, ℝ, < ) ∈
ℝ) |
| 27 | 18, 19, 25, 26 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → inf(𝑅, ℝ, < ) ∈
ℝ) |
| 28 | 5, 27 | eqeltrid 2845 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑆 ∈ ℝ) |
| 29 | 28 | resqcld 14165 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑆↑2) ∈ ℝ) |
| 30 | 4, 29 | ltaddposd 11847 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (0 < (1 / 𝑛) ↔ (𝑆↑2) < ((𝑆↑2) + (1 / 𝑛)))) |
| 31 | 2, 30 | mpbid 232 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑆↑2) < ((𝑆↑2) + (1 / 𝑛))) |
| 32 | 29, 4 | readdcld 11290 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑆↑2) + (1 / 𝑛)) ∈ ℝ) |
| 33 | 28 | sqge0d 14177 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ (𝑆↑2)) |
| 34 | 29, 4, 33, 2 | addgegt0d 11836 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 < ((𝑆↑2) + (1 / 𝑛))) |
| 35 | 32, 34 | elrpd 13074 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑆↑2) + (1 / 𝑛)) ∈
ℝ+) |
| 36 | 35 | rpge0d 13081 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ ((𝑆↑2) + (1 / 𝑛))) |
| 37 | | resqrtth 15294 |
. . . . . . . . . . 11
⊢ ((((𝑆↑2) + (1 / 𝑛)) ∈ ℝ ∧ 0 ≤
((𝑆↑2) + (1 / 𝑛))) →
((√‘((𝑆↑2)
+ (1 / 𝑛)))↑2) =
((𝑆↑2) + (1 / 𝑛))) |
| 38 | 32, 36, 37 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
((√‘((𝑆↑2)
+ (1 / 𝑛)))↑2) =
((𝑆↑2) + (1 / 𝑛))) |
| 39 | 31, 38 | breqtrrd 5171 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑆↑2) < ((√‘((𝑆↑2) + (1 / 𝑛)))↑2)) |
| 40 | 35 | rpsqrtcld 15450 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
(√‘((𝑆↑2)
+ (1 / 𝑛))) ∈
ℝ+) |
| 41 | 40 | rpred 13077 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
(√‘((𝑆↑2)
+ (1 / 𝑛))) ∈
ℝ) |
| 42 | | 0red 11264 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ∈
ℝ) |
| 43 | | infregelb 12252 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) ∧ 0 ∈ ℝ) → (0 ≤
inf(𝑅, ℝ, < )
↔ ∀𝑤 ∈
𝑅 0 ≤ 𝑤)) |
| 44 | 18, 19, 25, 42, 43 | syl31anc 1375 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (0 ≤ inf(𝑅, ℝ, < ) ↔
∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) |
| 45 | 21, 44 | mpbird 257 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ inf(𝑅, ℝ, <
)) |
| 46 | 45, 5 | breqtrrdi 5185 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ 𝑆) |
| 47 | 32, 36 | sqrtge0d 15459 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤
(√‘((𝑆↑2)
+ (1 / 𝑛)))) |
| 48 | 28, 41, 46, 47 | lt2sqd 14295 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑆 < (√‘((𝑆↑2) + (1 / 𝑛))) ↔ (𝑆↑2) < ((√‘((𝑆↑2) + (1 / 𝑛)))↑2))) |
| 49 | 39, 48 | mpbird 257 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑆 < (√‘((𝑆↑2) + (1 / 𝑛)))) |
| 50 | 28, 41 | ltnled 11408 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑆 < (√‘((𝑆↑2) + (1 / 𝑛))) ↔ ¬ (√‘((𝑆↑2) + (1 / 𝑛))) ≤ 𝑆)) |
| 51 | 49, 50 | mpbid 232 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ¬
(√‘((𝑆↑2)
+ (1 / 𝑛))) ≤ 𝑆) |
| 52 | 5 | breq2i 5151 |
. . . . . . . . 9
⊢
((√‘((𝑆↑2) + (1 / 𝑛))) ≤ 𝑆 ↔ (√‘((𝑆↑2) + (1 / 𝑛))) ≤ inf(𝑅, ℝ, < )) |
| 53 | | infregelb 12252 |
. . . . . . . . . 10
⊢ (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) ∧ (√‘((𝑆↑2) + (1 / 𝑛))) ∈ ℝ) →
((√‘((𝑆↑2)
+ (1 / 𝑛))) ≤ inf(𝑅, ℝ, < ) ↔
∀𝑤 ∈ 𝑅 (√‘((𝑆↑2) + (1 / 𝑛))) ≤ 𝑤)) |
| 54 | 18, 19, 25, 41, 53 | syl31anc 1375 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
((√‘((𝑆↑2)
+ (1 / 𝑛))) ≤ inf(𝑅, ℝ, < ) ↔
∀𝑤 ∈ 𝑅 (√‘((𝑆↑2) + (1 / 𝑛))) ≤ 𝑤)) |
| 55 | 52, 54 | bitrid 283 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
((√‘((𝑆↑2)
+ (1 / 𝑛))) ≤ 𝑆 ↔ ∀𝑤 ∈ 𝑅 (√‘((𝑆↑2) + (1 / 𝑛))) ≤ 𝑤)) |
| 56 | 15 | raleqi 3324 |
. . . . . . . . 9
⊢
(∀𝑤 ∈
𝑅 (√‘((𝑆↑2) + (1 / 𝑛))) ≤ 𝑤 ↔ ∀𝑤 ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))(√‘((𝑆↑2) + (1 / 𝑛))) ≤ 𝑤) |
| 57 | | fvex 6919 |
. . . . . . . . . . 11
⊢ (𝑁‘(𝐴𝑀𝑦)) ∈ V |
| 58 | 57 | rgenw 3065 |
. . . . . . . . . 10
⊢
∀𝑦 ∈
𝑌 (𝑁‘(𝐴𝑀𝑦)) ∈ V |
| 59 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) = (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) |
| 60 | | breq2 5147 |
. . . . . . . . . . 11
⊢ (𝑤 = (𝑁‘(𝐴𝑀𝑦)) → ((√‘((𝑆↑2) + (1 / 𝑛))) ≤ 𝑤 ↔ (√‘((𝑆↑2) + (1 / 𝑛))) ≤ (𝑁‘(𝐴𝑀𝑦)))) |
| 61 | 59, 60 | ralrnmptw 7114 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
𝑌 (𝑁‘(𝐴𝑀𝑦)) ∈ V → (∀𝑤 ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))(√‘((𝑆↑2) + (1 / 𝑛))) ≤ 𝑤 ↔ ∀𝑦 ∈ 𝑌 (√‘((𝑆↑2) + (1 / 𝑛))) ≤ (𝑁‘(𝐴𝑀𝑦)))) |
| 62 | 58, 61 | ax-mp 5 |
. . . . . . . . 9
⊢
(∀𝑤 ∈
ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))(√‘((𝑆↑2) + (1 / 𝑛))) ≤ 𝑤 ↔ ∀𝑦 ∈ 𝑌 (√‘((𝑆↑2) + (1 / 𝑛))) ≤ (𝑁‘(𝐴𝑀𝑦))) |
| 63 | 56, 62 | bitri 275 |
. . . . . . . 8
⊢
(∀𝑤 ∈
𝑅 (√‘((𝑆↑2) + (1 / 𝑛))) ≤ 𝑤 ↔ ∀𝑦 ∈ 𝑌 (√‘((𝑆↑2) + (1 / 𝑛))) ≤ (𝑁‘(𝐴𝑀𝑦))) |
| 64 | 55, 63 | bitrdi 287 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
((√‘((𝑆↑2)
+ (1 / 𝑛))) ≤ 𝑆 ↔ ∀𝑦 ∈ 𝑌 (√‘((𝑆↑2) + (1 / 𝑛))) ≤ (𝑁‘(𝐴𝑀𝑦)))) |
| 65 | 51, 64 | mtbid 324 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ¬ ∀𝑦 ∈ 𝑌 (√‘((𝑆↑2) + (1 / 𝑛))) ≤ (𝑁‘(𝐴𝑀𝑦))) |
| 66 | | rexnal 3100 |
. . . . . 6
⊢
(∃𝑦 ∈
𝑌 ¬
(√‘((𝑆↑2)
+ (1 / 𝑛))) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ ¬ ∀𝑦 ∈ 𝑌 (√‘((𝑆↑2) + (1 / 𝑛))) ≤ (𝑁‘(𝐴𝑀𝑦))) |
| 67 | 65, 66 | sylibr 234 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∃𝑦 ∈ 𝑌 ¬ (√‘((𝑆↑2) + (1 / 𝑛))) ≤ (𝑁‘(𝐴𝑀𝑦))) |
| 68 | 32 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑌) → ((𝑆↑2) + (1 / 𝑛)) ∈ ℝ) |
| 69 | | phnv 30833 |
. . . . . . . . . . . . 13
⊢ (𝑈 ∈ CPreHilOLD
→ 𝑈 ∈
NrmCVec) |
| 70 | 10, 69 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ∈ NrmCVec) |
| 71 | 70 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑌) → 𝑈 ∈ NrmCVec) |
| 72 | 12 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑋) |
| 73 | | inss1 4237 |
. . . . . . . . . . . . . . . 16
⊢
((SubSp‘𝑈)
∩ CBan) ⊆ (SubSp‘𝑈) |
| 74 | 73, 11 | sselid 3981 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑊 ∈ (SubSp‘𝑈)) |
| 75 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(SubSp‘𝑈) =
(SubSp‘𝑈) |
| 76 | 6, 9, 75 | sspba 30746 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) → 𝑌 ⊆ 𝑋) |
| 77 | 70, 74, 76 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑌 ⊆ 𝑋) |
| 78 | 77 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑌 ⊆ 𝑋) |
| 79 | 78 | sselda 3983 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑋) |
| 80 | 6, 7 | nvmcl 30665 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝑀𝑦) ∈ 𝑋) |
| 81 | 71, 72, 79, 80 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑌) → (𝐴𝑀𝑦) ∈ 𝑋) |
| 82 | 6, 8 | nvcl 30680 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝑀𝑦) ∈ 𝑋) → (𝑁‘(𝐴𝑀𝑦)) ∈ ℝ) |
| 83 | 71, 81, 82 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑌) → (𝑁‘(𝐴𝑀𝑦)) ∈ ℝ) |
| 84 | 83 | resqcld 14165 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑌) → ((𝑁‘(𝐴𝑀𝑦))↑2) ∈ ℝ) |
| 85 | 68, 84 | letrid 11413 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑌) → (((𝑆↑2) + (1 / 𝑛)) ≤ ((𝑁‘(𝐴𝑀𝑦))↑2) ∨ ((𝑁‘(𝐴𝑀𝑦))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))) |
| 86 | 85 | ord 865 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑌) → (¬ ((𝑆↑2) + (1 / 𝑛)) ≤ ((𝑁‘(𝐴𝑀𝑦))↑2) → ((𝑁‘(𝐴𝑀𝑦))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))) |
| 87 | 41 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑌) → (√‘((𝑆↑2) + (1 / 𝑛))) ∈ ℝ) |
| 88 | 47 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑌) → 0 ≤ (√‘((𝑆↑2) + (1 / 𝑛)))) |
| 89 | 6, 8 | nvge0 30692 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝑀𝑦) ∈ 𝑋) → 0 ≤ (𝑁‘(𝐴𝑀𝑦))) |
| 90 | 71, 81, 89 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑌) → 0 ≤ (𝑁‘(𝐴𝑀𝑦))) |
| 91 | 87, 83, 88, 90 | le2sqd 14296 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑌) → ((√‘((𝑆↑2) + (1 / 𝑛))) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ ((√‘((𝑆↑2) + (1 / 𝑛)))↑2) ≤ ((𝑁‘(𝐴𝑀𝑦))↑2))) |
| 92 | 38 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑌) → ((√‘((𝑆↑2) + (1 / 𝑛)))↑2) = ((𝑆↑2) + (1 / 𝑛))) |
| 93 | 92 | breq1d 5153 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑌) → (((√‘((𝑆↑2) + (1 / 𝑛)))↑2) ≤ ((𝑁‘(𝐴𝑀𝑦))↑2) ↔ ((𝑆↑2) + (1 / 𝑛)) ≤ ((𝑁‘(𝐴𝑀𝑦))↑2))) |
| 94 | 91, 93 | bitrd 279 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑌) → ((√‘((𝑆↑2) + (1 / 𝑛))) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ ((𝑆↑2) + (1 / 𝑛)) ≤ ((𝑁‘(𝐴𝑀𝑦))↑2))) |
| 95 | 94 | notbid 318 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑌) → (¬ (√‘((𝑆↑2) + (1 / 𝑛))) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ ¬ ((𝑆↑2) + (1 / 𝑛)) ≤ ((𝑁‘(𝐴𝑀𝑦))↑2))) |
| 96 | 6, 7, 8, 13 | imsdval 30705 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐴𝐷𝑦) = (𝑁‘(𝐴𝑀𝑦))) |
| 97 | 71, 72, 79, 96 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑌) → (𝐴𝐷𝑦) = (𝑁‘(𝐴𝑀𝑦))) |
| 98 | 97 | oveq1d 7446 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑌) → ((𝐴𝐷𝑦)↑2) = ((𝑁‘(𝐴𝑀𝑦))↑2)) |
| 99 | 98 | breq1d 5153 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑌) → (((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + (1 / 𝑛)) ↔ ((𝑁‘(𝐴𝑀𝑦))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))) |
| 100 | 86, 95, 99 | 3imtr4d 294 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑌) → (¬ (√‘((𝑆↑2) + (1 / 𝑛))) ≤ (𝑁‘(𝐴𝑀𝑦)) → ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))) |
| 101 | 100 | reximdva 3168 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∃𝑦 ∈ 𝑌 ¬ (√‘((𝑆↑2) + (1 / 𝑛))) ≤ (𝑁‘(𝐴𝑀𝑦)) → ∃𝑦 ∈ 𝑌 ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))) |
| 102 | 67, 101 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∃𝑦 ∈ 𝑌 ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + (1 / 𝑛))) |
| 103 | 102 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑛 ∈ ℕ ∃𝑦 ∈ 𝑌 ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + (1 / 𝑛))) |
| 104 | 9 | fvexi 6920 |
. . . 4
⊢ 𝑌 ∈ V |
| 105 | | nnenom 14021 |
. . . 4
⊢ ℕ
≈ ω |
| 106 | | oveq2 7439 |
. . . . . 6
⊢ (𝑦 = (𝑓‘𝑛) → (𝐴𝐷𝑦) = (𝐴𝐷(𝑓‘𝑛))) |
| 107 | 106 | oveq1d 7446 |
. . . . 5
⊢ (𝑦 = (𝑓‘𝑛) → ((𝐴𝐷𝑦)↑2) = ((𝐴𝐷(𝑓‘𝑛))↑2)) |
| 108 | 107 | breq1d 5153 |
. . . 4
⊢ (𝑦 = (𝑓‘𝑛) → (((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + (1 / 𝑛)) ↔ ((𝐴𝐷(𝑓‘𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))) |
| 109 | 104, 105,
108 | axcc4 10479 |
. . 3
⊢
(∀𝑛 ∈
ℕ ∃𝑦 ∈
𝑌 ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + (1 / 𝑛)) → ∃𝑓(𝑓:ℕ⟶𝑌 ∧ ∀𝑛 ∈ ℕ ((𝐴𝐷(𝑓‘𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))) |
| 110 | 103, 109 | syl 17 |
. 2
⊢ (𝜑 → ∃𝑓(𝑓:ℕ⟶𝑌 ∧ ∀𝑛 ∈ ℕ ((𝐴𝐷(𝑓‘𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))) |
| 111 | 10 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑓:ℕ⟶𝑌 ∧ ∀𝑛 ∈ ℕ ((𝐴𝐷(𝑓‘𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))) → 𝑈 ∈
CPreHilOLD) |
| 112 | 11 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑓:ℕ⟶𝑌 ∧ ∀𝑛 ∈ ℕ ((𝐴𝐷(𝑓‘𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))) → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan)) |
| 113 | 12 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑓:ℕ⟶𝑌 ∧ ∀𝑛 ∈ ℕ ((𝐴𝐷(𝑓‘𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))) → 𝐴 ∈ 𝑋) |
| 114 | | simprl 771 |
. . 3
⊢ ((𝜑 ∧ (𝑓:ℕ⟶𝑌 ∧ ∀𝑛 ∈ ℕ ((𝐴𝐷(𝑓‘𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))) → 𝑓:ℕ⟶𝑌) |
| 115 | | simprr 773 |
. . . 4
⊢ ((𝜑 ∧ (𝑓:ℕ⟶𝑌 ∧ ∀𝑛 ∈ ℕ ((𝐴𝐷(𝑓‘𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))) → ∀𝑛 ∈ ℕ ((𝐴𝐷(𝑓‘𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛))) |
| 116 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → (𝑓‘𝑛) = (𝑓‘𝑘)) |
| 117 | 116 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (𝐴𝐷(𝑓‘𝑛)) = (𝐴𝐷(𝑓‘𝑘))) |
| 118 | 117 | oveq1d 7446 |
. . . . . 6
⊢ (𝑛 = 𝑘 → ((𝐴𝐷(𝑓‘𝑛))↑2) = ((𝐴𝐷(𝑓‘𝑘))↑2)) |
| 119 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (1 / 𝑛) = (1 / 𝑘)) |
| 120 | 119 | oveq2d 7447 |
. . . . . 6
⊢ (𝑛 = 𝑘 → ((𝑆↑2) + (1 / 𝑛)) = ((𝑆↑2) + (1 / 𝑘))) |
| 121 | 118, 120 | breq12d 5156 |
. . . . 5
⊢ (𝑛 = 𝑘 → (((𝐴𝐷(𝑓‘𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)) ↔ ((𝐴𝐷(𝑓‘𝑘))↑2) ≤ ((𝑆↑2) + (1 / 𝑘)))) |
| 122 | 121 | rspccva 3621 |
. . . 4
⊢
((∀𝑛 ∈
ℕ ((𝐴𝐷(𝑓‘𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)) ∧ 𝑘 ∈ ℕ) → ((𝐴𝐷(𝑓‘𝑘))↑2) ≤ ((𝑆↑2) + (1 / 𝑘))) |
| 123 | 115, 122 | sylan 580 |
. . 3
⊢ (((𝜑 ∧ (𝑓:ℕ⟶𝑌 ∧ ∀𝑛 ∈ ℕ ((𝐴𝐷(𝑓‘𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))) ∧ 𝑘 ∈ ℕ) → ((𝐴𝐷(𝑓‘𝑘))↑2) ≤ ((𝑆↑2) + (1 / 𝑘))) |
| 124 | | eqid 2737 |
. . 3
⊢ (1 /
(((((𝐴𝐷((⇝𝑡‘𝐽)‘𝑓)) + 𝑆) / 2)↑2) − (𝑆↑2))) = (1 / (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝑓)) + 𝑆) / 2)↑2) − (𝑆↑2))) |
| 125 | 6, 7, 8, 9, 111, 112, 113, 13, 14, 15, 5, 114, 123, 124 | minvecolem4 30899 |
. 2
⊢ ((𝜑 ∧ (𝑓:ℕ⟶𝑌 ∧ ∀𝑛 ∈ ℕ ((𝐴𝐷(𝑓‘𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))) → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦))) |
| 126 | 110, 125 | exlimddv 1935 |
1
⊢ (𝜑 → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦))) |