Step | Hyp | Ref
| Expression |
1 | | lncon.1 |
. . 3
⊢ (𝑇 ∈ 𝐶 → 𝑆 ∈ ℝ) |
2 | | lncon.2 |
. . . 4
⊢ ((𝑇 ∈ 𝐶 ∧ 𝑦 ∈ ℋ) → (𝑁‘(𝑇‘𝑦)) ≤ (𝑆 ·
(normℎ‘𝑦))) |
3 | 2 | ralrimiva 2966 |
. . 3
⊢ (𝑇 ∈ 𝐶 → ∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑆 ·
(normℎ‘𝑦))) |
4 | | oveq1 6657 |
. . . . . 6
⊢ (𝑥 = 𝑆 → (𝑥 ·
(normℎ‘𝑦)) = (𝑆 ·
(normℎ‘𝑦))) |
5 | 4 | breq2d 4665 |
. . . . 5
⊢ (𝑥 = 𝑆 → ((𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦)) ↔ (𝑁‘(𝑇‘𝑦)) ≤ (𝑆 ·
(normℎ‘𝑦)))) |
6 | 5 | ralbidv 2986 |
. . . 4
⊢ (𝑥 = 𝑆 → (∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦)) ↔ ∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑆 ·
(normℎ‘𝑦)))) |
7 | 6 | rspcev 3309 |
. . 3
⊢ ((𝑆 ∈ ℝ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑆 ·
(normℎ‘𝑦))) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦))) |
8 | 1, 3, 7 | syl2anc 693 |
. 2
⊢ (𝑇 ∈ 𝐶 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦))) |
9 | | arch 11289 |
. . . . . 6
⊢ (𝑥 ∈ ℝ →
∃𝑛 ∈ ℕ
𝑥 < 𝑛) |
10 | 9 | adantr 481 |
. . . . 5
⊢ ((𝑥 ∈ ℝ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦))) → ∃𝑛 ∈ ℕ 𝑥 < 𝑛) |
11 | | nnre 11027 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ) |
12 | | simplll 798 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) ∧ 𝑦 ∈ ℋ) → 𝑥 ∈ ℝ) |
13 | | simpllr 799 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) ∧ 𝑦 ∈ ℋ) → 𝑛 ∈ ℝ) |
14 | | normcl 27982 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℋ →
(normℎ‘𝑦) ∈ ℝ) |
15 | 14 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) ∧ 𝑦 ∈ ℋ) →
(normℎ‘𝑦) ∈ ℝ) |
16 | | normge0 27983 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℋ → 0 ≤
(normℎ‘𝑦)) |
17 | 16 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) ∧ 𝑦 ∈ ℋ) → 0 ≤
(normℎ‘𝑦)) |
18 | | ltle 10126 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (𝑥 < 𝑛 → 𝑥 ≤ 𝑛)) |
19 | 18 | imp 445 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) → 𝑥 ≤ 𝑛) |
20 | 19 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) ∧ 𝑦 ∈ ℋ) → 𝑥 ≤ 𝑛) |
21 | 12, 13, 15, 17, 20 | lemul1ad 10963 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) ∧ 𝑦 ∈ ℋ) → (𝑥 ·
(normℎ‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) |
22 | | lncon.4 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℋ → (𝑁‘(𝑇‘𝑦)) ∈ ℝ) |
23 | 22 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) ∧ 𝑦 ∈ ℋ) → (𝑁‘(𝑇‘𝑦)) ∈ ℝ) |
24 | | simpll 790 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) → 𝑥 ∈ ℝ) |
25 | | remulcl 10021 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧
(normℎ‘𝑦) ∈ ℝ) → (𝑥 ·
(normℎ‘𝑦)) ∈ ℝ) |
26 | 24, 14, 25 | syl2an 494 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) ∧ 𝑦 ∈ ℋ) → (𝑥 ·
(normℎ‘𝑦)) ∈ ℝ) |
27 | | simplr 792 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) → 𝑛 ∈ ℝ) |
28 | | remulcl 10021 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℝ ∧
(normℎ‘𝑦) ∈ ℝ) → (𝑛 ·
(normℎ‘𝑦)) ∈ ℝ) |
29 | 27, 14, 28 | syl2an 494 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) ∧ 𝑦 ∈ ℋ) → (𝑛 ·
(normℎ‘𝑦)) ∈ ℝ) |
30 | | letr 10131 |
. . . . . . . . . . . 12
⊢ (((𝑁‘(𝑇‘𝑦)) ∈ ℝ ∧ (𝑥 ·
(normℎ‘𝑦)) ∈ ℝ ∧ (𝑛 ·
(normℎ‘𝑦)) ∈ ℝ) → (((𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦)) ∧ (𝑥 ·
(normℎ‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) → (𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦)))) |
31 | 23, 26, 29, 30 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) ∧ 𝑦 ∈ ℋ) → (((𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦)) ∧ (𝑥 ·
(normℎ‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) → (𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦)))) |
32 | 21, 31 | mpan2d 710 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) ∧ 𝑦 ∈ ℋ) → ((𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦)) → (𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦)))) |
33 | 32 | ralimdva 2962 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ 𝑥 < 𝑛) → (∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦)) → ∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦)))) |
34 | 33 | impancom 456 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦))) → (𝑥 < 𝑛 → ∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦)))) |
35 | 34 | an32s 846 |
. . . . . . 7
⊢ (((𝑥 ∈ ℝ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦))) ∧ 𝑛 ∈ ℝ) → (𝑥 < 𝑛 → ∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦)))) |
36 | 11, 35 | sylan2 491 |
. . . . . 6
⊢ (((𝑥 ∈ ℝ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦))) ∧ 𝑛 ∈ ℕ) → (𝑥 < 𝑛 → ∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦)))) |
37 | 36 | reximdva 3017 |
. . . . 5
⊢ ((𝑥 ∈ ℝ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦))) → (∃𝑛 ∈ ℕ 𝑥 < 𝑛 → ∃𝑛 ∈ ℕ ∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦)))) |
38 | 10, 37 | mpd 15 |
. . . 4
⊢ ((𝑥 ∈ ℝ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦))) → ∃𝑛 ∈ ℕ ∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) |
39 | 38 | rexlimiva 3028 |
. . 3
⊢
(∃𝑥 ∈
ℝ ∀𝑦 ∈
ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦)) → ∃𝑛 ∈ ℕ ∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) |
40 | | simprr 796 |
. . . . . . . 8
⊢ (((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ (𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)) → 𝑧 ∈
ℝ+) |
41 | | simpll 790 |
. . . . . . . . 9
⊢ (((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ (𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)) → 𝑛 ∈
ℕ) |
42 | 41 | nnrpd 11870 |
. . . . . . . 8
⊢ (((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ (𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)) → 𝑛 ∈
ℝ+) |
43 | 40, 42 | rpdivcld 11889 |
. . . . . . 7
⊢ (((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ (𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)) → (𝑧 / 𝑛) ∈
ℝ+) |
44 | | simprr 796 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)
∧ 𝑤 ∈ ℋ))
→ 𝑤 ∈
ℋ) |
45 | | simprll 802 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)
∧ 𝑤 ∈ ℋ))
→ 𝑥 ∈
ℋ) |
46 | | hvsubcl 27874 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ ℋ ∧ 𝑥 ∈ ℋ) → (𝑤 −ℎ
𝑥) ∈
ℋ) |
47 | 44, 45, 46 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)
∧ 𝑤 ∈ ℋ))
→ (𝑤
−ℎ 𝑥) ∈ ℋ) |
48 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑤 −ℎ 𝑥) → (𝑇‘𝑦) = (𝑇‘(𝑤 −ℎ 𝑥))) |
49 | 48 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑤 −ℎ 𝑥) → (𝑁‘(𝑇‘𝑦)) = (𝑁‘(𝑇‘(𝑤 −ℎ 𝑥)))) |
50 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑤 −ℎ 𝑥) →
(normℎ‘𝑦) = (normℎ‘(𝑤 −ℎ
𝑥))) |
51 | 50 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑤 −ℎ 𝑥) → (𝑛 ·
(normℎ‘𝑦)) = (𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥)))) |
52 | 49, 51 | breq12d 4666 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑤 −ℎ 𝑥) → ((𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦)) ↔ (𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) ≤ (𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥))))) |
53 | 52 | rspcva 3307 |
. . . . . . . . . . . . 13
⊢ (((𝑤 −ℎ
𝑥) ∈ ℋ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) → (𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) ≤ (𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥)))) |
54 | 47, 53 | sylan 488 |
. . . . . . . . . . . 12
⊢ (((𝑛 ∈ ℕ ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)
∧ 𝑤 ∈ ℋ))
∧ ∀𝑦 ∈
ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) → (𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) ≤ (𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥)))) |
55 | 54 | an32s 846 |
. . . . . . . . . . 11
⊢ (((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℋ)) → (𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) ≤ (𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥)))) |
56 | 49 | eleq1d 2686 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑤 −ℎ 𝑥) → ((𝑁‘(𝑇‘𝑦)) ∈ ℝ ↔ (𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) ∈
ℝ)) |
57 | 56, 22 | vtoclga 3272 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 −ℎ
𝑥) ∈ ℋ →
(𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) ∈
ℝ) |
58 | 47, 57 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)
∧ 𝑤 ∈ ℋ))
→ (𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) ∈
ℝ) |
59 | 11 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)
∧ 𝑤 ∈ ℋ))
→ 𝑛 ∈
ℝ) |
60 | | normcl 27982 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 −ℎ
𝑥) ∈ ℋ →
(normℎ‘(𝑤 −ℎ 𝑥)) ∈
ℝ) |
61 | 47, 60 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)
∧ 𝑤 ∈ ℋ))
→ (normℎ‘(𝑤 −ℎ 𝑥)) ∈
ℝ) |
62 | | remulcl 10021 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℝ ∧
(normℎ‘(𝑤 −ℎ 𝑥)) ∈ ℝ) → (𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥))) ∈
ℝ) |
63 | 59, 61, 62 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)
∧ 𝑤 ∈ ℋ))
→ (𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥))) ∈
ℝ) |
64 | | simprlr 803 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)
∧ 𝑤 ∈ ℋ))
→ 𝑧 ∈
ℝ+) |
65 | 64 | rpred 11872 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)
∧ 𝑤 ∈ ℋ))
→ 𝑧 ∈
ℝ) |
66 | | lelttr 10128 |
. . . . . . . . . . . . 13
⊢ (((𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) ∈ ℝ ∧ (𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥))) ∈ ℝ ∧ 𝑧 ∈ ℝ) → (((𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) ≤ (𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥))) ∧ (𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥))) < 𝑧) → (𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) < 𝑧)) |
67 | 58, 63, 65, 66 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℕ ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)
∧ 𝑤 ∈ ℋ))
→ (((𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) ≤ (𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥))) ∧ (𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥))) < 𝑧) → (𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) < 𝑧)) |
68 | 67 | adantlr 751 |
. . . . . . . . . . 11
⊢ (((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℋ)) →
(((𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) ≤ (𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥))) ∧ (𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥))) < 𝑧) → (𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) < 𝑧)) |
69 | 55, 68 | mpand 711 |
. . . . . . . . . 10
⊢ (((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℋ)) → ((𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥))) < 𝑧 → (𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) < 𝑧)) |
70 | | nnrp 11842 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ+) |
71 | 70 | rpregt0d 11878 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (𝑛 ∈ ℝ ∧ 0 <
𝑛)) |
72 | 71 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℕ ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)
∧ 𝑤 ∈ ℋ))
→ (𝑛 ∈ ℝ
∧ 0 < 𝑛)) |
73 | | ltmuldiv2 10897 |
. . . . . . . . . . . 12
⊢
(((normℎ‘(𝑤 −ℎ 𝑥)) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ (𝑛 ∈ ℝ ∧ 0 <
𝑛)) → ((𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥))) < 𝑧 ↔ (normℎ‘(𝑤 −ℎ
𝑥)) < (𝑧 / 𝑛))) |
74 | 61, 65, 72, 73 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)
∧ 𝑤 ∈ ℋ))
→ ((𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥))) < 𝑧 ↔ (normℎ‘(𝑤 −ℎ
𝑥)) < (𝑧 / 𝑛))) |
75 | 74 | adantlr 751 |
. . . . . . . . . 10
⊢ (((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℋ)) → ((𝑛 ·
(normℎ‘(𝑤 −ℎ 𝑥))) < 𝑧 ↔ (normℎ‘(𝑤 −ℎ
𝑥)) < (𝑧 / 𝑛))) |
76 | | lncon.5 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ ℋ ∧ 𝑥 ∈ ℋ) → (𝑇‘(𝑤 −ℎ 𝑥)) = ((𝑇‘𝑤)𝑀(𝑇‘𝑥))) |
77 | 44, 45, 76 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)
∧ 𝑤 ∈ ℋ))
→ (𝑇‘(𝑤 −ℎ
𝑥)) = ((𝑇‘𝑤)𝑀(𝑇‘𝑥))) |
78 | 77 | adantlr 751 |
. . . . . . . . . . . 12
⊢ (((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℋ)) → (𝑇‘(𝑤 −ℎ 𝑥)) = ((𝑇‘𝑤)𝑀(𝑇‘𝑥))) |
79 | 78 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℋ)) → (𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) = (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥)))) |
80 | 79 | breq1d 4663 |
. . . . . . . . . 10
⊢ (((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℋ)) → ((𝑁‘(𝑇‘(𝑤 −ℎ 𝑥))) < 𝑧 ↔ (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥))) < 𝑧)) |
81 | 69, 75, 80 | 3imtr3d 282 |
. . . . . . . . 9
⊢ (((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+) ∧ 𝑤 ∈ ℋ)) →
((normℎ‘(𝑤 −ℎ 𝑥)) < (𝑧 / 𝑛) → (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥))) < 𝑧)) |
82 | 81 | anassrs 680 |
. . . . . . . 8
⊢ ((((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ (𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)) ∧ 𝑤 ∈ ℋ) →
((normℎ‘(𝑤 −ℎ 𝑥)) < (𝑧 / 𝑛) → (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥))) < 𝑧)) |
83 | 82 | ralrimiva 2966 |
. . . . . . 7
⊢ (((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ (𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)) →
∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < (𝑧 / 𝑛) → (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥))) < 𝑧)) |
84 | | breq2 4657 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑧 / 𝑛) →
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑦 ↔ (normℎ‘(𝑤 −ℎ
𝑥)) < (𝑧 / 𝑛))) |
85 | 84 | imbi1d 331 |
. . . . . . . . 9
⊢ (𝑦 = (𝑧 / 𝑛) →
(((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑦 → (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥))) < 𝑧) ↔
((normℎ‘(𝑤 −ℎ 𝑥)) < (𝑧 / 𝑛) → (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥))) < 𝑧))) |
86 | 85 | ralbidv 2986 |
. . . . . . . 8
⊢ (𝑦 = (𝑧 / 𝑛) → (∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑦 → (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥))) < 𝑧) ↔ ∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < (𝑧 / 𝑛) → (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥))) < 𝑧))) |
87 | 86 | rspcev 3309 |
. . . . . . 7
⊢ (((𝑧 / 𝑛) ∈ ℝ+ ∧
∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < (𝑧 / 𝑛) → (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥))) < 𝑧)) → ∃𝑦 ∈ ℝ+ ∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑦 → (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥))) < 𝑧)) |
88 | 43, 83, 87 | syl2anc 693 |
. . . . . 6
⊢ (((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) ∧ (𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+)) →
∃𝑦 ∈
ℝ+ ∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑦 → (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥))) < 𝑧)) |
89 | 88 | ralrimivva 2971 |
. . . . 5
⊢ ((𝑛 ∈ ℕ ∧
∀𝑦 ∈ ℋ
(𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦))) → ∀𝑥 ∈ ℋ ∀𝑧 ∈ ℝ+ ∃𝑦 ∈ ℝ+
∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑦 → (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥))) < 𝑧)) |
90 | 89 | rexlimiva 3028 |
. . . 4
⊢
(∃𝑛 ∈
ℕ ∀𝑦 ∈
ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦)) → ∀𝑥 ∈ ℋ ∀𝑧 ∈ ℝ+ ∃𝑦 ∈ ℝ+
∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑦 → (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥))) < 𝑧)) |
91 | | lncon.3 |
. . . 4
⊢ (𝑇 ∈ 𝐶 ↔ ∀𝑥 ∈ ℋ ∀𝑧 ∈ ℝ+ ∃𝑦 ∈ ℝ+
∀𝑤 ∈ ℋ
((normℎ‘(𝑤 −ℎ 𝑥)) < 𝑦 → (𝑁‘((𝑇‘𝑤)𝑀(𝑇‘𝑥))) < 𝑧)) |
92 | 90, 91 | sylibr 224 |
. . 3
⊢
(∃𝑛 ∈
ℕ ∀𝑦 ∈
ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑛 ·
(normℎ‘𝑦)) → 𝑇 ∈ 𝐶) |
93 | 39, 92 | syl 17 |
. 2
⊢
(∃𝑥 ∈
ℝ ∀𝑦 ∈
ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦)) → 𝑇 ∈ 𝐶) |
94 | 8, 93 | impbii 199 |
1
⊢ (𝑇 ∈ 𝐶 ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℋ (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 ·
(normℎ‘𝑦))) |