| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | lncon.1 | . . 3
⊢ (𝑇 ∈ 𝐶 → 𝑆 ∈ ℝ) | 
| 2 |  | lncon.2 | . . . 4
⊢ ((𝑇 ∈ 𝐶 ∧ 𝑦 ∈ ℋ) → (𝑁‘(𝑇‘𝑦)) ≤ (𝑆 ·
(normℎ‘𝑦))) | 
| 3 | 2 | ralrimiva 3146 | . . 3
⊢ (𝑇 ∈ 𝐶 → ∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑆 ·
(normℎ‘𝑦))) | 
| 4 |  | oveq1 7438 | . . . . . 6
⊢ (𝑥 = 𝑆 → (𝑥 ·
(normℎ‘𝑦)) = (𝑆 ·
(normℎ‘𝑦))) | 
| 5 | 4 | breq2d 5155 | . . . . 5
⊢ (𝑥 = 𝑆 → ((𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦)) ↔ (𝑁‘(𝑇‘𝑦)) ≤ (𝑆 ·
(normℎ‘𝑦)))) | 
| 6 | 5 | ralbidv 3178 | . . . 4
⊢ (𝑥 = 𝑆 → (∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦)) ↔ ∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑆 ·
(normℎ‘𝑦)))) | 
| 7 | 6 | rspcev 3622 | . . 3
⊢ ((𝑆 ∈ ℝ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑆 ·
(normℎ‘𝑦))) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦))) | 
| 8 | 1, 3, 7 | syl2anc 584 | . 2
⊢ (𝑇 ∈ 𝐶 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦))) | 
| 9 |  | arch 12523 | . . . . . 6
⊢ (𝑥 ∈ ℝ →
∃𝑛 ∈ ℕ
𝑥 < 𝑛) | 
| 10 | 9 | adantr 480 | . . . . 5
⊢ ((𝑥 ∈ ℝ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦))) → ∃𝑛 ∈ ℕ 𝑥 < 𝑛) | 
| 11 |  | nnre 12273 | . . . . . . 7
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ) | 
| 12 |  | simplll 775 | . . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) ∧ 𝑦 ∈ ℋ) → 𝑥 ∈ ℝ) | 
| 13 |  | simpllr 776 | . . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) ∧ 𝑦 ∈ ℋ) → 𝑛 ∈ ℝ) | 
| 14 |  | normcl 31144 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℋ →
(normℎ‘𝑦) ∈ ℝ) | 
| 15 | 14 | adantl 481 | . . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) ∧ 𝑦 ∈ ℋ) →
(normℎ‘𝑦) ∈ ℝ) | 
| 16 |  | normge0 31145 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℋ → 0 ≤
(normℎ‘𝑦)) | 
| 17 | 16 | adantl 481 | . . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) ∧ 𝑦 ∈ ℋ) → 0 ≤
(normℎ‘𝑦)) | 
| 18 |  | ltle 11349 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (𝑥 < 𝑛 → 𝑥 ≤ 𝑛)) | 
| 19 | 18 | imp 406 | . . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) → 𝑥 ≤ 𝑛) | 
| 20 | 19 | adantr 480 | . . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) ∧ 𝑦 ∈ ℋ) → 𝑥 ≤ 𝑛) | 
| 21 | 12, 13, 15, 17, 20 | lemul1ad 12207 | . . . . . . . . . . 11
⊢ ((((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) ∧ 𝑦 ∈ ℋ) → (𝑥 ·
(normℎ‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) | 
| 22 |  | lncon.4 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℋ → (𝑁‘(𝑇‘𝑦)) ∈ ℝ) | 
| 23 | 22 | adantl 481 | . . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) ∧ 𝑦 ∈ ℋ) → (𝑁‘(𝑇‘𝑦)) ∈ ℝ) | 
| 24 |  | simpll 767 | . . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) → 𝑥 ∈ ℝ) | 
| 25 |  | remulcl 11240 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧
(normℎ‘𝑦) ∈ ℝ) → (𝑥 ·
(normℎ‘𝑦)) ∈ ℝ) | 
| 26 | 24, 14, 25 | syl2an 596 | . . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) ∧ 𝑦 ∈ ℋ) → (𝑥 ·
(normℎ‘𝑦)) ∈ ℝ) | 
| 27 |  | simplr 769 | . . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) → 𝑛 ∈ ℝ) | 
| 28 |  | remulcl 11240 | . . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℝ ∧
(normℎ‘𝑦) ∈ ℝ) → (𝑛 ·
(normℎ‘𝑦)) ∈ ℝ) | 
| 29 | 27, 14, 28 | syl2an 596 | . . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) ∧ 𝑦 ∈ ℋ) → (𝑛 ·
(normℎ‘𝑦)) ∈ ℝ) | 
| 30 |  | letr 11355 | . . . . . . . . . . . 12
⊢ (((𝑁‘(𝑇‘𝑦)) ∈ ℝ ∧ (𝑥 ·
(normℎ‘𝑦)) ∈ ℝ ∧ (𝑛 ·
(normℎ‘𝑦)) ∈ ℝ) → (((𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦)) ∧ (𝑥 ·
(normℎ‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) → (𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦)))) | 
| 31 | 23, 26, 29, 30 | syl3anc 1373 | . . . . . . . . . . 11
⊢ ((((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) ∧ 𝑦 ∈ ℋ) → (((𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦)) ∧ (𝑥 ·
(normℎ‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) → (𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦)))) | 
| 32 | 21, 31 | mpan2d 694 | . . . . . . . . . 10
⊢ ((((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) ∧ 𝑦 ∈ ℋ) → ((𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦)) → (𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦)))) | 
| 33 | 32 | ralimdva 3167 | . . . . . . . . 9
⊢ (((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) → (∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦)) → ∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦)))) | 
| 34 | 33 | impancom 451 | . . . . . . . 8
⊢ (((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦))) → (𝑥 < 𝑛 → ∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦)))) | 
| 35 | 34 | an32s 652 | . . . . . . 7
⊢ (((𝑥 ∈ ℝ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦))) ∧ 𝑛 ∈ ℝ) → (𝑥 < 𝑛 → ∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦)))) | 
| 36 | 11, 35 | sylan2 593 | . . . . . 6
⊢ (((𝑥 ∈ ℝ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦))) ∧ 𝑛 ∈ ℕ) → (𝑥 < 𝑛 → ∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦)))) | 
| 37 | 36 | reximdva 3168 | . . . . 5
⊢ ((𝑥 ∈ ℝ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦))) → (∃𝑛 ∈ ℕ 𝑥 < 𝑛 → ∃𝑛 ∈ ℕ ∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦)))) | 
| 38 | 10, 37 | mpd 15 | . . . 4
⊢ ((𝑥 ∈ ℝ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦))) → ∃𝑛 ∈ ℕ ∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) | 
| 39 | 38 | rexlimiva 3147 | . . 3
⊢
(∃𝑥 ∈
ℝ ∀𝑦 ∈
ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦)) → ∃𝑛 ∈ ℕ ∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) | 
| 40 |  | simprr 773 | . . . . . . . 8
⊢ (((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ (𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)) → 𝑧 ∈
ℝ+) | 
| 41 |  | simpll 767 | . . . . . . . . 9
⊢ (((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ (𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)) → 𝑛 ∈
ℕ) | 
| 42 | 41 | nnrpd 13075 | . . . . . . . 8
⊢ (((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ (𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)) → 𝑛 ∈
ℝ+) | 
| 43 | 40, 42 | rpdivcld 13094 | . . . . . . 7
⊢ (((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ (𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)) → (𝑧 / 𝑛) ∈
ℝ+) | 
| 44 |  | simprr 773 | . . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)
∧ 𝑤 ∈ ℋ))
→ 𝑤 ∈
ℋ) | 
| 45 |  | simprll 779 | . . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)
∧ 𝑤 ∈ ℋ))
→ 𝑥 ∈
ℋ) | 
| 46 |  | hvsubcl 31036 | . . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ ℋ ∧ 𝑥 ∈ ℋ) → (𝑤 −ℎ
𝑥) ∈
ℋ) | 
| 47 | 44, 45, 46 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)
∧ 𝑤 ∈ ℋ))
→ (𝑤
−ℎ 𝑥) ∈ ℋ) | 
| 48 |  | 2fveq3 6911 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑤 −ℎ 𝑥) → (𝑁‘(𝑇‘𝑦)) = (𝑁‘(𝑇‘(𝑤 −ℎ 𝑥)))) | 
| 49 |  | fveq2 6906 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑤 −ℎ 𝑥) →
(normℎ‘𝑦) = (normℎ‘(𝑤 −ℎ
𝑥))) | 
| 50 | 49 | oveq2d 7447 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑤 −ℎ 𝑥) → (𝑛 ·
(normℎ‘𝑦)) = (𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥)))) | 
| 51 | 48, 50 | breq12d 5156 | . . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑤 −ℎ 𝑥) → ((𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦)) ↔ (𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) ≤ (𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥))))) | 
| 52 | 51 | rspcva 3620 | . . . . . . . . . . . . 13
⊢ (((𝑤 −ℎ
𝑥) ∈ ℋ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) → (𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) ≤ (𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥)))) | 
| 53 | 47, 52 | sylan 580 | . . . . . . . . . . . 12
⊢ (((𝑛 ∈ ℕ ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)
∧ 𝑤 ∈ ℋ))
∧ ∀𝑦 ∈
ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) → (𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) ≤ (𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥)))) | 
| 54 | 53 | an32s 652 | . . . . . . . . . . 11
⊢ (((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℋ)) → (𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) ≤ (𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥)))) | 
| 55 | 48 | eleq1d 2826 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑤 −ℎ 𝑥) → ((𝑁‘(𝑇‘𝑦)) ∈ ℝ ↔ (𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) ∈
ℝ)) | 
| 56 | 55, 22 | vtoclga 3577 | . . . . . . . . . . . . . 14
⊢ ((𝑤 −ℎ
𝑥) ∈ ℋ →
(𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) ∈
ℝ) | 
| 57 | 47, 56 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)
∧ 𝑤 ∈ ℋ))
→ (𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) ∈
ℝ) | 
| 58 | 11 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)
∧ 𝑤 ∈ ℋ))
→ 𝑛 ∈
ℝ) | 
| 59 |  | normcl 31144 | . . . . . . . . . . . . . . 15
⊢ ((𝑤 −ℎ
𝑥) ∈ ℋ →
(normℎ‘(𝑤 −ℎ 𝑥)) ∈
ℝ) | 
| 60 | 47, 59 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)
∧ 𝑤 ∈ ℋ))
→ (normℎ‘(𝑤 −ℎ 𝑥)) ∈
ℝ) | 
| 61 |  | remulcl 11240 | . . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℝ ∧
(normℎ‘(𝑤 −ℎ 𝑥)) ∈ ℝ) → (𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥))) ∈
ℝ) | 
| 62 | 58, 60, 61 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)
∧ 𝑤 ∈ ℋ))
→ (𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥))) ∈
ℝ) | 
| 63 |  | simprlr 780 | . . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)
∧ 𝑤 ∈ ℋ))
→ 𝑧 ∈
ℝ+) | 
| 64 | 63 | rpred 13077 | . . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)
∧ 𝑤 ∈ ℋ))
→ 𝑧 ∈
ℝ) | 
| 65 |  | lelttr 11351 | . . . . . . . . . . . . 13
⊢ (((𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) ∈ ℝ ∧ (𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥))) ∈ ℝ ∧ 𝑧 ∈ ℝ) → (((𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) ≤ (𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥))) ∧ (𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥))) < 𝑧) → (𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) < 𝑧)) | 
| 66 | 57, 62, 64, 65 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℕ ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)
∧ 𝑤 ∈ ℋ))
→ (((𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) ≤ (𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥))) ∧ (𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥))) < 𝑧) → (𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) < 𝑧)) | 
| 67 | 66 | adantlr 715 | . . . . . . . . . . 11
⊢ (((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℋ)) →
(((𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) ≤ (𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥))) ∧ (𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥))) < 𝑧) → (𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) < 𝑧)) | 
| 68 | 54, 67 | mpand 695 | . . . . . . . . . 10
⊢ (((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℋ)) → ((𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥))) < 𝑧 → (𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) < 𝑧)) | 
| 69 |  | nnrp 13046 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ+) | 
| 70 | 69 | rpregt0d 13083 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (𝑛 ∈ ℝ ∧ 0 <
𝑛)) | 
| 71 | 70 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℕ ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)
∧ 𝑤 ∈ ℋ))
→ (𝑛 ∈ ℝ
∧ 0 < 𝑛)) | 
| 72 |  | ltmuldiv2 12142 | . . . . . . . . . . . 12
⊢
(((normℎ‘(𝑤 −ℎ 𝑥)) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ (𝑛 ∈ ℝ ∧ 0 <
𝑛)) → ((𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥))) < 𝑧 ↔ (normℎ‘(𝑤 −ℎ
𝑥)) < (𝑧 / 𝑛))) | 
| 73 | 60, 64, 71, 72 | syl3anc 1373 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)
∧ 𝑤 ∈ ℋ))
→ ((𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥))) < 𝑧 ↔ (normℎ‘(𝑤 −ℎ
𝑥)) < (𝑧 / 𝑛))) | 
| 74 | 73 | adantlr 715 | . . . . . . . . . 10
⊢ (((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℋ)) → ((𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥))) < 𝑧 ↔ (normℎ‘(𝑤 −ℎ
𝑥)) < (𝑧 / 𝑛))) | 
| 75 |  | lncon.5 | . . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ ℋ ∧ 𝑥 ∈ ℋ) → (𝑇‘(𝑤 −ℎ 𝑥)) = ((𝑇‘𝑤)𝑀(𝑇‘𝑥))) | 
| 76 | 44, 45, 75 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)
∧ 𝑤 ∈ ℋ))
→ (𝑇‘(𝑤 −ℎ
𝑥)) = ((𝑇‘𝑤)𝑀(𝑇‘𝑥))) | 
| 77 | 76 | adantlr 715 | . . . . . . . . . . . 12
⊢ (((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℋ)) → (𝑇‘(𝑤 −ℎ 𝑥)) = ((𝑇‘𝑤)𝑀(𝑇‘𝑥))) | 
| 78 | 77 | fveq2d 6910 | . . . . . . . . . . 11
⊢ (((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℋ)) → (𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) = (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥)))) | 
| 79 | 78 | breq1d 5153 | . . . . . . . . . 10
⊢ (((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℋ)) → ((𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) < 𝑧 ↔ (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥))) < 𝑧)) | 
| 80 | 68, 74, 79 | 3imtr3d 293 | . . . . . . . . 9
⊢ (((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℋ)) →
((normℎ‘(𝑤 −ℎ 𝑥)) < (𝑧 / 𝑛) → (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥))) < 𝑧)) | 
| 81 | 80 | anassrs 467 | . . . . . . . 8
⊢ ((((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ (𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)) ∧ 𝑤 ∈ ℋ) →
((normℎ‘(𝑤 −ℎ 𝑥)) < (𝑧 / 𝑛) → (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥))) < 𝑧)) | 
| 82 | 81 | ralrimiva 3146 | . . . . . . 7
⊢ (((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ (𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)) →
∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < (𝑧 / 𝑛) → (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥))) < 𝑧)) | 
| 83 |  | breq2 5147 | . . . . . . . 8
⊢ (𝑦 = (𝑧 / 𝑛) →
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑦 ↔ (normℎ‘(𝑤 −ℎ
𝑥)) < (𝑧 / 𝑛))) | 
| 84 | 83 | rspceaimv 3628 | . . . . . . 7
⊢ (((𝑧 / 𝑛) ∈ ℝ+ ∧
∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < (𝑧 / 𝑛) → (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥))) < 𝑧)) → ∃𝑦 ∈ ℝ+ ∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑦 → (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥))) < 𝑧)) | 
| 85 | 43, 82, 84 | syl2anc 584 | . . . . . 6
⊢ (((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ (𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)) →
∃𝑦 ∈
ℝ+ ∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑦 → (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥))) < 𝑧)) | 
| 86 | 85 | ralrimivva 3202 | . . . . 5
⊢ ((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) → ∀𝑥 ∈ ℋ ∀𝑧 ∈ ℝ+ ∃𝑦 ∈ ℝ+
∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑦 → (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥))) < 𝑧)) | 
| 87 | 86 | rexlimiva 3147 | . . . 4
⊢
(∃𝑛 ∈
ℕ ∀𝑦 ∈
ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦)) → ∀𝑥 ∈ ℋ ∀𝑧 ∈ ℝ+ ∃𝑦 ∈ ℝ+
∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑦 → (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥))) < 𝑧)) | 
| 88 |  | lncon.3 | . . . 4
⊢ (𝑇 ∈ 𝐶 ↔ ∀𝑥 ∈ ℋ ∀𝑧 ∈ ℝ+ ∃𝑦 ∈ ℝ+
∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑦 → (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥))) < 𝑧)) | 
| 89 | 87, 88 | sylibr 234 | . . 3
⊢
(∃𝑛 ∈
ℕ ∀𝑦 ∈
ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦)) → 𝑇 ∈ 𝐶) | 
| 90 | 39, 89 | syl 17 | . 2
⊢
(∃𝑥 ∈
ℝ ∀𝑦 ∈
ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦)) → 𝑇 ∈ 𝐶) | 
| 91 | 8, 90 | impbii 209 | 1
⊢ (𝑇 ∈ 𝐶 ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦))) |