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 ) / 𝐷 ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑋 ) ) ) )