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

Theorem bposlem6 25234
Description: Lemma for bpos 25238. By using the various bounds at our disposal, arrive at an inequality that is false for 𝑁 large enough. (Contributed by Mario Carneiro, 14-Mar-2014.) (Revised by Wolf Lammen, 12-Sep-2020.)
Hypotheses
Ref Expression
bpos.1 (𝜑𝑁 ∈ (ℤ‘5))
bpos.2 (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)))
bpos.3 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))
bpos.4 𝐾 = (⌊‘((2 · 𝑁) / 3))
bpos.5 𝑀 = (⌊‘(√‘(2 · 𝑁)))
Assertion
Ref Expression
bposlem6 (𝜑 → ((4↑𝑁) / 𝑁) < (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))))
Distinct variable groups:   𝐹,𝑝   𝑛,𝑝,𝐾   𝑀,𝑝   𝑛,𝑁,𝑝   𝜑,𝑛,𝑝
Allowed substitution hints:   𝐹(𝑛)   𝑀(𝑛)

Proof of Theorem bposlem6
StepHypRef Expression
1 4nn 11388 . . . . 5 4 ∈ ℕ
2 5nn 11389 . . . . . . 7 5 ∈ ℕ
3 bpos.1 . . . . . . 7 (𝜑𝑁 ∈ (ℤ‘5))
4 eluznn 11960 . . . . . . 7 ((5 ∈ ℕ ∧ 𝑁 ∈ (ℤ‘5)) → 𝑁 ∈ ℕ)
52, 3, 4sylancr 567 . . . . . 6 (𝜑𝑁 ∈ ℕ)
65nnnn0d 11552 . . . . 5 (𝜑𝑁 ∈ ℕ0)
7 nnexpcl 13079 . . . . 5 ((4 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (4↑𝑁) ∈ ℕ)
81, 6, 7sylancr 567 . . . 4 (𝜑 → (4↑𝑁) ∈ ℕ)
98nnred 11236 . . 3 (𝜑 → (4↑𝑁) ∈ ℝ)
109, 5nndivred 11270 . 2 (𝜑 → ((4↑𝑁) / 𝑁) ∈ ℝ)
11 fzctr 12658 . . . . 5 (𝑁 ∈ ℕ0𝑁 ∈ (0...(2 · 𝑁)))
126, 11syl 17 . . . 4 (𝜑𝑁 ∈ (0...(2 · 𝑁)))
13 bccl2 13313 . . . 4 (𝑁 ∈ (0...(2 · 𝑁)) → ((2 · 𝑁)C𝑁) ∈ ℕ)
1412, 13syl 17 . . 3 (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℕ)
1514nnred 11236 . 2 (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℝ)
16 2nn 11386 . . . . . . 7 2 ∈ ℕ
17 nnmulcl 11244 . . . . . . 7 ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
1816, 5, 17sylancr 567 . . . . . 6 (𝜑 → (2 · 𝑁) ∈ ℕ)
1918nnrpd 12072 . . . . 5 (𝜑 → (2 · 𝑁) ∈ ℝ+)
2018nnred 11236 . . . . . . . 8 (𝜑 → (2 · 𝑁) ∈ ℝ)
2119rpge0d 12078 . . . . . . . 8 (𝜑 → 0 ≤ (2 · 𝑁))
2220, 21resqrtcld 14363 . . . . . . 7 (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ)
23 3nn 11387 . . . . . . 7 3 ∈ ℕ
24 nndivre 11257 . . . . . . 7 (((√‘(2 · 𝑁)) ∈ ℝ ∧ 3 ∈ ℕ) → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
2522, 23, 24sylancl 566 . . . . . 6 (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
26 2re 11291 . . . . . 6 2 ∈ ℝ
27 readdcl 10220 . . . . . 6 ((((√‘(2 · 𝑁)) / 3) ∈ ℝ ∧ 2 ∈ ℝ) → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
2825, 26, 27sylancl 566 . . . . 5 (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
2919, 28rpcxpcld 24696 . . . 4 (𝜑 → ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) ∈ ℝ+)
3029rpred 12074 . . 3 (𝜑 → ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) ∈ ℝ)
31 2rp 12039 . . . . 5 2 ∈ ℝ+
32 nnmulcl 11244 . . . . . . . . 9 ((4 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (4 · 𝑁) ∈ ℕ)
331, 5, 32sylancr 567 . . . . . . . 8 (𝜑 → (4 · 𝑁) ∈ ℕ)
3433nnred 11236 . . . . . . 7 (𝜑 → (4 · 𝑁) ∈ ℝ)
35 nndivre 11257 . . . . . . 7 (((4 · 𝑁) ∈ ℝ ∧ 3 ∈ ℕ) → ((4 · 𝑁) / 3) ∈ ℝ)
3634, 23, 35sylancl 566 . . . . . 6 (𝜑 → ((4 · 𝑁) / 3) ∈ ℝ)
37 5re 11300 . . . . . 6 5 ∈ ℝ
38 resubcl 10546 . . . . . 6 ((((4 · 𝑁) / 3) ∈ ℝ ∧ 5 ∈ ℝ) → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
3936, 37, 38sylancl 566 . . . . 5 (𝜑 → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
40 rpcxpcl 24642 . . . . 5 ((2 ∈ ℝ+ ∧ (((4 · 𝑁) / 3) − 5) ∈ ℝ) → (2↑𝑐(((4 · 𝑁) / 3) − 5)) ∈ ℝ+)
4131, 39, 40sylancr 567 . . . 4 (𝜑 → (2↑𝑐(((4 · 𝑁) / 3) − 5)) ∈ ℝ+)
4241rpred 12074 . . 3 (𝜑 → (2↑𝑐(((4 · 𝑁) / 3) − 5)) ∈ ℝ)
4330, 42remulcld 10271 . 2 (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))) ∈ ℝ)
44 df-5 11283 . . . . 5 5 = (4 + 1)
45 4z 11612 . . . . . 6 4 ∈ ℤ
46 uzid 11902 . . . . . 6 (4 ∈ ℤ → 4 ∈ (ℤ‘4))
47 peano2uz 11942 . . . . . 6 (4 ∈ (ℤ‘4) → (4 + 1) ∈ (ℤ‘4))
4845, 46, 47mp2b 10 . . . . 5 (4 + 1) ∈ (ℤ‘4)
4944, 48eqeltri 2845 . . . 4 5 ∈ (ℤ‘4)
50 eqid 2770 . . . . 5 (ℤ‘4) = (ℤ‘4)
5150uztrn2 11905 . . . 4 ((5 ∈ (ℤ‘4) ∧ 𝑁 ∈ (ℤ‘5)) → 𝑁 ∈ (ℤ‘4))
5249, 3, 51sylancr 567 . . 3 (𝜑𝑁 ∈ (ℤ‘4))
53 bclbnd 25225 . . 3 (𝑁 ∈ (ℤ‘4) → ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁))
5452, 53syl 17 . 2 (𝜑 → ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁))
55 bpos.3 . . . . . . . 8 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))
56 id 22 . . . . . . . . . 10 (𝑛 ∈ ℙ → 𝑛 ∈ ℙ)
57 pccl 15760 . . . . . . . . . 10 ((𝑛 ∈ ℙ ∧ ((2 · 𝑁)C𝑁) ∈ ℕ) → (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
5856, 14, 57syl2anr 576 . . . . . . . . 9 ((𝜑𝑛 ∈ ℙ) → (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
5958ralrimiva 3114 . . . . . . . 8 (𝜑 → ∀𝑛 ∈ ℙ (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
6055, 59pcmptcl 15801 . . . . . . 7 (𝜑 → (𝐹:ℕ⟶ℕ ∧ seq1( · , 𝐹):ℕ⟶ℕ))
6160simprd 477 . . . . . 6 (𝜑 → seq1( · , 𝐹):ℕ⟶ℕ)
62 bpos.2 . . . . . . . . 9 (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)))
63 bpos.4 . . . . . . . . 9 𝐾 = (⌊‘((2 · 𝑁) / 3))
64 bpos.5 . . . . . . . . 9 𝑀 = (⌊‘(√‘(2 · 𝑁)))
653, 62, 55, 63, 64bposlem4 25232 . . . . . . . 8 (𝜑𝑀 ∈ (3...𝐾))
66 elfzuz 12544 . . . . . . . 8 (𝑀 ∈ (3...𝐾) → 𝑀 ∈ (ℤ‘3))
6765, 66syl 17 . . . . . . 7 (𝜑𝑀 ∈ (ℤ‘3))
68 eluznn 11960 . . . . . . 7 ((3 ∈ ℕ ∧ 𝑀 ∈ (ℤ‘3)) → 𝑀 ∈ ℕ)
6923, 67, 68sylancr 567 . . . . . 6 (𝜑𝑀 ∈ ℕ)
7061, 69ffvelrnd 6503 . . . . 5 (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℕ)
7170nnred 11236 . . . 4 (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℝ)
72 2z 11610 . . . . . . . . 9 2 ∈ ℤ
73 nndivre 11257 . . . . . . . . . . . 12 (((2 · 𝑁) ∈ ℝ ∧ 3 ∈ ℕ) → ((2 · 𝑁) / 3) ∈ ℝ)
7420, 23, 73sylancl 566 . . . . . . . . . . 11 (𝜑 → ((2 · 𝑁) / 3) ∈ ℝ)
7574flcld 12806 . . . . . . . . . 10 (𝜑 → (⌊‘((2 · 𝑁) / 3)) ∈ ℤ)
7663, 75syl5eqel 2853 . . . . . . . . 9 (𝜑𝐾 ∈ ℤ)
77 zmulcl 11627 . . . . . . . . 9 ((2 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (2 · 𝐾) ∈ ℤ)
7872, 76, 77sylancr 567 . . . . . . . 8 (𝜑 → (2 · 𝐾) ∈ ℤ)
792nnzi 11602 . . . . . . . 8 5 ∈ ℤ
80 zsubcl 11620 . . . . . . . 8 (((2 · 𝐾) ∈ ℤ ∧ 5 ∈ ℤ) → ((2 · 𝐾) − 5) ∈ ℤ)
8178, 79, 80sylancl 566 . . . . . . 7 (𝜑 → ((2 · 𝐾) − 5) ∈ ℤ)
8281zred 11683 . . . . . 6 (𝜑 → ((2 · 𝐾) − 5) ∈ ℝ)
83 rpcxpcl 24642 . . . . . 6 ((2 ∈ ℝ+ ∧ ((2 · 𝐾) − 5) ∈ ℝ) → (2↑𝑐((2 · 𝐾) − 5)) ∈ ℝ+)
8431, 82, 83sylancr 567 . . . . 5 (𝜑 → (2↑𝑐((2 · 𝐾) − 5)) ∈ ℝ+)
8584rpred 12074 . . . 4 (𝜑 → (2↑𝑐((2 · 𝐾) − 5)) ∈ ℝ)
8671, 85remulcld 10271 . . 3 (𝜑 → ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2 · 𝐾) − 5))) ∈ ℝ)
873, 62, 55, 63bposlem3 25231 . . . 4 (𝜑 → (seq1( · , 𝐹)‘𝐾) = ((2 · 𝑁)C𝑁))
88 elfzuz3 12545 . . . . . . . . . 10 (𝑀 ∈ (3...𝐾) → 𝐾 ∈ (ℤ𝑀))
8965, 88syl 17 . . . . . . . . 9 (𝜑𝐾 ∈ (ℤ𝑀))
9055, 59, 69, 89pcmptdvds 15804 . . . . . . . 8 (𝜑 → (seq1( · , 𝐹)‘𝑀) ∥ (seq1( · , 𝐹)‘𝐾))
9170nnzd 11682 . . . . . . . . 9 (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℤ)
9270nnne0d 11266 . . . . . . . . 9 (𝜑 → (seq1( · , 𝐹)‘𝑀) ≠ 0)
93 uztrn 11904 . . . . . . . . . . . . 13 ((𝐾 ∈ (ℤ𝑀) ∧ 𝑀 ∈ (ℤ‘3)) → 𝐾 ∈ (ℤ‘3))
9489, 67, 93syl2anc 565 . . . . . . . . . . . 12 (𝜑𝐾 ∈ (ℤ‘3))
95 eluznn 11960 . . . . . . . . . . . 12 ((3 ∈ ℕ ∧ 𝐾 ∈ (ℤ‘3)) → 𝐾 ∈ ℕ)
9623, 94, 95sylancr 567 . . . . . . . . . . 11 (𝜑𝐾 ∈ ℕ)
9761, 96ffvelrnd 6503 . . . . . . . . . 10 (𝜑 → (seq1( · , 𝐹)‘𝐾) ∈ ℕ)
9897nnzd 11682 . . . . . . . . 9 (𝜑 → (seq1( · , 𝐹)‘𝐾) ∈ ℤ)
99 dvdsval2 15191 . . . . . . . . 9 (((seq1( · , 𝐹)‘𝑀) ∈ ℤ ∧ (seq1( · , 𝐹)‘𝑀) ≠ 0 ∧ (seq1( · , 𝐹)‘𝐾) ∈ ℤ) → ((seq1( · , 𝐹)‘𝑀) ∥ (seq1( · , 𝐹)‘𝐾) ↔ ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ))
10091, 92, 98, 99syl3anc 1475 . . . . . . . 8 (𝜑 → ((seq1( · , 𝐹)‘𝑀) ∥ (seq1( · , 𝐹)‘𝐾) ↔ ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ))
10190, 100mpbid 222 . . . . . . 7 (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ)
102101zred 11683 . . . . . 6 (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℝ)
10369nnred 11236 . . . . . . . . 9 (𝜑𝑀 ∈ ℝ)
10476zred 11683 . . . . . . . . 9 (𝜑𝐾 ∈ ℝ)
105 eluzle 11900 . . . . . . . . . 10 (𝐾 ∈ (ℤ𝑀) → 𝑀𝐾)
10689, 105syl 17 . . . . . . . . 9 (𝜑𝑀𝐾)
107 efchtdvds 25105 . . . . . . . . 9 ((𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑀𝐾) → (exp‘(θ‘𝑀)) ∥ (exp‘(θ‘𝐾)))
108103, 104, 106, 107syl3anc 1475 . . . . . . . 8 (𝜑 → (exp‘(θ‘𝑀)) ∥ (exp‘(θ‘𝐾)))
109 efchtcl 25057 . . . . . . . . . . 11 (𝑀 ∈ ℝ → (exp‘(θ‘𝑀)) ∈ ℕ)
110103, 109syl 17 . . . . . . . . . 10 (𝜑 → (exp‘(θ‘𝑀)) ∈ ℕ)
111110nnzd 11682 . . . . . . . . 9 (𝜑 → (exp‘(θ‘𝑀)) ∈ ℤ)
112110nnne0d 11266 . . . . . . . . 9 (𝜑 → (exp‘(θ‘𝑀)) ≠ 0)
113 efchtcl 25057 . . . . . . . . . . 11 (𝐾 ∈ ℝ → (exp‘(θ‘𝐾)) ∈ ℕ)
114104, 113syl 17 . . . . . . . . . 10 (𝜑 → (exp‘(θ‘𝐾)) ∈ ℕ)
115114nnzd 11682 . . . . . . . . 9 (𝜑 → (exp‘(θ‘𝐾)) ∈ ℤ)
116 dvdsval2 15191 . . . . . . . . 9 (((exp‘(θ‘𝑀)) ∈ ℤ ∧ (exp‘(θ‘𝑀)) ≠ 0 ∧ (exp‘(θ‘𝐾)) ∈ ℤ) → ((exp‘(θ‘𝑀)) ∥ (exp‘(θ‘𝐾)) ↔ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℤ))
117111, 112, 115, 116syl3anc 1475 . . . . . . . 8 (𝜑 → ((exp‘(θ‘𝑀)) ∥ (exp‘(θ‘𝐾)) ↔ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℤ))
118108, 117mpbid 222 . . . . . . 7 (𝜑 → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℤ)
119118zred 11683 . . . . . 6 (𝜑 → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℝ)
120 prmz 15595 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
121 fllt 12814 . . . . . . . . . . . . . . . . . 18 (((√‘(2 · 𝑁)) ∈ ℝ ∧ 𝑝 ∈ ℤ) → ((√‘(2 · 𝑁)) < 𝑝 ↔ (⌊‘(√‘(2 · 𝑁))) < 𝑝))
12222, 120, 121syl2an 575 . . . . . . . . . . . . . . . . 17 ((𝜑𝑝 ∈ ℙ) → ((√‘(2 · 𝑁)) < 𝑝 ↔ (⌊‘(√‘(2 · 𝑁))) < 𝑝))
12364breq1i 4791 . . . . . . . . . . . . . . . . 17 (𝑀 < 𝑝 ↔ (⌊‘(√‘(2 · 𝑁))) < 𝑝)
124122, 123syl6bbr 278 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 ∈ ℙ) → ((√‘(2 · 𝑁)) < 𝑝𝑀 < 𝑝))
125120zred 11683 . . . . . . . . . . . . . . . . 17 (𝑝 ∈ ℙ → 𝑝 ∈ ℝ)
126 ltnle 10318 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℝ ∧ 𝑝 ∈ ℝ) → (𝑀 < 𝑝 ↔ ¬ 𝑝𝑀))
127103, 125, 126syl2an 575 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 ∈ ℙ) → (𝑀 < 𝑝 ↔ ¬ 𝑝𝑀))
128124, 127bitrd 268 . . . . . . . . . . . . . . 15 ((𝜑𝑝 ∈ ℙ) → ((√‘(2 · 𝑁)) < 𝑝 ↔ ¬ 𝑝𝑀))
129 bposlem1 25229 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁))
1305, 129sylan 561 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁))
131125adantl 467 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑝 ∈ ℙ) → 𝑝 ∈ ℝ)
132 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 ∈ ℙ → 𝑝 ∈ ℙ)
133 pccl 15760 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑝 ∈ ℙ ∧ ((2 · 𝑁)C𝑁) ∈ ℕ) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
134132, 14, 133syl2anr 576 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑝 ∈ ℙ) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
135131, 134reexpcld 13231 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ∈ ℝ)
13620adantr 466 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑝 ∈ ℙ) → (2 · 𝑁) ∈ ℝ)
137131resqcld 13241 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑝 ∈ ℙ) → (𝑝↑2) ∈ ℝ)
138 lelttr 10329 . . . . . . . . . . . . . . . . . . . 20 (((𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ∈ ℝ ∧ (2 · 𝑁) ∈ ℝ ∧ (𝑝↑2) ∈ ℝ) → (((𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁) ∧ (2 · 𝑁) < (𝑝↑2)) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) < (𝑝↑2)))
139135, 136, 137, 138syl3anc 1475 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑝 ∈ ℙ) → (((𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁) ∧ (2 · 𝑁) < (𝑝↑2)) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) < (𝑝↑2)))
140130, 139mpand 667 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑝 ∈ ℙ) → ((2 · 𝑁) < (𝑝↑2) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) < (𝑝↑2)))
141 resqrtth 14203 . . . . . . . . . . . . . . . . . . . . 21 (((2 · 𝑁) ∈ ℝ ∧ 0 ≤ (2 · 𝑁)) → ((√‘(2 · 𝑁))↑2) = (2 · 𝑁))
14220, 21, 141syl2anc 565 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((√‘(2 · 𝑁))↑2) = (2 · 𝑁))
143142breq1d 4794 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((√‘(2 · 𝑁))↑2) < (𝑝↑2) ↔ (2 · 𝑁) < (𝑝↑2)))
144143adantr 466 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑝 ∈ ℙ) → (((√‘(2 · 𝑁))↑2) < (𝑝↑2) ↔ (2 · 𝑁) < (𝑝↑2)))
145134nn0zd 11681 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑝 ∈ ℙ) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ∈ ℤ)
14672a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑝 ∈ ℙ) → 2 ∈ ℤ)
147 prmgt1 15615 . . . . . . . . . . . . . . . . . . . 20 (𝑝 ∈ ℙ → 1 < 𝑝)
148147adantl 467 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑝 ∈ ℙ) → 1 < 𝑝)
149131, 145, 146, 148ltexp2d 13244 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑝 ∈ ℙ) → ((𝑝 pCnt ((2 · 𝑁)C𝑁)) < 2 ↔ (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) < (𝑝↑2)))
150140, 144, 1493imtr4d 283 . . . . . . . . . . . . . . . . 17 ((𝜑𝑝 ∈ ℙ) → (((√‘(2 · 𝑁))↑2) < (𝑝↑2) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) < 2))
151 df-2 11280 . . . . . . . . . . . . . . . . . 18 2 = (1 + 1)
152151breq2i 4792 . . . . . . . . . . . . . . . . 17 ((𝑝 pCnt ((2 · 𝑁)C𝑁)) < 2 ↔ (𝑝 pCnt ((2 · 𝑁)C𝑁)) < (1 + 1))
153150, 152syl6ib 241 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 ∈ ℙ) → (((√‘(2 · 𝑁))↑2) < (𝑝↑2) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) < (1 + 1)))
15422adantr 466 . . . . . . . . . . . . . . . . 17 ((𝜑𝑝 ∈ ℙ) → (√‘(2 · 𝑁)) ∈ ℝ)
15520, 21sqrtge0d 14366 . . . . . . . . . . . . . . . . . 18 (𝜑 → 0 ≤ (√‘(2 · 𝑁)))
156155adantr 466 . . . . . . . . . . . . . . . . 17 ((𝜑𝑝 ∈ ℙ) → 0 ≤ (√‘(2 · 𝑁)))
157 prmnn 15594 . . . . . . . . . . . . . . . . . . . 20 (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
158157nnrpd 12072 . . . . . . . . . . . . . . . . . . 19 (𝑝 ∈ ℙ → 𝑝 ∈ ℝ+)
159158rpge0d 12078 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ ℙ → 0 ≤ 𝑝)
160159adantl 467 . . . . . . . . . . . . . . . . 17 ((𝜑𝑝 ∈ ℙ) → 0 ≤ 𝑝)
161154, 131, 156, 160lt2sqd 13249 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 ∈ ℙ) → ((√‘(2 · 𝑁)) < 𝑝 ↔ ((√‘(2 · 𝑁))↑2) < (𝑝↑2)))
162 1z 11608 . . . . . . . . . . . . . . . . 17 1 ∈ ℤ
163 zleltp1 11629 . . . . . . . . . . . . . . . . 17 (((𝑝 pCnt ((2 · 𝑁)C𝑁)) ∈ ℤ ∧ 1 ∈ ℤ) → ((𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1 ↔ (𝑝 pCnt ((2 · 𝑁)C𝑁)) < (1 + 1)))
164145, 162, 163sylancl 566 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 ∈ ℙ) → ((𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1 ↔ (𝑝 pCnt ((2 · 𝑁)C𝑁)) < (1 + 1)))
165153, 161, 1643imtr4d 283 . . . . . . . . . . . . . . 15 ((𝜑𝑝 ∈ ℙ) → ((√‘(2 · 𝑁)) < 𝑝 → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1))
166128, 165sylbird 250 . . . . . . . . . . . . . 14 ((𝜑𝑝 ∈ ℙ) → (¬ 𝑝𝑀 → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1))
167166imp 393 . . . . . . . . . . . . 13 (((𝜑𝑝 ∈ ℙ) ∧ ¬ 𝑝𝑀) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1)
168167adantrl 687 . . . . . . . . . . . 12 (((𝜑𝑝 ∈ ℙ) ∧ (𝑝𝐾 ∧ ¬ 𝑝𝑀)) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1)
169 iftrue 4229 . . . . . . . . . . . . 13 ((𝑝𝐾 ∧ ¬ 𝑝𝑀) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = (𝑝 pCnt ((2 · 𝑁)C𝑁)))
170169adantl 467 . . . . . . . . . . . 12 (((𝜑𝑝 ∈ ℙ) ∧ (𝑝𝐾 ∧ ¬ 𝑝𝑀)) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = (𝑝 pCnt ((2 · 𝑁)C𝑁)))
171 iftrue 4229 . . . . . . . . . . . . 13 ((𝑝𝐾 ∧ ¬ 𝑝𝑀) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0) = 1)
172171adantl 467 . . . . . . . . . . . 12 (((𝜑𝑝 ∈ ℙ) ∧ (𝑝𝐾 ∧ ¬ 𝑝𝑀)) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0) = 1)
173168, 170, 1723brtr4d 4816 . . . . . . . . . . 11 (((𝜑𝑝 ∈ ℙ) ∧ (𝑝𝐾 ∧ ¬ 𝑝𝑀)) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0))
174 0le0 11311 . . . . . . . . . . . . 13 0 ≤ 0
175 iffalse 4232 . . . . . . . . . . . . . 14 (¬ (𝑝𝐾 ∧ ¬ 𝑝𝑀) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = 0)
176 iffalse 4232 . . . . . . . . . . . . . 14 (¬ (𝑝𝐾 ∧ ¬ 𝑝𝑀) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0) = 0)
177175, 176breq12d 4797 . . . . . . . . . . . . 13 (¬ (𝑝𝐾 ∧ ¬ 𝑝𝑀) → (if((𝑝𝐾 ∧ ¬ 𝑝𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0) ↔ 0 ≤ 0))
178174, 177mpbiri 248 . . . . . . . . . . . 12 (¬ (𝑝𝐾 ∧ ¬ 𝑝𝑀) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0))
179178adantl 467 . . . . . . . . . . 11 (((𝜑𝑝 ∈ ℙ) ∧ ¬ (𝑝𝐾 ∧ ¬ 𝑝𝑀)) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0))
180173, 179pm2.61dan 796 . . . . . . . . . 10 ((𝜑𝑝 ∈ ℙ) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0))
18159adantr 466 . . . . . . . . . . 11 ((𝜑𝑝 ∈ ℙ) → ∀𝑛 ∈ ℙ (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
18269adantr 466 . . . . . . . . . . 11 ((𝜑𝑝 ∈ ℙ) → 𝑀 ∈ ℕ)
183 simpr 471 . . . . . . . . . . 11 ((𝜑𝑝 ∈ ℙ) → 𝑝 ∈ ℙ)
184 oveq1 6799 . . . . . . . . . . 11 (𝑛 = 𝑝 → (𝑛 pCnt ((2 · 𝑁)C𝑁)) = (𝑝 pCnt ((2 · 𝑁)C𝑁)))
18589adantr 466 . . . . . . . . . . 11 ((𝜑𝑝 ∈ ℙ) → 𝐾 ∈ (ℤ𝑀))
18655, 181, 182, 183, 184, 185pcmpt2 15803 . . . . . . . . . 10 ((𝜑𝑝 ∈ ℙ) → (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) = if((𝑝𝐾 ∧ ¬ 𝑝𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0))
187 eqid 2770 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1))
188187prmorcht 25124 . . . . . . . . . . . . . . 15 (𝐾 ∈ ℕ → (exp‘(θ‘𝐾)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾))
18996, 188syl 17 . . . . . . . . . . . . . 14 (𝜑 → (exp‘(θ‘𝐾)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾))
190187prmorcht 25124 . . . . . . . . . . . . . . 15 (𝑀 ∈ ℕ → (exp‘(θ‘𝑀)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀))
19169, 190syl 17 . . . . . . . . . . . . . 14 (𝜑 → (exp‘(θ‘𝑀)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀))
192189, 191oveq12d 6810 . . . . . . . . . . . . 13 (𝜑 → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) = ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾) / (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀)))
193192adantr 466 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ ℙ) → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) = ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾) / (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀)))
194193oveq2d 6808 . . . . . . . . . . 11 ((𝜑𝑝 ∈ ℙ) → (𝑝 pCnt ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))) = (𝑝 pCnt ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾) / (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀))))
195 nncn 11229 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
196195exp1d 13209 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (𝑛↑1) = 𝑛)
197196ifeq1d 4241 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → if(𝑛 ∈ ℙ, (𝑛↑1), 1) = if(𝑛 ∈ ℙ, 𝑛, 1))
198197mpteq2ia 4872 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑1), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1))
199198eqcomi 2779 . . . . . . . . . . . 12 (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑1), 1))
200 1nn0 11509 . . . . . . . . . . . . . . 15 1 ∈ ℕ0
201200a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℙ) → 1 ∈ ℕ0)
202201ralrimiva 3114 . . . . . . . . . . . . 13 (𝜑 → ∀𝑛 ∈ ℙ 1 ∈ ℕ0)
203202adantr 466 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ ℙ) → ∀𝑛 ∈ ℙ 1 ∈ ℕ0)
204 eqidd 2771 . . . . . . . . . . . 12 (𝑛 = 𝑝 → 1 = 1)
205199, 203, 182, 183, 204, 185pcmpt2 15803 . . . . . . . . . . 11 ((𝜑𝑝 ∈ ℙ) → (𝑝 pCnt ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾) / (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀))) = if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0))
206194, 205eqtrd 2804 . . . . . . . . . 10 ((𝜑𝑝 ∈ ℙ) → (𝑝 pCnt ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))) = if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0))
207180, 186, 2063brtr4d 4816 . . . . . . . . 9 ((𝜑𝑝 ∈ ℙ) → (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) ≤ (𝑝 pCnt ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))))
208207ralrimiva 3114 . . . . . . . 8 (𝜑 → ∀𝑝 ∈ ℙ (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) ≤ (𝑝 pCnt ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))))
209 pc2dvds 15789 . . . . . . . . 9 ((((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ ∧ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℤ) → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) ≤ (𝑝 pCnt ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))))))
210101, 118, 209syl2anc 565 . . . . . . . 8 (𝜑 → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) ≤ (𝑝 pCnt ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))))))
211208, 210mpbird 247 . . . . . . 7 (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))))
212114nnred 11236 . . . . . . . . . 10 (𝜑 → (exp‘(θ‘𝐾)) ∈ ℝ)
213110nnred 11236 . . . . . . . . . 10 (𝜑 → (exp‘(θ‘𝑀)) ∈ ℝ)
214114nngt0d 11265 . . . . . . . . . 10 (𝜑 → 0 < (exp‘(θ‘𝐾)))
215110nngt0d 11265 . . . . . . . . . 10 (𝜑 → 0 < (exp‘(θ‘𝑀)))
216212, 213, 214, 215divgt0d 11160 . . . . . . . . 9 (𝜑 → 0 < ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))))
217 elnnz 11588 . . . . . . . . 9 (((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℕ ↔ (((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℤ ∧ 0 < ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))))
218118, 216, 217sylanbrc 564 . . . . . . . 8 (𝜑 → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℕ)
219 dvdsle 15240 . . . . . . . 8 ((((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ ∧ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℕ) → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ≤ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))))
220101, 218, 219syl2anc 565 . . . . . . 7 (𝜑 → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ≤ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))))
221211, 220mpd 15 . . . . . 6 (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ≤ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))))
222 nndivre 11257 . . . . . . . 8 (((exp‘(θ‘𝐾)) ∈ ℝ ∧ 4 ∈ ℕ) → ((exp‘(θ‘𝐾)) / 4) ∈ ℝ)
223212, 1, 222sylancl 566 . . . . . . 7 (𝜑 → ((exp‘(θ‘𝐾)) / 4) ∈ ℝ)
224 4re 11298 . . . . . . . . . 10 4 ∈ ℝ
225224a1i 11 . . . . . . . . 9 (𝜑 → 4 ∈ ℝ)
226 6re 11302 . . . . . . . . . 10 6 ∈ ℝ
227226a1i 11 . . . . . . . . 9 (𝜑 → 6 ∈ ℝ)
228 4lt6 11406 . . . . . . . . . 10 4 < 6
229228a1i 11 . . . . . . . . 9 (𝜑 → 4 < 6)
230 cht3 25119 . . . . . . . . . . . 12 (θ‘3) = (log‘6)
231230fveq2i 6335 . . . . . . . . . . 11 (exp‘(θ‘3)) = (exp‘(log‘6))
232 6pos 11320 . . . . . . . . . . . . 13 0 < 6
233226, 232elrpii 12037 . . . . . . . . . . . 12 6 ∈ ℝ+
234 reeflog 24547 . . . . . . . . . . . 12 (6 ∈ ℝ+ → (exp‘(log‘6)) = 6)
235233, 234ax-mp 5 . . . . . . . . . . 11 (exp‘(log‘6)) = 6
236231, 235eqtri 2792 . . . . . . . . . 10 (exp‘(θ‘3)) = 6
237 3re 11295 . . . . . . . . . . . . 13 3 ∈ ℝ
238237a1i 11 . . . . . . . . . . . 12 (𝜑 → 3 ∈ ℝ)
239 eluzle 11900 . . . . . . . . . . . . 13 (𝑀 ∈ (ℤ‘3) → 3 ≤ 𝑀)
24067, 239syl 17 . . . . . . . . . . . 12 (𝜑 → 3 ≤ 𝑀)
241 chtwordi 25102 . . . . . . . . . . . 12 ((3 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 3 ≤ 𝑀) → (θ‘3) ≤ (θ‘𝑀))
242238, 103, 240, 241syl3anc 1475 . . . . . . . . . . 11 (𝜑 → (θ‘3) ≤ (θ‘𝑀))
243 chtcl 25055 . . . . . . . . . . . . 13 (3 ∈ ℝ → (θ‘3) ∈ ℝ)
244237, 243ax-mp 5 . . . . . . . . . . . 12 (θ‘3) ∈ ℝ
245 chtcl 25055 . . . . . . . . . . . . 13 (𝑀 ∈ ℝ → (θ‘𝑀) ∈ ℝ)
246103, 245syl 17 . . . . . . . . . . . 12 (𝜑 → (θ‘𝑀) ∈ ℝ)
247 efle 15053 . . . . . . . . . . . 12 (((θ‘3) ∈ ℝ ∧ (θ‘𝑀) ∈ ℝ) → ((θ‘3) ≤ (θ‘𝑀) ↔ (exp‘(θ‘3)) ≤ (exp‘(θ‘𝑀))))
248244, 246, 247sylancr 567 . . . . . . . . . . 11 (𝜑 → ((θ‘3) ≤ (θ‘𝑀) ↔ (exp‘(θ‘3)) ≤ (exp‘(θ‘𝑀))))
249242, 248mpbid 222 . . . . . . . . . 10 (𝜑 → (exp‘(θ‘3)) ≤ (exp‘(θ‘𝑀)))
250236, 249syl5eqbrr 4820 . . . . . . . . 9 (𝜑 → 6 ≤ (exp‘(θ‘𝑀)))
251225, 227, 213, 229, 250ltletrd 10398 . . . . . . . 8 (𝜑 → 4 < (exp‘(θ‘𝑀)))
252 4pos 11317 . . . . . . . . . 10 0 < 4
253252a1i 11 . . . . . . . . 9 (𝜑 → 0 < 4)
254 ltdiv2 11110 . . . . . . . . 9 (((4 ∈ ℝ ∧ 0 < 4) ∧ ((exp‘(θ‘𝑀)) ∈ ℝ ∧ 0 < (exp‘(θ‘𝑀))) ∧ ((exp‘(θ‘𝐾)) ∈ ℝ ∧ 0 < (exp‘(θ‘𝐾)))) → (4 < (exp‘(θ‘𝑀)) ↔ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) < ((exp‘(θ‘𝐾)) / 4)))
255225, 253, 213, 215, 212, 214, 254syl222anc 1491 . . . . . . . 8 (𝜑 → (4 < (exp‘(θ‘𝑀)) ↔ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) < ((exp‘(θ‘𝐾)) / 4)))
256251, 255mpbid 222 . . . . . . 7 (𝜑 → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) < ((exp‘(θ‘𝐾)) / 4))
25726a1i 11 . . . . . . . . . . . . 13 (𝜑 → 2 ∈ ℝ)
258 2lt3 11396 . . . . . . . . . . . . . 14 2 < 3
259258a1i 11 . . . . . . . . . . . . 13 (𝜑 → 2 < 3)
260238, 103, 104, 240, 106letrd 10395 . . . . . . . . . . . . 13 (𝜑 → 3 ≤ 𝐾)
261257, 238, 104, 259, 260ltletrd 10398 . . . . . . . . . . . 12 (𝜑 → 2 < 𝐾)
262 chtub 25157 . . . . . . . . . . . 12 ((𝐾 ∈ ℝ ∧ 2 < 𝐾) → (θ‘𝐾) < ((log‘2) · ((2 · 𝐾) − 3)))
263104, 261, 262syl2anc 565 . . . . . . . . . . 11 (𝜑 → (θ‘𝐾) < ((log‘2) · ((2 · 𝐾) − 3)))
264 chtcl 25055 . . . . . . . . . . . . 13 (𝐾 ∈ ℝ → (θ‘𝐾) ∈ ℝ)
265104, 264syl 17 . . . . . . . . . . . 12 (𝜑 → (θ‘𝐾) ∈ ℝ)
266 relogcl 24542 . . . . . . . . . . . . . 14 (2 ∈ ℝ+ → (log‘2) ∈ ℝ)
26731, 266ax-mp 5 . . . . . . . . . . . . 13 (log‘2) ∈ ℝ
26823nnzi 11602 . . . . . . . . . . . . . . 15 3 ∈ ℤ
269 zsubcl 11620 . . . . . . . . . . . . . . 15 (((2 · 𝐾) ∈ ℤ ∧ 3 ∈ ℤ) → ((2 · 𝐾) − 3) ∈ ℤ)
27078, 268, 269sylancl 566 . . . . . . . . . . . . . 14 (𝜑 → ((2 · 𝐾) − 3) ∈ ℤ)
271270zred 11683 . . . . . . . . . . . . 13 (𝜑 → ((2 · 𝐾) − 3) ∈ ℝ)
272 remulcl 10222 . . . . . . . . . . . . 13 (((log‘2) ∈ ℝ ∧ ((2 · 𝐾) − 3) ∈ ℝ) → ((log‘2) · ((2 · 𝐾) − 3)) ∈ ℝ)
273267, 271, 272sylancr 567 . . . . . . . . . . . 12 (𝜑 → ((log‘2) · ((2 · 𝐾) − 3)) ∈ ℝ)
274 eflt 15052 . . . . . . . . . . . 12 (((θ‘𝐾) ∈ ℝ ∧ ((log‘2) · ((2 · 𝐾) − 3)) ∈ ℝ) → ((θ‘𝐾) < ((log‘2) · ((2 · 𝐾) − 3)) ↔ (exp‘(θ‘𝐾)) < (exp‘((log‘2) · ((2 · 𝐾) − 3)))))
275265, 273, 274syl2anc 565 . . . . . . . . . . 11 (𝜑 → ((θ‘𝐾) < ((log‘2) · ((2 · 𝐾) − 3)) ↔ (exp‘(θ‘𝐾)) < (exp‘((log‘2) · ((2 · 𝐾) − 3)))))
276263, 275mpbid 222 . . . . . . . . . 10 (𝜑 → (exp‘(θ‘𝐾)) < (exp‘((log‘2) · ((2 · 𝐾) − 3))))
277 reexplog 24561 . . . . . . . . . . . 12 ((2 ∈ ℝ+ ∧ ((2 · 𝐾) − 3) ∈ ℤ) → (2↑((2 · 𝐾) − 3)) = (exp‘(((2 · 𝐾) − 3) · (log‘2))))
27831, 270, 277sylancr 567 . . . . . . . . . . 11 (𝜑 → (2↑((2 · 𝐾) − 3)) = (exp‘(((2 · 𝐾) − 3) · (log‘2))))
279270zcnd 11684 . . . . . . . . . . . . 13 (𝜑 → ((2 · 𝐾) − 3) ∈ ℂ)
280267recni 10253 . . . . . . . . . . . . 13 (log‘2) ∈ ℂ
281 mulcom 10223 . . . . . . . . . . . . 13 ((((2 · 𝐾) − 3) ∈ ℂ ∧ (log‘2) ∈ ℂ) → (((2 · 𝐾) − 3) · (log‘2)) = ((log‘2) · ((2 · 𝐾) − 3)))
282279, 280, 281sylancl 566 . . . . . . . . . . . 12 (𝜑 → (((2 · 𝐾) − 3) · (log‘2)) = ((log‘2) · ((2 · 𝐾) − 3)))
283282fveq2d 6336 . . . . . . . . . . 11 (𝜑 → (exp‘(((2 · 𝐾) − 3) · (log‘2))) = (exp‘((log‘2) · ((2 · 𝐾) − 3))))
284278, 283eqtrd 2804 . . . . . . . . . 10 (𝜑 → (2↑((2 · 𝐾) − 3)) = (exp‘((log‘2) · ((2 · 𝐾) − 3))))
285276, 284breqtrrd 4812 . . . . . . . . 9 (𝜑 → (exp‘(θ‘𝐾)) < (2↑((2 · 𝐾) − 3)))
286 3p2e5 11361 . . . . . . . . . . . . . . . 16 (3 + 2) = 5
287286oveq1i 6802 . . . . . . . . . . . . . . 15 ((3 + 2) − 2) = (5 − 2)
288 3cn 11296 . . . . . . . . . . . . . . . 16 3 ∈ ℂ
289 2cn 11292 . . . . . . . . . . . . . . . 16 2 ∈ ℂ
290288, 289pncan3oi 10498 . . . . . . . . . . . . . . 15 ((3 + 2) − 2) = 3
291287, 290eqtr3i 2794 . . . . . . . . . . . . . 14 (5 − 2) = 3
292291oveq2i 6803 . . . . . . . . . . . . 13 ((2 · 𝐾) − (5 − 2)) = ((2 · 𝐾) − 3)
29378zcnd 11684 . . . . . . . . . . . . . 14 (𝜑 → (2 · 𝐾) ∈ ℂ)
294 5cn 11301 . . . . . . . . . . . . . . 15 5 ∈ ℂ
295 subsub 10512 . . . . . . . . . . . . . . 15 (((2 · 𝐾) ∈ ℂ ∧ 5 ∈ ℂ ∧ 2 ∈ ℂ) → ((2 · 𝐾) − (5 − 2)) = (((2 · 𝐾) − 5) + 2))
296294, 289, 295mp3an23 1563 . . . . . . . . . . . . . 14 ((2 · 𝐾) ∈ ℂ → ((2 · 𝐾) − (5 − 2)) = (((2 · 𝐾) − 5) + 2))
297293, 296syl 17 . . . . . . . . . . . . 13 (𝜑 → ((2 · 𝐾) − (5 − 2)) = (((2 · 𝐾) − 5) + 2))
298292, 297syl5eqr 2818 . . . . . . . . . . . 12 (𝜑 → ((2 · 𝐾) − 3) = (((2 · 𝐾) − 5) + 2))
299298oveq2d 6808 . . . . . . . . . . 11 (𝜑 → (2↑𝑐((2 · 𝐾) − 3)) = (2↑𝑐(((2 · 𝐾) − 5) + 2)))
300 2ne0 11314 . . . . . . . . . . . . 13 2 ≠ 0
301 cxpexpz 24633 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ 2 ≠ 0 ∧ ((2 · 𝐾) − 3) ∈ ℤ) → (2↑𝑐((2 · 𝐾) − 3)) = (2↑((2 · 𝐾) − 3)))
302289, 300, 301mp3an12 1561 . . . . . . . . . . . 12 (((2 · 𝐾) − 3) ∈ ℤ → (2↑𝑐((2 · 𝐾) − 3)) = (2↑((2 · 𝐾) − 3)))
303270, 302syl 17 . . . . . . . . . . 11 (𝜑 → (2↑𝑐((2 · 𝐾) − 3)) = (2↑((2 · 𝐾) − 3)))
30481zcnd 11684 . . . . . . . . . . . 12 (𝜑 → ((2 · 𝐾) − 5) ∈ ℂ)
305 2cnne0 11443 . . . . . . . . . . . . 13 (2 ∈ ℂ ∧ 2 ≠ 0)
306 cxpadd 24645 . . . . . . . . . . . . 13 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ ((2 · 𝐾) − 5) ∈ ℂ ∧ 2 ∈ ℂ) → (2↑𝑐(((2 · 𝐾) − 5) + 2)) = ((2↑𝑐((2 · 𝐾) − 5)) · (2↑𝑐2)))
307305, 289, 306mp3an13 1562 . . . . . . . . . . . 12 (((2 · 𝐾) − 5) ∈ ℂ → (2↑𝑐(((2 · 𝐾) − 5) + 2)) = ((2↑𝑐((2 · 𝐾) − 5)) · (2↑𝑐2)))
308304, 307syl 17 . . . . . . . . . . 11 (𝜑 → (2↑𝑐(((2 · 𝐾) − 5) + 2)) = ((2↑𝑐((2 · 𝐾) − 5)) · (2↑𝑐2)))
309299, 303, 3083eqtr3d 2812 . . . . . . . . . 10 (𝜑 → (2↑((2 · 𝐾) − 3)) = ((2↑𝑐((2 · 𝐾) − 5)) · (2↑𝑐2)))
310 2nn0 11510 . . . . . . . . . . . . 13 2 ∈ ℕ0
311 cxpexp 24634 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ 2 ∈ ℕ0) → (2↑𝑐2) = (2↑2))
312289, 310, 311mp2an 664 . . . . . . . . . . . 12 (2↑𝑐2) = (2↑2)
313 sq2 13166 . . . . . . . . . . . 12 (2↑2) = 4
314312, 313eqtri 2792 . . . . . . . . . . 11 (2↑𝑐2) = 4
315314oveq2i 6803 . . . . . . . . . 10 ((2↑𝑐((2 · 𝐾) − 5)) · (2↑𝑐2)) = ((2↑𝑐((2 · 𝐾) − 5)) · 4)
316309, 315syl6eq 2820 . . . . . . . . 9 (𝜑 → (2↑((2 · 𝐾) − 3)) = ((2↑𝑐((2 · 𝐾) − 5)) · 4))
317285, 316breqtrd 4810 . . . . . . . 8 (𝜑 → (exp‘(θ‘𝐾)) < ((2↑𝑐((2 · 𝐾) − 5)) · 4))
318224, 252pm3.2i 447 . . . . . . . . . 10 (4 ∈ ℝ ∧ 0 < 4)
319318a1i 11 . . . . . . . . 9 (𝜑 → (4 ∈ ℝ ∧ 0 < 4))
320 ltdivmul2 11101 . . . . . . . . 9 (((exp‘(θ‘𝐾)) ∈ ℝ ∧ (2↑𝑐((2 · 𝐾) − 5)) ∈ ℝ ∧ (4 ∈ ℝ ∧ 0 < 4)) → (((exp‘(θ‘𝐾)) / 4) < (2↑𝑐((2 · 𝐾) − 5)) ↔ (exp‘(θ‘𝐾)) < ((2↑𝑐((2 · 𝐾) − 5)) · 4)))
321212, 85, 319, 320syl3anc 1475 . . . . . . . 8 (𝜑 → (((exp‘(θ‘𝐾)) / 4) < (2↑𝑐((2 · 𝐾) − 5)) ↔ (exp‘(θ‘𝐾)) < ((2↑𝑐((2 · 𝐾) − 5)) · 4)))
322317, 321mpbird 247 . . . . . . 7 (𝜑 → ((exp‘(θ‘𝐾)) / 4) < (2↑𝑐((2 · 𝐾) − 5)))
323119, 223, 85, 256, 322lttrd 10399 . . . . . 6 (𝜑 → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) < (2↑𝑐((2 · 𝐾) − 5)))
324102, 119, 85, 221, 323lelttrd 10396 . . . . 5 (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) < (2↑𝑐((2 · 𝐾) − 5)))
32597nnred 11236 . . . . . 6 (𝜑 → (seq1( · , 𝐹)‘𝐾) ∈ ℝ)
326 nnre 11228 . . . . . . . 8 ((seq1( · , 𝐹)‘𝑀) ∈ ℕ → (seq1( · , 𝐹)‘𝑀) ∈ ℝ)
327 nngt0 11250 . . . . . . . 8 ((seq1( · , 𝐹)‘𝑀) ∈ ℕ → 0 < (seq1( · , 𝐹)‘𝑀))
328326, 327jca 495 . . . . . . 7 ((seq1( · , 𝐹)‘𝑀) ∈ ℕ → ((seq1( · , 𝐹)‘𝑀) ∈ ℝ ∧ 0 < (seq1( · , 𝐹)‘𝑀)))
32970, 328syl 17 . . . . . 6 (𝜑 → ((seq1( · , 𝐹)‘𝑀) ∈ ℝ ∧ 0 < (seq1( · , 𝐹)‘𝑀)))
330 ltdivmul 11099 . . . . . 6 (((seq1( · , 𝐹)‘𝐾) ∈ ℝ ∧ (2↑𝑐((2 · 𝐾) − 5)) ∈ ℝ ∧ ((seq1( · , 𝐹)‘𝑀) ∈ ℝ ∧ 0 < (seq1( · , 𝐹)‘𝑀))) → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) < (2↑𝑐((2 · 𝐾) − 5)) ↔ (seq1( · , 𝐹)‘𝐾) < ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2 · 𝐾) − 5)))))
331325, 85, 329, 330syl3anc 1475 . . . . 5 (𝜑 → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) < (2↑𝑐((2 · 𝐾) − 5)) ↔ (seq1( · , 𝐹)‘𝐾) < ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2 · 𝐾) − 5)))))
332324, 331mpbid 222 . . . 4 (𝜑 → (seq1( · , 𝐹)‘𝐾) < ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2 · 𝐾) − 5))))
33387, 332eqbrtrrd 4808 . . 3 (𝜑 → ((2 · 𝑁)C𝑁) < ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2 · 𝐾) − 5))))
33430, 85remulcld 10271 . . . 4 (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐((2 · 𝐾) − 5))) ∈ ℝ)
3353, 62, 55, 63, 64bposlem5 25233 . . . . 5 (𝜑 → (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)))
33671, 30, 84lemul1d 12117 . . . . 5 (𝜑 → ((seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) ↔ ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2 · 𝐾) − 5))) ≤ (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐((2 · 𝐾) − 5)))))
337335, 336mpbid 222 . . . 4 (𝜑 → ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2 · 𝐾) − 5))) ≤ (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐((2 · 𝐾) − 5))))
33878zred 11683 . . . . . . 7 (𝜑 → (2 · 𝐾) ∈ ℝ)
33937a1i 11 . . . . . . 7 (𝜑 → 5 ∈ ℝ)
340 flle 12807 . . . . . . . . . . 11 (((2 · 𝑁) / 3) ∈ ℝ → (⌊‘((2 · 𝑁) / 3)) ≤ ((2 · 𝑁) / 3))
34174, 340syl 17 . . . . . . . . . 10 (𝜑 → (⌊‘((2 · 𝑁) / 3)) ≤ ((2 · 𝑁) / 3))
34263, 341syl5eqbr 4819 . . . . . . . . 9 (𝜑𝐾 ≤ ((2 · 𝑁) / 3))
343 2pos 11313 . . . . . . . . . . . 12 0 < 2
34426, 343pm3.2i 447 . . . . . . . . . . 11 (2 ∈ ℝ ∧ 0 < 2)
345344a1i 11 . . . . . . . . . 10 (𝜑 → (2 ∈ ℝ ∧ 0 < 2))
346 lemul2 11077 . . . . . . . . . 10 ((𝐾 ∈ ℝ ∧ ((2 · 𝑁) / 3) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝐾 ≤ ((2 · 𝑁) / 3) ↔ (2 · 𝐾) ≤ (2 · ((2 · 𝑁) / 3))))
347104, 74, 345, 346syl3anc 1475 . . . . . . . . 9 (𝜑 → (𝐾 ≤ ((2 · 𝑁) / 3) ↔ (2 · 𝐾) ≤ (2 · ((2 · 𝑁) / 3))))
348342, 347mpbid 222 . . . . . . . 8 (𝜑 → (2 · 𝐾) ≤ (2 · ((2 · 𝑁) / 3)))
34918nncnd 11237 . . . . . . . . . 10 (𝜑 → (2 · 𝑁) ∈ ℂ)
350 3ne0 11316 . . . . . . . . . . . 12 3 ≠ 0
351288, 350pm3.2i 447 . . . . . . . . . . 11 (3 ∈ ℂ ∧ 3 ≠ 0)
352 divass 10904 . . . . . . . . . . 11 ((2 ∈ ℂ ∧ (2 · 𝑁) ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((2 · (2 · 𝑁)) / 3) = (2 · ((2 · 𝑁) / 3)))
353289, 351, 352mp3an13 1562 . . . . . . . . . 10 ((2 · 𝑁) ∈ ℂ → ((2 · (2 · 𝑁)) / 3) = (2 · ((2 · 𝑁) / 3)))
354349, 353syl 17 . . . . . . . . 9 (𝜑 → ((2 · (2 · 𝑁)) / 3) = (2 · ((2 · 𝑁) / 3)))
355 2t2e4 11378 . . . . . . . . . . . 12 (2 · 2) = 4
356355oveq1i 6802 . . . . . . . . . . 11 ((2 · 2) · 𝑁) = (4 · 𝑁)
3575nncnd 11237 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℂ)
358 mulass 10225 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((2 · 2) · 𝑁) = (2 · (2 · 𝑁)))
359289, 289, 358mp3an12 1561 . . . . . . . . . . . 12 (𝑁 ∈ ℂ → ((2 · 2) · 𝑁) = (2 · (2 · 𝑁)))
360357, 359syl 17 . . . . . . . . . . 11 (𝜑 → ((2 · 2) · 𝑁) = (2 · (2 · 𝑁)))
361356, 360syl5reqr 2819 . . . . . . . . . 10 (𝜑 → (2 · (2 · 𝑁)) = (4 · 𝑁))
362361oveq1d 6807 . . . . . . . . 9 (𝜑 → ((2 · (2 · 𝑁)) / 3) = ((4 · 𝑁) / 3))
363354, 362eqtr3d 2806 . . . . . . . 8 (𝜑 → (2 · ((2 · 𝑁) / 3)) = ((4 · 𝑁) / 3))
364348, 363breqtrd 4810 . . . . . . 7 (𝜑 → (2 · 𝐾) ≤ ((4 · 𝑁) / 3))
365338, 36, 339, 364lesub1dd 10844 . . . . . 6 (𝜑 → ((2 · 𝐾) − 5) ≤ (((4 · 𝑁) / 3) − 5))
366 1lt2 11395 . . . . . . . 8 1 < 2
367366a1i 11 . . . . . . 7 (𝜑 → 1 < 2)
368257, 367, 82, 39cxpled 24686 . . . . . 6 (𝜑 → (((2 · 𝐾) − 5) ≤ (((4 · 𝑁) / 3) − 5) ↔ (2↑𝑐((2 · 𝐾) − 5)) ≤ (2↑𝑐(((4 · 𝑁) / 3) − 5))))
369365, 368mpbid 222 . . . . 5 (𝜑 → (2↑𝑐((2 · 𝐾) − 5)) ≤ (2↑𝑐(((4 · 𝑁) / 3) − 5)))
37085, 42, 29lemul2d 12118 . . . . 5 (𝜑 → ((2↑𝑐((2 · 𝐾) − 5)) ≤ (2↑𝑐(((4 · 𝑁) / 3) − 5)) ↔ (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐((2 · 𝐾) − 5))) ≤ (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5)))))
371369, 370mpbid 222 . . . 4 (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐((2 · 𝐾) − 5))) ≤ (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))))
37286, 334, 43, 337, 371letrd 10395 . . 3 (𝜑 → ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2 · 𝐾) − 5))) ≤ (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))))
37315, 86, 43, 333, 372ltletrd 10398 . 2 (𝜑 → ((2 · 𝑁)C𝑁) < (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))))
37410, 15, 43, 54, 373lttrd 10399 1 (𝜑 → ((4↑𝑁) / 𝑁) < (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382   = wceq 1630  wcel 2144  wne 2942  wral 3060  wrex 3061  ifcif 4223   class class class wbr 4784  cmpt 4861  wf 6027  cfv 6031  (class class class)co 6792  cc 10135  cr 10136  0cc0 10137  1c1 10138   + caddc 10140   · cmul 10142   < clt 10275  cle 10276  cmin 10467   / cdiv 10885  cn 11221  2c2 11271  3c3 11272  4c4 11273  5c5 11274  6c6 11275  0cn0 11493  cz 11578  cuz 11887  +crp 12034  ...cfz 12532  cfl 12798  seqcseq 13007  cexp 13066  Ccbc 13292  csqrt 14180  expce 14997  cdvds 15188  cprime 15591   pCnt cpc 15747  logclog 24521  𝑐ccxp 24522  θccht 25037
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-8 2146  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-rep 4902  ax-sep 4912  ax-nul 4920  ax-pow 4971  ax-pr 5034  ax-un 7095  ax-inf2 8701  ax-cnex 10193  ax-resscn 10194  ax-1cn 10195  ax-icn 10196  ax-addcl 10197  ax-addrcl 10198  ax-mulcl 10199  ax-mulrcl 10200  ax-mulcom 10201  ax-addass 10202  ax-mulass 10203  ax-distr 10204  ax-i2m1 10205  ax-1ne0 10206  ax-1rid 10207  ax-rnegex 10208  ax-rrecex 10209  ax-cnre 10210  ax-pre-lttri 10211  ax-pre-lttrn 10212  ax-pre-ltadd 10213  ax-pre-mulgt0 10214  ax-pre-sup 10215  ax-addf 10216  ax-mulf 10217
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1071  df-3an 1072  df-tru 1633  df-fal 1636  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-nel 3046  df-ral 3065  df-rex 3066  df-reu 3067  df-rmo 3068  df-rab 3069  df-v 3351  df-sbc 3586  df-csb 3681  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-pss 3737  df-nul 4062  df-if 4224  df-pw 4297  df-sn 4315  df-pr 4317  df-tp 4319  df-op 4321  df-uni 4573  df-int 4610  df-iun 4654  df-iin 4655  df-br 4785  df-opab 4845  df-mpt 4862  df-tr 4885  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6753  df-ov 6795  df-oprab 6796  df-mpt2 6797  df-of 7043  df-om 7212  df-1st 7314  df-2nd 7315  df-supp 7446  df-wrecs 7558  df-recs 7620  df-rdg 7658  df-1o 7712  df-2o 7713  df-oadd 7716  df-er 7895  df-map 8010  df-pm 8011  df-ixp 8062  df-en 8109  df-dom 8110  df-sdom 8111  df-fin 8112  df-fsupp 8431  df-fi 8472  df-sup 8503  df-inf 8504  df-oi 8570  df-card 8964  df-cda 9191  df-pnf 10277  df-mnf 10278  df-xr 10279  df-ltxr 10280  df-le 10281  df-sub 10469  df-neg 10470  df-div 10886  df-nn 11222  df-2 11280  df-3 11281  df-4 11282  df-5 11283  df-6 11284  df-7 11285  df-8 11286  df-9 11287  df-n0 11494  df-xnn0 11565  df-z 11579  df-dec 11695  df-uz 11888  df-q 11991  df-rp 12035  df-xneg 12150  df-xadd 12151  df-xmul 12152  df-ioo 12383  df-ioc 12384  df-ico 12385  df-icc 12386  df-fz 12533  df-fzo 12673  df-fl 12800  df-mod 12876  df-seq 13008  df-exp 13067  df-fac 13264  df-bc 13293  df-hash 13321  df-shft 14014  df-cj 14046  df-re 14047  df-im 14048  df-sqrt 14182  df-abs 14183  df-limsup 14409  df-clim 14426  df-rlim 14427  df-sum 14624  df-ef 15003  df-sin 15005  df-cos 15006  df-pi 15008  df-dvds 15189  df-gcd 15424  df-prm 15592  df-pc 15748  df-struct 16065  df-ndx 16066  df-slot 16067  df-base 16069  df-sets 16070  df-ress 16071  df-plusg 16161  df-mulr 16162  df-starv 16163  df-sca 16164  df-vsca 16165  df-ip 16166  df-tset 16167  df-ple 16168  df-ds 16171  df-unif 16172  df-hom 16173  df-cco 16174  df-rest 16290  df-topn 16291  df-0g 16309  df-gsum 16310  df-topgen 16311  df-pt 16312  df-prds 16315  df-xrs 16369  df-qtop 16374  df-imas 16375  df-xps 16377  df-mre 16453  df-mrc 16454  df-acs 16456  df-mgm 17449  df-sgrp 17491  df-mnd 17502  df-submnd 17543  df-mulg 17748  df-cntz 17956  df-cmn 18401  df-psmet 19952  df-xmet 19953  df-met 19954  df-bl 19955  df-mopn 19956  df-fbas 19957  df-fg 19958  df-cnfld 19961  df-top 20918  df-topon 20935  df-topsp 20957  df-bases 20970  df-cld 21043  df-ntr 21044  df-cls 21045  df-nei 21122  df-lp 21160  df-perf 21161  df-cn 21251  df-cnp 21252  df-haus 21339  df-tx 21585  df-hmeo 21778  df-fil 21869  df-fm 21961  df-flim 21962  df-flf 21963  df-xms 22344  df-ms 22345  df-tms 22346  df-cncf 22900  df-limc 23849  df-dv 23850  df-log 24523  df-cxp 24524  df-cht 25043  df-ppi 25046
This theorem is referenced by:  bposlem9  25237
  Copyright terms: Public domain W3C validator