MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  chtub Structured version   Visualization version   GIF version

Theorem chtub 24871
Description: An upper bound on the Chebyshev function. (Contributed by Mario Carneiro, 13-Mar-2014.) (Revised 22-Sep-2014.)
Assertion
Ref Expression
chtub ((𝑁 ∈ ℝ ∧ 2 < 𝑁) → (θ‘𝑁) < ((log‘2) · ((2 · 𝑁) − 3)))

Proof of Theorem chtub
Dummy variables 𝑘 𝑛 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6158 . . . . 5 ((⌊‘𝑁) = 2 → (θ‘(⌊‘𝑁)) = (θ‘2))
2 2re 11050 . . . . . . . . . . 11 2 ∈ ℝ
3 1lt2 11154 . . . . . . . . . . 11 1 < 2
4 rplogcl 24288 . . . . . . . . . . 11 ((2 ∈ ℝ ∧ 1 < 2) → (log‘2) ∈ ℝ+)
52, 3, 4mp2an 707 . . . . . . . . . 10 (log‘2) ∈ ℝ+
6 elrp 11794 . . . . . . . . . 10 ((log‘2) ∈ ℝ+ ↔ ((log‘2) ∈ ℝ ∧ 0 < (log‘2)))
75, 6mpbi 220 . . . . . . . . 9 ((log‘2) ∈ ℝ ∧ 0 < (log‘2))
87simpli 474 . . . . . . . 8 (log‘2) ∈ ℝ
98recni 10012 . . . . . . 7 (log‘2) ∈ ℂ
109mulid1i 10002 . . . . . 6 ((log‘2) · 1) = (log‘2)
11 cht2 24832 . . . . . 6 (θ‘2) = (log‘2)
1210, 11eqtr4i 2646 . . . . 5 ((log‘2) · 1) = (θ‘2)
131, 12syl6reqr 2674 . . . 4 ((⌊‘𝑁) = 2 → ((log‘2) · 1) = (θ‘(⌊‘𝑁)))
14 chtfl 24809 . . . . 5 (𝑁 ∈ ℝ → (θ‘(⌊‘𝑁)) = (θ‘𝑁))
1514adantr 481 . . . 4 ((𝑁 ∈ ℝ ∧ 2 < 𝑁) → (θ‘(⌊‘𝑁)) = (θ‘𝑁))
1613, 15sylan9eqr 2677 . . 3 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → ((log‘2) · 1) = (θ‘𝑁))
17 2t2e4 11137 . . . . . . 7 (2 · 2) = 4
18 df-4 11041 . . . . . . 7 4 = (3 + 1)
1917, 18eqtri 2643 . . . . . 6 (2 · 2) = (3 + 1)
20 simplr 791 . . . . . . 7 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → 2 < 𝑁)
212a1i 11 . . . . . . . 8 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → 2 ∈ ℝ)
22 simpl 473 . . . . . . . . 9 ((𝑁 ∈ ℝ ∧ 2 < 𝑁) → 𝑁 ∈ ℝ)
2322adantr 481 . . . . . . . 8 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → 𝑁 ∈ ℝ)
24 2pos 11072 . . . . . . . . . 10 0 < 2
252, 24pm3.2i 471 . . . . . . . . 9 (2 ∈ ℝ ∧ 0 < 2)
2625a1i 11 . . . . . . . 8 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → (2 ∈ ℝ ∧ 0 < 2))
27 ltmul2 10834 . . . . . . . 8 ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (2 < 𝑁 ↔ (2 · 2) < (2 · 𝑁)))
2821, 23, 26, 27syl3anc 1323 . . . . . . 7 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → (2 < 𝑁 ↔ (2 · 2) < (2 · 𝑁)))
2920, 28mpbid 222 . . . . . 6 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → (2 · 2) < (2 · 𝑁))
3019, 29syl5eqbrr 4659 . . . . 5 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → (3 + 1) < (2 · 𝑁))
31 3re 11054 . . . . . . 7 3 ∈ ℝ
3231a1i 11 . . . . . 6 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → 3 ∈ ℝ)
33 1red 10015 . . . . . 6 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → 1 ∈ ℝ)
34 remulcl 9981 . . . . . . . 8 ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (2 · 𝑁) ∈ ℝ)
352, 22, 34sylancr 694 . . . . . . 7 ((𝑁 ∈ ℝ ∧ 2 < 𝑁) → (2 · 𝑁) ∈ ℝ)
3635adantr 481 . . . . . 6 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → (2 · 𝑁) ∈ ℝ)
3732, 33, 36ltaddsub2d 10588 . . . . 5 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → ((3 + 1) < (2 · 𝑁) ↔ 1 < ((2 · 𝑁) − 3)))
3830, 37mpbid 222 . . . 4 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → 1 < ((2 · 𝑁) − 3))
39 resubcl 10305 . . . . . . 7 (((2 · 𝑁) ∈ ℝ ∧ 3 ∈ ℝ) → ((2 · 𝑁) − 3) ∈ ℝ)
4035, 31, 39sylancl 693 . . . . . 6 ((𝑁 ∈ ℝ ∧ 2 < 𝑁) → ((2 · 𝑁) − 3) ∈ ℝ)
4140adantr 481 . . . . 5 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → ((2 · 𝑁) − 3) ∈ ℝ)
427a1i 11 . . . . 5 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → ((log‘2) ∈ ℝ ∧ 0 < (log‘2)))
43 ltmul2 10834 . . . . 5 ((1 ∈ ℝ ∧ ((2 · 𝑁) − 3) ∈ ℝ ∧ ((log‘2) ∈ ℝ ∧ 0 < (log‘2))) → (1 < ((2 · 𝑁) − 3) ↔ ((log‘2) · 1) < ((log‘2) · ((2 · 𝑁) − 3))))
4433, 41, 42, 43syl3anc 1323 . . . 4 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → (1 < ((2 · 𝑁) − 3) ↔ ((log‘2) · 1) < ((log‘2) · ((2 · 𝑁) − 3))))
4538, 44mpbid 222 . . 3 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → ((log‘2) · 1) < ((log‘2) · ((2 · 𝑁) − 3)))
4616, 45eqbrtrrd 4647 . 2 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → (θ‘𝑁) < ((log‘2) · ((2 · 𝑁) − 3)))
47 chtcl 24769 . . . 4 (𝑁 ∈ ℝ → (θ‘𝑁) ∈ ℝ)
4847ad2antrr 761 . . 3 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → (θ‘𝑁) ∈ ℝ)
49 reflcl 12553 . . . . . . 7 (𝑁 ∈ ℝ → (⌊‘𝑁) ∈ ℝ)
5049ad2antrr 761 . . . . . 6 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → (⌊‘𝑁) ∈ ℝ)
51 remulcl 9981 . . . . . 6 ((2 ∈ ℝ ∧ (⌊‘𝑁) ∈ ℝ) → (2 · (⌊‘𝑁)) ∈ ℝ)
522, 50, 51sylancr 694 . . . . 5 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → (2 · (⌊‘𝑁)) ∈ ℝ)
53 resubcl 10305 . . . . 5 (((2 · (⌊‘𝑁)) ∈ ℝ ∧ 3 ∈ ℝ) → ((2 · (⌊‘𝑁)) − 3) ∈ ℝ)
5452, 31, 53sylancl 693 . . . 4 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → ((2 · (⌊‘𝑁)) − 3) ∈ ℝ)
55 remulcl 9981 . . . 4 (((log‘2) ∈ ℝ ∧ ((2 · (⌊‘𝑁)) − 3) ∈ ℝ) → ((log‘2) · ((2 · (⌊‘𝑁)) − 3)) ∈ ℝ)
568, 54, 55sylancr 694 . . 3 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → ((log‘2) · ((2 · (⌊‘𝑁)) − 3)) ∈ ℝ)
5740adantr 481 . . . 4 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → ((2 · 𝑁) − 3) ∈ ℝ)
58 remulcl 9981 . . . 4 (((log‘2) ∈ ℝ ∧ ((2 · 𝑁) − 3) ∈ ℝ) → ((log‘2) · ((2 · 𝑁) − 3)) ∈ ℝ)
598, 57, 58sylancr 694 . . 3 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → ((log‘2) · ((2 · 𝑁) − 3)) ∈ ℝ)
6015adantr 481 . . . 4 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → (θ‘(⌊‘𝑁)) = (θ‘𝑁))
61 simpr 477 . . . . . 6 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → (⌊‘𝑁) ∈ (ℤ‘(2 + 1)))
62 df-3 11040 . . . . . . 7 3 = (2 + 1)
6362fveq2i 6161 . . . . . 6 (ℤ‘3) = (ℤ‘(2 + 1))
6461, 63syl6eleqr 2709 . . . . 5 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → (⌊‘𝑁) ∈ (ℤ‘3))
65 eluzfz2 12307 . . . . . 6 ((⌊‘𝑁) ∈ (ℤ‘3) → (⌊‘𝑁) ∈ (3...(⌊‘𝑁)))
66 3z 11370 . . . . . . 7 3 ∈ ℤ
67 oveq2 6623 . . . . . . . 8 (𝑥 = 3 → (3...𝑥) = (3...3))
6867raleqdv 3137 . . . . . . 7 (𝑥 = 3 → (∀𝑘 ∈ (3...𝑥)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ ∀𝑘 ∈ (3...3)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))))
69 oveq2 6623 . . . . . . . 8 (𝑥 = 𝑛 → (3...𝑥) = (3...𝑛))
7069raleqdv 3137 . . . . . . 7 (𝑥 = 𝑛 → (∀𝑘 ∈ (3...𝑥)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ ∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))))
71 oveq2 6623 . . . . . . . 8 (𝑥 = (𝑛 + 1) → (3...𝑥) = (3...(𝑛 + 1)))
7271raleqdv 3137 . . . . . . 7 (𝑥 = (𝑛 + 1) → (∀𝑘 ∈ (3...𝑥)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ ∀𝑘 ∈ (3...(𝑛 + 1))(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))))
73 oveq2 6623 . . . . . . . 8 (𝑥 = (⌊‘𝑁) → (3...𝑥) = (3...(⌊‘𝑁)))
7473raleqdv 3137 . . . . . . 7 (𝑥 = (⌊‘𝑁) → (∀𝑘 ∈ (3...𝑥)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ ∀𝑘 ∈ (3...(⌊‘𝑁))(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))))
75 6lt8 11176 . . . . . . . . . . 11 6 < 8
76 6re 11061 . . . . . . . . . . . . 13 6 ∈ ℝ
77 6pos 11079 . . . . . . . . . . . . 13 0 < 6
7876, 77elrpii 11795 . . . . . . . . . . . 12 6 ∈ ℝ+
79 8re 11065 . . . . . . . . . . . . 13 8 ∈ ℝ
80 8pos 11081 . . . . . . . . . . . . 13 0 < 8
8179, 80elrpii 11795 . . . . . . . . . . . 12 8 ∈ ℝ+
82 logltb 24284 . . . . . . . . . . . 12 ((6 ∈ ℝ+ ∧ 8 ∈ ℝ+) → (6 < 8 ↔ (log‘6) < (log‘8)))
8378, 81, 82mp2an 707 . . . . . . . . . . 11 (6 < 8 ↔ (log‘6) < (log‘8))
8475, 83mpbi 220 . . . . . . . . . 10 (log‘6) < (log‘8)
8584a1i 11 . . . . . . . . 9 (𝑘 ∈ (3...3) → (log‘6) < (log‘8))
86 elfz1eq 12310 . . . . . . . . . . 11 (𝑘 ∈ (3...3) → 𝑘 = 3)
8786fveq2d 6162 . . . . . . . . . 10 (𝑘 ∈ (3...3) → (θ‘𝑘) = (θ‘3))
88 cht3 24833 . . . . . . . . . 10 (θ‘3) = (log‘6)
8987, 88syl6eq 2671 . . . . . . . . 9 (𝑘 ∈ (3...3) → (θ‘𝑘) = (log‘6))
9086oveq2d 6631 . . . . . . . . . . . . 13 (𝑘 ∈ (3...3) → (2 · 𝑘) = (2 · 3))
9190oveq1d 6630 . . . . . . . . . . . 12 (𝑘 ∈ (3...3) → ((2 · 𝑘) − 3) = ((2 · 3) − 3))
92 3cn 11055 . . . . . . . . . . . . . . 15 3 ∈ ℂ
93922timesi 11107 . . . . . . . . . . . . . 14 (2 · 3) = (3 + 3)
9493oveq1i 6625 . . . . . . . . . . . . 13 ((2 · 3) − 3) = ((3 + 3) − 3)
9592, 92pncan3oi 10257 . . . . . . . . . . . . 13 ((3 + 3) − 3) = 3
9694, 95eqtri 2643 . . . . . . . . . . . 12 ((2 · 3) − 3) = 3
9791, 96syl6eq 2671 . . . . . . . . . . 11 (𝑘 ∈ (3...3) → ((2 · 𝑘) − 3) = 3)
9897oveq2d 6631 . . . . . . . . . 10 (𝑘 ∈ (3...3) → ((log‘2) · ((2 · 𝑘) − 3)) = ((log‘2) · 3))
99 2rp 11797 . . . . . . . . . . . . . . 15 2 ∈ ℝ+
100 relogcl 24260 . . . . . . . . . . . . . . 15 (2 ∈ ℝ+ → (log‘2) ∈ ℝ)
10199, 100ax-mp 5 . . . . . . . . . . . . . 14 (log‘2) ∈ ℝ
102101recni 10012 . . . . . . . . . . . . 13 (log‘2) ∈ ℂ
103102, 92mulcomi 10006 . . . . . . . . . . . 12 ((log‘2) · 3) = (3 · (log‘2))
104 relogexp 24280 . . . . . . . . . . . . 13 ((2 ∈ ℝ+ ∧ 3 ∈ ℤ) → (log‘(2↑3)) = (3 · (log‘2)))
10599, 66, 104mp2an 707 . . . . . . . . . . . 12 (log‘(2↑3)) = (3 · (log‘2))
106103, 105eqtr4i 2646 . . . . . . . . . . 11 ((log‘2) · 3) = (log‘(2↑3))
107 cu2 12919 . . . . . . . . . . . 12 (2↑3) = 8
108107fveq2i 6161 . . . . . . . . . . 11 (log‘(2↑3)) = (log‘8)
109106, 108eqtri 2643 . . . . . . . . . 10 ((log‘2) · 3) = (log‘8)
11098, 109syl6eq 2671 . . . . . . . . 9 (𝑘 ∈ (3...3) → ((log‘2) · ((2 · 𝑘) − 3)) = (log‘8))
11185, 89, 1103brtr4d 4655 . . . . . . . 8 (𝑘 ∈ (3...3) → (θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)))
112111rgen 2918 . . . . . . 7 𝑘 ∈ (3...3)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))
113 df-2 11039 . . . . . . . . . . . . . . . . . 18 2 = (1 + 1)
114 2div2e1 11110 . . . . . . . . . . . . . . . . . . . 20 (2 / 2) = 1
115 eluzle 11660 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (ℤ‘3) → 3 ≤ 𝑛)
11662, 115syl5eqbrr 4659 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (ℤ‘3) → (2 + 1) ≤ 𝑛)
117 2z 11369 . . . . . . . . . . . . . . . . . . . . . . 23 2 ∈ ℤ
118 eluzelz 11657 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (ℤ‘3) → 𝑛 ∈ ℤ)
119 zltp1le 11387 . . . . . . . . . . . . . . . . . . . . . . 23 ((2 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (2 < 𝑛 ↔ (2 + 1) ≤ 𝑛))
120117, 118, 119sylancr 694 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (ℤ‘3) → (2 < 𝑛 ↔ (2 + 1) ≤ 𝑛))
121116, 120mpbird 247 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (ℤ‘3) → 2 < 𝑛)
122 eluzelre 11658 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (ℤ‘3) → 𝑛 ∈ ℝ)
123 ltdiv1 10847 . . . . . . . . . . . . . . . . . . . . . . 23 ((2 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (2 < 𝑛 ↔ (2 / 2) < (𝑛 / 2)))
1242, 25, 123mp3an13 1412 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℝ → (2 < 𝑛 ↔ (2 / 2) < (𝑛 / 2)))
125122, 124syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (ℤ‘3) → (2 < 𝑛 ↔ (2 / 2) < (𝑛 / 2)))
126121, 125mpbid 222 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (ℤ‘3) → (2 / 2) < (𝑛 / 2))
127114, 126syl5eqbrr 4659 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (ℤ‘3) → 1 < (𝑛 / 2))
128122rehalfcld 11239 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (ℤ‘3) → (𝑛 / 2) ∈ ℝ)
129 1re 9999 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℝ
130 ltadd1 10455 . . . . . . . . . . . . . . . . . . . . 21 ((1 ∈ ℝ ∧ (𝑛 / 2) ∈ ℝ ∧ 1 ∈ ℝ) → (1 < (𝑛 / 2) ↔ (1 + 1) < ((𝑛 / 2) + 1)))
131129, 129, 130mp3an13 1412 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 / 2) ∈ ℝ → (1 < (𝑛 / 2) ↔ (1 + 1) < ((𝑛 / 2) + 1)))
132128, 131syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (ℤ‘3) → (1 < (𝑛 / 2) ↔ (1 + 1) < ((𝑛 / 2) + 1)))
133127, 132mpbid 222 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (ℤ‘3) → (1 + 1) < ((𝑛 / 2) + 1))
134113, 133syl5eqbr 4658 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (ℤ‘3) → 2 < ((𝑛 / 2) + 1))
135134adantr 481 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → 2 < ((𝑛 / 2) + 1))
136 peano2z 11378 . . . . . . . . . . . . . . . . . 18 ((𝑛 / 2) ∈ ℤ → ((𝑛 / 2) + 1) ∈ ℤ)
137136adantl 482 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ∈ ℤ)
138 zltp1le 11387 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℤ ∧ ((𝑛 / 2) + 1) ∈ ℤ) → (2 < ((𝑛 / 2) + 1) ↔ (2 + 1) ≤ ((𝑛 / 2) + 1)))
139117, 137, 138sylancr 694 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 < ((𝑛 / 2) + 1) ↔ (2 + 1) ≤ ((𝑛 / 2) + 1)))
140135, 139mpbid 222 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 + 1) ≤ ((𝑛 / 2) + 1))
14162, 140syl5eqbr 4658 . . . . . . . . . . . . . 14 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → 3 ≤ ((𝑛 / 2) + 1))
142 1red 10015 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (ℤ‘3) → 1 ∈ ℝ)
143 ltle 10086 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℝ ∧ (𝑛 / 2) ∈ ℝ) → (1 < (𝑛 / 2) → 1 ≤ (𝑛 / 2)))
144129, 128, 143sylancr 694 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (ℤ‘3) → (1 < (𝑛 / 2) → 1 ≤ (𝑛 / 2)))
145127, 144mpd 15 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (ℤ‘3) → 1 ≤ (𝑛 / 2))
146142, 128, 128, 145leadd2dd 10602 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ℤ‘3) → ((𝑛 / 2) + 1) ≤ ((𝑛 / 2) + (𝑛 / 2)))
147122recnd 10028 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (ℤ‘3) → 𝑛 ∈ ℂ)
1481472halvesd 11238 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ℤ‘3) → ((𝑛 / 2) + (𝑛 / 2)) = 𝑛)
149146, 148breqtrd 4649 . . . . . . . . . . . . . . 15 (𝑛 ∈ (ℤ‘3) → ((𝑛 / 2) + 1) ≤ 𝑛)
150149adantr 481 . . . . . . . . . . . . . 14 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ≤ 𝑛)
151 elfz 12290 . . . . . . . . . . . . . . . 16 ((((𝑛 / 2) + 1) ∈ ℤ ∧ 3 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝑛 / 2) + 1) ∈ (3...𝑛) ↔ (3 ≤ ((𝑛 / 2) + 1) ∧ ((𝑛 / 2) + 1) ≤ 𝑛)))
15266, 151mp3an2 1409 . . . . . . . . . . . . . . 15 ((((𝑛 / 2) + 1) ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝑛 / 2) + 1) ∈ (3...𝑛) ↔ (3 ≤ ((𝑛 / 2) + 1) ∧ ((𝑛 / 2) + 1) ≤ 𝑛)))
153136, 118, 152syl2anr 495 . . . . . . . . . . . . . 14 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (((𝑛 / 2) + 1) ∈ (3...𝑛) ↔ (3 ≤ ((𝑛 / 2) + 1) ∧ ((𝑛 / 2) + 1) ≤ 𝑛)))
154141, 150, 153mpbir2and 956 . . . . . . . . . . . . 13 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ∈ (3...𝑛))
155 fveq2 6158 . . . . . . . . . . . . . . 15 (𝑘 = ((𝑛 / 2) + 1) → (θ‘𝑘) = (θ‘((𝑛 / 2) + 1)))
156 oveq2 6623 . . . . . . . . . . . . . . . . 17 (𝑘 = ((𝑛 / 2) + 1) → (2 · 𝑘) = (2 · ((𝑛 / 2) + 1)))
157156oveq1d 6630 . . . . . . . . . . . . . . . 16 (𝑘 = ((𝑛 / 2) + 1) → ((2 · 𝑘) − 3) = ((2 · ((𝑛 / 2) + 1)) − 3))
158157oveq2d 6631 . . . . . . . . . . . . . . 15 (𝑘 = ((𝑛 / 2) + 1) → ((log‘2) · ((2 · 𝑘) − 3)) = ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3)))
159155, 158breq12d 4636 . . . . . . . . . . . . . 14 (𝑘 = ((𝑛 / 2) + 1) → ((θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ (θ‘((𝑛 / 2) + 1)) < ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3))))
160159rspcv 3295 . . . . . . . . . . . . 13 (((𝑛 / 2) + 1) ∈ (3...𝑛) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → (θ‘((𝑛 / 2) + 1)) < ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3))))
161154, 160syl 17 . . . . . . . . . . . 12 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → (θ‘((𝑛 / 2) + 1)) < ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3))))
162128recnd 10028 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (ℤ‘3) → (𝑛 / 2) ∈ ℂ)
163162adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (𝑛 / 2) ∈ ℂ)
164 2cn 11051 . . . . . . . . . . . . . . . . . . . . 21 2 ∈ ℂ
165 ax-1cn 9954 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℂ
166 adddi 9985 . . . . . . . . . . . . . . . . . . . . 21 ((2 ∈ ℂ ∧ (𝑛 / 2) ∈ ℂ ∧ 1 ∈ ℂ) → (2 · ((𝑛 / 2) + 1)) = ((2 · (𝑛 / 2)) + (2 · 1)))
167164, 165, 166mp3an13 1412 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 / 2) ∈ ℂ → (2 · ((𝑛 / 2) + 1)) = ((2 · (𝑛 / 2)) + (2 · 1)))
168163, 167syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 · ((𝑛 / 2) + 1)) = ((2 · (𝑛 / 2)) + (2 · 1)))
169147adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → 𝑛 ∈ ℂ)
170 2ne0 11073 . . . . . . . . . . . . . . . . . . . . . 22 2 ≠ 0
171 divcan2 10653 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (2 · (𝑛 / 2)) = 𝑛)
172164, 170, 171mp3an23 1413 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ℂ → (2 · (𝑛 / 2)) = 𝑛)
173169, 172syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 · (𝑛 / 2)) = 𝑛)
174164mulid1i 10002 . . . . . . . . . . . . . . . . . . . . 21 (2 · 1) = 2
175174a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 · 1) = 2)
176173, 175oveq12d 6633 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · (𝑛 / 2)) + (2 · 1)) = (𝑛 + 2))
177168, 176eqtrd 2655 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 · ((𝑛 / 2) + 1)) = (𝑛 + 2))
178177oveq1d 6630 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · ((𝑛 / 2) + 1)) − 3) = ((𝑛 + 2) − 3))
179 2p1e3 11111 . . . . . . . . . . . . . . . . . . . 20 (2 + 1) = 3
18092, 164, 165, 179subaddrii 10330 . . . . . . . . . . . . . . . . . . 19 (3 − 2) = 1
181180oveq2i 6626 . . . . . . . . . . . . . . . . . 18 (𝑛 − (3 − 2)) = (𝑛 − 1)
182 subsub3 10273 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℂ ∧ 3 ∈ ℂ ∧ 2 ∈ ℂ) → (𝑛 − (3 − 2)) = ((𝑛 + 2) − 3))
18392, 164, 182mp3an23 1413 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℂ → (𝑛 − (3 − 2)) = ((𝑛 + 2) − 3))
184169, 183syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (𝑛 − (3 − 2)) = ((𝑛 + 2) − 3))
185181, 184syl5reqr 2670 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 + 2) − 3) = (𝑛 − 1))
186178, 185eqtrd 2655 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · ((𝑛 / 2) + 1)) − 3) = (𝑛 − 1))
187186oveq2d 6631 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3)) = ((log‘2) · (𝑛 − 1)))
188187breq2d 4635 . . . . . . . . . . . . . 14 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((θ‘((𝑛 / 2) + 1)) < ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3)) ↔ (θ‘((𝑛 / 2) + 1)) < ((log‘2) · (𝑛 − 1))))
189137zred 11442 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ∈ ℝ)
190 chtcl 24769 . . . . . . . . . . . . . . . 16 (((𝑛 / 2) + 1) ∈ ℝ → (θ‘((𝑛 / 2) + 1)) ∈ ℝ)
191189, 190syl 17 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (θ‘((𝑛 / 2) + 1)) ∈ ℝ)
192122adantr 481 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → 𝑛 ∈ ℝ)
193 peano2rem 10308 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℝ → (𝑛 − 1) ∈ ℝ)
194192, 193syl 17 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (𝑛 − 1) ∈ ℝ)
195 remulcl 9981 . . . . . . . . . . . . . . . 16 (((log‘2) ∈ ℝ ∧ (𝑛 − 1) ∈ ℝ) → ((log‘2) · (𝑛 − 1)) ∈ ℝ)
196101, 194, 195sylancr 694 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2) · (𝑛 − 1)) ∈ ℝ)
197 remulcl 9981 . . . . . . . . . . . . . . . 16 (((log‘2) ∈ ℝ ∧ 𝑛 ∈ ℝ) → ((log‘2) · 𝑛) ∈ ℝ)
198101, 192, 197sylancr 694 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2) · 𝑛) ∈ ℝ)
199191, 196, 198ltadd1d 10580 . . . . . . . . . . . . . 14 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((θ‘((𝑛 / 2) + 1)) < ((log‘2) · (𝑛 − 1)) ↔ ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) < (((log‘2) · (𝑛 − 1)) + ((log‘2) · 𝑛))))
200102a1i 11 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (log‘2) ∈ ℂ)
201194recnd 10028 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (𝑛 − 1) ∈ ℂ)
202200, 201, 169adddid 10024 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2) · ((𝑛 − 1) + 𝑛)) = (((log‘2) · (𝑛 − 1)) + ((log‘2) · 𝑛)))
203 adddi 9985 . . . . . . . . . . . . . . . . . . . . . 22 ((2 ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → (2 · (𝑛 + 1)) = ((2 · 𝑛) + (2 · 1)))
204164, 165, 203mp3an13 1412 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ℂ → (2 · (𝑛 + 1)) = ((2 · 𝑛) + (2 · 1)))
205169, 204syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 · (𝑛 + 1)) = ((2 · 𝑛) + (2 · 1)))
206174oveq2i 6626 . . . . . . . . . . . . . . . . . . . 20 ((2 · 𝑛) + (2 · 1)) = ((2 · 𝑛) + 2)
207205, 206syl6eq 2671 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 · (𝑛 + 1)) = ((2 · 𝑛) + 2))
208207oveq1d 6630 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · (𝑛 + 1)) − 3) = (((2 · 𝑛) + 2) − 3))
209 zmulcl 11386 . . . . . . . . . . . . . . . . . . . . . 22 ((2 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (2 · 𝑛) ∈ ℤ)
210117, 118, 209sylancr 694 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (ℤ‘3) → (2 · 𝑛) ∈ ℤ)
211210zcnd 11443 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (ℤ‘3) → (2 · 𝑛) ∈ ℂ)
212211adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 · 𝑛) ∈ ℂ)
213 subsub3 10273 . . . . . . . . . . . . . . . . . . . 20 (((2 · 𝑛) ∈ ℂ ∧ 3 ∈ ℂ ∧ 2 ∈ ℂ) → ((2 · 𝑛) − (3 − 2)) = (((2 · 𝑛) + 2) − 3))
21492, 164, 213mp3an23 1413 . . . . . . . . . . . . . . . . . . 19 ((2 · 𝑛) ∈ ℂ → ((2 · 𝑛) − (3 − 2)) = (((2 · 𝑛) + 2) − 3))
215212, 214syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · 𝑛) − (3 − 2)) = (((2 · 𝑛) + 2) − 3))
216180oveq2i 6626 . . . . . . . . . . . . . . . . . . 19 ((2 · 𝑛) − (3 − 2)) = ((2 · 𝑛) − 1)
2171692timesd 11235 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 · 𝑛) = (𝑛 + 𝑛))
218217oveq1d 6630 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · 𝑛) − 1) = ((𝑛 + 𝑛) − 1))
219165a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → 1 ∈ ℂ)
220169, 169, 219addsubd 10373 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 + 𝑛) − 1) = ((𝑛 − 1) + 𝑛))
221218, 220eqtrd 2655 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · 𝑛) − 1) = ((𝑛 − 1) + 𝑛))
222216, 221syl5eq 2667 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · 𝑛) − (3 − 2)) = ((𝑛 − 1) + 𝑛))
223208, 215, 2223eqtr2rd 2662 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 − 1) + 𝑛) = ((2 · (𝑛 + 1)) − 3))
224223oveq2d 6631 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2) · ((𝑛 − 1) + 𝑛)) = ((log‘2) · ((2 · (𝑛 + 1)) − 3)))
225202, 224eqtr3d 2657 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (((log‘2) · (𝑛 − 1)) + ((log‘2) · 𝑛)) = ((log‘2) · ((2 · (𝑛 + 1)) − 3)))
226225breq2d 4635 . . . . . . . . . . . . . 14 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) < (((log‘2) · (𝑛 − 1)) + ((log‘2) · 𝑛)) ↔ ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
227188, 199, 2263bitrd 294 . . . . . . . . . . . . 13 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((θ‘((𝑛 / 2) + 1)) < ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3)) ↔ ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
228 3nn 11146 . . . . . . . . . . . . . . . . 17 3 ∈ ℕ
229 elfzuz 12296 . . . . . . . . . . . . . . . . . 18 (((𝑛 / 2) + 1) ∈ (3...𝑛) → ((𝑛 / 2) + 1) ∈ (ℤ‘3))
230154, 229syl 17 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ∈ (ℤ‘3))
231 eluznn 11718 . . . . . . . . . . . . . . . . 17 ((3 ∈ ℕ ∧ ((𝑛 / 2) + 1) ∈ (ℤ‘3)) → ((𝑛 / 2) + 1) ∈ ℕ)
232228, 230, 231sylancr 694 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ∈ ℕ)
233 chtublem 24870 . . . . . . . . . . . . . . . 16 (((𝑛 / 2) + 1) ∈ ℕ → (θ‘((2 · ((𝑛 / 2) + 1)) − 1)) ≤ ((θ‘((𝑛 / 2) + 1)) + ((log‘4) · (((𝑛 / 2) + 1) − 1))))
234232, 233syl 17 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (θ‘((2 · ((𝑛 / 2) + 1)) − 1)) ≤ ((θ‘((𝑛 / 2) + 1)) + ((log‘4) · (((𝑛 / 2) + 1) − 1))))
235177oveq1d 6630 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · ((𝑛 / 2) + 1)) − 1) = ((𝑛 + 2) − 1))
236 addsubass 10251 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 2) − 1) = (𝑛 + (2 − 1)))
237164, 165, 236mp3an23 1413 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℂ → ((𝑛 + 2) − 1) = (𝑛 + (2 − 1)))
238169, 237syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 + 2) − 1) = (𝑛 + (2 − 1)))
239 2m1e1 11095 . . . . . . . . . . . . . . . . . . 19 (2 − 1) = 1
240239oveq2i 6626 . . . . . . . . . . . . . . . . . 18 (𝑛 + (2 − 1)) = (𝑛 + 1)
241238, 240syl6eq 2671 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 + 2) − 1) = (𝑛 + 1))
242235, 241eqtrd 2655 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · ((𝑛 / 2) + 1)) − 1) = (𝑛 + 1))
243242fveq2d 6162 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (θ‘((2 · ((𝑛 / 2) + 1)) − 1)) = (θ‘(𝑛 + 1)))
244 pncan 10247 . . . . . . . . . . . . . . . . . . 19 (((𝑛 / 2) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑛 / 2) + 1) − 1) = (𝑛 / 2))
245163, 165, 244sylancl 693 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (((𝑛 / 2) + 1) − 1) = (𝑛 / 2))
246245oveq2d 6631 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘4) · (((𝑛 / 2) + 1) − 1)) = ((log‘4) · (𝑛 / 2)))
247 relogexp 24280 . . . . . . . . . . . . . . . . . . . . 21 ((2 ∈ ℝ+ ∧ 2 ∈ ℤ) → (log‘(2↑2)) = (2 · (log‘2)))
24899, 117, 247mp2an 707 . . . . . . . . . . . . . . . . . . . 20 (log‘(2↑2)) = (2 · (log‘2))
249 sq2 12916 . . . . . . . . . . . . . . . . . . . . 21 (2↑2) = 4
250249fveq2i 6161 . . . . . . . . . . . . . . . . . . . 20 (log‘(2↑2)) = (log‘4)
251164, 102mulcomi 10006 . . . . . . . . . . . . . . . . . . . 20 (2 · (log‘2)) = ((log‘2) · 2)
252248, 250, 2513eqtr3i 2651 . . . . . . . . . . . . . . . . . . 19 (log‘4) = ((log‘2) · 2)
253252oveq1i 6625 . . . . . . . . . . . . . . . . . 18 ((log‘4) · (𝑛 / 2)) = (((log‘2) · 2) · (𝑛 / 2))
254164a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → 2 ∈ ℂ)
255200, 254, 163mulassd 10023 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (((log‘2) · 2) · (𝑛 / 2)) = ((log‘2) · (2 · (𝑛 / 2))))
256253, 255syl5eq 2667 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘4) · (𝑛 / 2)) = ((log‘2) · (2 · (𝑛 / 2))))
257173oveq2d 6631 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2) · (2 · (𝑛 / 2))) = ((log‘2) · 𝑛))
258246, 256, 2573eqtrd 2659 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘4) · (((𝑛 / 2) + 1) − 1)) = ((log‘2) · 𝑛))
259258oveq2d 6631 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((θ‘((𝑛 / 2) + 1)) + ((log‘4) · (((𝑛 / 2) + 1) − 1))) = ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)))
260234, 243, 2593brtr3d 4654 . . . . . . . . . . . . . 14 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (θ‘(𝑛 + 1)) ≤ ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)))
261 peano2uz 11701 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (ℤ‘3) → (𝑛 + 1) ∈ (ℤ‘3))
262 eluzelz 11657 . . . . . . . . . . . . . . . . . . 19 ((𝑛 + 1) ∈ (ℤ‘3) → (𝑛 + 1) ∈ ℤ)
263261, 262syl 17 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (ℤ‘3) → (𝑛 + 1) ∈ ℤ)
264263zred 11442 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (ℤ‘3) → (𝑛 + 1) ∈ ℝ)
265264adantr 481 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (𝑛 + 1) ∈ ℝ)
266 chtcl 24769 . . . . . . . . . . . . . . . 16 ((𝑛 + 1) ∈ ℝ → (θ‘(𝑛 + 1)) ∈ ℝ)
267265, 266syl 17 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (θ‘(𝑛 + 1)) ∈ ℝ)
268191, 198readdcld 10029 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) ∈ ℝ)
269 zmulcl 11386 . . . . . . . . . . . . . . . . . . . 20 ((2 ∈ ℤ ∧ (𝑛 + 1) ∈ ℤ) → (2 · (𝑛 + 1)) ∈ ℤ)
270117, 263, 269sylancr 694 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (ℤ‘3) → (2 · (𝑛 + 1)) ∈ ℤ)
271270zred 11442 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (ℤ‘3) → (2 · (𝑛 + 1)) ∈ ℝ)
272 resubcl 10305 . . . . . . . . . . . . . . . . . 18 (((2 · (𝑛 + 1)) ∈ ℝ ∧ 3 ∈ ℝ) → ((2 · (𝑛 + 1)) − 3) ∈ ℝ)
273271, 31, 272sylancl 693 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (ℤ‘3) → ((2 · (𝑛 + 1)) − 3) ∈ ℝ)
274273adantr 481 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · (𝑛 + 1)) − 3) ∈ ℝ)
275 remulcl 9981 . . . . . . . . . . . . . . . 16 (((log‘2) ∈ ℝ ∧ ((2 · (𝑛 + 1)) − 3) ∈ ℝ) → ((log‘2) · ((2 · (𝑛 + 1)) − 3)) ∈ ℝ)
276101, 274, 275sylancr 694 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2) · ((2 · (𝑛 + 1)) − 3)) ∈ ℝ)
277 lelttr 10088 . . . . . . . . . . . . . . 15 (((θ‘(𝑛 + 1)) ∈ ℝ ∧ ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) ∈ ℝ ∧ ((log‘2) · ((2 · (𝑛 + 1)) − 3)) ∈ ℝ) → (((θ‘(𝑛 + 1)) ≤ ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) ∧ ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))) → (θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
278267, 268, 276, 277syl3anc 1323 . . . . . . . . . . . . . 14 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (((θ‘(𝑛 + 1)) ≤ ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) ∧ ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))) → (θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
279260, 278mpand 710 . . . . . . . . . . . . 13 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3)) → (θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
280227, 279sylbid 230 . . . . . . . . . . . 12 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((θ‘((𝑛 / 2) + 1)) < ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3)) → (θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
281161, 280syld 47 . . . . . . . . . . 11 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → (θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
282 eluzfz2 12307 . . . . . . . . . . . . . 14 (𝑛 ∈ (ℤ‘3) → 𝑛 ∈ (3...𝑛))
283 fveq2 6158 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑛 → (θ‘𝑘) = (θ‘𝑛))
284 oveq2 6623 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑛 → (2 · 𝑘) = (2 · 𝑛))
285284oveq1d 6630 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑛 → ((2 · 𝑘) − 3) = ((2 · 𝑛) − 3))
286285oveq2d 6631 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑛 → ((log‘2) · ((2 · 𝑘) − 3)) = ((log‘2) · ((2 · 𝑛) − 3)))
287283, 286breq12d 4636 . . . . . . . . . . . . . . 15 (𝑘 = 𝑛 → ((θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ (θ‘𝑛) < ((log‘2) · ((2 · 𝑛) − 3))))
288287rspcv 3295 . . . . . . . . . . . . . 14 (𝑛 ∈ (3...𝑛) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → (θ‘𝑛) < ((log‘2) · ((2 · 𝑛) − 3))))
289282, 288syl 17 . . . . . . . . . . . . 13 (𝑛 ∈ (ℤ‘3) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → (θ‘𝑛) < ((log‘2) · ((2 · 𝑛) − 3))))
290289adantr 481 . . . . . . . . . . . 12 ((𝑛 ∈ (ℤ‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → (θ‘𝑛) < ((log‘2) · ((2 · 𝑛) − 3))))
291210zred 11442 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (ℤ‘3) → (2 · 𝑛) ∈ ℝ)
29231a1i 11 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (ℤ‘3) → 3 ∈ ℝ)
293122ltp1d 10914 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (ℤ‘3) → 𝑛 < (𝑛 + 1))
29425a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (ℤ‘3) → (2 ∈ ℝ ∧ 0 < 2))
295 ltmul2 10834 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℝ ∧ (𝑛 + 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝑛 < (𝑛 + 1) ↔ (2 · 𝑛) < (2 · (𝑛 + 1))))
296122, 264, 294, 295syl3anc 1323 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (ℤ‘3) → (𝑛 < (𝑛 + 1) ↔ (2 · 𝑛) < (2 · (𝑛 + 1))))
297293, 296mpbid 222 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (ℤ‘3) → (2 · 𝑛) < (2 · (𝑛 + 1)))
298291, 271, 292, 297ltsub1dd 10599 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ℤ‘3) → ((2 · 𝑛) − 3) < ((2 · (𝑛 + 1)) − 3))
299 resubcl 10305 . . . . . . . . . . . . . . . . . 18 (((2 · 𝑛) ∈ ℝ ∧ 3 ∈ ℝ) → ((2 · 𝑛) − 3) ∈ ℝ)
300291, 31, 299sylancl 693 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (ℤ‘3) → ((2 · 𝑛) − 3) ∈ ℝ)
3017a1i 11 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (ℤ‘3) → ((log‘2) ∈ ℝ ∧ 0 < (log‘2)))
302 ltmul2 10834 . . . . . . . . . . . . . . . . 17 ((((2 · 𝑛) − 3) ∈ ℝ ∧ ((2 · (𝑛 + 1)) − 3) ∈ ℝ ∧ ((log‘2) ∈ ℝ ∧ 0 < (log‘2))) → (((2 · 𝑛) − 3) < ((2 · (𝑛 + 1)) − 3) ↔ ((log‘2) · ((2 · 𝑛) − 3)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
303300, 273, 301, 302syl3anc 1323 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ℤ‘3) → (((2 · 𝑛) − 3) < ((2 · (𝑛 + 1)) − 3) ↔ ((log‘2) · ((2 · 𝑛) − 3)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
304298, 303mpbid 222 . . . . . . . . . . . . . . 15 (𝑛 ∈ (ℤ‘3) → ((log‘2) · ((2 · 𝑛) − 3)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3)))
305 chtcl 24769 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℝ → (θ‘𝑛) ∈ ℝ)
306122, 305syl 17 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ℤ‘3) → (θ‘𝑛) ∈ ℝ)
307 remulcl 9981 . . . . . . . . . . . . . . . . 17 (((log‘2) ∈ ℝ ∧ ((2 · 𝑛) − 3) ∈ ℝ) → ((log‘2) · ((2 · 𝑛) − 3)) ∈ ℝ)
308101, 300, 307sylancr 694 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ℤ‘3) → ((log‘2) · ((2 · 𝑛) − 3)) ∈ ℝ)
309101, 273, 275sylancr 694 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ℤ‘3) → ((log‘2) · ((2 · (𝑛 + 1)) − 3)) ∈ ℝ)
310 lttr 10074 . . . . . . . . . . . . . . . 16 (((θ‘𝑛) ∈ ℝ ∧ ((log‘2) · ((2 · 𝑛) − 3)) ∈ ℝ ∧ ((log‘2) · ((2 · (𝑛 + 1)) − 3)) ∈ ℝ) → (((θ‘𝑛) < ((log‘2) · ((2 · 𝑛) − 3)) ∧ ((log‘2) · ((2 · 𝑛) − 3)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))) → (θ‘𝑛) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
311306, 308, 309, 310syl3anc 1323 . . . . . . . . . . . . . . 15 (𝑛 ∈ (ℤ‘3) → (((θ‘𝑛) < ((log‘2) · ((2 · 𝑛) − 3)) ∧ ((log‘2) · ((2 · 𝑛) − 3)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))) → (θ‘𝑛) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
312304, 311mpan2d 709 . . . . . . . . . . . . . 14 (𝑛 ∈ (ℤ‘3) → ((θ‘𝑛) < ((log‘2) · ((2 · 𝑛) − 3)) → (θ‘𝑛) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
313312adantr 481 . . . . . . . . . . . . 13 ((𝑛 ∈ (ℤ‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) → ((θ‘𝑛) < ((log‘2) · ((2 · 𝑛) − 3)) → (θ‘𝑛) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
314118adantr 481 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) → 𝑛 ∈ ℤ)
315 dvdsval2 14929 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℤ ∧ 2 ≠ 0 ∧ (𝑛 + 1) ∈ ℤ) → (2 ∥ (𝑛 + 1) ↔ ((𝑛 + 1) / 2) ∈ ℤ))
316117, 170, 315mp3an12 1411 . . . . . . . . . . . . . . . . . 18 ((𝑛 + 1) ∈ ℤ → (2 ∥ (𝑛 + 1) ↔ ((𝑛 + 1) / 2) ∈ ℤ))
317263, 316syl 17 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (ℤ‘3) → (2 ∥ (𝑛 + 1) ↔ ((𝑛 + 1) / 2) ∈ ℤ))
318 2lt3 11155 . . . . . . . . . . . . . . . . . . . . . . . 24 2 < 3
3192, 31ltnlei 10118 . . . . . . . . . . . . . . . . . . . . . . . 24 (2 < 3 ↔ ¬ 3 ≤ 2)
320318, 319mpbi 220 . . . . . . . . . . . . . . . . . . . . . . 23 ¬ 3 ≤ 2
321 breq2 4627 . . . . . . . . . . . . . . . . . . . . . . 23 (2 = (𝑛 + 1) → (3 ≤ 2 ↔ 3 ≤ (𝑛 + 1)))
322320, 321mtbii 316 . . . . . . . . . . . . . . . . . . . . . 22 (2 = (𝑛 + 1) → ¬ 3 ≤ (𝑛 + 1))
323 eluzle 11660 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 + 1) ∈ (ℤ‘3) → 3 ≤ (𝑛 + 1))
324261, 323syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (ℤ‘3) → 3 ≤ (𝑛 + 1))
325322, 324nsyl3 133 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (ℤ‘3) → ¬ 2 = (𝑛 + 1))
326325adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 + 1) ∈ ℙ) → ¬ 2 = (𝑛 + 1))
327 uzid 11662 . . . . . . . . . . . . . . . . . . . . . 22 (2 ∈ ℤ → 2 ∈ (ℤ‘2))
328117, 327ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 2 ∈ (ℤ‘2)
329 simpr 477 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 + 1) ∈ ℙ) → (𝑛 + 1) ∈ ℙ)
330 dvdsprm 15358 . . . . . . . . . . . . . . . . . . . . 21 ((2 ∈ (ℤ‘2) ∧ (𝑛 + 1) ∈ ℙ) → (2 ∥ (𝑛 + 1) ↔ 2 = (𝑛 + 1)))
331328, 329, 330sylancr 694 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 + 1) ∈ ℙ) → (2 ∥ (𝑛 + 1) ↔ 2 = (𝑛 + 1)))
332326, 331mtbird 315 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 + 1) ∈ ℙ) → ¬ 2 ∥ (𝑛 + 1))
333332ex 450 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (ℤ‘3) → ((𝑛 + 1) ∈ ℙ → ¬ 2 ∥ (𝑛 + 1)))
334333con2d 129 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (ℤ‘3) → (2 ∥ (𝑛 + 1) → ¬ (𝑛 + 1) ∈ ℙ))
335317, 334sylbird 250 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ℤ‘3) → (((𝑛 + 1) / 2) ∈ ℤ → ¬ (𝑛 + 1) ∈ ℙ))
336335imp 445 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) → ¬ (𝑛 + 1) ∈ ℙ)
337 chtnprm 24814 . . . . . . . . . . . . . . 15 ((𝑛 ∈ ℤ ∧ ¬ (𝑛 + 1) ∈ ℙ) → (θ‘(𝑛 + 1)) = (θ‘𝑛))
338314, 336, 337syl2anc 692 . . . . . . . . . . . . . 14 ((𝑛 ∈ (ℤ‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) → (θ‘(𝑛 + 1)) = (θ‘𝑛))
339338breq1d 4633 . . . . . . . . . . . . 13 ((𝑛 ∈ (ℤ‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) → ((θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3)) ↔ (θ‘𝑛) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
340313, 339sylibrd 249 . . . . . . . . . . . 12 ((𝑛 ∈ (ℤ‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) → ((θ‘𝑛) < ((log‘2) · ((2 · 𝑛) − 3)) → (θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
341290, 340syld 47 . . . . . . . . . . 11 ((𝑛 ∈ (ℤ‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → (θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
342 zeo 11423 . . . . . . . . . . . 12 (𝑛 ∈ ℤ → ((𝑛 / 2) ∈ ℤ ∨ ((𝑛 + 1) / 2) ∈ ℤ))
343118, 342syl 17 . . . . . . . . . . 11 (𝑛 ∈ (ℤ‘3) → ((𝑛 / 2) ∈ ℤ ∨ ((𝑛 + 1) / 2) ∈ ℤ))
344281, 341, 343mpjaodan 826 . . . . . . . . . 10 (𝑛 ∈ (ℤ‘3) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → (θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
345 ovex 6643 . . . . . . . . . . 11 (𝑛 + 1) ∈ V
346 fveq2 6158 . . . . . . . . . . . 12 (𝑘 = (𝑛 + 1) → (θ‘𝑘) = (θ‘(𝑛 + 1)))
347 oveq2 6623 . . . . . . . . . . . . . 14 (𝑘 = (𝑛 + 1) → (2 · 𝑘) = (2 · (𝑛 + 1)))
348347oveq1d 6630 . . . . . . . . . . . . 13 (𝑘 = (𝑛 + 1) → ((2 · 𝑘) − 3) = ((2 · (𝑛 + 1)) − 3))
349348oveq2d 6631 . . . . . . . . . . . 12 (𝑘 = (𝑛 + 1) → ((log‘2) · ((2 · 𝑘) − 3)) = ((log‘2) · ((2 · (𝑛 + 1)) − 3)))
350346, 349breq12d 4636 . . . . . . . . . . 11 (𝑘 = (𝑛 + 1) → ((θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ (θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
351345, 350ralsn 4200 . . . . . . . . . 10 (∀𝑘 ∈ {(𝑛 + 1)} (θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ (θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3)))
352344, 351syl6ibr 242 . . . . . . . . 9 (𝑛 ∈ (ℤ‘3) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → ∀𝑘 ∈ {(𝑛 + 1)} (θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))))
353352ancld 575 . . . . . . . 8 (𝑛 ∈ (ℤ‘3) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ∧ ∀𝑘 ∈ {(𝑛 + 1)} (θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)))))
354 ralun 3779 . . . . . . . . 9 ((∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ∧ ∀𝑘 ∈ {(𝑛 + 1)} (θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))) → ∀𝑘 ∈ ((3...𝑛) ∪ {(𝑛 + 1)})(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)))
355 fzsuc 12346 . . . . . . . . . 10 (𝑛 ∈ (ℤ‘3) → (3...(𝑛 + 1)) = ((3...𝑛) ∪ {(𝑛 + 1)}))
356355raleqdv 3137 . . . . . . . . 9 (𝑛 ∈ (ℤ‘3) → (∀𝑘 ∈ (3...(𝑛 + 1))(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ ∀𝑘 ∈ ((3...𝑛) ∪ {(𝑛 + 1)})(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))))
357354, 356syl5ibr 236 . . . . . . . 8 (𝑛 ∈ (ℤ‘3) → ((∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ∧ ∀𝑘 ∈ {(𝑛 + 1)} (θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))) → ∀𝑘 ∈ (3...(𝑛 + 1))(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))))
358353, 357syld 47 . . . . . . 7 (𝑛 ∈ (ℤ‘3) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → ∀𝑘 ∈ (3...(𝑛 + 1))(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))))
35966, 68, 70, 72, 74, 112, 358uzind4i 11710 . . . . . 6 ((⌊‘𝑁) ∈ (ℤ‘3) → ∀𝑘 ∈ (3...(⌊‘𝑁))(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)))
360 fveq2 6158 . . . . . . . 8 (𝑘 = (⌊‘𝑁) → (θ‘𝑘) = (θ‘(⌊‘𝑁)))
361 oveq2 6623 . . . . . . . . . 10 (𝑘 = (⌊‘𝑁) → (2 · 𝑘) = (2 · (⌊‘𝑁)))
362361oveq1d 6630 . . . . . . . . 9 (𝑘 = (⌊‘𝑁) → ((2 · 𝑘) − 3) = ((2 · (⌊‘𝑁)) − 3))
363362oveq2d 6631 . . . . . . . 8 (𝑘 = (⌊‘𝑁) → ((log‘2) · ((2 · 𝑘) − 3)) = ((log‘2) · ((2 · (⌊‘𝑁)) − 3)))
364360, 363breq12d 4636 . . . . . . 7 (𝑘 = (⌊‘𝑁) → ((θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ (θ‘(⌊‘𝑁)) < ((log‘2) · ((2 · (⌊‘𝑁)) − 3))))
365364rspcv 3295 . . . . . 6 ((⌊‘𝑁) ∈ (3...(⌊‘𝑁)) → (∀𝑘 ∈ (3...(⌊‘𝑁))(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → (θ‘(⌊‘𝑁)) < ((log‘2) · ((2 · (⌊‘𝑁)) − 3))))
36665, 359, 365sylc 65 . . . . 5 ((⌊‘𝑁) ∈ (ℤ‘3) → (θ‘(⌊‘𝑁)) < ((log‘2) · ((2 · (⌊‘𝑁)) − 3)))
36764, 366syl 17 . . . 4 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → (θ‘(⌊‘𝑁)) < ((log‘2) · ((2 · (⌊‘𝑁)) − 3)))
36860, 367eqbrtrrd 4647 . . 3 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → (θ‘𝑁) < ((log‘2) · ((2 · (⌊‘𝑁)) − 3)))
36935adantr 481 . . . . 5 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → (2 · 𝑁) ∈ ℝ)
37031a1i 11 . . . . 5 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → 3 ∈ ℝ)
371 flle 12556 . . . . . . 7 (𝑁 ∈ ℝ → (⌊‘𝑁) ≤ 𝑁)
372371ad2antrr 761 . . . . . 6 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → (⌊‘𝑁) ≤ 𝑁)
37322adantr 481 . . . . . . 7 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → 𝑁 ∈ ℝ)
37425a1i 11 . . . . . . 7 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → (2 ∈ ℝ ∧ 0 < 2))
375 lemul2 10836 . . . . . . 7 (((⌊‘𝑁) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((⌊‘𝑁) ≤ 𝑁 ↔ (2 · (⌊‘𝑁)) ≤ (2 · 𝑁)))
37650, 373, 374, 375syl3anc 1323 . . . . . 6 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → ((⌊‘𝑁) ≤ 𝑁 ↔ (2 · (⌊‘𝑁)) ≤ (2 · 𝑁)))
377372, 376mpbid 222 . . . . 5 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → (2 · (⌊‘𝑁)) ≤ (2 · 𝑁))
37852, 369, 370, 377lesub1dd 10603 . . . 4 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → ((2 · (⌊‘𝑁)) − 3) ≤ ((2 · 𝑁) − 3))
3797a1i 11 . . . . 5 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → ((log‘2) ∈ ℝ ∧ 0 < (log‘2)))
380 lemul2 10836 . . . . 5 ((((2 · (⌊‘𝑁)) − 3) ∈ ℝ ∧ ((2 · 𝑁) − 3) ∈ ℝ ∧ ((log‘2) ∈ ℝ ∧ 0 < (log‘2))) → (((2 · (⌊‘𝑁)) − 3) ≤ ((2 · 𝑁) − 3) ↔ ((log‘2) · ((2 · (⌊‘𝑁)) − 3)) ≤ ((log‘2) · ((2 · 𝑁) − 3))))
38154, 57, 379, 380syl3anc 1323 . . . 4 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → (((2 · (⌊‘𝑁)) − 3) ≤ ((2 · 𝑁) − 3) ↔ ((log‘2) · ((2 · (⌊‘𝑁)) − 3)) ≤ ((log‘2) · ((2 · 𝑁) − 3))))
382378, 381mpbid 222 . . 3 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → ((log‘2) · ((2 · (⌊‘𝑁)) − 3)) ≤ ((log‘2) · ((2 · 𝑁) − 3)))
38348, 56, 59, 368, 382ltletrd 10157 . 2 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → (θ‘𝑁) < ((log‘2) · ((2 · 𝑁) − 3)))
384117a1i 11 . . . 4 ((𝑁 ∈ ℝ ∧ 2 < 𝑁) → 2 ∈ ℤ)
385 flcl 12552 . . . . 5 (𝑁 ∈ ℝ → (⌊‘𝑁) ∈ ℤ)
386385adantr 481 . . . 4 ((𝑁 ∈ ℝ ∧ 2 < 𝑁) → (⌊‘𝑁) ∈ ℤ)
387 ltle 10086 . . . . . . 7 ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (2 < 𝑁 → 2 ≤ 𝑁))
3882, 387mpan 705 . . . . . 6 (𝑁 ∈ ℝ → (2 < 𝑁 → 2 ≤ 𝑁))
389 flge 12562 . . . . . . 7 ((𝑁 ∈ ℝ ∧ 2 ∈ ℤ) → (2 ≤ 𝑁 ↔ 2 ≤ (⌊‘𝑁)))
390117, 389mpan2 706 . . . . . 6 (𝑁 ∈ ℝ → (2 ≤ 𝑁 ↔ 2 ≤ (⌊‘𝑁)))
391388, 390sylibd 229 . . . . 5 (𝑁 ∈ ℝ → (2 < 𝑁 → 2 ≤ (⌊‘𝑁)))
392391imp 445 . . . 4 ((𝑁 ∈ ℝ ∧ 2 < 𝑁) → 2 ≤ (⌊‘𝑁))
393 eluz2 11653 . . . 4 ((⌊‘𝑁) ∈ (ℤ‘2) ↔ (2 ∈ ℤ ∧ (⌊‘𝑁) ∈ ℤ ∧ 2 ≤ (⌊‘𝑁)))
394384, 386, 392, 393syl3anbrc 1244 . . 3 ((𝑁 ∈ ℝ ∧ 2 < 𝑁) → (⌊‘𝑁) ∈ (ℤ‘2))
395 uzp1 11681 . . 3 ((⌊‘𝑁) ∈ (ℤ‘2) → ((⌊‘𝑁) = 2 ∨ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))))
396394, 395syl 17 . 2 ((𝑁 ∈ ℝ ∧ 2 < 𝑁) → ((⌊‘𝑁) = 2 ∨ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))))
39746, 383, 396mpjaodan 826 1 ((𝑁 ∈ ℝ ∧ 2 < 𝑁) → (θ‘𝑁) < ((log‘2) · ((2 · 𝑁) − 3)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384   = wceq 1480  wcel 1987  wne 2790  wral 2908  cun 3558  {csn 4155   class class class wbr 4623  cfv 5857  (class class class)co 6615  cc 9894  cr 9895  0cc0 9896  1c1 9897   + caddc 9899   · cmul 9901   < clt 10034  cle 10035  cmin 10226   / cdiv 10644  cn 10980  2c2 11030  3c3 11031  4c4 11032  6c6 11034  8c8 11036  cz 11337  cuz 11647  +crp 11792  ...cfz 12284  cfl 12547  cexp 12816  cdvds 14926  cprime 15328  logclog 24239  θccht 24751
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-inf2 8498  ax-cnex 9952  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-mulcom 9960  ax-addass 9961  ax-mulass 9962  ax-distr 9963  ax-i2m1 9964  ax-1ne0 9965  ax-1rid 9966  ax-rnegex 9967  ax-rrecex 9968  ax-cnre 9969  ax-pre-lttri 9970  ax-pre-lttrn 9971  ax-pre-ltadd 9972  ax-pre-mulgt0 9973  ax-pre-sup 9974  ax-addf 9975  ax-mulf 9976
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-int 4448  df-iun 4494  df-iin 4495  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-se 5044  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-isom 5866  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-of 6862  df-om 7028  df-1st 7128  df-2nd 7129  df-supp 7256  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-1o 7520  df-2o 7521  df-oadd 7524  df-er 7702  df-map 7819  df-pm 7820  df-ixp 7869  df-en 7916  df-dom 7917  df-sdom 7918  df-fin 7919  df-fsupp 8236  df-fi 8277  df-sup 8308  df-inf 8309  df-oi 8375  df-card 8725  df-cda 8950  df-pnf 10036  df-mnf 10037  df-xr 10038  df-ltxr 10039  df-le 10040  df-sub 10228  df-neg 10229  df-div 10645  df-nn 10981  df-2 11039  df-3 11040  df-4 11041  df-5 11042  df-6 11043  df-7 11044  df-8 11045  df-9 11046  df-n0 11253  df-z 11338  df-dec 11454  df-uz 11648  df-q 11749  df-rp 11793  df-xneg 11906  df-xadd 11907  df-xmul 11908  df-ioo 12137  df-ioc 12138  df-ico 12139  df-icc 12140  df-fz 12285  df-fzo 12423  df-fl 12549  df-mod 12625  df-seq 12758  df-exp 12817  df-fac 13017  df-bc 13046  df-hash 13074  df-shft 13757  df-cj 13789  df-re 13790  df-im 13791  df-sqrt 13925  df-abs 13926  df-limsup 14152  df-clim 14169  df-rlim 14170  df-sum 14367  df-ef 14742  df-sin 14744  df-cos 14745  df-pi 14747  df-dvds 14927  df-gcd 15160  df-prm 15329  df-pc 15485  df-struct 15802  df-ndx 15803  df-slot 15804  df-base 15805  df-sets 15806  df-ress 15807  df-plusg 15894  df-mulr 15895  df-starv 15896  df-sca 15897  df-vsca 15898  df-ip 15899  df-tset 15900  df-ple 15901  df-ds 15904  df-unif 15905  df-hom 15906  df-cco 15907  df-rest 16023  df-topn 16024  df-0g 16042  df-gsum 16043  df-topgen 16044  df-pt 16045  df-prds 16048  df-xrs 16102  df-qtop 16107  df-imas 16108  df-xps 16110  df-mre 16186  df-mrc 16187  df-acs 16189  df-mgm 17182  df-sgrp 17224  df-mnd 17235  df-submnd 17276  df-mulg 17481  df-cntz 17690  df-cmn 18135  df-psmet 19678  df-xmet 19679  df-met 19680  df-bl 19681  df-mopn 19682  df-fbas 19683  df-fg 19684  df-cnfld 19687  df-top 20639  df-topon 20656  df-topsp 20677  df-bases 20690  df-cld 20763  df-ntr 20764  df-cls 20765  df-nei 20842  df-lp 20880  df-perf 20881  df-cn 20971  df-cnp 20972  df-haus 21059  df-tx 21305  df-hmeo 21498  df-fil 21590  df-fm 21682  df-flim 21683  df-flf 21684  df-xms 22065  df-ms 22066  df-tms 22067  df-cncf 22621  df-limc 23570  df-dv 23571  df-log 24241  df-cht 24757
This theorem is referenced by:  bposlem6  24948  chto1ub  25099
  Copyright terms: Public domain W3C validator