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

Metamath Proof Explorer

Theorem dchrisum0lem1a

Description: Lemma for dchrisum0lem1 . (Contributed by Mario Carneiro, 7-Jun-2016)

Ref Expression
Assertion dchrisum0lem1a ( ( ( 𝜑 ∧ 𝑋 ∈ ℝ+ ) ∧ 𝐷 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ) → ( 𝑋 ≤ ( ( 𝑋 ↑ 2 ) / 𝐷 ) ∧ ( ⌊ ‘ ( ( 𝑋 ↑ 2 ) / 𝐷 ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑋 ) ) ) )

Proof

Step Hyp Ref Expression
1 elfznn ⊢ ( 𝐷 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) → 𝐷 ∈ ℕ )
2 1 adantl ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℝ+ ) ∧ 𝐷 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ) → 𝐷 ∈ ℕ )
3 2 nnred ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℝ+ ) ∧ 𝐷 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ) → 𝐷 ∈ ℝ )
4 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℝ+ ) → 𝑋 ∈ ℝ+ )
5 4 rpregt0d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℝ+ ) → ( 𝑋 ∈ ℝ ∧ 0 < 𝑋 ) )
6 5 adantr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℝ+ ) ∧ 𝐷 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ) → ( 𝑋 ∈ ℝ ∧ 0 < 𝑋 ) )
7 6 simpld ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℝ+ ) ∧ 𝐷 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ) → 𝑋 ∈ ℝ )
8 4 adantr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℝ+ ) ∧ 𝐷 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ) → 𝑋 ∈ ℝ+ )
9 8 rpge0d ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℝ+ ) ∧ 𝐷 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ) → 0 ≤ 𝑋 )
10 4 rpred ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℝ+ ) → 𝑋 ∈ ℝ )
11 fznnfl ⊢ ( 𝑋 ∈ ℝ → ( 𝐷 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ↔ ( 𝐷 ∈ ℕ ∧ 𝐷 ≤ 𝑋 ) ) )
12 10 11 syl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℝ+ ) → ( 𝐷 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ↔ ( 𝐷 ∈ ℕ ∧ 𝐷 ≤ 𝑋 ) ) )
13 12 simplbda ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℝ+ ) ∧ 𝐷 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ) → 𝐷 ≤ 𝑋 )
14 3 7 7 9 13 lemul2ad ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℝ+ ) ∧ 𝐷 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ) → ( 𝑋 · 𝐷 ) ≤ ( 𝑋 · 𝑋 ) )
15 rpcn ⊢ ( 𝑋 ∈ ℝ+ → 𝑋 ∈ ℂ )
16 15 adantl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℝ+ ) → 𝑋 ∈ ℂ )
17 16 sqvald ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℝ+ ) → ( 𝑋 ↑ 2 ) = ( 𝑋 · 𝑋 ) )
18 17 adantr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℝ+ ) ∧ 𝐷 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ) → ( 𝑋 ↑ 2 ) = ( 𝑋 · 𝑋 ) )
19 14 18 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℝ+ ) ∧ 𝐷 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ) → ( 𝑋 · 𝐷 ) ≤ ( 𝑋 ↑ 2 ) )
20 2z ⊢ 2 ∈ ℤ
21 rpexpcl ⊢ ( ( 𝑋 ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( 𝑋 ↑ 2 ) ∈ ℝ+ )
22 4 20 21 sylancl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℝ+ ) → ( 𝑋 ↑ 2 ) ∈ ℝ+ )
23 22 rpred ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℝ+ ) → ( 𝑋 ↑ 2 ) ∈ ℝ )
24 23 adantr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℝ+ ) ∧ 𝐷 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ) → ( 𝑋 ↑ 2 ) ∈ ℝ )
25 2 nnrpd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℝ+ ) ∧ 𝐷 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ) → 𝐷 ∈ ℝ+ )
26 7 24 25 lemuldivd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℝ+ ) ∧ 𝐷 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ) → ( ( 𝑋 · 𝐷 ) ≤ ( 𝑋 ↑ 2 ) ↔ 𝑋 ≤ ( ( 𝑋 ↑ 2 ) / 𝐷 ) ) )
27 19 26 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℝ+ ) ∧ 𝐷 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ) → 𝑋 ≤ ( ( 𝑋 ↑ 2 ) / 𝐷 ) )
28 nndivre ⊢ ( ( ( 𝑋 ↑ 2 ) ∈ ℝ ∧ 𝐷 ∈ ℕ ) → ( ( 𝑋 ↑ 2 ) / 𝐷 ) ∈ ℝ )
29 23 1 28 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℝ+ ) ∧ 𝐷 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ) → ( ( 𝑋 ↑ 2 ) / 𝐷 ) ∈ ℝ )
30 flword2 ⊢ ( ( 𝑋 ∈ ℝ ∧ ( ( 𝑋 ↑ 2 ) / 𝐷 ) ∈ ℝ ∧ 𝑋 ≤ ( ( 𝑋 ↑ 2 ) / 𝐷 ) ) → ( ⌊ ‘ ( ( 𝑋 ↑ 2 ) / 𝐷 ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑋 ) ) )
31 7 29 27 30 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℝ+ ) ∧ 𝐷 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ) → ( ⌊ ‘ ( ( 𝑋 ↑ 2 ) / 𝐷 ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑋 ) ) )
32 27 31 jca ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℝ+ ) ∧ 𝐷 ∈ ( 1 ... ( ⌊ ‘ 𝑋 ) ) ) → ( 𝑋 ≤ ( ( 𝑋 ↑ 2 ) / 𝐷 ) ∧ ( ⌊ ‘ ( ( 𝑋 ↑ 2 ) / 𝐷 ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑋 ) ) ) )