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

Theorem chtub 24651
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 6085 . . . . 5 ((⌊‘𝑁) = 2 → (θ‘(⌊‘𝑁)) = (θ‘2))
2 2re 10934 . . . . . . . . . . 11 2 ∈ ℝ
3 1lt2 11038 . . . . . . . . . . 11 1 < 2
4 rplogcl 24068 . . . . . . . . . . 11 ((2 ∈ ℝ ∧ 1 < 2) → (log‘2) ∈ ℝ+)
52, 3, 4mp2an 703 . . . . . . . . . 10 (log‘2) ∈ ℝ+
6 elrp 11663 . . . . . . . . . 10 ((log‘2) ∈ ℝ+ ↔ ((log‘2) ∈ ℝ ∧ 0 < (log‘2)))
75, 6mpbi 218 . . . . . . . . 9 ((log‘2) ∈ ℝ ∧ 0 < (log‘2))
87simpli 472 . . . . . . . 8 (log‘2) ∈ ℝ
98recni 9905 . . . . . . 7 (log‘2) ∈ ℂ
109mulid1i 9895 . . . . . 6 ((log‘2) · 1) = (log‘2)
11 cht2 24612 . . . . . 6 (θ‘2) = (log‘2)
1210, 11eqtr4i 2631 . . . . 5 ((log‘2) · 1) = (θ‘2)
131, 12syl6reqr 2659 . . . 4 ((⌊‘𝑁) = 2 → ((log‘2) · 1) = (θ‘(⌊‘𝑁)))
14 chtfl 24589 . . . . 5 (𝑁 ∈ ℝ → (θ‘(⌊‘𝑁)) = (θ‘𝑁))
1514adantr 479 . . . 4 ((𝑁 ∈ ℝ ∧ 2 < 𝑁) → (θ‘(⌊‘𝑁)) = (θ‘𝑁))
1613, 15sylan9eqr 2662 . . 3 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → ((log‘2) · 1) = (θ‘𝑁))
17 2t2e4 11021 . . . . . . 7 (2 · 2) = 4
18 df-4 10925 . . . . . . 7 4 = (3 + 1)
1917, 18eqtri 2628 . . . . . 6 (2 · 2) = (3 + 1)
20 simplr 787 . . . . . . 7 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → 2 < 𝑁)
212a1i 11 . . . . . . . 8 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → 2 ∈ ℝ)
22 simpl 471 . . . . . . . . 9 ((𝑁 ∈ ℝ ∧ 2 < 𝑁) → 𝑁 ∈ ℝ)
2322adantr 479 . . . . . . . 8 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → 𝑁 ∈ ℝ)
24 2pos 10956 . . . . . . . . . 10 0 < 2
252, 24pm3.2i 469 . . . . . . . . 9 (2 ∈ ℝ ∧ 0 < 2)
2625a1i 11 . . . . . . . 8 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → (2 ∈ ℝ ∧ 0 < 2))
27 ltmul2 10720 . . . . . . . 8 ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (2 < 𝑁 ↔ (2 · 2) < (2 · 𝑁)))
2821, 23, 26, 27syl3anc 1317 . . . . . . 7 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → (2 < 𝑁 ↔ (2 · 2) < (2 · 𝑁)))
2920, 28mpbid 220 . . . . . 6 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → (2 · 2) < (2 · 𝑁))
3019, 29syl5eqbrr 4610 . . . . 5 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → (3 + 1) < (2 · 𝑁))
31 3re 10938 . . . . . . 7 3 ∈ ℝ
3231a1i 11 . . . . . 6 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → 3 ∈ ℝ)
33 1red 9908 . . . . . 6 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → 1 ∈ ℝ)
34 remulcl 9874 . . . . . . . 8 ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (2 · 𝑁) ∈ ℝ)
352, 22, 34sylancr 693 . . . . . . 7 ((𝑁 ∈ ℝ ∧ 2 < 𝑁) → (2 · 𝑁) ∈ ℝ)
3635adantr 479 . . . . . 6 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → (2 · 𝑁) ∈ ℝ)
3732, 33, 36ltaddsub2d 10474 . . . . 5 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → ((3 + 1) < (2 · 𝑁) ↔ 1 < ((2 · 𝑁) − 3)))
3830, 37mpbid 220 . . . 4 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → 1 < ((2 · 𝑁) − 3))
39 resubcl 10193 . . . . . . 7 (((2 · 𝑁) ∈ ℝ ∧ 3 ∈ ℝ) → ((2 · 𝑁) − 3) ∈ ℝ)
4035, 31, 39sylancl 692 . . . . . 6 ((𝑁 ∈ ℝ ∧ 2 < 𝑁) → ((2 · 𝑁) − 3) ∈ ℝ)
4140adantr 479 . . . . 5 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → ((2 · 𝑁) − 3) ∈ ℝ)
427a1i 11 . . . . 5 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → ((log‘2) ∈ ℝ ∧ 0 < (log‘2)))
43 ltmul2 10720 . . . . 5 ((1 ∈ ℝ ∧ ((2 · 𝑁) − 3) ∈ ℝ ∧ ((log‘2) ∈ ℝ ∧ 0 < (log‘2))) → (1 < ((2 · 𝑁) − 3) ↔ ((log‘2) · 1) < ((log‘2) · ((2 · 𝑁) − 3))))
4433, 41, 42, 43syl3anc 1317 . . . 4 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → (1 < ((2 · 𝑁) − 3) ↔ ((log‘2) · 1) < ((log‘2) · ((2 · 𝑁) − 3))))
4538, 44mpbid 220 . . 3 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → ((log‘2) · 1) < ((log‘2) · ((2 · 𝑁) − 3)))
4616, 45eqbrtrrd 4598 . 2 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) = 2) → (θ‘𝑁) < ((log‘2) · ((2 · 𝑁) − 3)))
47 chtcl 24549 . . . 4 (𝑁 ∈ ℝ → (θ‘𝑁) ∈ ℝ)
4847ad2antrr 757 . . 3 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → (θ‘𝑁) ∈ ℝ)
49 reflcl 12411 . . . . . . 7 (𝑁 ∈ ℝ → (⌊‘𝑁) ∈ ℝ)
5049ad2antrr 757 . . . . . 6 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → (⌊‘𝑁) ∈ ℝ)
51 remulcl 9874 . . . . . 6 ((2 ∈ ℝ ∧ (⌊‘𝑁) ∈ ℝ) → (2 · (⌊‘𝑁)) ∈ ℝ)
522, 50, 51sylancr 693 . . . . 5 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → (2 · (⌊‘𝑁)) ∈ ℝ)
53 resubcl 10193 . . . . 5 (((2 · (⌊‘𝑁)) ∈ ℝ ∧ 3 ∈ ℝ) → ((2 · (⌊‘𝑁)) − 3) ∈ ℝ)
5452, 31, 53sylancl 692 . . . 4 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → ((2 · (⌊‘𝑁)) − 3) ∈ ℝ)
55 remulcl 9874 . . . 4 (((log‘2) ∈ ℝ ∧ ((2 · (⌊‘𝑁)) − 3) ∈ ℝ) → ((log‘2) · ((2 · (⌊‘𝑁)) − 3)) ∈ ℝ)
568, 54, 55sylancr 693 . . 3 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → ((log‘2) · ((2 · (⌊‘𝑁)) − 3)) ∈ ℝ)
5740adantr 479 . . . 4 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → ((2 · 𝑁) − 3) ∈ ℝ)
58 remulcl 9874 . . . 4 (((log‘2) ∈ ℝ ∧ ((2 · 𝑁) − 3) ∈ ℝ) → ((log‘2) · ((2 · 𝑁) − 3)) ∈ ℝ)
598, 57, 58sylancr 693 . . 3 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → ((log‘2) · ((2 · 𝑁) − 3)) ∈ ℝ)
6015adantr 479 . . . 4 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → (θ‘(⌊‘𝑁)) = (θ‘𝑁))
61 simpr 475 . . . . . 6 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → (⌊‘𝑁) ∈ (ℤ‘(2 + 1)))
62 df-3 10924 . . . . . . 7 3 = (2 + 1)
6362fveq2i 6088 . . . . . 6 (ℤ‘3) = (ℤ‘(2 + 1))
6461, 63syl6eleqr 2695 . . . . 5 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → (⌊‘𝑁) ∈ (ℤ‘3))
65 eluzfz2 12172 . . . . . 6 ((⌊‘𝑁) ∈ (ℤ‘3) → (⌊‘𝑁) ∈ (3...(⌊‘𝑁)))
66 3z 11240 . . . . . . 7 3 ∈ ℤ
67 oveq2 6532 . . . . . . . 8 (𝑥 = 3 → (3...𝑥) = (3...3))
6867raleqdv 3117 . . . . . . 7 (𝑥 = 3 → (∀𝑘 ∈ (3...𝑥)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ ∀𝑘 ∈ (3...3)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))))
69 oveq2 6532 . . . . . . . 8 (𝑥 = 𝑛 → (3...𝑥) = (3...𝑛))
7069raleqdv 3117 . . . . . . 7 (𝑥 = 𝑛 → (∀𝑘 ∈ (3...𝑥)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ ∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))))
71 oveq2 6532 . . . . . . . 8 (𝑥 = (𝑛 + 1) → (3...𝑥) = (3...(𝑛 + 1)))
7271raleqdv 3117 . . . . . . 7 (𝑥 = (𝑛 + 1) → (∀𝑘 ∈ (3...𝑥)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ ∀𝑘 ∈ (3...(𝑛 + 1))(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))))
73 oveq2 6532 . . . . . . . 8 (𝑥 = (⌊‘𝑁) → (3...𝑥) = (3...(⌊‘𝑁)))
7473raleqdv 3117 . . . . . . 7 (𝑥 = (⌊‘𝑁) → (∀𝑘 ∈ (3...𝑥)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ ∀𝑘 ∈ (3...(⌊‘𝑁))(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))))
75 6lt8 11060 . . . . . . . . . . 11 6 < 8
76 6re 10945 . . . . . . . . . . . . 13 6 ∈ ℝ
77 6pos 10963 . . . . . . . . . . . . 13 0 < 6
7876, 77elrpii 11664 . . . . . . . . . . . 12 6 ∈ ℝ+
79 8re 10949 . . . . . . . . . . . . 13 8 ∈ ℝ
80 8pos 10965 . . . . . . . . . . . . 13 0 < 8
8179, 80elrpii 11664 . . . . . . . . . . . 12 8 ∈ ℝ+
82 logltb 24064 . . . . . . . . . . . 12 ((6 ∈ ℝ+ ∧ 8 ∈ ℝ+) → (6 < 8 ↔ (log‘6) < (log‘8)))
8378, 81, 82mp2an 703 . . . . . . . . . . 11 (6 < 8 ↔ (log‘6) < (log‘8))
8475, 83mpbi 218 . . . . . . . . . 10 (log‘6) < (log‘8)
8584a1i 11 . . . . . . . . 9 (𝑘 ∈ (3...3) → (log‘6) < (log‘8))
86 elfz1eq 12175 . . . . . . . . . . 11 (𝑘 ∈ (3...3) → 𝑘 = 3)
8786fveq2d 6089 . . . . . . . . . 10 (𝑘 ∈ (3...3) → (θ‘𝑘) = (θ‘3))
88 cht3 24613 . . . . . . . . . 10 (θ‘3) = (log‘6)
8987, 88syl6eq 2656 . . . . . . . . 9 (𝑘 ∈ (3...3) → (θ‘𝑘) = (log‘6))
9086oveq2d 6540 . . . . . . . . . . . . 13 (𝑘 ∈ (3...3) → (2 · 𝑘) = (2 · 3))
9190oveq1d 6539 . . . . . . . . . . . 12 (𝑘 ∈ (3...3) → ((2 · 𝑘) − 3) = ((2 · 3) − 3))
92 3cn 10939 . . . . . . . . . . . . . . 15 3 ∈ ℂ
93922timesi 10991 . . . . . . . . . . . . . 14 (2 · 3) = (3 + 3)
9493oveq1i 6534 . . . . . . . . . . . . 13 ((2 · 3) − 3) = ((3 + 3) − 3)
9592, 92pncan3oi 10145 . . . . . . . . . . . . 13 ((3 + 3) − 3) = 3
9694, 95eqtri 2628 . . . . . . . . . . . 12 ((2 · 3) − 3) = 3
9791, 96syl6eq 2656 . . . . . . . . . . 11 (𝑘 ∈ (3...3) → ((2 · 𝑘) − 3) = 3)
9897oveq2d 6540 . . . . . . . . . 10 (𝑘 ∈ (3...3) → ((log‘2) · ((2 · 𝑘) − 3)) = ((log‘2) · 3))
99 2rp 11666 . . . . . . . . . . . . . . 15 2 ∈ ℝ+
100 relogcl 24040 . . . . . . . . . . . . . . 15 (2 ∈ ℝ+ → (log‘2) ∈ ℝ)
10199, 100ax-mp 5 . . . . . . . . . . . . . 14 (log‘2) ∈ ℝ
102101recni 9905 . . . . . . . . . . . . 13 (log‘2) ∈ ℂ
103102, 92mulcomi 9899 . . . . . . . . . . . 12 ((log‘2) · 3) = (3 · (log‘2))
104 relogexp 24060 . . . . . . . . . . . . 13 ((2 ∈ ℝ+ ∧ 3 ∈ ℤ) → (log‘(2↑3)) = (3 · (log‘2)))
10599, 66, 104mp2an 703 . . . . . . . . . . . 12 (log‘(2↑3)) = (3 · (log‘2))
106103, 105eqtr4i 2631 . . . . . . . . . . 11 ((log‘2) · 3) = (log‘(2↑3))
107 cu2 12777 . . . . . . . . . . . 12 (2↑3) = 8
108107fveq2i 6088 . . . . . . . . . . 11 (log‘(2↑3)) = (log‘8)
109106, 108eqtri 2628 . . . . . . . . . 10 ((log‘2) · 3) = (log‘8)
11098, 109syl6eq 2656 . . . . . . . . 9 (𝑘 ∈ (3...3) → ((log‘2) · ((2 · 𝑘) − 3)) = (log‘8))
11185, 89, 1103brtr4d 4606 . . . . . . . 8 (𝑘 ∈ (3...3) → (θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)))
112111rgen 2902 . . . . . . 7 𝑘 ∈ (3...3)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))
113 df-2 10923 . . . . . . . . . . . . . . . . . 18 2 = (1 + 1)
114 2div2e1 10994 . . . . . . . . . . . . . . . . . . . 20 (2 / 2) = 1
115 eluzle 11529 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (ℤ‘3) → 3 ≤ 𝑛)
11662, 115syl5eqbrr 4610 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (ℤ‘3) → (2 + 1) ≤ 𝑛)
117 2z 11239 . . . . . . . . . . . . . . . . . . . . . . 23 2 ∈ ℤ
118 eluzelz 11526 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (ℤ‘3) → 𝑛 ∈ ℤ)
119 zltp1le 11257 . . . . . . . . . . . . . . . . . . . . . . 23 ((2 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (2 < 𝑛 ↔ (2 + 1) ≤ 𝑛))
120117, 118, 119sylancr 693 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (ℤ‘3) → (2 < 𝑛 ↔ (2 + 1) ≤ 𝑛))
121116, 120mpbird 245 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (ℤ‘3) → 2 < 𝑛)
122 eluzelre 11527 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (ℤ‘3) → 𝑛 ∈ ℝ)
123 ltdiv1 10733 . . . . . . . . . . . . . . . . . . . . . . 23 ((2 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (2 < 𝑛 ↔ (2 / 2) < (𝑛 / 2)))
1242, 25, 123mp3an13 1406 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ ℝ → (2 < 𝑛 ↔ (2 / 2) < (𝑛 / 2)))
125122, 124syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (ℤ‘3) → (2 < 𝑛 ↔ (2 / 2) < (𝑛 / 2)))
126121, 125mpbid 220 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (ℤ‘3) → (2 / 2) < (𝑛 / 2))
127114, 126syl5eqbrr 4610 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (ℤ‘3) → 1 < (𝑛 / 2))
128122rehalfcld 11123 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (ℤ‘3) → (𝑛 / 2) ∈ ℝ)
129 1re 9892 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℝ
130 ltadd1 10341 . . . . . . . . . . . . . . . . . . . . 21 ((1 ∈ ℝ ∧ (𝑛 / 2) ∈ ℝ ∧ 1 ∈ ℝ) → (1 < (𝑛 / 2) ↔ (1 + 1) < ((𝑛 / 2) + 1)))
131129, 129, 130mp3an13 1406 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 / 2) ∈ ℝ → (1 < (𝑛 / 2) ↔ (1 + 1) < ((𝑛 / 2) + 1)))
132128, 131syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (ℤ‘3) → (1 < (𝑛 / 2) ↔ (1 + 1) < ((𝑛 / 2) + 1)))
133127, 132mpbid 220 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (ℤ‘3) → (1 + 1) < ((𝑛 / 2) + 1))
134113, 133syl5eqbr 4609 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (ℤ‘3) → 2 < ((𝑛 / 2) + 1))
135134adantr 479 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → 2 < ((𝑛 / 2) + 1))
136 peano2z 11248 . . . . . . . . . . . . . . . . . 18 ((𝑛 / 2) ∈ ℤ → ((𝑛 / 2) + 1) ∈ ℤ)
137136adantl 480 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ∈ ℤ)
138 zltp1le 11257 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℤ ∧ ((𝑛 / 2) + 1) ∈ ℤ) → (2 < ((𝑛 / 2) + 1) ↔ (2 + 1) ≤ ((𝑛 / 2) + 1)))
139117, 137, 138sylancr 693 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 < ((𝑛 / 2) + 1) ↔ (2 + 1) ≤ ((𝑛 / 2) + 1)))
140135, 139mpbid 220 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 + 1) ≤ ((𝑛 / 2) + 1))
14162, 140syl5eqbr 4609 . . . . . . . . . . . . . 14 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → 3 ≤ ((𝑛 / 2) + 1))
142 1red 9908 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (ℤ‘3) → 1 ∈ ℝ)
143 ltle 9974 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℝ ∧ (𝑛 / 2) ∈ ℝ) → (1 < (𝑛 / 2) → 1 ≤ (𝑛 / 2)))
144129, 128, 143sylancr 693 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (ℤ‘3) → (1 < (𝑛 / 2) → 1 ≤ (𝑛 / 2)))
145127, 144mpd 15 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (ℤ‘3) → 1 ≤ (𝑛 / 2))
146142, 128, 128, 145leadd2dd 10488 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ℤ‘3) → ((𝑛 / 2) + 1) ≤ ((𝑛 / 2) + (𝑛 / 2)))
147122recnd 9921 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (ℤ‘3) → 𝑛 ∈ ℂ)
1481472halvesd 11122 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ℤ‘3) → ((𝑛 / 2) + (𝑛 / 2)) = 𝑛)
149146, 148breqtrd 4600 . . . . . . . . . . . . . . 15 (𝑛 ∈ (ℤ‘3) → ((𝑛 / 2) + 1) ≤ 𝑛)
150149adantr 479 . . . . . . . . . . . . . 14 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ≤ 𝑛)
151 elfz 12155 . . . . . . . . . . . . . . . 16 ((((𝑛 / 2) + 1) ∈ ℤ ∧ 3 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝑛 / 2) + 1) ∈ (3...𝑛) ↔ (3 ≤ ((𝑛 / 2) + 1) ∧ ((𝑛 / 2) + 1) ≤ 𝑛)))
15266, 151mp3an2 1403 . . . . . . . . . . . . . . 15 ((((𝑛 / 2) + 1) ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝑛 / 2) + 1) ∈ (3...𝑛) ↔ (3 ≤ ((𝑛 / 2) + 1) ∧ ((𝑛 / 2) + 1) ≤ 𝑛)))
153136, 118, 152syl2anr 493 . . . . . . . . . . . . . 14 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (((𝑛 / 2) + 1) ∈ (3...𝑛) ↔ (3 ≤ ((𝑛 / 2) + 1) ∧ ((𝑛 / 2) + 1) ≤ 𝑛)))
154141, 150, 153mpbir2and 958 . . . . . . . . . . . . 13 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ∈ (3...𝑛))
155 fveq2 6085 . . . . . . . . . . . . . . 15 (𝑘 = ((𝑛 / 2) + 1) → (θ‘𝑘) = (θ‘((𝑛 / 2) + 1)))
156 oveq2 6532 . . . . . . . . . . . . . . . . 17 (𝑘 = ((𝑛 / 2) + 1) → (2 · 𝑘) = (2 · ((𝑛 / 2) + 1)))
157156oveq1d 6539 . . . . . . . . . . . . . . . 16 (𝑘 = ((𝑛 / 2) + 1) → ((2 · 𝑘) − 3) = ((2 · ((𝑛 / 2) + 1)) − 3))
158157oveq2d 6540 . . . . . . . . . . . . . . 15 (𝑘 = ((𝑛 / 2) + 1) → ((log‘2) · ((2 · 𝑘) − 3)) = ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3)))
159155, 158breq12d 4587 . . . . . . . . . . . . . 14 (𝑘 = ((𝑛 / 2) + 1) → ((θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ (θ‘((𝑛 / 2) + 1)) < ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3))))
160159rspcv 3274 . . . . . . . . . . . . 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 9921 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (ℤ‘3) → (𝑛 / 2) ∈ ℂ)
163162adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (𝑛 / 2) ∈ ℂ)
164 2cn 10935 . . . . . . . . . . . . . . . . . . . . 21 2 ∈ ℂ
165 ax-1cn 9847 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℂ
166 adddi 9878 . . . . . . . . . . . . . . . . . . . . 21 ((2 ∈ ℂ ∧ (𝑛 / 2) ∈ ℂ ∧ 1 ∈ ℂ) → (2 · ((𝑛 / 2) + 1)) = ((2 · (𝑛 / 2)) + (2 · 1)))
167164, 165, 166mp3an13 1406 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 / 2) ∈ ℂ → (2 · ((𝑛 / 2) + 1)) = ((2 · (𝑛 / 2)) + (2 · 1)))
168163, 167syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 · ((𝑛 / 2) + 1)) = ((2 · (𝑛 / 2)) + (2 · 1)))
169147adantr 479 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → 𝑛 ∈ ℂ)
170 2ne0 10957 . . . . . . . . . . . . . . . . . . . . . 22 2 ≠ 0
171 divcan2 10539 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (2 · (𝑛 / 2)) = 𝑛)
172164, 170, 171mp3an23 1407 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ℂ → (2 · (𝑛 / 2)) = 𝑛)
173169, 172syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 · (𝑛 / 2)) = 𝑛)
174164mulid1i 9895 . . . . . . . . . . . . . . . . . . . . 21 (2 · 1) = 2
175174a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 · 1) = 2)
176173, 175oveq12d 6542 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · (𝑛 / 2)) + (2 · 1)) = (𝑛 + 2))
177168, 176eqtrd 2640 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 · ((𝑛 / 2) + 1)) = (𝑛 + 2))
178177oveq1d 6539 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · ((𝑛 / 2) + 1)) − 3) = ((𝑛 + 2) − 3))
179 2p1e3 10995 . . . . . . . . . . . . . . . . . . . 20 (2 + 1) = 3
18092, 164, 165, 179subaddrii 10218 . . . . . . . . . . . . . . . . . . 19 (3 − 2) = 1
181180oveq2i 6535 . . . . . . . . . . . . . . . . . 18 (𝑛 − (3 − 2)) = (𝑛 − 1)
182 subsub3 10161 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℂ ∧ 3 ∈ ℂ ∧ 2 ∈ ℂ) → (𝑛 − (3 − 2)) = ((𝑛 + 2) − 3))
18392, 164, 182mp3an23 1407 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℂ → (𝑛 − (3 − 2)) = ((𝑛 + 2) − 3))
184169, 183syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (𝑛 − (3 − 2)) = ((𝑛 + 2) − 3))
185181, 184syl5reqr 2655 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 + 2) − 3) = (𝑛 − 1))
186178, 185eqtrd 2640 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · ((𝑛 / 2) + 1)) − 3) = (𝑛 − 1))
187186oveq2d 6540 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3)) = ((log‘2) · (𝑛 − 1)))
188187breq2d 4586 . . . . . . . . . . . . . 14 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((θ‘((𝑛 / 2) + 1)) < ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3)) ↔ (θ‘((𝑛 / 2) + 1)) < ((log‘2) · (𝑛 − 1))))
189137zred 11311 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ∈ ℝ)
190 chtcl 24549 . . . . . . . . . . . . . . . 16 (((𝑛 / 2) + 1) ∈ ℝ → (θ‘((𝑛 / 2) + 1)) ∈ ℝ)
191189, 190syl 17 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (θ‘((𝑛 / 2) + 1)) ∈ ℝ)
192122adantr 479 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → 𝑛 ∈ ℝ)
193 peano2rem 10196 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℝ → (𝑛 − 1) ∈ ℝ)
194192, 193syl 17 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (𝑛 − 1) ∈ ℝ)
195 remulcl 9874 . . . . . . . . . . . . . . . 16 (((log‘2) ∈ ℝ ∧ (𝑛 − 1) ∈ ℝ) → ((log‘2) · (𝑛 − 1)) ∈ ℝ)
196101, 194, 195sylancr 693 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2) · (𝑛 − 1)) ∈ ℝ)
197 remulcl 9874 . . . . . . . . . . . . . . . 16 (((log‘2) ∈ ℝ ∧ 𝑛 ∈ ℝ) → ((log‘2) · 𝑛) ∈ ℝ)
198101, 192, 197sylancr 693 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2) · 𝑛) ∈ ℝ)
199191, 196, 198ltadd1d 10466 . . . . . . . . . . . . . 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 9921 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (𝑛 − 1) ∈ ℂ)
202200, 201, 169adddid 9917 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2) · ((𝑛 − 1) + 𝑛)) = (((log‘2) · (𝑛 − 1)) + ((log‘2) · 𝑛)))
203 adddi 9878 . . . . . . . . . . . . . . . . . . . . . 22 ((2 ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → (2 · (𝑛 + 1)) = ((2 · 𝑛) + (2 · 1)))
204164, 165, 203mp3an13 1406 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ℂ → (2 · (𝑛 + 1)) = ((2 · 𝑛) + (2 · 1)))
205169, 204syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 · (𝑛 + 1)) = ((2 · 𝑛) + (2 · 1)))
206174oveq2i 6535 . . . . . . . . . . . . . . . . . . . 20 ((2 · 𝑛) + (2 · 1)) = ((2 · 𝑛) + 2)
207205, 206syl6eq 2656 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 · (𝑛 + 1)) = ((2 · 𝑛) + 2))
208207oveq1d 6539 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · (𝑛 + 1)) − 3) = (((2 · 𝑛) + 2) − 3))
209 zmulcl 11256 . . . . . . . . . . . . . . . . . . . . . 22 ((2 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (2 · 𝑛) ∈ ℤ)
210117, 118, 209sylancr 693 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (ℤ‘3) → (2 · 𝑛) ∈ ℤ)
211210zcnd 11312 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (ℤ‘3) → (2 · 𝑛) ∈ ℂ)
212211adantr 479 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 · 𝑛) ∈ ℂ)
213 subsub3 10161 . . . . . . . . . . . . . . . . . . . 20 (((2 · 𝑛) ∈ ℂ ∧ 3 ∈ ℂ ∧ 2 ∈ ℂ) → ((2 · 𝑛) − (3 − 2)) = (((2 · 𝑛) + 2) − 3))
21492, 164, 213mp3an23 1407 . . . . . . . . . . . . . . . . . . 19 ((2 · 𝑛) ∈ ℂ → ((2 · 𝑛) − (3 − 2)) = (((2 · 𝑛) + 2) − 3))
215212, 214syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · 𝑛) − (3 − 2)) = (((2 · 𝑛) + 2) − 3))
216180oveq2i 6535 . . . . . . . . . . . . . . . . . . 19 ((2 · 𝑛) − (3 − 2)) = ((2 · 𝑛) − 1)
2171692timesd 11119 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (2 · 𝑛) = (𝑛 + 𝑛))
218217oveq1d 6539 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · 𝑛) − 1) = ((𝑛 + 𝑛) − 1))
219165a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → 1 ∈ ℂ)
220169, 169, 219addsubd 10261 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 + 𝑛) − 1) = ((𝑛 − 1) + 𝑛))
221218, 220eqtrd 2640 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · 𝑛) − 1) = ((𝑛 − 1) + 𝑛))
222216, 221syl5eq 2652 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · 𝑛) − (3 − 2)) = ((𝑛 − 1) + 𝑛))
223208, 215, 2223eqtr2rd 2647 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 − 1) + 𝑛) = ((2 · (𝑛 + 1)) − 3))
224223oveq2d 6540 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2) · ((𝑛 − 1) + 𝑛)) = ((log‘2) · ((2 · (𝑛 + 1)) − 3)))
225202, 224eqtr3d 2642 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (((log‘2) · (𝑛 − 1)) + ((log‘2) · 𝑛)) = ((log‘2) · ((2 · (𝑛 + 1)) − 3)))
226225breq2d 4586 . . . . . . . . . . . . . 14 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) < (((log‘2) · (𝑛 − 1)) + ((log‘2) · 𝑛)) ↔ ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
227188, 199, 2263bitrd 292 . . . . . . . . . . . . 13 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((θ‘((𝑛 / 2) + 1)) < ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3)) ↔ ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
228 3nn 11030 . . . . . . . . . . . . . . . . 17 3 ∈ ℕ
229 elfzuz 12161 . . . . . . . . . . . . . . . . . 18 (((𝑛 / 2) + 1) ∈ (3...𝑛) → ((𝑛 / 2) + 1) ∈ (ℤ‘3))
230154, 229syl 17 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ∈ (ℤ‘3))
231 eluznn 11587 . . . . . . . . . . . . . . . . 17 ((3 ∈ ℕ ∧ ((𝑛 / 2) + 1) ∈ (ℤ‘3)) → ((𝑛 / 2) + 1) ∈ ℕ)
232228, 230, 231sylancr 693 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 / 2) + 1) ∈ ℕ)
233 chtublem 24650 . . . . . . . . . . . . . . . 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 6539 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · ((𝑛 / 2) + 1)) − 1) = ((𝑛 + 2) − 1))
236 addsubass 10139 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 2) − 1) = (𝑛 + (2 − 1)))
237164, 165, 236mp3an23 1407 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℂ → ((𝑛 + 2) − 1) = (𝑛 + (2 − 1)))
238169, 237syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 + 2) − 1) = (𝑛 + (2 − 1)))
239 2m1e1 10979 . . . . . . . . . . . . . . . . . . 19 (2 − 1) = 1
240239oveq2i 6535 . . . . . . . . . . . . . . . . . 18 (𝑛 + (2 − 1)) = (𝑛 + 1)
241238, 240syl6eq 2656 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((𝑛 + 2) − 1) = (𝑛 + 1))
242235, 241eqtrd 2640 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · ((𝑛 / 2) + 1)) − 1) = (𝑛 + 1))
243242fveq2d 6089 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (θ‘((2 · ((𝑛 / 2) + 1)) − 1)) = (θ‘(𝑛 + 1)))
244 pncan 10135 . . . . . . . . . . . . . . . . . . 19 (((𝑛 / 2) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑛 / 2) + 1) − 1) = (𝑛 / 2))
245163, 165, 244sylancl 692 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (((𝑛 / 2) + 1) − 1) = (𝑛 / 2))
246245oveq2d 6540 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘4) · (((𝑛 / 2) + 1) − 1)) = ((log‘4) · (𝑛 / 2)))
247 relogexp 24060 . . . . . . . . . . . . . . . . . . . . 21 ((2 ∈ ℝ+ ∧ 2 ∈ ℤ) → (log‘(2↑2)) = (2 · (log‘2)))
24899, 117, 247mp2an 703 . . . . . . . . . . . . . . . . . . . 20 (log‘(2↑2)) = (2 · (log‘2))
249 sq2 12774 . . . . . . . . . . . . . . . . . . . . 21 (2↑2) = 4
250249fveq2i 6088 . . . . . . . . . . . . . . . . . . . 20 (log‘(2↑2)) = (log‘4)
251164, 102mulcomi 9899 . . . . . . . . . . . . . . . . . . . 20 (2 · (log‘2)) = ((log‘2) · 2)
252248, 250, 2513eqtr3i 2636 . . . . . . . . . . . . . . . . . . 19 (log‘4) = ((log‘2) · 2)
253252oveq1i 6534 . . . . . . . . . . . . . . . . . 18 ((log‘4) · (𝑛 / 2)) = (((log‘2) · 2) · (𝑛 / 2))
254164a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → 2 ∈ ℂ)
255200, 254, 163mulassd 9916 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (((log‘2) · 2) · (𝑛 / 2)) = ((log‘2) · (2 · (𝑛 / 2))))
256253, 255syl5eq 2652 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘4) · (𝑛 / 2)) = ((log‘2) · (2 · (𝑛 / 2))))
257173oveq2d 6540 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2) · (2 · (𝑛 / 2))) = ((log‘2) · 𝑛))
258246, 256, 2573eqtrd 2644 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘4) · (((𝑛 / 2) + 1) − 1)) = ((log‘2) · 𝑛))
259258oveq2d 6540 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((θ‘((𝑛 / 2) + 1)) + ((log‘4) · (((𝑛 / 2) + 1) − 1))) = ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)))
260234, 243, 2593brtr3d 4605 . . . . . . . . . . . . . 14 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (θ‘(𝑛 + 1)) ≤ ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)))
261 peano2uz 11570 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (ℤ‘3) → (𝑛 + 1) ∈ (ℤ‘3))
262 eluzelz 11526 . . . . . . . . . . . . . . . . . . 19 ((𝑛 + 1) ∈ (ℤ‘3) → (𝑛 + 1) ∈ ℤ)
263261, 262syl 17 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (ℤ‘3) → (𝑛 + 1) ∈ ℤ)
264263zred 11311 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (ℤ‘3) → (𝑛 + 1) ∈ ℝ)
265264adantr 479 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (𝑛 + 1) ∈ ℝ)
266 chtcl 24549 . . . . . . . . . . . . . . . 16 ((𝑛 + 1) ∈ ℝ → (θ‘(𝑛 + 1)) ∈ ℝ)
267265, 266syl 17 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (θ‘(𝑛 + 1)) ∈ ℝ)
268191, 198readdcld 9922 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) ∈ ℝ)
269 zmulcl 11256 . . . . . . . . . . . . . . . . . . . 20 ((2 ∈ ℤ ∧ (𝑛 + 1) ∈ ℤ) → (2 · (𝑛 + 1)) ∈ ℤ)
270117, 263, 269sylancr 693 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (ℤ‘3) → (2 · (𝑛 + 1)) ∈ ℤ)
271270zred 11311 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (ℤ‘3) → (2 · (𝑛 + 1)) ∈ ℝ)
272 resubcl 10193 . . . . . . . . . . . . . . . . . 18 (((2 · (𝑛 + 1)) ∈ ℝ ∧ 3 ∈ ℝ) → ((2 · (𝑛 + 1)) − 3) ∈ ℝ)
273271, 31, 272sylancl 692 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (ℤ‘3) → ((2 · (𝑛 + 1)) − 3) ∈ ℝ)
274273adantr 479 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((2 · (𝑛 + 1)) − 3) ∈ ℝ)
275 remulcl 9874 . . . . . . . . . . . . . . . 16 (((log‘2) ∈ ℝ ∧ ((2 · (𝑛 + 1)) − 3) ∈ ℝ) → ((log‘2) · ((2 · (𝑛 + 1)) − 3)) ∈ ℝ)
276101, 274, 275sylancr 693 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((log‘2) · ((2 · (𝑛 + 1)) − 3)) ∈ ℝ)
277 lelttr 9976 . . . . . . . . . . . . . . 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 1317 . . . . . . . . . . . . . 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 706 . . . . . . . . . . . . 13 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (((θ‘((𝑛 / 2) + 1)) + ((log‘2) · 𝑛)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3)) → (θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
280227, 279sylbid 228 . . . . . . . . . . . 12 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → ((θ‘((𝑛 / 2) + 1)) < ((log‘2) · ((2 · ((𝑛 / 2) + 1)) − 3)) → (θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
281161, 280syld 45 . . . . . . . . . . 11 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 / 2) ∈ ℤ) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → (θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
282 eluzfz2 12172 . . . . . . . . . . . . . 14 (𝑛 ∈ (ℤ‘3) → 𝑛 ∈ (3...𝑛))
283 fveq2 6085 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑛 → (θ‘𝑘) = (θ‘𝑛))
284 oveq2 6532 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑛 → (2 · 𝑘) = (2 · 𝑛))
285284oveq1d 6539 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑛 → ((2 · 𝑘) − 3) = ((2 · 𝑛) − 3))
286285oveq2d 6540 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑛 → ((log‘2) · ((2 · 𝑘) − 3)) = ((log‘2) · ((2 · 𝑛) − 3)))
287283, 286breq12d 4587 . . . . . . . . . . . . . . 15 (𝑘 = 𝑛 → ((θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ (θ‘𝑛) < ((log‘2) · ((2 · 𝑛) − 3))))
288287rspcv 3274 . . . . . . . . . . . . . 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 479 . . . . . . . . . . . 12 ((𝑛 ∈ (ℤ‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → (θ‘𝑛) < ((log‘2) · ((2 · 𝑛) − 3))))
291210zred 11311 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (ℤ‘3) → (2 · 𝑛) ∈ ℝ)
29231a1i 11 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (ℤ‘3) → 3 ∈ ℝ)
293122ltp1d 10800 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (ℤ‘3) → 𝑛 < (𝑛 + 1))
29425a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (ℤ‘3) → (2 ∈ ℝ ∧ 0 < 2))
295 ltmul2 10720 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℝ ∧ (𝑛 + 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝑛 < (𝑛 + 1) ↔ (2 · 𝑛) < (2 · (𝑛 + 1))))
296122, 264, 294, 295syl3anc 1317 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (ℤ‘3) → (𝑛 < (𝑛 + 1) ↔ (2 · 𝑛) < (2 · (𝑛 + 1))))
297293, 296mpbid 220 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (ℤ‘3) → (2 · 𝑛) < (2 · (𝑛 + 1)))
298291, 271, 292, 297ltsub1dd 10485 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ℤ‘3) → ((2 · 𝑛) − 3) < ((2 · (𝑛 + 1)) − 3))
299 resubcl 10193 . . . . . . . . . . . . . . . . . 18 (((2 · 𝑛) ∈ ℝ ∧ 3 ∈ ℝ) → ((2 · 𝑛) − 3) ∈ ℝ)
300291, 31, 299sylancl 692 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (ℤ‘3) → ((2 · 𝑛) − 3) ∈ ℝ)
3017a1i 11 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (ℤ‘3) → ((log‘2) ∈ ℝ ∧ 0 < (log‘2)))
302 ltmul2 10720 . . . . . . . . . . . . . . . . 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 1317 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ℤ‘3) → (((2 · 𝑛) − 3) < ((2 · (𝑛 + 1)) − 3) ↔ ((log‘2) · ((2 · 𝑛) − 3)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
304298, 303mpbid 220 . . . . . . . . . . . . . . 15 (𝑛 ∈ (ℤ‘3) → ((log‘2) · ((2 · 𝑛) − 3)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3)))
305 chtcl 24549 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℝ → (θ‘𝑛) ∈ ℝ)
306122, 305syl 17 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ℤ‘3) → (θ‘𝑛) ∈ ℝ)
307 remulcl 9874 . . . . . . . . . . . . . . . . 17 (((log‘2) ∈ ℝ ∧ ((2 · 𝑛) − 3) ∈ ℝ) → ((log‘2) · ((2 · 𝑛) − 3)) ∈ ℝ)
308101, 300, 307sylancr 693 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ℤ‘3) → ((log‘2) · ((2 · 𝑛) − 3)) ∈ ℝ)
309101, 273, 275sylancr 693 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ℤ‘3) → ((log‘2) · ((2 · (𝑛 + 1)) − 3)) ∈ ℝ)
310 lttr 9962 . . . . . . . . . . . . . . . 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 1317 . . . . . . . . . . . . . . 15 (𝑛 ∈ (ℤ‘3) → (((θ‘𝑛) < ((log‘2) · ((2 · 𝑛) − 3)) ∧ ((log‘2) · ((2 · 𝑛) − 3)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))) → (θ‘𝑛) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
312304, 311mpan2d 705 . . . . . . . . . . . . . 14 (𝑛 ∈ (ℤ‘3) → ((θ‘𝑛) < ((log‘2) · ((2 · 𝑛) − 3)) → (θ‘𝑛) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
313312adantr 479 . . . . . . . . . . . . 13 ((𝑛 ∈ (ℤ‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) → ((θ‘𝑛) < ((log‘2) · ((2 · 𝑛) − 3)) → (θ‘𝑛) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
314118adantr 479 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) → 𝑛 ∈ ℤ)
315 dvdsval2 14767 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℤ ∧ 2 ≠ 0 ∧ (𝑛 + 1) ∈ ℤ) → (2 ∥ (𝑛 + 1) ↔ ((𝑛 + 1) / 2) ∈ ℤ))
316117, 170, 315mp3an12 1405 . . . . . . . . . . . . . . . . . 18 ((𝑛 + 1) ∈ ℤ → (2 ∥ (𝑛 + 1) ↔ ((𝑛 + 1) / 2) ∈ ℤ))
317263, 316syl 17 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (ℤ‘3) → (2 ∥ (𝑛 + 1) ↔ ((𝑛 + 1) / 2) ∈ ℤ))
318 2lt3 11039 . . . . . . . . . . . . . . . . . . . . . . . 24 2 < 3
3192, 31ltnlei 10006 . . . . . . . . . . . . . . . . . . . . . . . 24 (2 < 3 ↔ ¬ 3 ≤ 2)
320318, 319mpbi 218 . . . . . . . . . . . . . . . . . . . . . . 23 ¬ 3 ≤ 2
321 breq2 4578 . . . . . . . . . . . . . . . . . . . . . . 23 (2 = (𝑛 + 1) → (3 ≤ 2 ↔ 3 ≤ (𝑛 + 1)))
322320, 321mtbii 314 . . . . . . . . . . . . . . . . . . . . . 22 (2 = (𝑛 + 1) → ¬ 3 ≤ (𝑛 + 1))
323 eluzle 11529 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 + 1) ∈ (ℤ‘3) → 3 ≤ (𝑛 + 1))
324261, 323syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (ℤ‘3) → 3 ≤ (𝑛 + 1))
325322, 324nsyl3 131 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (ℤ‘3) → ¬ 2 = (𝑛 + 1))
326325adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 + 1) ∈ ℙ) → ¬ 2 = (𝑛 + 1))
327 uzid 11531 . . . . . . . . . . . . . . . . . . . . . 22 (2 ∈ ℤ → 2 ∈ (ℤ‘2))
328117, 327ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 2 ∈ (ℤ‘2)
329 simpr 475 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 + 1) ∈ ℙ) → (𝑛 + 1) ∈ ℙ)
330 dvdsprm 15196 . . . . . . . . . . . . . . . . . . . . 21 ((2 ∈ (ℤ‘2) ∧ (𝑛 + 1) ∈ ℙ) → (2 ∥ (𝑛 + 1) ↔ 2 = (𝑛 + 1)))
331328, 329, 330sylancr 693 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 + 1) ∈ ℙ) → (2 ∥ (𝑛 + 1) ↔ 2 = (𝑛 + 1)))
332326, 331mtbird 313 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ (ℤ‘3) ∧ (𝑛 + 1) ∈ ℙ) → ¬ 2 ∥ (𝑛 + 1))
333332ex 448 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (ℤ‘3) → ((𝑛 + 1) ∈ ℙ → ¬ 2 ∥ (𝑛 + 1)))
334333con2d 127 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (ℤ‘3) → (2 ∥ (𝑛 + 1) → ¬ (𝑛 + 1) ∈ ℙ))
335317, 334sylbird 248 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ℤ‘3) → (((𝑛 + 1) / 2) ∈ ℤ → ¬ (𝑛 + 1) ∈ ℙ))
336335imp 443 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) → ¬ (𝑛 + 1) ∈ ℙ)
337 chtnprm 24594 . . . . . . . . . . . . . . 15 ((𝑛 ∈ ℤ ∧ ¬ (𝑛 + 1) ∈ ℙ) → (θ‘(𝑛 + 1)) = (θ‘𝑛))
338314, 336, 337syl2anc 690 . . . . . . . . . . . . . 14 ((𝑛 ∈ (ℤ‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) → (θ‘(𝑛 + 1)) = (θ‘𝑛))
339338breq1d 4584 . . . . . . . . . . . . 13 ((𝑛 ∈ (ℤ‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) → ((θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3)) ↔ (θ‘𝑛) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
340313, 339sylibrd 247 . . . . . . . . . . . 12 ((𝑛 ∈ (ℤ‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) → ((θ‘𝑛) < ((log‘2) · ((2 · 𝑛) − 3)) → (θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
341290, 340syld 45 . . . . . . . . . . 11 ((𝑛 ∈ (ℤ‘3) ∧ ((𝑛 + 1) / 2) ∈ ℤ) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → (θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
342 zeo 11292 . . . . . . . . . . . 12 (𝑛 ∈ ℤ → ((𝑛 / 2) ∈ ℤ ∨ ((𝑛 + 1) / 2) ∈ ℤ))
343118, 342syl 17 . . . . . . . . . . 11 (𝑛 ∈ (ℤ‘3) → ((𝑛 / 2) ∈ ℤ ∨ ((𝑛 + 1) / 2) ∈ ℤ))
344281, 341, 343mpjaodan 822 . . . . . . . . . 10 (𝑛 ∈ (ℤ‘3) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → (θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
345 ovex 6552 . . . . . . . . . . 11 (𝑛 + 1) ∈ V
346 fveq2 6085 . . . . . . . . . . . 12 (𝑘 = (𝑛 + 1) → (θ‘𝑘) = (θ‘(𝑛 + 1)))
347 oveq2 6532 . . . . . . . . . . . . . 14 (𝑘 = (𝑛 + 1) → (2 · 𝑘) = (2 · (𝑛 + 1)))
348347oveq1d 6539 . . . . . . . . . . . . 13 (𝑘 = (𝑛 + 1) → ((2 · 𝑘) − 3) = ((2 · (𝑛 + 1)) − 3))
349348oveq2d 6540 . . . . . . . . . . . 12 (𝑘 = (𝑛 + 1) → ((log‘2) · ((2 · 𝑘) − 3)) = ((log‘2) · ((2 · (𝑛 + 1)) − 3)))
350346, 349breq12d 4587 . . . . . . . . . . 11 (𝑘 = (𝑛 + 1) → ((θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ (θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3))))
351345, 350ralsn 4165 . . . . . . . . . 10 (∀𝑘 ∈ {(𝑛 + 1)} (θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ (θ‘(𝑛 + 1)) < ((log‘2) · ((2 · (𝑛 + 1)) − 3)))
352344, 351syl6ibr 240 . . . . . . . . 9 (𝑛 ∈ (ℤ‘3) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → ∀𝑘 ∈ {(𝑛 + 1)} (θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))))
353352ancld 573 . . . . . . . 8 (𝑛 ∈ (ℤ‘3) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ∧ ∀𝑘 ∈ {(𝑛 + 1)} (θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)))))
354 ralun 3753 . . . . . . . . 9 ((∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ∧ ∀𝑘 ∈ {(𝑛 + 1)} (θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))) → ∀𝑘 ∈ ((3...𝑛) ∪ {(𝑛 + 1)})(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)))
355 fzsuc 12210 . . . . . . . . . 10 (𝑛 ∈ (ℤ‘3) → (3...(𝑛 + 1)) = ((3...𝑛) ∪ {(𝑛 + 1)}))
356355raleqdv 3117 . . . . . . . . 9 (𝑛 ∈ (ℤ‘3) → (∀𝑘 ∈ (3...(𝑛 + 1))(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ ∀𝑘 ∈ ((3...𝑛) ∪ {(𝑛 + 1)})(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))))
357354, 356syl5ibr 234 . . . . . . . 8 (𝑛 ∈ (ℤ‘3) → ((∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ∧ ∀𝑘 ∈ {(𝑛 + 1)} (θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))) → ∀𝑘 ∈ (3...(𝑛 + 1))(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))))
358353, 357syld 45 . . . . . . 7 (𝑛 ∈ (ℤ‘3) → (∀𝑘 ∈ (3...𝑛)(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → ∀𝑘 ∈ (3...(𝑛 + 1))(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3))))
35966, 68, 70, 72, 74, 112, 358uzind4i 11579 . . . . . 6 ((⌊‘𝑁) ∈ (ℤ‘3) → ∀𝑘 ∈ (3...(⌊‘𝑁))(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)))
360 fveq2 6085 . . . . . . . 8 (𝑘 = (⌊‘𝑁) → (θ‘𝑘) = (θ‘(⌊‘𝑁)))
361 oveq2 6532 . . . . . . . . . 10 (𝑘 = (⌊‘𝑁) → (2 · 𝑘) = (2 · (⌊‘𝑁)))
362361oveq1d 6539 . . . . . . . . 9 (𝑘 = (⌊‘𝑁) → ((2 · 𝑘) − 3) = ((2 · (⌊‘𝑁)) − 3))
363362oveq2d 6540 . . . . . . . 8 (𝑘 = (⌊‘𝑁) → ((log‘2) · ((2 · 𝑘) − 3)) = ((log‘2) · ((2 · (⌊‘𝑁)) − 3)))
364360, 363breq12d 4587 . . . . . . 7 (𝑘 = (⌊‘𝑁) → ((θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) ↔ (θ‘(⌊‘𝑁)) < ((log‘2) · ((2 · (⌊‘𝑁)) − 3))))
365364rspcv 3274 . . . . . 6 ((⌊‘𝑁) ∈ (3...(⌊‘𝑁)) → (∀𝑘 ∈ (3...(⌊‘𝑁))(θ‘𝑘) < ((log‘2) · ((2 · 𝑘) − 3)) → (θ‘(⌊‘𝑁)) < ((log‘2) · ((2 · (⌊‘𝑁)) − 3))))
36665, 359, 365sylc 62 . . . . 5 ((⌊‘𝑁) ∈ (ℤ‘3) → (θ‘(⌊‘𝑁)) < ((log‘2) · ((2 · (⌊‘𝑁)) − 3)))
36764, 366syl 17 . . . 4 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → (θ‘(⌊‘𝑁)) < ((log‘2) · ((2 · (⌊‘𝑁)) − 3)))
36860, 367eqbrtrrd 4598 . . 3 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → (θ‘𝑁) < ((log‘2) · ((2 · (⌊‘𝑁)) − 3)))
36935adantr 479 . . . . 5 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → (2 · 𝑁) ∈ ℝ)
37031a1i 11 . . . . 5 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → 3 ∈ ℝ)
371 flle 12414 . . . . . . 7 (𝑁 ∈ ℝ → (⌊‘𝑁) ≤ 𝑁)
372371ad2antrr 757 . . . . . 6 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → (⌊‘𝑁) ≤ 𝑁)
37322adantr 479 . . . . . . 7 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → 𝑁 ∈ ℝ)
37425a1i 11 . . . . . . 7 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → (2 ∈ ℝ ∧ 0 < 2))
375 lemul2 10722 . . . . . . 7 (((⌊‘𝑁) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((⌊‘𝑁) ≤ 𝑁 ↔ (2 · (⌊‘𝑁)) ≤ (2 · 𝑁)))
37650, 373, 374, 375syl3anc 1317 . . . . . 6 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → ((⌊‘𝑁) ≤ 𝑁 ↔ (2 · (⌊‘𝑁)) ≤ (2 · 𝑁)))
377372, 376mpbid 220 . . . . 5 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → (2 · (⌊‘𝑁)) ≤ (2 · 𝑁))
37852, 369, 370, 377lesub1dd 10489 . . . 4 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → ((2 · (⌊‘𝑁)) − 3) ≤ ((2 · 𝑁) − 3))
3797a1i 11 . . . . 5 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → ((log‘2) ∈ ℝ ∧ 0 < (log‘2)))
380 lemul2 10722 . . . . 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 1317 . . . 4 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → (((2 · (⌊‘𝑁)) − 3) ≤ ((2 · 𝑁) − 3) ↔ ((log‘2) · ((2 · (⌊‘𝑁)) − 3)) ≤ ((log‘2) · ((2 · 𝑁) − 3))))
382378, 381mpbid 220 . . 3 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → ((log‘2) · ((2 · (⌊‘𝑁)) − 3)) ≤ ((log‘2) · ((2 · 𝑁) − 3)))
38348, 56, 59, 368, 382ltletrd 10045 . 2 (((𝑁 ∈ ℝ ∧ 2 < 𝑁) ∧ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))) → (θ‘𝑁) < ((log‘2) · ((2 · 𝑁) − 3)))
384117a1i 11 . . . 4 ((𝑁 ∈ ℝ ∧ 2 < 𝑁) → 2 ∈ ℤ)
385 flcl 12410 . . . . 5 (𝑁 ∈ ℝ → (⌊‘𝑁) ∈ ℤ)
386385adantr 479 . . . 4 ((𝑁 ∈ ℝ ∧ 2 < 𝑁) → (⌊‘𝑁) ∈ ℤ)
387 ltle 9974 . . . . . . 7 ((2 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (2 < 𝑁 → 2 ≤ 𝑁))
3882, 387mpan 701 . . . . . 6 (𝑁 ∈ ℝ → (2 < 𝑁 → 2 ≤ 𝑁))
389 flge 12420 . . . . . . 7 ((𝑁 ∈ ℝ ∧ 2 ∈ ℤ) → (2 ≤ 𝑁 ↔ 2 ≤ (⌊‘𝑁)))
390117, 389mpan2 702 . . . . . 6 (𝑁 ∈ ℝ → (2 ≤ 𝑁 ↔ 2 ≤ (⌊‘𝑁)))
391388, 390sylibd 227 . . . . 5 (𝑁 ∈ ℝ → (2 < 𝑁 → 2 ≤ (⌊‘𝑁)))
392391imp 443 . . . 4 ((𝑁 ∈ ℝ ∧ 2 < 𝑁) → 2 ≤ (⌊‘𝑁))
393 eluz2 11522 . . . 4 ((⌊‘𝑁) ∈ (ℤ‘2) ↔ (2 ∈ ℤ ∧ (⌊‘𝑁) ∈ ℤ ∧ 2 ≤ (⌊‘𝑁)))
394384, 386, 392, 393syl3anbrc 1238 . . 3 ((𝑁 ∈ ℝ ∧ 2 < 𝑁) → (⌊‘𝑁) ∈ (ℤ‘2))
395 uzp1 11550 . . 3 ((⌊‘𝑁) ∈ (ℤ‘2) → ((⌊‘𝑁) = 2 ∨ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))))
396394, 395syl 17 . 2 ((𝑁 ∈ ℝ ∧ 2 < 𝑁) → ((⌊‘𝑁) = 2 ∨ (⌊‘𝑁) ∈ (ℤ‘(2 + 1))))
39746, 383, 396mpjaodan 822 1 ((𝑁 ∈ ℝ ∧ 2 < 𝑁) → (θ‘𝑁) < ((log‘2) · ((2 · 𝑁) − 3)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382   = wceq 1474  wcel 1976  wne 2776  wral 2892  cun 3534  {csn 4121   class class class wbr 4574  cfv 5787  (class class class)co 6524  cc 9787  cr 9788  0cc0 9789  1c1 9790   + caddc 9792   · cmul 9794   < clt 9927  cle 9928  cmin 10114   / cdiv 10530  cn 10864  2c2 10914  3c3 10915  4c4 10916  6c6 10918  8c8 10920  cz 11207  cuz 11516  +crp 11661  ...cfz 12149  cfl 12405  cexp 12674  cdvds 14764  cprime 15166  logclog 24019  θccht 24531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-rep 4690  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-inf2 8395  ax-cnex 9845  ax-resscn 9846  ax-1cn 9847  ax-icn 9848  ax-addcl 9849  ax-addrcl 9850  ax-mulcl 9851  ax-mulrcl 9852  ax-mulcom 9853  ax-addass 9854  ax-mulass 9855  ax-distr 9856  ax-i2m1 9857  ax-1ne0 9858  ax-1rid 9859  ax-rnegex 9860  ax-rrecex 9861  ax-cnre 9862  ax-pre-lttri 9863  ax-pre-lttrn 9864  ax-pre-ltadd 9865  ax-pre-mulgt0 9866  ax-pre-sup 9867  ax-addf 9868  ax-mulf 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-nel 2779  df-ral 2897  df-rex 2898  df-reu 2899  df-rmo 2900  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-pss 3552  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-tp 4126  df-op 4128  df-uni 4364  df-int 4402  df-iun 4448  df-iin 4449  df-br 4575  df-opab 4635  df-mpt 4636  df-tr 4672  df-eprel 4936  df-id 4940  df-po 4946  df-so 4947  df-fr 4984  df-se 4985  df-we 4986  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-pred 5580  df-ord 5626  df-on 5627  df-lim 5628  df-suc 5629  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-isom 5796  df-riota 6486  df-ov 6527  df-oprab 6528  df-mpt2 6529  df-of 6769  df-om 6932  df-1st 7033  df-2nd 7034  df-supp 7157  df-wrecs 7268  df-recs 7329  df-rdg 7367  df-1o 7421  df-2o 7422  df-oadd 7425  df-er 7603  df-map 7720  df-pm 7721  df-ixp 7769  df-en 7816  df-dom 7817  df-sdom 7818  df-fin 7819  df-fsupp 8133  df-fi 8174  df-sup 8205  df-inf 8206  df-oi 8272  df-card 8622  df-cda 8847  df-pnf 9929  df-mnf 9930  df-xr 9931  df-ltxr 9932  df-le 9933  df-sub 10116  df-neg 10117  df-div 10531  df-nn 10865  df-2 10923  df-3 10924  df-4 10925  df-5 10926  df-6 10927  df-7 10928  df-8 10929  df-9 10930  df-n0 11137  df-z 11208  df-dec 11323  df-uz 11517  df-q 11618  df-rp 11662  df-xneg 11775  df-xadd 11776  df-xmul 11777  df-ioo 12003  df-ioc 12004  df-ico 12005  df-icc 12006  df-fz 12150  df-fzo 12287  df-fl 12407  df-mod 12483  df-seq 12616  df-exp 12675  df-fac 12875  df-bc 12904  df-hash 12932  df-shft 13598  df-cj 13630  df-re 13631  df-im 13632  df-sqrt 13766  df-abs 13767  df-limsup 13993  df-clim 14010  df-rlim 14011  df-sum 14208  df-ef 14580  df-sin 14582  df-cos 14583  df-pi 14585  df-dvds 14765  df-gcd 14998  df-prm 15167  df-pc 15323  df-struct 15640  df-ndx 15641  df-slot 15642  df-base 15643  df-sets 15644  df-ress 15645  df-plusg 15724  df-mulr 15725  df-starv 15726  df-sca 15727  df-vsca 15728  df-ip 15729  df-tset 15730  df-ple 15731  df-ds 15734  df-unif 15735  df-hom 15736  df-cco 15737  df-rest 15849  df-topn 15850  df-0g 15868  df-gsum 15869  df-topgen 15870  df-pt 15871  df-prds 15874  df-xrs 15928  df-qtop 15933  df-imas 15934  df-xps 15936  df-mre 16012  df-mrc 16013  df-acs 16015  df-mgm 17008  df-sgrp 17050  df-mnd 17061  df-submnd 17102  df-mulg 17307  df-cntz 17516  df-cmn 17961  df-psmet 19502  df-xmet 19503  df-met 19504  df-bl 19505  df-mopn 19506  df-fbas 19507  df-fg 19508  df-cnfld 19511  df-top 20460  df-bases 20461  df-topon 20462  df-topsp 20463  df-cld 20572  df-ntr 20573  df-cls 20574  df-nei 20651  df-lp 20689  df-perf 20690  df-cn 20780  df-cnp 20781  df-haus 20868  df-tx 21114  df-hmeo 21307  df-fil 21399  df-fm 21491  df-flim 21492  df-flf 21493  df-xms 21873  df-ms 21874  df-tms 21875  df-cncf 22417  df-limc 23350  df-dv 23351  df-log 24021  df-cht 24537
This theorem is referenced by:  bposlem6  24728  chto1ub  24879
  Copyright terms: Public domain W3C validator