This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lnconi

Description: Lemma for lnopconi and lnfnconi . (Contributed by NM, 7-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypotheses lncon.1 ⊢ ( 𝑇 ∈ 𝐶 → 𝑆 ∈ ℝ )
lncon.2 ⊢ ( ( 𝑇 ∈ 𝐶 ∧ 𝑦 ∈ ℋ ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑆 · ( normℎ ‘ 𝑦 ) ) )
lncon.3 ⊢ ( 𝑇 ∈ 𝐶 ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑦 → ( 𝑁 ‘ ( ( 𝑇 ‘ 𝑤 ) 𝑀 ( 𝑇 ‘ 𝑥 ) ) ) < 𝑧 ) )
lncon.4 ⊢ ( 𝑦 ∈ ℋ → ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ∈ ℝ )
lncon.5 ⊢ ( ( 𝑤 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ ( 𝑤 −ℎ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑤 ) 𝑀 ( 𝑇 ‘ 𝑥 ) ) )
Assertion lnconi ( 𝑇 ∈ 𝐶 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 lncon.1 ⊢ ( 𝑇 ∈ 𝐶 → 𝑆 ∈ ℝ )
2 lncon.2 ⊢ ( ( 𝑇 ∈ 𝐶 ∧ 𝑦 ∈ ℋ ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑆 · ( normℎ ‘ 𝑦 ) ) )
3 lncon.3 ⊢ ( 𝑇 ∈ 𝐶 ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑦 → ( 𝑁 ‘ ( ( 𝑇 ‘ 𝑤 ) 𝑀 ( 𝑇 ‘ 𝑥 ) ) ) < 𝑧 ) )
4 lncon.4 ⊢ ( 𝑦 ∈ ℋ → ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ∈ ℝ )
5 lncon.5 ⊢ ( ( 𝑤 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ ( 𝑤 −ℎ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑤 ) 𝑀 ( 𝑇 ‘ 𝑥 ) ) )
6 2 ralrimiva ⊢ ( 𝑇 ∈ 𝐶 → ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑆 · ( normℎ ‘ 𝑦 ) ) )
7 oveq1 ⊢ ( 𝑥 = 𝑆 → ( 𝑥 · ( normℎ ‘ 𝑦 ) ) = ( 𝑆 · ( normℎ ‘ 𝑦 ) ) )
8 7 breq2d ⊢ ( 𝑥 = 𝑆 → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ↔ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑆 · ( normℎ ‘ 𝑦 ) ) ) )
9 8 ralbidv ⊢ ( 𝑥 = 𝑆 → ( ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑆 · ( normℎ ‘ 𝑦 ) ) ) )
10 9 rspcev ⊢ ( ( 𝑆 ∈ ℝ ∧ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑆 · ( normℎ ‘ 𝑦 ) ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) )
11 1 6 10 syl2anc ⊢ ( 𝑇 ∈ 𝐶 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) )
12 arch ⊢ ( 𝑥 ∈ ℝ → ∃ 𝑛 ∈ ℕ 𝑥 < 𝑛 )
13 12 adantr ⊢ ( ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ) → ∃ 𝑛 ∈ ℕ 𝑥 < 𝑛 )
14 nnre ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ )
15 simplll ⊢ ( ( ( ( 𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 < 𝑛 ) ∧ 𝑦 ∈ ℋ ) → 𝑥 ∈ ℝ )
16 simpllr ⊢ ( ( ( ( 𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 < 𝑛 ) ∧ 𝑦 ∈ ℋ ) → 𝑛 ∈ ℝ )
17 normcl ⊢ ( 𝑦 ∈ ℋ → ( normℎ ‘ 𝑦 ) ∈ ℝ )
18 17 adantl ⊢ ( ( ( ( 𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 < 𝑛 ) ∧ 𝑦 ∈ ℋ ) → ( normℎ ‘ 𝑦 ) ∈ ℝ )
19 normge0 ⊢ ( 𝑦 ∈ ℋ → 0 ≤ ( normℎ ‘ 𝑦 ) )
20 19 adantl ⊢ ( ( ( ( 𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 < 𝑛 ) ∧ 𝑦 ∈ ℋ ) → 0 ≤ ( normℎ ‘ 𝑦 ) )
21 ltle ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ ) → ( 𝑥 < 𝑛 → 𝑥 ≤ 𝑛 ) )
22 21 imp ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 < 𝑛 ) → 𝑥 ≤ 𝑛 )
23 22 adantr ⊢ ( ( ( ( 𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 < 𝑛 ) ∧ 𝑦 ∈ ℋ ) → 𝑥 ≤ 𝑛 )
24 15 16 18 20 23 lemul1ad ⊢ ( ( ( ( 𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 < 𝑛 ) ∧ 𝑦 ∈ ℋ ) → ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) )
25 4 adantl ⊢ ( ( ( ( 𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 < 𝑛 ) ∧ 𝑦 ∈ ℋ ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ∈ ℝ )
26 simpll ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 < 𝑛 ) → 𝑥 ∈ ℝ )
27 remulcl ⊢ ( ( 𝑥 ∈ ℝ ∧ ( normℎ ‘ 𝑦 ) ∈ ℝ ) → ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ∈ ℝ )
28 26 17 27 syl2an ⊢ ( ( ( ( 𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 < 𝑛 ) ∧ 𝑦 ∈ ℋ ) → ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ∈ ℝ )
29 simplr ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 < 𝑛 ) → 𝑛 ∈ ℝ )
30 remulcl ⊢ ( ( 𝑛 ∈ ℝ ∧ ( normℎ ‘ 𝑦 ) ∈ ℝ ) → ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ∈ ℝ )
31 29 17 30 syl2an ⊢ ( ( ( ( 𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 < 𝑛 ) ∧ 𝑦 ∈ ℋ ) → ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ∈ ℝ )
32 letr ⊢ ( ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ∈ ℝ ∧ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ∈ ℝ ∧ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ∈ ℝ ) → ( ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ∧ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ) )
33 25 28 31 32 syl3anc ⊢ ( ( ( ( 𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 < 𝑛 ) ∧ 𝑦 ∈ ℋ ) → ( ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ∧ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ) )
34 24 33 mpan2d ⊢ ( ( ( ( 𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 < 𝑛 ) ∧ 𝑦 ∈ ℋ ) → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ) )
35 34 ralimdva ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ 𝑥 < 𝑛 ) → ( ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) → ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ) )
36 35 impancom ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑛 ∈ ℝ ) ∧ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ) → ( 𝑥 < 𝑛 → ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ) )
37 36 an32s ⊢ ( ( ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ) ∧ 𝑛 ∈ ℝ ) → ( 𝑥 < 𝑛 → ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ) )
38 14 37 sylan2 ⊢ ( ( ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑥 < 𝑛 → ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ) )
39 38 reximdva ⊢ ( ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ) → ( ∃ 𝑛 ∈ ℕ 𝑥 < 𝑛 → ∃ 𝑛 ∈ ℕ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ) )
40 13 39 mpd ⊢ ( ( 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) ) → ∃ 𝑛 ∈ ℕ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) )
41 40 rexlimiva ⊢ ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) → ∃ 𝑛 ∈ ℕ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) )
42 simprr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+ ) ) → 𝑧 ∈ ℝ+ )
43 simpll ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+ ) ) → 𝑛 ∈ ℕ )
44 43 nnrpd ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+ ) ) → 𝑛 ∈ ℝ+ )
45 42 44 rpdivcld ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+ ) ) → ( 𝑧 / 𝑛 ) ∈ ℝ+ )
46 simprr ⊢ ( ( 𝑛 ∈ ℕ ∧ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) ) → 𝑤 ∈ ℋ )
47 simprll ⊢ ( ( 𝑛 ∈ ℕ ∧ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) ) → 𝑥 ∈ ℋ )
48 hvsubcl ⊢ ( ( 𝑤 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑤 −ℎ 𝑥 ) ∈ ℋ )
49 46 47 48 syl2anc ⊢ ( ( 𝑛 ∈ ℕ ∧ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) ) → ( 𝑤 −ℎ 𝑥 ) ∈ ℋ )
50 2fveq3 ⊢ ( 𝑦 = ( 𝑤 −ℎ 𝑥 ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ ( 𝑤 −ℎ 𝑥 ) ) ) )
51 fveq2 ⊢ ( 𝑦 = ( 𝑤 −ℎ 𝑥 ) → ( normℎ ‘ 𝑦 ) = ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) )
52 51 oveq2d ⊢ ( 𝑦 = ( 𝑤 −ℎ 𝑥 ) → ( 𝑛 · ( normℎ ‘ 𝑦 ) ) = ( 𝑛 · ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) ) )
53 50 52 breq12d ⊢ ( 𝑦 = ( 𝑤 −ℎ 𝑥 ) → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ↔ ( 𝑁 ‘ ( 𝑇 ‘ ( 𝑤 −ℎ 𝑥 ) ) ) ≤ ( 𝑛 · ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) ) ) )
54 53 rspcva ⊢ ( ( ( 𝑤 −ℎ 𝑥 ) ∈ ℋ ∧ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ) → ( 𝑁 ‘ ( 𝑇 ‘ ( 𝑤 −ℎ 𝑥 ) ) ) ≤ ( 𝑛 · ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) ) )
55 49 54 sylan ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) ) ∧ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ) → ( 𝑁 ‘ ( 𝑇 ‘ ( 𝑤 −ℎ 𝑥 ) ) ) ≤ ( 𝑛 · ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) ) )
56 55 an32s ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ) ∧ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) ) → ( 𝑁 ‘ ( 𝑇 ‘ ( 𝑤 −ℎ 𝑥 ) ) ) ≤ ( 𝑛 · ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) ) )
57 50 eleq1d ⊢ ( 𝑦 = ( 𝑤 −ℎ 𝑥 ) → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ∈ ℝ ↔ ( 𝑁 ‘ ( 𝑇 ‘ ( 𝑤 −ℎ 𝑥 ) ) ) ∈ ℝ ) )
58 57 4 vtoclga ⊢ ( ( 𝑤 −ℎ 𝑥 ) ∈ ℋ → ( 𝑁 ‘ ( 𝑇 ‘ ( 𝑤 −ℎ 𝑥 ) ) ) ∈ ℝ )
59 49 58 syl ⊢ ( ( 𝑛 ∈ ℕ ∧ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) ) → ( 𝑁 ‘ ( 𝑇 ‘ ( 𝑤 −ℎ 𝑥 ) ) ) ∈ ℝ )
60 14 adantr ⊢ ( ( 𝑛 ∈ ℕ ∧ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) ) → 𝑛 ∈ ℝ )
61 normcl ⊢ ( ( 𝑤 −ℎ 𝑥 ) ∈ ℋ → ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) ∈ ℝ )
62 49 61 syl ⊢ ( ( 𝑛 ∈ ℕ ∧ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) ) → ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) ∈ ℝ )
63 remulcl ⊢ ( ( 𝑛 ∈ ℝ ∧ ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) ∈ ℝ ) → ( 𝑛 · ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) ) ∈ ℝ )
64 60 62 63 syl2anc ⊢ ( ( 𝑛 ∈ ℕ ∧ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) ) → ( 𝑛 · ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) ) ∈ ℝ )
65 simprlr ⊢ ( ( 𝑛 ∈ ℕ ∧ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) ) → 𝑧 ∈ ℝ+ )
66 65 rpred ⊢ ( ( 𝑛 ∈ ℕ ∧ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) ) → 𝑧 ∈ ℝ )
67 lelttr ⊢ ( ( ( 𝑁 ‘ ( 𝑇 ‘ ( 𝑤 −ℎ 𝑥 ) ) ) ∈ ℝ ∧ ( 𝑛 · ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) ) ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( ( 𝑁 ‘ ( 𝑇 ‘ ( 𝑤 −ℎ 𝑥 ) ) ) ≤ ( 𝑛 · ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) ) ∧ ( 𝑛 · ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) ) < 𝑧 ) → ( 𝑁 ‘ ( 𝑇 ‘ ( 𝑤 −ℎ 𝑥 ) ) ) < 𝑧 ) )
68 59 64 66 67 syl3anc ⊢ ( ( 𝑛 ∈ ℕ ∧ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) ) → ( ( ( 𝑁 ‘ ( 𝑇 ‘ ( 𝑤 −ℎ 𝑥 ) ) ) ≤ ( 𝑛 · ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) ) ∧ ( 𝑛 · ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) ) < 𝑧 ) → ( 𝑁 ‘ ( 𝑇 ‘ ( 𝑤 −ℎ 𝑥 ) ) ) < 𝑧 ) )
69 68 adantlr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ) ∧ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) ) → ( ( ( 𝑁 ‘ ( 𝑇 ‘ ( 𝑤 −ℎ 𝑥 ) ) ) ≤ ( 𝑛 · ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) ) ∧ ( 𝑛 · ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) ) < 𝑧 ) → ( 𝑁 ‘ ( 𝑇 ‘ ( 𝑤 −ℎ 𝑥 ) ) ) < 𝑧 ) )
70 56 69 mpand ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ) ∧ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) ) → ( ( 𝑛 · ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) ) < 𝑧 → ( 𝑁 ‘ ( 𝑇 ‘ ( 𝑤 −ℎ 𝑥 ) ) ) < 𝑧 ) )
71 nnrp ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ+ )
72 71 rpregt0d ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 ∈ ℝ ∧ 0 < 𝑛 ) )
73 72 adantr ⊢ ( ( 𝑛 ∈ ℕ ∧ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) ) → ( 𝑛 ∈ ℝ ∧ 0 < 𝑛 ) )
74 ltmuldiv2 ⊢ ( ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ ( 𝑛 ∈ ℝ ∧ 0 < 𝑛 ) ) → ( ( 𝑛 · ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) ) < 𝑧 ↔ ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < ( 𝑧 / 𝑛 ) ) )
75 62 66 73 74 syl3anc ⊢ ( ( 𝑛 ∈ ℕ ∧ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) ) → ( ( 𝑛 · ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) ) < 𝑧 ↔ ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < ( 𝑧 / 𝑛 ) ) )
76 75 adantlr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ) ∧ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) ) → ( ( 𝑛 · ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) ) < 𝑧 ↔ ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < ( 𝑧 / 𝑛 ) ) )
77 46 47 5 syl2anc ⊢ ( ( 𝑛 ∈ ℕ ∧ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) ) → ( 𝑇 ‘ ( 𝑤 −ℎ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑤 ) 𝑀 ( 𝑇 ‘ 𝑥 ) ) )
78 77 adantlr ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ) ∧ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) ) → ( 𝑇 ‘ ( 𝑤 −ℎ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑤 ) 𝑀 ( 𝑇 ‘ 𝑥 ) ) )
79 78 fveq2d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ) ∧ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) ) → ( 𝑁 ‘ ( 𝑇 ‘ ( 𝑤 −ℎ 𝑥 ) ) ) = ( 𝑁 ‘ ( ( 𝑇 ‘ 𝑤 ) 𝑀 ( 𝑇 ‘ 𝑥 ) ) ) )
80 79 breq1d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ) ∧ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) ) → ( ( 𝑁 ‘ ( 𝑇 ‘ ( 𝑤 −ℎ 𝑥 ) ) ) < 𝑧 ↔ ( 𝑁 ‘ ( ( 𝑇 ‘ 𝑤 ) 𝑀 ( 𝑇 ‘ 𝑥 ) ) ) < 𝑧 ) )
81 70 76 80 3imtr3d ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ) ∧ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑤 ∈ ℋ ) ) → ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < ( 𝑧 / 𝑛 ) → ( 𝑁 ‘ ( ( 𝑇 ‘ 𝑤 ) 𝑀 ( 𝑇 ‘ 𝑥 ) ) ) < 𝑧 ) )
82 81 anassrs ⊢ ( ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑤 ∈ ℋ ) → ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < ( 𝑧 / 𝑛 ) → ( 𝑁 ‘ ( ( 𝑇 ‘ 𝑤 ) 𝑀 ( 𝑇 ‘ 𝑥 ) ) ) < 𝑧 ) )
83 82 ralrimiva ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+ ) ) → ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < ( 𝑧 / 𝑛 ) → ( 𝑁 ‘ ( ( 𝑇 ‘ 𝑤 ) 𝑀 ( 𝑇 ‘ 𝑥 ) ) ) < 𝑧 ) )
84 breq2 ⊢ ( 𝑦 = ( 𝑧 / 𝑛 ) → ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑦 ↔ ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < ( 𝑧 / 𝑛 ) ) )
85 84 rspceaimv ⊢ ( ( ( 𝑧 / 𝑛 ) ∈ ℝ+ ∧ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < ( 𝑧 / 𝑛 ) → ( 𝑁 ‘ ( ( 𝑇 ‘ 𝑤 ) 𝑀 ( 𝑇 ‘ 𝑥 ) ) ) < 𝑧 ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑦 → ( 𝑁 ‘ ( ( 𝑇 ‘ 𝑤 ) 𝑀 ( 𝑇 ‘ 𝑥 ) ) ) < 𝑧 ) )
86 45 83 85 syl2anc ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℝ+ ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑦 → ( 𝑁 ‘ ( ( 𝑇 ‘ 𝑤 ) 𝑀 ( 𝑇 ‘ 𝑥 ) ) ) < 𝑧 ) )
87 86 ralrimivva ⊢ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) ) → ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑦 → ( 𝑁 ‘ ( ( 𝑇 ‘ 𝑤 ) 𝑀 ( 𝑇 ‘ 𝑥 ) ) ) < 𝑧 ) )
88 87 rexlimiva ⊢ ( ∃ 𝑛 ∈ ℕ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) → ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑦 → ( 𝑁 ‘ ( ( 𝑇 ‘ 𝑤 ) 𝑀 ( 𝑇 ‘ 𝑥 ) ) ) < 𝑧 ) )
89 88 3 sylibr ⊢ ( ∃ 𝑛 ∈ ℕ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑛 · ( normℎ ‘ 𝑦 ) ) → 𝑇 ∈ 𝐶 )
90 41 89 syl ⊢ ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) → 𝑇 ∈ 𝐶 )
91 11 90 impbii ⊢ ( 𝑇 ∈ 𝐶 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) )