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

Theorem bposlem6 27347
Description: Lemma for bpos 27351. 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 12346 . . . . 5 4 ∈ ℕ
2 5nn 12349 . . . . . . 7 5 ∈ ℕ
3 bpos.1 . . . . . . 7 (𝜑𝑁 ∈ (ℤ‘5))
4 eluznn 12957 . . . . . . 7 ((5 ∈ ℕ ∧ 𝑁 ∈ (ℤ‘5)) → 𝑁 ∈ ℕ)
52, 3, 4sylancr 587 . . . . . 6 (𝜑𝑁 ∈ ℕ)
65nnnn0d 12584 . . . . 5 (𝜑𝑁 ∈ ℕ0)
7 nnexpcl 14111 . . . . 5 ((4 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (4↑𝑁) ∈ ℕ)
81, 6, 7sylancr 587 . . . 4 (𝜑 → (4↑𝑁) ∈ ℕ)
98nnred 12278 . . 3 (𝜑 → (4↑𝑁) ∈ ℝ)
109, 5nndivred 12317 . 2 (𝜑 → ((4↑𝑁) / 𝑁) ∈ ℝ)
11 fzctr 13676 . . . . 5 (𝑁 ∈ ℕ0𝑁 ∈ (0...(2 · 𝑁)))
126, 11syl 17 . . . 4 (𝜑𝑁 ∈ (0...(2 · 𝑁)))
13 bccl2 14358 . . . 4 (𝑁 ∈ (0...(2 · 𝑁)) → ((2 · 𝑁)C𝑁) ∈ ℕ)
1412, 13syl 17 . . 3 (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℕ)
1514nnred 12278 . 2 (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℝ)
16 2nn 12336 . . . . . . 7 2 ∈ ℕ
17 nnmulcl 12287 . . . . . . 7 ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
1816, 5, 17sylancr 587 . . . . . 6 (𝜑 → (2 · 𝑁) ∈ ℕ)
1918nnrpd 13072 . . . . 5 (𝜑 → (2 · 𝑁) ∈ ℝ+)
2018nnred 12278 . . . . . . . 8 (𝜑 → (2 · 𝑁) ∈ ℝ)
2119rpge0d 13078 . . . . . . . 8 (𝜑 → 0 ≤ (2 · 𝑁))
2220, 21resqrtcld 15452 . . . . . . 7 (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ)
23 3nn 12342 . . . . . . 7 3 ∈ ℕ
24 nndivre 12304 . . . . . . 7 (((√‘(2 · 𝑁)) ∈ ℝ ∧ 3 ∈ ℕ) → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
2522, 23, 24sylancl 586 . . . . . 6 (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
26 2re 12337 . . . . . 6 2 ∈ ℝ
27 readdcl 11235 . . . . . 6 ((((√‘(2 · 𝑁)) / 3) ∈ ℝ ∧ 2 ∈ ℝ) → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
2825, 26, 27sylancl 586 . . . . 5 (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
2919, 28rpcxpcld 26789 . . . 4 (𝜑 → ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) ∈ ℝ+)
3029rpred 13074 . . 3 (𝜑 → ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) ∈ ℝ)
31 2rp 13036 . . . . 5 2 ∈ ℝ+
32 nnmulcl 12287 . . . . . . . . 9 ((4 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (4 · 𝑁) ∈ ℕ)
331, 5, 32sylancr 587 . . . . . . . 8 (𝜑 → (4 · 𝑁) ∈ ℕ)
3433nnred 12278 . . . . . . 7 (𝜑 → (4 · 𝑁) ∈ ℝ)
35 nndivre 12304 . . . . . . 7 (((4 · 𝑁) ∈ ℝ ∧ 3 ∈ ℕ) → ((4 · 𝑁) / 3) ∈ ℝ)
3634, 23, 35sylancl 586 . . . . . 6 (𝜑 → ((4 · 𝑁) / 3) ∈ ℝ)
37 5re 12350 . . . . . 6 5 ∈ ℝ
38 resubcl 11570 . . . . . 6 ((((4 · 𝑁) / 3) ∈ ℝ ∧ 5 ∈ ℝ) → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
3936, 37, 38sylancl 586 . . . . 5 (𝜑 → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
40 rpcxpcl 26732 . . . . 5 ((2 ∈ ℝ+ ∧ (((4 · 𝑁) / 3) − 5) ∈ ℝ) → (2↑𝑐(((4 · 𝑁) / 3) − 5)) ∈ ℝ+)
4131, 39, 40sylancr 587 . . . 4 (𝜑 → (2↑𝑐(((4 · 𝑁) / 3) − 5)) ∈ ℝ+)
4241rpred 13074 . . 3 (𝜑 → (2↑𝑐(((4 · 𝑁) / 3) − 5)) ∈ ℝ)
4330, 42remulcld 11288 . 2 (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))) ∈ ℝ)
44 df-5 12329 . . . . 5 5 = (4 + 1)
45 4z 12648 . . . . . 6 4 ∈ ℤ
46 uzid 12890 . . . . . 6 (4 ∈ ℤ → 4 ∈ (ℤ‘4))
47 peano2uz 12940 . . . . . 6 (4 ∈ (ℤ‘4) → (4 + 1) ∈ (ℤ‘4))
4845, 46, 47mp2b 10 . . . . 5 (4 + 1) ∈ (ℤ‘4)
4944, 48eqeltri 2834 . . . 4 5 ∈ (ℤ‘4)
50 eqid 2734 . . . . 5 (ℤ‘4) = (ℤ‘4)
5150uztrn2 12894 . . . 4 ((5 ∈ (ℤ‘4) ∧ 𝑁 ∈ (ℤ‘5)) → 𝑁 ∈ (ℤ‘4))
5249, 3, 51sylancr 587 . . 3 (𝜑𝑁 ∈ (ℤ‘4))
53 bclbnd 27338 . . 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 16882 . . . . . . . . . 10 ((𝑛 ∈ ℙ ∧ ((2 · 𝑁)C𝑁) ∈ ℕ) → (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
5856, 14, 57syl2anr 597 . . . . . . . . 9 ((𝜑𝑛 ∈ ℙ) → (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
5958ralrimiva 3143 . . . . . . . 8 (𝜑 → ∀𝑛 ∈ ℙ (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
6055, 59pcmptcl 16924 . . . . . . 7 (𝜑 → (𝐹:ℕ⟶ℕ ∧ seq1( · , 𝐹):ℕ⟶ℕ))
6160simprd 495 . . . . . 6 (𝜑 → seq1( · , 𝐹):ℕ⟶ℕ)
62 bpos.2 . . . . . . . . 9 (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)))
63 bpos.4 . . . . . . . . 9 𝐾 = (⌊‘((2 · 𝑁) / 3))
64 bpos.5 . . . . . . . . 9 𝑀 = (⌊‘(√‘(2 · 𝑁)))
653, 62, 55, 63, 64bposlem4 27345 . . . . . . . 8 (𝜑𝑀 ∈ (3...𝐾))
66 elfzuz 13556 . . . . . . . 8 (𝑀 ∈ (3...𝐾) → 𝑀 ∈ (ℤ‘3))
6765, 66syl 17 . . . . . . 7 (𝜑𝑀 ∈ (ℤ‘3))
68 eluznn 12957 . . . . . . 7 ((3 ∈ ℕ ∧ 𝑀 ∈ (ℤ‘3)) → 𝑀 ∈ ℕ)
6923, 67, 68sylancr 587 . . . . . 6 (𝜑𝑀 ∈ ℕ)
7061, 69ffvelcdmd 7104 . . . . 5 (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℕ)
7170nnred 12278 . . . 4 (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℝ)
72 2z 12646 . . . . . . . . 9 2 ∈ ℤ
73 nndivre 12304 . . . . . . . . . . . 12 (((2 · 𝑁) ∈ ℝ ∧ 3 ∈ ℕ) → ((2 · 𝑁) / 3) ∈ ℝ)
7420, 23, 73sylancl 586 . . . . . . . . . . 11 (𝜑 → ((2 · 𝑁) / 3) ∈ ℝ)
7574flcld 13834 . . . . . . . . . 10 (𝜑 → (⌊‘((2 · 𝑁) / 3)) ∈ ℤ)
7663, 75eqeltrid 2842 . . . . . . . . 9 (𝜑𝐾 ∈ ℤ)
77 zmulcl 12663 . . . . . . . . 9 ((2 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (2 · 𝐾) ∈ ℤ)
7872, 76, 77sylancr 587 . . . . . . . 8 (𝜑 → (2 · 𝐾) ∈ ℤ)
792nnzi 12638 . . . . . . . 8 5 ∈ ℤ
80 zsubcl 12656 . . . . . . . 8 (((2 · 𝐾) ∈ ℤ ∧ 5 ∈ ℤ) → ((2 · 𝐾) − 5) ∈ ℤ)
8178, 79, 80sylancl 586 . . . . . . 7 (𝜑 → ((2 · 𝐾) − 5) ∈ ℤ)
8281zred 12719 . . . . . 6 (𝜑 → ((2 · 𝐾) − 5) ∈ ℝ)
83 rpcxpcl 26732 . . . . . 6 ((2 ∈ ℝ+ ∧ ((2 · 𝐾) − 5) ∈ ℝ) → (2↑𝑐((2 · 𝐾) − 5)) ∈ ℝ+)
8431, 82, 83sylancr 587 . . . . 5 (𝜑 → (2↑𝑐((2 · 𝐾) − 5)) ∈ ℝ+)
8584rpred 13074 . . . 4 (𝜑 → (2↑𝑐((2 · 𝐾) − 5)) ∈ ℝ)
8671, 85remulcld 11288 . . 3 (𝜑 → ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2 · 𝐾) − 5))) ∈ ℝ)
873, 62, 55, 63bposlem3 27344 . . . 4 (𝜑 → (seq1( · , 𝐹)‘𝐾) = ((2 · 𝑁)C𝑁))
88 elfzuz3 13557 . . . . . . . . . 10 (𝑀 ∈ (3...𝐾) → 𝐾 ∈ (ℤ𝑀))
8965, 88syl 17 . . . . . . . . 9 (𝜑𝐾 ∈ (ℤ𝑀))
9055, 59, 69, 89pcmptdvds 16927 . . . . . . . 8 (𝜑 → (seq1( · , 𝐹)‘𝑀) ∥ (seq1( · , 𝐹)‘𝐾))
9170nnzd 12637 . . . . . . . . 9 (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℤ)
9270nnne0d 12313 . . . . . . . . 9 (𝜑 → (seq1( · , 𝐹)‘𝑀) ≠ 0)
93 uztrn 12893 . . . . . . . . . . . . 13 ((𝐾 ∈ (ℤ𝑀) ∧ 𝑀 ∈ (ℤ‘3)) → 𝐾 ∈ (ℤ‘3))
9489, 67, 93syl2anc 584 . . . . . . . . . . . 12 (𝜑𝐾 ∈ (ℤ‘3))
95 eluznn 12957 . . . . . . . . . . . 12 ((3 ∈ ℕ ∧ 𝐾 ∈ (ℤ‘3)) → 𝐾 ∈ ℕ)
9623, 94, 95sylancr 587 . . . . . . . . . . 11 (𝜑𝐾 ∈ ℕ)
9761, 96ffvelcdmd 7104 . . . . . . . . . 10 (𝜑 → (seq1( · , 𝐹)‘𝐾) ∈ ℕ)
9897nnzd 12637 . . . . . . . . 9 (𝜑 → (seq1( · , 𝐹)‘𝐾) ∈ ℤ)
99 dvdsval2 16289 . . . . . . . . 9 (((seq1( · , 𝐹)‘𝑀) ∈ ℤ ∧ (seq1( · , 𝐹)‘𝑀) ≠ 0 ∧ (seq1( · , 𝐹)‘𝐾) ∈ ℤ) → ((seq1( · , 𝐹)‘𝑀) ∥ (seq1( · , 𝐹)‘𝐾) ↔ ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ))
10091, 92, 98, 99syl3anc 1370 . . . . . . . 8 (𝜑 → ((seq1( · , 𝐹)‘𝑀) ∥ (seq1( · , 𝐹)‘𝐾) ↔ ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ))
10190, 100mpbid 232 . . . . . . 7 (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ)
102101zred 12719 . . . . . 6 (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℝ)
10369nnred 12278 . . . . . . . . 9 (𝜑𝑀 ∈ ℝ)
10476zred 12719 . . . . . . . . 9 (𝜑𝐾 ∈ ℝ)
105 eluzle 12888 . . . . . . . . . 10 (𝐾 ∈ (ℤ𝑀) → 𝑀𝐾)
10689, 105syl 17 . . . . . . . . 9 (𝜑𝑀𝐾)
107 efchtdvds 27216 . . . . . . . . 9 ((𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑀𝐾) → (exp‘(θ‘𝑀)) ∥ (exp‘(θ‘𝐾)))
108103, 104, 106, 107syl3anc 1370 . . . . . . . 8 (𝜑 → (exp‘(θ‘𝑀)) ∥ (exp‘(θ‘𝐾)))
109 efchtcl 27168 . . . . . . . . . . 11 (𝑀 ∈ ℝ → (exp‘(θ‘𝑀)) ∈ ℕ)
110103, 109syl 17 . . . . . . . . . 10 (𝜑 → (exp‘(θ‘𝑀)) ∈ ℕ)
111110nnzd 12637 . . . . . . . . 9 (𝜑 → (exp‘(θ‘𝑀)) ∈ ℤ)
112110nnne0d 12313 . . . . . . . . 9 (𝜑 → (exp‘(θ‘𝑀)) ≠ 0)
113 efchtcl 27168 . . . . . . . . . . 11 (𝐾 ∈ ℝ → (exp‘(θ‘𝐾)) ∈ ℕ)
114104, 113syl 17 . . . . . . . . . 10 (𝜑 → (exp‘(θ‘𝐾)) ∈ ℕ)
115114nnzd 12637 . . . . . . . . 9 (𝜑 → (exp‘(θ‘𝐾)) ∈ ℤ)
116 dvdsval2 16289 . . . . . . . . 9 (((exp‘(θ‘𝑀)) ∈ ℤ ∧ (exp‘(θ‘𝑀)) ≠ 0 ∧ (exp‘(θ‘𝐾)) ∈ ℤ) → ((exp‘(θ‘𝑀)) ∥ (exp‘(θ‘𝐾)) ↔ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℤ))
117111, 112, 115, 116syl3anc 1370 . . . . . . . 8 (𝜑 → ((exp‘(θ‘𝑀)) ∥ (exp‘(θ‘𝐾)) ↔ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℤ))
118108, 117mpbid 232 . . . . . . 7 (𝜑 → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℤ)
119118zred 12719 . . . . . 6 (𝜑 → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℝ)
120 prmz 16708 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
121 fllt 13842 . . . . . . . . . . . . . . . . . 18 (((√‘(2 · 𝑁)) ∈ ℝ ∧ 𝑝 ∈ ℤ) → ((√‘(2 · 𝑁)) < 𝑝 ↔ (⌊‘(√‘(2 · 𝑁))) < 𝑝))
12222, 120, 121syl2an 596 . . . . . . . . . . . . . . . . 17 ((𝜑𝑝 ∈ ℙ) → ((√‘(2 · 𝑁)) < 𝑝 ↔ (⌊‘(√‘(2 · 𝑁))) < 𝑝))
12364breq1i 5154 . . . . . . . . . . . . . . . . 17 (𝑀 < 𝑝 ↔ (⌊‘(√‘(2 · 𝑁))) < 𝑝)
124122, 123bitr4di 289 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 ∈ ℙ) → ((√‘(2 · 𝑁)) < 𝑝𝑀 < 𝑝))
125120zred 12719 . . . . . . . . . . . . . . . . 17 (𝑝 ∈ ℙ → 𝑝 ∈ ℝ)
126 ltnle 11337 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℝ ∧ 𝑝 ∈ ℝ) → (𝑀 < 𝑝 ↔ ¬ 𝑝𝑀))
127103, 125, 126syl2an 596 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 ∈ ℙ) → (𝑀 < 𝑝 ↔ ¬ 𝑝𝑀))
128124, 127bitrd 279 . . . . . . . . . . . . . . 15 ((𝜑𝑝 ∈ ℙ) → ((√‘(2 · 𝑁)) < 𝑝 ↔ ¬ 𝑝𝑀))
129 bposlem1 27342 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁))
1305, 129sylan 580 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁))
131125adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑝 ∈ ℙ) → 𝑝 ∈ ℝ)
132 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 ∈ ℙ → 𝑝 ∈ ℙ)
133 pccl 16882 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑝 ∈ ℙ ∧ ((2 · 𝑁)C𝑁) ∈ ℕ) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
134132, 14, 133syl2anr 597 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑝 ∈ ℙ) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
135131, 134reexpcld 14199 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ∈ ℝ)
13620adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑝 ∈ ℙ) → (2 · 𝑁) ∈ ℝ)
137131resqcld 14161 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑝 ∈ ℙ) → (𝑝↑2) ∈ ℝ)
138 lelttr 11348 . . . . . . . . . . . . . . . . . . . 20 (((𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ∈ ℝ ∧ (2 · 𝑁) ∈ ℝ ∧ (𝑝↑2) ∈ ℝ) → (((𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁) ∧ (2 · 𝑁) < (𝑝↑2)) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) < (𝑝↑2)))
139135, 136, 137, 138syl3anc 1370 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑝 ∈ ℙ) → (((𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁) ∧ (2 · 𝑁) < (𝑝↑2)) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) < (𝑝↑2)))
140130, 139mpand 695 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑝 ∈ ℙ) → ((2 · 𝑁) < (𝑝↑2) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) < (𝑝↑2)))
141 resqrtth 15290 . . . . . . . . . . . . . . . . . . . . 21 (((2 · 𝑁) ∈ ℝ ∧ 0 ≤ (2 · 𝑁)) → ((√‘(2 · 𝑁))↑2) = (2 · 𝑁))
14220, 21, 141syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((√‘(2 · 𝑁))↑2) = (2 · 𝑁))
143142breq1d 5157 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((√‘(2 · 𝑁))↑2) < (𝑝↑2) ↔ (2 · 𝑁) < (𝑝↑2)))
144143adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑝 ∈ ℙ) → (((√‘(2 · 𝑁))↑2) < (𝑝↑2) ↔ (2 · 𝑁) < (𝑝↑2)))
145134nn0zd 12636 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑝 ∈ ℙ) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ∈ ℤ)
14672a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑝 ∈ ℙ) → 2 ∈ ℤ)
147 prmgt1 16730 . . . . . . . . . . . . . . . . . . . 20 (𝑝 ∈ ℙ → 1 < 𝑝)
148147adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑝 ∈ ℙ) → 1 < 𝑝)
149131, 145, 146, 148ltexp2d 14286 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑝 ∈ ℙ) → ((𝑝 pCnt ((2 · 𝑁)C𝑁)) < 2 ↔ (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) < (𝑝↑2)))
150140, 144, 1493imtr4d 294 . . . . . . . . . . . . . . . . 17 ((𝜑𝑝 ∈ ℙ) → (((√‘(2 · 𝑁))↑2) < (𝑝↑2) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) < 2))
151 df-2 12326 . . . . . . . . . . . . . . . . . 18 2 = (1 + 1)
152151breq2i 5155 . . . . . . . . . . . . . . . . 17 ((𝑝 pCnt ((2 · 𝑁)C𝑁)) < 2 ↔ (𝑝 pCnt ((2 · 𝑁)C𝑁)) < (1 + 1))
153150, 152imbitrdi 251 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 ∈ ℙ) → (((√‘(2 · 𝑁))↑2) < (𝑝↑2) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) < (1 + 1)))
15422adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑝 ∈ ℙ) → (√‘(2 · 𝑁)) ∈ ℝ)
15520, 21sqrtge0d 15455 . . . . . . . . . . . . . . . . . 18 (𝜑 → 0 ≤ (√‘(2 · 𝑁)))
156155adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑝 ∈ ℙ) → 0 ≤ (√‘(2 · 𝑁)))
157 prmnn 16707 . . . . . . . . . . . . . . . . . . . 20 (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
158157nnrpd 13072 . . . . . . . . . . . . . . . . . . 19 (𝑝 ∈ ℙ → 𝑝 ∈ ℝ+)
159158rpge0d 13078 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ ℙ → 0 ≤ 𝑝)
160159adantl 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑝 ∈ ℙ) → 0 ≤ 𝑝)
161154, 131, 156, 160lt2sqd 14291 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 ∈ ℙ) → ((√‘(2 · 𝑁)) < 𝑝 ↔ ((√‘(2 · 𝑁))↑2) < (𝑝↑2)))
162 1z 12644 . . . . . . . . . . . . . . . . 17 1 ∈ ℤ
163 zleltp1 12665 . . . . . . . . . . . . . . . . 17 (((𝑝 pCnt ((2 · 𝑁)C𝑁)) ∈ ℤ ∧ 1 ∈ ℤ) → ((𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1 ↔ (𝑝 pCnt ((2 · 𝑁)C𝑁)) < (1 + 1)))
164145, 162, 163sylancl 586 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 ∈ ℙ) → ((𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1 ↔ (𝑝 pCnt ((2 · 𝑁)C𝑁)) < (1 + 1)))
165153, 161, 1643imtr4d 294 . . . . . . . . . . . . . . 15 ((𝜑𝑝 ∈ ℙ) → ((√‘(2 · 𝑁)) < 𝑝 → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1))
166128, 165sylbird 260 . . . . . . . . . . . . . 14 ((𝜑𝑝 ∈ ℙ) → (¬ 𝑝𝑀 → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1))
167166imp 406 . . . . . . . . . . . . 13 (((𝜑𝑝 ∈ ℙ) ∧ ¬ 𝑝𝑀) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1)
168167adantrl 716 . . . . . . . . . . . 12 (((𝜑𝑝 ∈ ℙ) ∧ (𝑝𝐾 ∧ ¬ 𝑝𝑀)) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1)
169 iftrue 4536 . . . . . . . . . . . . 13 ((𝑝𝐾 ∧ ¬ 𝑝𝑀) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = (𝑝 pCnt ((2 · 𝑁)C𝑁)))
170169adantl 481 . . . . . . . . . . . 12 (((𝜑𝑝 ∈ ℙ) ∧ (𝑝𝐾 ∧ ¬ 𝑝𝑀)) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = (𝑝 pCnt ((2 · 𝑁)C𝑁)))
171 iftrue 4536 . . . . . . . . . . . . 13 ((𝑝𝐾 ∧ ¬ 𝑝𝑀) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0) = 1)
172171adantl 481 . . . . . . . . . . . 12 (((𝜑𝑝 ∈ ℙ) ∧ (𝑝𝐾 ∧ ¬ 𝑝𝑀)) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0) = 1)
173168, 170, 1723brtr4d 5179 . . . . . . . . . . 11 (((𝜑𝑝 ∈ ℙ) ∧ (𝑝𝐾 ∧ ¬ 𝑝𝑀)) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0))
174 0le0 12364 . . . . . . . . . . . . 13 0 ≤ 0
175 iffalse 4539 . . . . . . . . . . . . . 14 (¬ (𝑝𝐾 ∧ ¬ 𝑝𝑀) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = 0)
176 iffalse 4539 . . . . . . . . . . . . . 14 (¬ (𝑝𝐾 ∧ ¬ 𝑝𝑀) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0) = 0)
177175, 176breq12d 5160 . . . . . . . . . . . . 13 (¬ (𝑝𝐾 ∧ ¬ 𝑝𝑀) → (if((𝑝𝐾 ∧ ¬ 𝑝𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0) ↔ 0 ≤ 0))
178174, 177mpbiri 258 . . . . . . . . . . . 12 (¬ (𝑝𝐾 ∧ ¬ 𝑝𝑀) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0))
179178adantl 481 . . . . . . . . . . 11 (((𝜑𝑝 ∈ ℙ) ∧ ¬ (𝑝𝐾 ∧ ¬ 𝑝𝑀)) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0))
180173, 179pm2.61dan 813 . . . . . . . . . 10 ((𝜑𝑝 ∈ ℙ) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0))
18159adantr 480 . . . . . . . . . . 11 ((𝜑𝑝 ∈ ℙ) → ∀𝑛 ∈ ℙ (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
18269adantr 480 . . . . . . . . . . 11 ((𝜑𝑝 ∈ ℙ) → 𝑀 ∈ ℕ)
183 simpr 484 . . . . . . . . . . 11 ((𝜑𝑝 ∈ ℙ) → 𝑝 ∈ ℙ)
184 oveq1 7437 . . . . . . . . . . 11 (𝑛 = 𝑝 → (𝑛 pCnt ((2 · 𝑁)C𝑁)) = (𝑝 pCnt ((2 · 𝑁)C𝑁)))
18589adantr 480 . . . . . . . . . . 11 ((𝜑𝑝 ∈ ℙ) → 𝐾 ∈ (ℤ𝑀))
18655, 181, 182, 183, 184, 185pcmpt2 16926 . . . . . . . . . 10 ((𝜑𝑝 ∈ ℙ) → (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) = if((𝑝𝐾 ∧ ¬ 𝑝𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0))
187 eqid 2734 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1))
188187prmorcht 27235 . . . . . . . . . . . . . . 15 (𝐾 ∈ ℕ → (exp‘(θ‘𝐾)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾))
18996, 188syl 17 . . . . . . . . . . . . . 14 (𝜑 → (exp‘(θ‘𝐾)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾))
190187prmorcht 27235 . . . . . . . . . . . . . . 15 (𝑀 ∈ ℕ → (exp‘(θ‘𝑀)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀))
19169, 190syl 17 . . . . . . . . . . . . . 14 (𝜑 → (exp‘(θ‘𝑀)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀))
192189, 191oveq12d 7448 . . . . . . . . . . . . 13 (𝜑 → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) = ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾) / (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀)))
193192adantr 480 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ ℙ) → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) = ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾) / (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀)))
194193oveq2d 7446 . . . . . . . . . . 11 ((𝜑𝑝 ∈ ℙ) → (𝑝 pCnt ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))) = (𝑝 pCnt ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾) / (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀))))
195 nncn 12271 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
196195exp1d 14177 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (𝑛↑1) = 𝑛)
197196ifeq1d 4549 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → if(𝑛 ∈ ℙ, (𝑛↑1), 1) = if(𝑛 ∈ ℙ, 𝑛, 1))
198197mpteq2ia 5250 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑1), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1))
199198eqcomi 2743 . . . . . . . . . . . 12 (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑1), 1))
200 1nn0 12539 . . . . . . . . . . . . . . 15 1 ∈ ℕ0
201200a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℙ) → 1 ∈ ℕ0)
202201ralrimiva 3143 . . . . . . . . . . . . 13 (𝜑 → ∀𝑛 ∈ ℙ 1 ∈ ℕ0)
203202adantr 480 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ ℙ) → ∀𝑛 ∈ ℙ 1 ∈ ℕ0)
204 eqidd 2735 . . . . . . . . . . . 12 (𝑛 = 𝑝 → 1 = 1)
205199, 203, 182, 183, 204, 185pcmpt2 16926 . . . . . . . . . . 11 ((𝜑𝑝 ∈ ℙ) → (𝑝 pCnt ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾) / (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀))) = if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0))
206194, 205eqtrd 2774 . . . . . . . . . 10 ((𝜑𝑝 ∈ ℙ) → (𝑝 pCnt ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))) = if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0))
207180, 186, 2063brtr4d 5179 . . . . . . . . 9 ((𝜑𝑝 ∈ ℙ) → (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) ≤ (𝑝 pCnt ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))))
208207ralrimiva 3143 . . . . . . . 8 (𝜑 → ∀𝑝 ∈ ℙ (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) ≤ (𝑝 pCnt ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))))
209 pc2dvds 16912 . . . . . . . . 9 ((((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ ∧ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℤ) → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) ≤ (𝑝 pCnt ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))))))
210101, 118, 209syl2anc 584 . . . . . . . 8 (𝜑 → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) ≤ (𝑝 pCnt ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))))))
211208, 210mpbird 257 . . . . . . 7 (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))))
212114nnred 12278 . . . . . . . . . 10 (𝜑 → (exp‘(θ‘𝐾)) ∈ ℝ)
213110nnred 12278 . . . . . . . . . 10 (𝜑 → (exp‘(θ‘𝑀)) ∈ ℝ)
214114nngt0d 12312 . . . . . . . . . 10 (𝜑 → 0 < (exp‘(θ‘𝐾)))
215110nngt0d 12312 . . . . . . . . . 10 (𝜑 → 0 < (exp‘(θ‘𝑀)))
216212, 213, 214, 215divgt0d 12200 . . . . . . . . 9 (𝜑 → 0 < ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))))
217 elnnz 12620 . . . . . . . . 9 (((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℕ ↔ (((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℤ ∧ 0 < ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))))
218118, 216, 217sylanbrc 583 . . . . . . . 8 (𝜑 → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℕ)
219 dvdsle 16343 . . . . . . . 8 ((((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ ∧ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℕ) → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ≤ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))))
220101, 218, 219syl2anc 584 . . . . . . 7 (𝜑 → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ≤ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))))
221211, 220mpd 15 . . . . . 6 (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ≤ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))))
222 nndivre 12304 . . . . . . . 8 (((exp‘(θ‘𝐾)) ∈ ℝ ∧ 4 ∈ ℕ) → ((exp‘(θ‘𝐾)) / 4) ∈ ℝ)
223212, 1, 222sylancl 586 . . . . . . 7 (𝜑 → ((exp‘(θ‘𝐾)) / 4) ∈ ℝ)
224 4re 12347 . . . . . . . . . 10 4 ∈ ℝ
225224a1i 11 . . . . . . . . 9 (𝜑 → 4 ∈ ℝ)
226 6re 12353 . . . . . . . . . 10 6 ∈ ℝ
227226a1i 11 . . . . . . . . 9 (𝜑 → 6 ∈ ℝ)
228 4lt6 12445 . . . . . . . . . 10 4 < 6
229228a1i 11 . . . . . . . . 9 (𝜑 → 4 < 6)
230 cht3 27230 . . . . . . . . . . . 12 (θ‘3) = (log‘6)
231230fveq2i 6909 . . . . . . . . . . 11 (exp‘(θ‘3)) = (exp‘(log‘6))
232 6pos 12373 . . . . . . . . . . . . 13 0 < 6
233226, 232elrpii 13034 . . . . . . . . . . . 12 6 ∈ ℝ+
234 reeflog 26636 . . . . . . . . . . . 12 (6 ∈ ℝ+ → (exp‘(log‘6)) = 6)
235233, 234ax-mp 5 . . . . . . . . . . 11 (exp‘(log‘6)) = 6
236231, 235eqtri 2762 . . . . . . . . . 10 (exp‘(θ‘3)) = 6
237 3re 12343 . . . . . . . . . . . . 13 3 ∈ ℝ
238237a1i 11 . . . . . . . . . . . 12 (𝜑 → 3 ∈ ℝ)
239 eluzle 12888 . . . . . . . . . . . . 13 (𝑀 ∈ (ℤ‘3) → 3 ≤ 𝑀)
24067, 239syl 17 . . . . . . . . . . . 12 (𝜑 → 3 ≤ 𝑀)
241 chtwordi 27213 . . . . . . . . . . . 12 ((3 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 3 ≤ 𝑀) → (θ‘3) ≤ (θ‘𝑀))
242238, 103, 240, 241syl3anc 1370 . . . . . . . . . . 11 (𝜑 → (θ‘3) ≤ (θ‘𝑀))
243 chtcl 27166 . . . . . . . . . . . . 13 (3 ∈ ℝ → (θ‘3) ∈ ℝ)
244237, 243ax-mp 5 . . . . . . . . . . . 12 (θ‘3) ∈ ℝ
245 chtcl 27166 . . . . . . . . . . . . 13 (𝑀 ∈ ℝ → (θ‘𝑀) ∈ ℝ)
246103, 245syl 17 . . . . . . . . . . . 12 (𝜑 → (θ‘𝑀) ∈ ℝ)
247 efle 16150 . . . . . . . . . . . 12 (((θ‘3) ∈ ℝ ∧ (θ‘𝑀) ∈ ℝ) → ((θ‘3) ≤ (θ‘𝑀) ↔ (exp‘(θ‘3)) ≤ (exp‘(θ‘𝑀))))
248244, 246, 247sylancr 587 . . . . . . . . . . 11 (𝜑 → ((θ‘3) ≤ (θ‘𝑀) ↔ (exp‘(θ‘3)) ≤ (exp‘(θ‘𝑀))))
249242, 248mpbid 232 . . . . . . . . . 10 (𝜑 → (exp‘(θ‘3)) ≤ (exp‘(θ‘𝑀)))
250236, 249eqbrtrrid 5183 . . . . . . . . 9 (𝜑 → 6 ≤ (exp‘(θ‘𝑀)))
251225, 227, 213, 229, 250ltletrd 11418 . . . . . . . 8 (𝜑 → 4 < (exp‘(θ‘𝑀)))
252 4pos 12370 . . . . . . . . . 10 0 < 4
253252a1i 11 . . . . . . . . 9 (𝜑 → 0 < 4)
254 ltdiv2 12151 . . . . . . . . 9 (((4 ∈ ℝ ∧ 0 < 4) ∧ ((exp‘(θ‘𝑀)) ∈ ℝ ∧ 0 < (exp‘(θ‘𝑀))) ∧ ((exp‘(θ‘𝐾)) ∈ ℝ ∧ 0 < (exp‘(θ‘𝐾)))) → (4 < (exp‘(θ‘𝑀)) ↔ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) < ((exp‘(θ‘𝐾)) / 4)))
255225, 253, 213, 215, 212, 214, 254syl222anc 1385 . . . . . . . 8 (𝜑 → (4 < (exp‘(θ‘𝑀)) ↔ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) < ((exp‘(θ‘𝐾)) / 4)))
256251, 255mpbid 232 . . . . . . 7 (𝜑 → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) < ((exp‘(θ‘𝐾)) / 4))
25726a1i 11 . . . . . . . . . . . . 13 (𝜑 → 2 ∈ ℝ)
258 2lt3 12435 . . . . . . . . . . . . . 14 2 < 3
259258a1i 11 . . . . . . . . . . . . 13 (𝜑 → 2 < 3)
260238, 103, 104, 240, 106letrd 11415 . . . . . . . . . . . . 13 (𝜑 → 3 ≤ 𝐾)
261257, 238, 104, 259, 260ltletrd 11418 . . . . . . . . . . . 12 (𝜑 → 2 < 𝐾)
262 chtub 27270 . . . . . . . . . . . 12 ((𝐾 ∈ ℝ ∧ 2 < 𝐾) → (θ‘𝐾) < ((log‘2) · ((2 · 𝐾) − 3)))
263104, 261, 262syl2anc 584 . . . . . . . . . . 11 (𝜑 → (θ‘𝐾) < ((log‘2) · ((2 · 𝐾) − 3)))
264 chtcl 27166 . . . . . . . . . . . . 13 (𝐾 ∈ ℝ → (θ‘𝐾) ∈ ℝ)
265104, 264syl 17 . . . . . . . . . . . 12 (𝜑 → (θ‘𝐾) ∈ ℝ)
266 relogcl 26631 . . . . . . . . . . . . . 14 (2 ∈ ℝ+ → (log‘2) ∈ ℝ)
26731, 266ax-mp 5 . . . . . . . . . . . . 13 (log‘2) ∈ ℝ
268 3z 12647 . . . . . . . . . . . . . . 15 3 ∈ ℤ
269 zsubcl 12656 . . . . . . . . . . . . . . 15 (((2 · 𝐾) ∈ ℤ ∧ 3 ∈ ℤ) → ((2 · 𝐾) − 3) ∈ ℤ)
27078, 268, 269sylancl 586 . . . . . . . . . . . . . 14 (𝜑 → ((2 · 𝐾) − 3) ∈ ℤ)
271270zred 12719 . . . . . . . . . . . . 13 (𝜑 → ((2 · 𝐾) − 3) ∈ ℝ)
272 remulcl 11237 . . . . . . . . . . . . 13 (((log‘2) ∈ ℝ ∧ ((2 · 𝐾) − 3) ∈ ℝ) → ((log‘2) · ((2 · 𝐾) − 3)) ∈ ℝ)
273267, 271, 272sylancr 587 . . . . . . . . . . . 12 (𝜑 → ((log‘2) · ((2 · 𝐾) − 3)) ∈ ℝ)
274 eflt 16149 . . . . . . . . . . . 12 (((θ‘𝐾) ∈ ℝ ∧ ((log‘2) · ((2 · 𝐾) − 3)) ∈ ℝ) → ((θ‘𝐾) < ((log‘2) · ((2 · 𝐾) − 3)) ↔ (exp‘(θ‘𝐾)) < (exp‘((log‘2) · ((2 · 𝐾) − 3)))))
275265, 273, 274syl2anc 584 . . . . . . . . . . 11 (𝜑 → ((θ‘𝐾) < ((log‘2) · ((2 · 𝐾) − 3)) ↔ (exp‘(θ‘𝐾)) < (exp‘((log‘2) · ((2 · 𝐾) − 3)))))
276263, 275mpbid 232 . . . . . . . . . 10 (𝜑 → (exp‘(θ‘𝐾)) < (exp‘((log‘2) · ((2 · 𝐾) − 3))))
277 reexplog 26651 . . . . . . . . . . . 12 ((2 ∈ ℝ+ ∧ ((2 · 𝐾) − 3) ∈ ℤ) → (2↑((2 · 𝐾) − 3)) = (exp‘(((2 · 𝐾) − 3) · (log‘2))))
27831, 270, 277sylancr 587 . . . . . . . . . . 11 (𝜑 → (2↑((2 · 𝐾) − 3)) = (exp‘(((2 · 𝐾) − 3) · (log‘2))))
279270zcnd 12720 . . . . . . . . . . . . 13 (𝜑 → ((2 · 𝐾) − 3) ∈ ℂ)
280267recni 11272 . . . . . . . . . . . . 13 (log‘2) ∈ ℂ
281 mulcom 11238 . . . . . . . . . . . . 13 ((((2 · 𝐾) − 3) ∈ ℂ ∧ (log‘2) ∈ ℂ) → (((2 · 𝐾) − 3) · (log‘2)) = ((log‘2) · ((2 · 𝐾) − 3)))
282279, 280, 281sylancl 586 . . . . . . . . . . . 12 (𝜑 → (((2 · 𝐾) − 3) · (log‘2)) = ((log‘2) · ((2 · 𝐾) − 3)))
283282fveq2d 6910 . . . . . . . . . . 11 (𝜑 → (exp‘(((2 · 𝐾) − 3) · (log‘2))) = (exp‘((log‘2) · ((2 · 𝐾) − 3))))
284278, 283eqtrd 2774 . . . . . . . . . 10 (𝜑 → (2↑((2 · 𝐾) − 3)) = (exp‘((log‘2) · ((2 · 𝐾) − 3))))
285276, 284breqtrrd 5175 . . . . . . . . 9 (𝜑 → (exp‘(θ‘𝐾)) < (2↑((2 · 𝐾) − 3)))
286 3p2e5 12414 . . . . . . . . . . . . . . . 16 (3 + 2) = 5
287286oveq1i 7440 . . . . . . . . . . . . . . 15 ((3 + 2) − 2) = (5 − 2)
288 3cn 12344 . . . . . . . . . . . . . . . 16 3 ∈ ℂ
289 2cn 12338 . . . . . . . . . . . . . . . 16 2 ∈ ℂ
290288, 289pncan3oi 11521 . . . . . . . . . . . . . . 15 ((3 + 2) − 2) = 3
291287, 290eqtr3i 2764 . . . . . . . . . . . . . 14 (5 − 2) = 3
292291oveq2i 7441 . . . . . . . . . . . . 13 ((2 · 𝐾) − (5 − 2)) = ((2 · 𝐾) − 3)
29378zcnd 12720 . . . . . . . . . . . . . 14 (𝜑 → (2 · 𝐾) ∈ ℂ)
294 5cn 12351 . . . . . . . . . . . . . . 15 5 ∈ ℂ
295 subsub 11536 . . . . . . . . . . . . . . 15 (((2 · 𝐾) ∈ ℂ ∧ 5 ∈ ℂ ∧ 2 ∈ ℂ) → ((2 · 𝐾) − (5 − 2)) = (((2 · 𝐾) − 5) + 2))
296294, 289, 295mp3an23 1452 . . . . . . . . . . . . . 14 ((2 · 𝐾) ∈ ℂ → ((2 · 𝐾) − (5 − 2)) = (((2 · 𝐾) − 5) + 2))
297293, 296syl 17 . . . . . . . . . . . . 13 (𝜑 → ((2 · 𝐾) − (5 − 2)) = (((2 · 𝐾) − 5) + 2))
298292, 297eqtr3id 2788 . . . . . . . . . . . 12 (𝜑 → ((2 · 𝐾) − 3) = (((2 · 𝐾) − 5) + 2))
299298oveq2d 7446 . . . . . . . . . . 11 (𝜑 → (2↑𝑐((2 · 𝐾) − 3)) = (2↑𝑐(((2 · 𝐾) − 5) + 2)))
300 2ne0 12367 . . . . . . . . . . . 12 2 ≠ 0
301 cxpexpz 26723 . . . . . . . . . . . 12 ((2 ∈ ℂ ∧ 2 ≠ 0 ∧ ((2 · 𝐾) − 3) ∈ ℤ) → (2↑𝑐((2 · 𝐾) − 3)) = (2↑((2 · 𝐾) − 3)))
302289, 300, 270, 301mp3an12i 1464 . . . . . . . . . . 11 (𝜑 → (2↑𝑐((2 · 𝐾) − 3)) = (2↑((2 · 𝐾) − 3)))
30381zcnd 12720 . . . . . . . . . . . 12 (𝜑 → ((2 · 𝐾) − 5) ∈ ℂ)
304 2cnne0 12473 . . . . . . . . . . . . 13 (2 ∈ ℂ ∧ 2 ≠ 0)
305 cxpadd 26735 . . . . . . . . . . . . 13 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ ((2 · 𝐾) − 5) ∈ ℂ ∧ 2 ∈ ℂ) → (2↑𝑐(((2 · 𝐾) − 5) + 2)) = ((2↑𝑐((2 · 𝐾) − 5)) · (2↑𝑐2)))
306304, 289, 305mp3an13 1451 . . . . . . . . . . . 12 (((2 · 𝐾) − 5) ∈ ℂ → (2↑𝑐(((2 · 𝐾) − 5) + 2)) = ((2↑𝑐((2 · 𝐾) − 5)) · (2↑𝑐2)))
307303, 306syl 17 . . . . . . . . . . 11 (𝜑 → (2↑𝑐(((2 · 𝐾) − 5) + 2)) = ((2↑𝑐((2 · 𝐾) − 5)) · (2↑𝑐2)))
308299, 302, 3073eqtr3d 2782 . . . . . . . . . 10 (𝜑 → (2↑((2 · 𝐾) − 3)) = ((2↑𝑐((2 · 𝐾) − 5)) · (2↑𝑐2)))
309 2nn0 12540 . . . . . . . . . . . . 13 2 ∈ ℕ0
310 cxpexp 26724 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ 2 ∈ ℕ0) → (2↑𝑐2) = (2↑2))
311289, 309, 310mp2an 692 . . . . . . . . . . . 12 (2↑𝑐2) = (2↑2)
312 sq2 14232 . . . . . . . . . . . 12 (2↑2) = 4
313311, 312eqtri 2762 . . . . . . . . . . 11 (2↑𝑐2) = 4
314313oveq2i 7441 . . . . . . . . . 10 ((2↑𝑐((2 · 𝐾) − 5)) · (2↑𝑐2)) = ((2↑𝑐((2 · 𝐾) − 5)) · 4)
315308, 314eqtrdi 2790 . . . . . . . . 9 (𝜑 → (2↑((2 · 𝐾) − 3)) = ((2↑𝑐((2 · 𝐾) − 5)) · 4))
316285, 315breqtrd 5173 . . . . . . . 8 (𝜑 → (exp‘(θ‘𝐾)) < ((2↑𝑐((2 · 𝐾) − 5)) · 4))
317224, 252pm3.2i 470 . . . . . . . . . 10 (4 ∈ ℝ ∧ 0 < 4)
318317a1i 11 . . . . . . . . 9 (𝜑 → (4 ∈ ℝ ∧ 0 < 4))
319 ltdivmul2 12142 . . . . . . . . 9 (((exp‘(θ‘𝐾)) ∈ ℝ ∧ (2↑𝑐((2 · 𝐾) − 5)) ∈ ℝ ∧ (4 ∈ ℝ ∧ 0 < 4)) → (((exp‘(θ‘𝐾)) / 4) < (2↑𝑐((2 · 𝐾) − 5)) ↔ (exp‘(θ‘𝐾)) < ((2↑𝑐((2 · 𝐾) − 5)) · 4)))
320212, 85, 318, 319syl3anc 1370 . . . . . . . 8 (𝜑 → (((exp‘(θ‘𝐾)) / 4) < (2↑𝑐((2 · 𝐾) − 5)) ↔ (exp‘(θ‘𝐾)) < ((2↑𝑐((2 · 𝐾) − 5)) · 4)))
321316, 320mpbird 257 . . . . . . 7 (𝜑 → ((exp‘(θ‘𝐾)) / 4) < (2↑𝑐((2 · 𝐾) − 5)))
322119, 223, 85, 256, 321lttrd 11419 . . . . . 6 (𝜑 → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) < (2↑𝑐((2 · 𝐾) − 5)))
323102, 119, 85, 221, 322lelttrd 11416 . . . . 5 (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) < (2↑𝑐((2 · 𝐾) − 5)))
32497nnred 12278 . . . . . 6 (𝜑 → (seq1( · , 𝐹)‘𝐾) ∈ ℝ)
325 nnre 12270 . . . . . . . 8 ((seq1( · , 𝐹)‘𝑀) ∈ ℕ → (seq1( · , 𝐹)‘𝑀) ∈ ℝ)
326 nngt0 12294 . . . . . . . 8 ((seq1( · , 𝐹)‘𝑀) ∈ ℕ → 0 < (seq1( · , 𝐹)‘𝑀))
327325, 326jca 511 . . . . . . 7 ((seq1( · , 𝐹)‘𝑀) ∈ ℕ → ((seq1( · , 𝐹)‘𝑀) ∈ ℝ ∧ 0 < (seq1( · , 𝐹)‘𝑀)))
32870, 327syl 17 . . . . . 6 (𝜑 → ((seq1( · , 𝐹)‘𝑀) ∈ ℝ ∧ 0 < (seq1( · , 𝐹)‘𝑀)))
329 ltdivmul 12140 . . . . . 6 (((seq1( · , 𝐹)‘𝐾) ∈ ℝ ∧ (2↑𝑐((2 · 𝐾) − 5)) ∈ ℝ ∧ ((seq1( · , 𝐹)‘𝑀) ∈ ℝ ∧ 0 < (seq1( · , 𝐹)‘𝑀))) → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) < (2↑𝑐((2 · 𝐾) − 5)) ↔ (seq1( · , 𝐹)‘𝐾) < ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2 · 𝐾) − 5)))))
330324, 85, 328, 329syl3anc 1370 . . . . 5 (𝜑 → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) < (2↑𝑐((2 · 𝐾) − 5)) ↔ (seq1( · , 𝐹)‘𝐾) < ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2 · 𝐾) − 5)))))
331323, 330mpbid 232 . . . 4 (𝜑 → (seq1( · , 𝐹)‘𝐾) < ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2 · 𝐾) − 5))))
33287, 331eqbrtrrd 5171 . . 3 (𝜑 → ((2 · 𝑁)C𝑁) < ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2 · 𝐾) − 5))))
33330, 85remulcld 11288 . . . 4 (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐((2 · 𝐾) − 5))) ∈ ℝ)
3343, 62, 55, 63, 64bposlem5 27346 . . . . 5 (𝜑 → (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)))
33571, 30, 84lemul1d 13117 . . . . 5 (𝜑 → ((seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) ↔ ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2 · 𝐾) − 5))) ≤ (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐((2 · 𝐾) − 5)))))
336334, 335mpbid 232 . . . 4 (𝜑 → ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2 · 𝐾) − 5))) ≤ (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐((2 · 𝐾) − 5))))
33778zred 12719 . . . . . . 7 (𝜑 → (2 · 𝐾) ∈ ℝ)
33837a1i 11 . . . . . . 7 (𝜑 → 5 ∈ ℝ)
339 flle 13835 . . . . . . . . . . 11 (((2 · 𝑁) / 3) ∈ ℝ → (⌊‘((2 · 𝑁) / 3)) ≤ ((2 · 𝑁) / 3))
34074, 339syl 17 . . . . . . . . . 10 (𝜑 → (⌊‘((2 · 𝑁) / 3)) ≤ ((2 · 𝑁) / 3))
34163, 340eqbrtrid 5182 . . . . . . . . 9 (𝜑𝐾 ≤ ((2 · 𝑁) / 3))
342 2pos 12366 . . . . . . . . . . . 12 0 < 2
34326, 342pm3.2i 470 . . . . . . . . . . 11 (2 ∈ ℝ ∧ 0 < 2)
344343a1i 11 . . . . . . . . . 10 (𝜑 → (2 ∈ ℝ ∧ 0 < 2))
345 lemul2 12117 . . . . . . . . . 10 ((𝐾 ∈ ℝ ∧ ((2 · 𝑁) / 3) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝐾 ≤ ((2 · 𝑁) / 3) ↔ (2 · 𝐾) ≤ (2 · ((2 · 𝑁) / 3))))
346104, 74, 344, 345syl3anc 1370 . . . . . . . . 9 (𝜑 → (𝐾 ≤ ((2 · 𝑁) / 3) ↔ (2 · 𝐾) ≤ (2 · ((2 · 𝑁) / 3))))
347341, 346mpbid 232 . . . . . . . 8 (𝜑 → (2 · 𝐾) ≤ (2 · ((2 · 𝑁) / 3)))
34818nncnd 12279 . . . . . . . . . 10 (𝜑 → (2 · 𝑁) ∈ ℂ)
349 3ne0 12369 . . . . . . . . . . . 12 3 ≠ 0
350288, 349pm3.2i 470 . . . . . . . . . . 11 (3 ∈ ℂ ∧ 3 ≠ 0)
351 divass 11937 . . . . . . . . . . 11 ((2 ∈ ℂ ∧ (2 · 𝑁) ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((2 · (2 · 𝑁)) / 3) = (2 · ((2 · 𝑁) / 3)))
352289, 350, 351mp3an13 1451 . . . . . . . . . 10 ((2 · 𝑁) ∈ ℂ → ((2 · (2 · 𝑁)) / 3) = (2 · ((2 · 𝑁) / 3)))
353348, 352syl 17 . . . . . . . . 9 (𝜑 → ((2 · (2 · 𝑁)) / 3) = (2 · ((2 · 𝑁) / 3)))
3545nncnd 12279 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℂ)
355 mulass 11240 . . . . . . . . . . . 12 ((2 ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((2 · 2) · 𝑁) = (2 · (2 · 𝑁)))
356289, 289, 354, 355mp3an12i 1464 . . . . . . . . . . 11 (𝜑 → ((2 · 2) · 𝑁) = (2 · (2 · 𝑁)))
357 2t2e4 12427 . . . . . . . . . . . 12 (2 · 2) = 4
358357oveq1i 7440 . . . . . . . . . . 11 ((2 · 2) · 𝑁) = (4 · 𝑁)
359356, 358eqtr3di 2789 . . . . . . . . . 10 (𝜑 → (2 · (2 · 𝑁)) = (4 · 𝑁))
360359oveq1d 7445 . . . . . . . . 9 (𝜑 → ((2 · (2 · 𝑁)) / 3) = ((4 · 𝑁) / 3))
361353, 360eqtr3d 2776 . . . . . . . 8 (𝜑 → (2 · ((2 · 𝑁) / 3)) = ((4 · 𝑁) / 3))
362347, 361breqtrd 5173 . . . . . . 7 (𝜑 → (2 · 𝐾) ≤ ((4 · 𝑁) / 3))
363337, 36, 338, 362lesub1dd 11876 . . . . . 6 (𝜑 → ((2 · 𝐾) − 5) ≤ (((4 · 𝑁) / 3) − 5))
364 1lt2 12434 . . . . . . . 8 1 < 2
365364a1i 11 . . . . . . 7 (𝜑 → 1 < 2)
366257, 365, 82, 39cxpled 26776 . . . . . 6 (𝜑 → (((2 · 𝐾) − 5) ≤ (((4 · 𝑁) / 3) − 5) ↔ (2↑𝑐((2 · 𝐾) − 5)) ≤ (2↑𝑐(((4 · 𝑁) / 3) − 5))))
367363, 366mpbid 232 . . . . 5 (𝜑 → (2↑𝑐((2 · 𝐾) − 5)) ≤ (2↑𝑐(((4 · 𝑁) / 3) − 5)))
36885, 42, 29lemul2d 13118 . . . . 5 (𝜑 → ((2↑𝑐((2 · 𝐾) − 5)) ≤ (2↑𝑐(((4 · 𝑁) / 3) − 5)) ↔ (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐((2 · 𝐾) − 5))) ≤ (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5)))))
369367, 368mpbid 232 . . . 4 (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐((2 · 𝐾) − 5))) ≤ (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))))
37086, 333, 43, 336, 369letrd 11415 . . 3 (𝜑 → ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2 · 𝐾) − 5))) ≤ (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))))
37115, 86, 43, 332, 370ltletrd 11418 . 2 (𝜑 → ((2 · 𝑁)C𝑁) < (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))))
37210, 15, 43, 54, 371lttrd 11419 1 (𝜑 → ((4↑𝑁) / 𝑁) < (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1536  wcel 2105  wne 2937  wral 3058  wrex 3067  ifcif 4530   class class class wbr 5147  cmpt 5230  wf 6558  cfv 6562  (class class class)co 7430  cc 11150  cr 11151  0cc0 11152  1c1 11153   + caddc 11155   · cmul 11157   < clt 11292  cle 11293  cmin 11489   / cdiv 11917  cn 12263  2c2 12318  3c3 12319  4c4 12320  5c5 12321  6c6 12322  0cn0 12523  cz 12610  cuz 12875  +crp 13031  ...cfz 13543  cfl 13826  seqcseq 14038  cexp 14098  Ccbc 14337  csqrt 15268  expce 16093  cdvds 16286  cprime 16704   pCnt cpc 16869  logclog 26610  𝑐ccxp 26611  θccht 27148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230  ax-addf 11231
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-iin 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-of 7696  df-om 7887  df-1st 8012  df-2nd 8013  df-supp 8184  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-2o 8505  df-oadd 8508  df-er 8743  df-map 8866  df-pm 8867  df-ixp 8936  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-fsupp 9399  df-fi 9448  df-sup 9479  df-inf 9480  df-oi 9547  df-dju 9938  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-4 12328  df-5 12329  df-6 12330  df-7 12331  df-8 12332  df-9 12333  df-n0 12524  df-xnn0 12597  df-z 12611  df-dec 12731  df-uz 12876  df-q 12988  df-rp 13032  df-xneg 13151  df-xadd 13152  df-xmul 13153  df-ioo 13387  df-ioc 13388  df-ico 13389  df-icc 13390  df-fz 13544  df-fzo 13691  df-fl 13828  df-mod 13906  df-seq 14039  df-exp 14099  df-fac 14309  df-bc 14338  df-hash 14366  df-shft 15102  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-limsup 15503  df-clim 15520  df-rlim 15521  df-sum 15719  df-ef 16099  df-sin 16101  df-cos 16102  df-pi 16104  df-dvds 16287  df-gcd 16528  df-prm 16705  df-pc 16870  df-struct 17180  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-ress 17274  df-plusg 17310  df-mulr 17311  df-starv 17312  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-hom 17321  df-cco 17322  df-rest 17468  df-topn 17469  df-0g 17487  df-gsum 17488  df-topgen 17489  df-pt 17490  df-prds 17493  df-xrs 17548  df-qtop 17553  df-imas 17554  df-xps 17556  df-mre 17630  df-mrc 17631  df-acs 17633  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-submnd 18809  df-mulg 19098  df-cntz 19347  df-cmn 19814  df-psmet 21373  df-xmet 21374  df-met 21375  df-bl 21376  df-mopn 21377  df-fbas 21378  df-fg 21379  df-cnfld 21382  df-top 22915  df-topon 22932  df-topsp 22954  df-bases 22968  df-cld 23042  df-ntr 23043  df-cls 23044  df-nei 23121  df-lp 23159  df-perf 23160  df-cn 23250  df-cnp 23251  df-haus 23338  df-tx 23585  df-hmeo 23778  df-fil 23869  df-fm 23961  df-flim 23962  df-flf 23963  df-xms 24345  df-ms 24346  df-tms 24347  df-cncf 24917  df-limc 25915  df-dv 25916  df-log 26612  df-cxp 26613  df-cht 27154  df-ppi 27157
This theorem is referenced by:  bposlem9  27350
  Copyright terms: Public domain W3C validator