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

Theorem bposlem6 25986
 Description: Lemma for bpos 25990. 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 11770 . . . . 5 4 ∈ ℕ
2 5nn 11773 . . . . . . 7 5 ∈ ℕ
3 bpos.1 . . . . . . 7 (𝜑𝑁 ∈ (ℤ‘5))
4 eluznn 12371 . . . . . . 7 ((5 ∈ ℕ ∧ 𝑁 ∈ (ℤ‘5)) → 𝑁 ∈ ℕ)
52, 3, 4sylancr 590 . . . . . 6 (𝜑𝑁 ∈ ℕ)
65nnnn0d 12007 . . . . 5 (𝜑𝑁 ∈ ℕ0)
7 nnexpcl 13505 . . . . 5 ((4 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (4↑𝑁) ∈ ℕ)
81, 6, 7sylancr 590 . . . 4 (𝜑 → (4↑𝑁) ∈ ℕ)
98nnred 11702 . . 3 (𝜑 → (4↑𝑁) ∈ ℝ)
109, 5nndivred 11741 . 2 (𝜑 → ((4↑𝑁) / 𝑁) ∈ ℝ)
11 fzctr 13081 . . . . 5 (𝑁 ∈ ℕ0𝑁 ∈ (0...(2 · 𝑁)))
126, 11syl 17 . . . 4 (𝜑𝑁 ∈ (0...(2 · 𝑁)))
13 bccl2 13746 . . . 4 (𝑁 ∈ (0...(2 · 𝑁)) → ((2 · 𝑁)C𝑁) ∈ ℕ)
1412, 13syl 17 . . 3 (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℕ)
1514nnred 11702 . 2 (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℝ)
16 2nn 11760 . . . . . . 7 2 ∈ ℕ
17 nnmulcl 11711 . . . . . . 7 ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
1816, 5, 17sylancr 590 . . . . . 6 (𝜑 → (2 · 𝑁) ∈ ℕ)
1918nnrpd 12483 . . . . 5 (𝜑 → (2 · 𝑁) ∈ ℝ+)
2018nnred 11702 . . . . . . . 8 (𝜑 → (2 · 𝑁) ∈ ℝ)
2119rpge0d 12489 . . . . . . . 8 (𝜑 → 0 ≤ (2 · 𝑁))
2220, 21resqrtcld 14838 . . . . . . 7 (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ)
23 3nn 11766 . . . . . . 7 3 ∈ ℕ
24 nndivre 11728 . . . . . . 7 (((√‘(2 · 𝑁)) ∈ ℝ ∧ 3 ∈ ℕ) → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
2522, 23, 24sylancl 589 . . . . . 6 (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
26 2re 11761 . . . . . 6 2 ∈ ℝ
27 readdcl 10671 . . . . . 6 ((((√‘(2 · 𝑁)) / 3) ∈ ℝ ∧ 2 ∈ ℝ) → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
2825, 26, 27sylancl 589 . . . . 5 (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
2919, 28rpcxpcld 25436 . . . 4 (𝜑 → ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) ∈ ℝ+)
3029rpred 12485 . . 3 (𝜑 → ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) ∈ ℝ)
31 2rp 12448 . . . . 5 2 ∈ ℝ+
32 nnmulcl 11711 . . . . . . . . 9 ((4 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (4 · 𝑁) ∈ ℕ)
331, 5, 32sylancr 590 . . . . . . . 8 (𝜑 → (4 · 𝑁) ∈ ℕ)
3433nnred 11702 . . . . . . 7 (𝜑 → (4 · 𝑁) ∈ ℝ)
35 nndivre 11728 . . . . . . 7 (((4 · 𝑁) ∈ ℝ ∧ 3 ∈ ℕ) → ((4 · 𝑁) / 3) ∈ ℝ)
3634, 23, 35sylancl 589 . . . . . 6 (𝜑 → ((4 · 𝑁) / 3) ∈ ℝ)
37 5re 11774 . . . . . 6 5 ∈ ℝ
38 resubcl 11001 . . . . . 6 ((((4 · 𝑁) / 3) ∈ ℝ ∧ 5 ∈ ℝ) → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
3936, 37, 38sylancl 589 . . . . 5 (𝜑 → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
40 rpcxpcl 25380 . . . . 5 ((2 ∈ ℝ+ ∧ (((4 · 𝑁) / 3) − 5) ∈ ℝ) → (2↑𝑐(((4 · 𝑁) / 3) − 5)) ∈ ℝ+)
4131, 39, 40sylancr 590 . . . 4 (𝜑 → (2↑𝑐(((4 · 𝑁) / 3) − 5)) ∈ ℝ+)
4241rpred 12485 . . 3 (𝜑 → (2↑𝑐(((4 · 𝑁) / 3) − 5)) ∈ ℝ)
4330, 42remulcld 10722 . 2 (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))) ∈ ℝ)
44 df-5 11753 . . . . 5 5 = (4 + 1)
45 4z 12068 . . . . . 6 4 ∈ ℤ
46 uzid 12310 . . . . . 6 (4 ∈ ℤ → 4 ∈ (ℤ‘4))
47 peano2uz 12354 . . . . . 6 (4 ∈ (ℤ‘4) → (4 + 1) ∈ (ℤ‘4))
4845, 46, 47mp2b 10 . . . . 5 (4 + 1) ∈ (ℤ‘4)
4944, 48eqeltri 2848 . . . 4 5 ∈ (ℤ‘4)
50 eqid 2758 . . . . 5 (ℤ‘4) = (ℤ‘4)
5150uztrn2 12314 . . . 4 ((5 ∈ (ℤ‘4) ∧ 𝑁 ∈ (ℤ‘5)) → 𝑁 ∈ (ℤ‘4))
5249, 3, 51sylancr 590 . . 3 (𝜑𝑁 ∈ (ℤ‘4))
53 bclbnd 25977 . . 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 16255 . . . . . . . . . 10 ((𝑛 ∈ ℙ ∧ ((2 · 𝑁)C𝑁) ∈ ℕ) → (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
5856, 14, 57syl2anr 599 . . . . . . . . 9 ((𝜑𝑛 ∈ ℙ) → (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
5958ralrimiva 3113 . . . . . . . 8 (𝜑 → ∀𝑛 ∈ ℙ (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
6055, 59pcmptcl 16296 . . . . . . 7 (𝜑 → (𝐹:ℕ⟶ℕ ∧ seq1( · , 𝐹):ℕ⟶ℕ))
6160simprd 499 . . . . . 6 (𝜑 → seq1( · , 𝐹):ℕ⟶ℕ)
62 bpos.2 . . . . . . . . 9 (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)))
63 bpos.4 . . . . . . . . 9 𝐾 = (⌊‘((2 · 𝑁) / 3))
64 bpos.5 . . . . . . . . 9 𝑀 = (⌊‘(√‘(2 · 𝑁)))
653, 62, 55, 63, 64bposlem4 25984 . . . . . . . 8 (𝜑𝑀 ∈ (3...𝐾))
66 elfzuz 12965 . . . . . . . 8 (𝑀 ∈ (3...𝐾) → 𝑀 ∈ (ℤ‘3))
6765, 66syl 17 . . . . . . 7 (𝜑𝑀 ∈ (ℤ‘3))
68 eluznn 12371 . . . . . . 7 ((3 ∈ ℕ ∧ 𝑀 ∈ (ℤ‘3)) → 𝑀 ∈ ℕ)
6923, 67, 68sylancr 590 . . . . . 6 (𝜑𝑀 ∈ ℕ)
7061, 69ffvelrnd 6849 . . . . 5 (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℕ)
7170nnred 11702 . . . 4 (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℝ)
72 2z 12066 . . . . . . . . 9 2 ∈ ℤ
73 nndivre 11728 . . . . . . . . . . . 12 (((2 · 𝑁) ∈ ℝ ∧ 3 ∈ ℕ) → ((2 · 𝑁) / 3) ∈ ℝ)
7420, 23, 73sylancl 589 . . . . . . . . . . 11 (𝜑 → ((2 · 𝑁) / 3) ∈ ℝ)
7574flcld 13230 . . . . . . . . . 10 (𝜑 → (⌊‘((2 · 𝑁) / 3)) ∈ ℤ)
7663, 75eqeltrid 2856 . . . . . . . . 9 (𝜑𝐾 ∈ ℤ)
77 zmulcl 12083 . . . . . . . . 9 ((2 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (2 · 𝐾) ∈ ℤ)
7872, 76, 77sylancr 590 . . . . . . . 8 (𝜑 → (2 · 𝐾) ∈ ℤ)
792nnzi 12058 . . . . . . . 8 5 ∈ ℤ
80 zsubcl 12076 . . . . . . . 8 (((2 · 𝐾) ∈ ℤ ∧ 5 ∈ ℤ) → ((2 · 𝐾) − 5) ∈ ℤ)
8178, 79, 80sylancl 589 . . . . . . 7 (𝜑 → ((2 · 𝐾) − 5) ∈ ℤ)
8281zred 12139 . . . . . 6 (𝜑 → ((2 · 𝐾) − 5) ∈ ℝ)
83 rpcxpcl 25380 . . . . . 6 ((2 ∈ ℝ+ ∧ ((2 · 𝐾) − 5) ∈ ℝ) → (2↑𝑐((2 · 𝐾) − 5)) ∈ ℝ+)
8431, 82, 83sylancr 590 . . . . 5 (𝜑 → (2↑𝑐((2 · 𝐾) − 5)) ∈ ℝ+)
8584rpred 12485 . . . 4 (𝜑 → (2↑𝑐((2 · 𝐾) − 5)) ∈ ℝ)
8671, 85remulcld 10722 . . 3 (𝜑 → ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2 · 𝐾) − 5))) ∈ ℝ)
873, 62, 55, 63bposlem3 25983 . . . 4 (𝜑 → (seq1( · , 𝐹)‘𝐾) = ((2 · 𝑁)C𝑁))
88 elfzuz3 12966 . . . . . . . . . 10 (𝑀 ∈ (3...𝐾) → 𝐾 ∈ (ℤ𝑀))
8965, 88syl 17 . . . . . . . . 9 (𝜑𝐾 ∈ (ℤ𝑀))
9055, 59, 69, 89pcmptdvds 16299 . . . . . . . 8 (𝜑 → (seq1( · , 𝐹)‘𝑀) ∥ (seq1( · , 𝐹)‘𝐾))
9170nnzd 12138 . . . . . . . . 9 (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℤ)
9270nnne0d 11737 . . . . . . . . 9 (𝜑 → (seq1( · , 𝐹)‘𝑀) ≠ 0)
93 uztrn 12313 . . . . . . . . . . . . 13 ((𝐾 ∈ (ℤ𝑀) ∧ 𝑀 ∈ (ℤ‘3)) → 𝐾 ∈ (ℤ‘3))
9489, 67, 93syl2anc 587 . . . . . . . . . . . 12 (𝜑𝐾 ∈ (ℤ‘3))
95 eluznn 12371 . . . . . . . . . . . 12 ((3 ∈ ℕ ∧ 𝐾 ∈ (ℤ‘3)) → 𝐾 ∈ ℕ)
9623, 94, 95sylancr 590 . . . . . . . . . . 11 (𝜑𝐾 ∈ ℕ)
9761, 96ffvelrnd 6849 . . . . . . . . . 10 (𝜑 → (seq1( · , 𝐹)‘𝐾) ∈ ℕ)
9897nnzd 12138 . . . . . . . . 9 (𝜑 → (seq1( · , 𝐹)‘𝐾) ∈ ℤ)
99 dvdsval2 15671 . . . . . . . . 9 (((seq1( · , 𝐹)‘𝑀) ∈ ℤ ∧ (seq1( · , 𝐹)‘𝑀) ≠ 0 ∧ (seq1( · , 𝐹)‘𝐾) ∈ ℤ) → ((seq1( · , 𝐹)‘𝑀) ∥ (seq1( · , 𝐹)‘𝐾) ↔ ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ))
10091, 92, 98, 99syl3anc 1368 . . . . . . . 8 (𝜑 → ((seq1( · , 𝐹)‘𝑀) ∥ (seq1( · , 𝐹)‘𝐾) ↔ ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ))
10190, 100mpbid 235 . . . . . . 7 (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ)
102101zred 12139 . . . . . 6 (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℝ)
10369nnred 11702 . . . . . . . . 9 (𝜑𝑀 ∈ ℝ)
10476zred 12139 . . . . . . . . 9 (𝜑𝐾 ∈ ℝ)
105 eluzle 12308 . . . . . . . . . 10 (𝐾 ∈ (ℤ𝑀) → 𝑀𝐾)
10689, 105syl 17 . . . . . . . . 9 (𝜑𝑀𝐾)
107 efchtdvds 25857 . . . . . . . . 9 ((𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑀𝐾) → (exp‘(θ‘𝑀)) ∥ (exp‘(θ‘𝐾)))
108103, 104, 106, 107syl3anc 1368 . . . . . . . 8 (𝜑 → (exp‘(θ‘𝑀)) ∥ (exp‘(θ‘𝐾)))
109 efchtcl 25809 . . . . . . . . . . 11 (𝑀 ∈ ℝ → (exp‘(θ‘𝑀)) ∈ ℕ)
110103, 109syl 17 . . . . . . . . . 10 (𝜑 → (exp‘(θ‘𝑀)) ∈ ℕ)
111110nnzd 12138 . . . . . . . . 9 (𝜑 → (exp‘(θ‘𝑀)) ∈ ℤ)
112110nnne0d 11737 . . . . . . . . 9 (𝜑 → (exp‘(θ‘𝑀)) ≠ 0)
113 efchtcl 25809 . . . . . . . . . . 11 (𝐾 ∈ ℝ → (exp‘(θ‘𝐾)) ∈ ℕ)
114104, 113syl 17 . . . . . . . . . 10 (𝜑 → (exp‘(θ‘𝐾)) ∈ ℕ)
115114nnzd 12138 . . . . . . . . 9 (𝜑 → (exp‘(θ‘𝐾)) ∈ ℤ)
116 dvdsval2 15671 . . . . . . . . 9 (((exp‘(θ‘𝑀)) ∈ ℤ ∧ (exp‘(θ‘𝑀)) ≠ 0 ∧ (exp‘(θ‘𝐾)) ∈ ℤ) → ((exp‘(θ‘𝑀)) ∥ (exp‘(θ‘𝐾)) ↔ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℤ))
117111, 112, 115, 116syl3anc 1368 . . . . . . . 8 (𝜑 → ((exp‘(θ‘𝑀)) ∥ (exp‘(θ‘𝐾)) ↔ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℤ))
118108, 117mpbid 235 . . . . . . 7 (𝜑 → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℤ)
119118zred 12139 . . . . . 6 (𝜑 → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℝ)
120 prmz 16085 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
121 fllt 13238 . . . . . . . . . . . . . . . . . 18 (((√‘(2 · 𝑁)) ∈ ℝ ∧ 𝑝 ∈ ℤ) → ((√‘(2 · 𝑁)) < 𝑝 ↔ (⌊‘(√‘(2 · 𝑁))) < 𝑝))
12222, 120, 121syl2an 598 . . . . . . . . . . . . . . . . 17 ((𝜑𝑝 ∈ ℙ) → ((√‘(2 · 𝑁)) < 𝑝 ↔ (⌊‘(√‘(2 · 𝑁))) < 𝑝))
12364breq1i 5043 . . . . . . . . . . . . . . . . 17 (𝑀 < 𝑝 ↔ (⌊‘(√‘(2 · 𝑁))) < 𝑝)
124122, 123bitr4di 292 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 ∈ ℙ) → ((√‘(2 · 𝑁)) < 𝑝𝑀 < 𝑝))
125120zred 12139 . . . . . . . . . . . . . . . . 17 (𝑝 ∈ ℙ → 𝑝 ∈ ℝ)
126 ltnle 10771 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℝ ∧ 𝑝 ∈ ℝ) → (𝑀 < 𝑝 ↔ ¬ 𝑝𝑀))
127103, 125, 126syl2an 598 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 ∈ ℙ) → (𝑀 < 𝑝 ↔ ¬ 𝑝𝑀))
128124, 127bitrd 282 . . . . . . . . . . . . . . 15 ((𝜑𝑝 ∈ ℙ) → ((√‘(2 · 𝑁)) < 𝑝 ↔ ¬ 𝑝𝑀))
129 bposlem1 25981 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁))
1305, 129sylan 583 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁))
131125adantl 485 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑝 ∈ ℙ) → 𝑝 ∈ ℝ)
132 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 ∈ ℙ → 𝑝 ∈ ℙ)
133 pccl 16255 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑝 ∈ ℙ ∧ ((2 · 𝑁)C𝑁) ∈ ℕ) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
134132, 14, 133syl2anr 599 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑝 ∈ ℙ) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
135131, 134reexpcld 13590 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ∈ ℝ)
13620adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑝 ∈ ℙ) → (2 · 𝑁) ∈ ℝ)
137131resqcld 13674 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑝 ∈ ℙ) → (𝑝↑2) ∈ ℝ)
138 lelttr 10782 . . . . . . . . . . . . . . . . . . . 20 (((𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ∈ ℝ ∧ (2 · 𝑁) ∈ ℝ ∧ (𝑝↑2) ∈ ℝ) → (((𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁) ∧ (2 · 𝑁) < (𝑝↑2)) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) < (𝑝↑2)))
139135, 136, 137, 138syl3anc 1368 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑝 ∈ ℙ) → (((𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁) ∧ (2 · 𝑁) < (𝑝↑2)) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) < (𝑝↑2)))
140130, 139mpand 694 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑝 ∈ ℙ) → ((2 · 𝑁) < (𝑝↑2) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) < (𝑝↑2)))
141 resqrtth 14676 . . . . . . . . . . . . . . . . . . . . 21 (((2 · 𝑁) ∈ ℝ ∧ 0 ≤ (2 · 𝑁)) → ((√‘(2 · 𝑁))↑2) = (2 · 𝑁))
14220, 21, 141syl2anc 587 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((√‘(2 · 𝑁))↑2) = (2 · 𝑁))
143142breq1d 5046 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((√‘(2 · 𝑁))↑2) < (𝑝↑2) ↔ (2 · 𝑁) < (𝑝↑2)))
144143adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑝 ∈ ℙ) → (((√‘(2 · 𝑁))↑2) < (𝑝↑2) ↔ (2 · 𝑁) < (𝑝↑2)))
145134nn0zd 12137 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑝 ∈ ℙ) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ∈ ℤ)
14672a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑝 ∈ ℙ) → 2 ∈ ℤ)
147 prmgt1 16107 . . . . . . . . . . . . . . . . . . . 20 (𝑝 ∈ ℙ → 1 < 𝑝)
148147adantl 485 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑝 ∈ ℙ) → 1 < 𝑝)
149131, 145, 146, 148ltexp2d 13677 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑝 ∈ ℙ) → ((𝑝 pCnt ((2 · 𝑁)C𝑁)) < 2 ↔ (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) < (𝑝↑2)))
150140, 144, 1493imtr4d 297 . . . . . . . . . . . . . . . . 17 ((𝜑𝑝 ∈ ℙ) → (((√‘(2 · 𝑁))↑2) < (𝑝↑2) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) < 2))
151 df-2 11750 . . . . . . . . . . . . . . . . . 18 2 = (1 + 1)
152151breq2i 5044 . . . . . . . . . . . . . . . . 17 ((𝑝 pCnt ((2 · 𝑁)C𝑁)) < 2 ↔ (𝑝 pCnt ((2 · 𝑁)C𝑁)) < (1 + 1))
153150, 152syl6ib 254 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 ∈ ℙ) → (((√‘(2 · 𝑁))↑2) < (𝑝↑2) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) < (1 + 1)))
15422adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑𝑝 ∈ ℙ) → (√‘(2 · 𝑁)) ∈ ℝ)
15520, 21sqrtge0d 14841 . . . . . . . . . . . . . . . . . 18 (𝜑 → 0 ≤ (√‘(2 · 𝑁)))
156155adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑𝑝 ∈ ℙ) → 0 ≤ (√‘(2 · 𝑁)))
157 prmnn 16084 . . . . . . . . . . . . . . . . . . . 20 (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
158157nnrpd 12483 . . . . . . . . . . . . . . . . . . 19 (𝑝 ∈ ℙ → 𝑝 ∈ ℝ+)
159158rpge0d 12489 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ ℙ → 0 ≤ 𝑝)
160159adantl 485 . . . . . . . . . . . . . . . . 17 ((𝜑𝑝 ∈ ℙ) → 0 ≤ 𝑝)
161154, 131, 156, 160lt2sqd 13682 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 ∈ ℙ) → ((√‘(2 · 𝑁)) < 𝑝 ↔ ((√‘(2 · 𝑁))↑2) < (𝑝↑2)))
162 1z 12064 . . . . . . . . . . . . . . . . 17 1 ∈ ℤ
163 zleltp1 12085 . . . . . . . . . . . . . . . . 17 (((𝑝 pCnt ((2 · 𝑁)C𝑁)) ∈ ℤ ∧ 1 ∈ ℤ) → ((𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1 ↔ (𝑝 pCnt ((2 · 𝑁)C𝑁)) < (1 + 1)))
164145, 162, 163sylancl 589 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 ∈ ℙ) → ((𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1 ↔ (𝑝 pCnt ((2 · 𝑁)C𝑁)) < (1 + 1)))
165153, 161, 1643imtr4d 297 . . . . . . . . . . . . . . 15 ((𝜑𝑝 ∈ ℙ) → ((√‘(2 · 𝑁)) < 𝑝 → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1))
166128, 165sylbird 263 . . . . . . . . . . . . . 14 ((𝜑𝑝 ∈ ℙ) → (¬ 𝑝𝑀 → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1))
167166imp 410 . . . . . . . . . . . . 13 (((𝜑𝑝 ∈ ℙ) ∧ ¬ 𝑝𝑀) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1)
168167adantrl 715 . . . . . . . . . . . 12 (((𝜑𝑝 ∈ ℙ) ∧ (𝑝𝐾 ∧ ¬ 𝑝𝑀)) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1)
169 iftrue 4429 . . . . . . . . . . . . 13 ((𝑝𝐾 ∧ ¬ 𝑝𝑀) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = (𝑝 pCnt ((2 · 𝑁)C𝑁)))
170169adantl 485 . . . . . . . . . . . 12 (((𝜑𝑝 ∈ ℙ) ∧ (𝑝𝐾 ∧ ¬ 𝑝𝑀)) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = (𝑝 pCnt ((2 · 𝑁)C𝑁)))
171 iftrue 4429 . . . . . . . . . . . . 13 ((𝑝𝐾 ∧ ¬ 𝑝𝑀) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0) = 1)
172171adantl 485 . . . . . . . . . . . 12 (((𝜑𝑝 ∈ ℙ) ∧ (𝑝𝐾 ∧ ¬ 𝑝𝑀)) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0) = 1)
173168, 170, 1723brtr4d 5068 . . . . . . . . . . 11 (((𝜑𝑝 ∈ ℙ) ∧ (𝑝𝐾 ∧ ¬ 𝑝𝑀)) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0))
174 0le0 11788 . . . . . . . . . . . . 13 0 ≤ 0
175 iffalse 4432 . . . . . . . . . . . . . 14 (¬ (𝑝𝐾 ∧ ¬ 𝑝𝑀) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = 0)
176 iffalse 4432 . . . . . . . . . . . . . 14 (¬ (𝑝𝐾 ∧ ¬ 𝑝𝑀) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0) = 0)
177175, 176breq12d 5049 . . . . . . . . . . . . 13 (¬ (𝑝𝐾 ∧ ¬ 𝑝𝑀) → (if((𝑝𝐾 ∧ ¬ 𝑝𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0) ↔ 0 ≤ 0))
178174, 177mpbiri 261 . . . . . . . . . . . 12 (¬ (𝑝𝐾 ∧ ¬ 𝑝𝑀) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0))
179178adantl 485 . . . . . . . . . . 11 (((𝜑𝑝 ∈ ℙ) ∧ ¬ (𝑝𝐾 ∧ ¬ 𝑝𝑀)) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0))
180173, 179pm2.61dan 812 . . . . . . . . . 10 ((𝜑𝑝 ∈ ℙ) → if((𝑝𝐾 ∧ ¬ 𝑝𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0))
18159adantr 484 . . . . . . . . . . 11 ((𝜑𝑝 ∈ ℙ) → ∀𝑛 ∈ ℙ (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
18269adantr 484 . . . . . . . . . . 11 ((𝜑𝑝 ∈ ℙ) → 𝑀 ∈ ℕ)
183 simpr 488 . . . . . . . . . . 11 ((𝜑𝑝 ∈ ℙ) → 𝑝 ∈ ℙ)
184 oveq1 7163 . . . . . . . . . . 11 (𝑛 = 𝑝 → (𝑛 pCnt ((2 · 𝑁)C𝑁)) = (𝑝 pCnt ((2 · 𝑁)C𝑁)))
18589adantr 484 . . . . . . . . . . 11 ((𝜑𝑝 ∈ ℙ) → 𝐾 ∈ (ℤ𝑀))
18655, 181, 182, 183, 184, 185pcmpt2 16298 . . . . . . . . . 10 ((𝜑𝑝 ∈ ℙ) → (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) = if((𝑝𝐾 ∧ ¬ 𝑝𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0))
187 eqid 2758 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1))
188187prmorcht 25876 . . . . . . . . . . . . . . 15 (𝐾 ∈ ℕ → (exp‘(θ‘𝐾)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾))
18996, 188syl 17 . . . . . . . . . . . . . 14 (𝜑 → (exp‘(θ‘𝐾)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾))
190187prmorcht 25876 . . . . . . . . . . . . . . 15 (𝑀 ∈ ℕ → (exp‘(θ‘𝑀)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀))
19169, 190syl 17 . . . . . . . . . . . . . 14 (𝜑 → (exp‘(θ‘𝑀)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀))
192189, 191oveq12d 7174 . . . . . . . . . . . . 13 (𝜑 → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) = ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾) / (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀)))
193192adantr 484 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ ℙ) → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) = ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾) / (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀)))
194193oveq2d 7172 . . . . . . . . . . 11 ((𝜑𝑝 ∈ ℙ) → (𝑝 pCnt ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))) = (𝑝 pCnt ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾) / (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀))))
195 nncn 11695 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
196195exp1d 13568 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (𝑛↑1) = 𝑛)
197196ifeq1d 4442 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → if(𝑛 ∈ ℙ, (𝑛↑1), 1) = if(𝑛 ∈ ℙ, 𝑛, 1))
198197mpteq2ia 5127 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑1), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1))
199198eqcomi 2767 . . . . . . . . . . . 12 (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑1), 1))
200 1nn0 11963 . . . . . . . . . . . . . . 15 1 ∈ ℕ0
201200a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℙ) → 1 ∈ ℕ0)
202201ralrimiva 3113 . . . . . . . . . . . . 13 (𝜑 → ∀𝑛 ∈ ℙ 1 ∈ ℕ0)
203202adantr 484 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ ℙ) → ∀𝑛 ∈ ℙ 1 ∈ ℕ0)
204 eqidd 2759 . . . . . . . . . . . 12 (𝑛 = 𝑝 → 1 = 1)
205199, 203, 182, 183, 204, 185pcmpt2 16298 . . . . . . . . . . 11 ((𝜑𝑝 ∈ ℙ) → (𝑝 pCnt ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾) / (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀))) = if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0))
206194, 205eqtrd 2793 . . . . . . . . . 10 ((𝜑𝑝 ∈ ℙ) → (𝑝 pCnt ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))) = if((𝑝𝐾 ∧ ¬ 𝑝𝑀), 1, 0))
207180, 186, 2063brtr4d 5068 . . . . . . . . 9 ((𝜑𝑝 ∈ ℙ) → (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) ≤ (𝑝 pCnt ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))))
208207ralrimiva 3113 . . . . . . . 8 (𝜑 → ∀𝑝 ∈ ℙ (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) ≤ (𝑝 pCnt ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))))
209 pc2dvds 16284 . . . . . . . . 9 ((((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ ∧ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℤ) → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) ≤ (𝑝 pCnt ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))))))
210101, 118, 209syl2anc 587 . . . . . . . 8 (𝜑 → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) ≤ (𝑝 pCnt ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))))))
211208, 210mpbird 260 . . . . . . 7 (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))))
212114nnred 11702 . . . . . . . . . 10 (𝜑 → (exp‘(θ‘𝐾)) ∈ ℝ)
213110nnred 11702 . . . . . . . . . 10 (𝜑 → (exp‘(θ‘𝑀)) ∈ ℝ)
214114nngt0d 11736 . . . . . . . . . 10 (𝜑 → 0 < (exp‘(θ‘𝐾)))
215110nngt0d 11736 . . . . . . . . . 10 (𝜑 → 0 < (exp‘(θ‘𝑀)))
216212, 213, 214, 215divgt0d 11626 . . . . . . . . 9 (𝜑 → 0 < ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))))
217 elnnz 12043 . . . . . . . . 9 (((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℕ ↔ (((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℤ ∧ 0 < ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))))
218118, 216, 217sylanbrc 586 . . . . . . . 8 (𝜑 → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℕ)
219 dvdsle 15724 . . . . . . . 8 ((((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ ∧ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℕ) → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ≤ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))))
220101, 218, 219syl2anc 587 . . . . . . 7 (𝜑 → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ≤ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))))
221211, 220mpd 15 . . . . . 6 (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ≤ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))))
222 nndivre 11728 . . . . . . . 8 (((exp‘(θ‘𝐾)) ∈ ℝ ∧ 4 ∈ ℕ) → ((exp‘(θ‘𝐾)) / 4) ∈ ℝ)
223212, 1, 222sylancl 589 . . . . . . 7 (𝜑 → ((exp‘(θ‘𝐾)) / 4) ∈ ℝ)
224 4re 11771 . . . . . . . . . 10 4 ∈ ℝ
225224a1i 11 . . . . . . . . 9 (𝜑 → 4 ∈ ℝ)
226 6re 11777 . . . . . . . . . 10 6 ∈ ℝ
227226a1i 11 . . . . . . . . 9 (𝜑 → 6 ∈ ℝ)
228 4lt6 11869 . . . . . . . . . 10 4 < 6
229228a1i 11 . . . . . . . . 9 (𝜑 → 4 < 6)
230 cht3 25871 . . . . . . . . . . . 12 (θ‘3) = (log‘6)
231230fveq2i 6666 . . . . . . . . . . 11 (exp‘(θ‘3)) = (exp‘(log‘6))
232 6pos 11797 . . . . . . . . . . . . 13 0 < 6
233226, 232elrpii 12446 . . . . . . . . . . . 12 6 ∈ ℝ+
234 reeflog 25285 . . . . . . . . . . . 12 (6 ∈ ℝ+ → (exp‘(log‘6)) = 6)
235233, 234ax-mp 5 . . . . . . . . . . 11 (exp‘(log‘6)) = 6
236231, 235eqtri 2781 . . . . . . . . . 10 (exp‘(θ‘3)) = 6
237 3re 11767 . . . . . . . . . . . . 13 3 ∈ ℝ
238237a1i 11 . . . . . . . . . . . 12 (𝜑 → 3 ∈ ℝ)
239 eluzle 12308 . . . . . . . . . . . . 13 (𝑀 ∈ (ℤ‘3) → 3 ≤ 𝑀)
24067, 239syl 17 . . . . . . . . . . . 12 (𝜑 → 3 ≤ 𝑀)
241 chtwordi 25854 . . . . . . . . . . . 12 ((3 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 3 ≤ 𝑀) → (θ‘3) ≤ (θ‘𝑀))
242238, 103, 240, 241syl3anc 1368 . . . . . . . . . . 11 (𝜑 → (θ‘3) ≤ (θ‘𝑀))
243 chtcl 25807 . . . . . . . . . . . . 13 (3 ∈ ℝ → (θ‘3) ∈ ℝ)
244237, 243ax-mp 5 . . . . . . . . . . . 12 (θ‘3) ∈ ℝ
245 chtcl 25807 . . . . . . . . . . . . 13 (𝑀 ∈ ℝ → (θ‘𝑀) ∈ ℝ)
246103, 245syl 17 . . . . . . . . . . . 12 (𝜑 → (θ‘𝑀) ∈ ℝ)
247 efle 15532 . . . . . . . . . . . 12 (((θ‘3) ∈ ℝ ∧ (θ‘𝑀) ∈ ℝ) → ((θ‘3) ≤ (θ‘𝑀) ↔ (exp‘(θ‘3)) ≤ (exp‘(θ‘𝑀))))
248244, 246, 247sylancr 590 . . . . . . . . . . 11 (𝜑 → ((θ‘3) ≤ (θ‘𝑀) ↔ (exp‘(θ‘3)) ≤ (exp‘(θ‘𝑀))))
249242, 248mpbid 235 . . . . . . . . . 10 (𝜑 → (exp‘(θ‘3)) ≤ (exp‘(θ‘𝑀)))
250236, 249eqbrtrrid 5072 . . . . . . . . 9 (𝜑 → 6 ≤ (exp‘(θ‘𝑀)))
251225, 227, 213, 229, 250ltletrd 10851 . . . . . . . 8 (𝜑 → 4 < (exp‘(θ‘𝑀)))
252 4pos 11794 . . . . . . . . . 10 0 < 4
253252a1i 11 . . . . . . . . 9 (𝜑 → 0 < 4)
254 ltdiv2 11577 . . . . . . . . 9 (((4 ∈ ℝ ∧ 0 < 4) ∧ ((exp‘(θ‘𝑀)) ∈ ℝ ∧ 0 < (exp‘(θ‘𝑀))) ∧ ((exp‘(θ‘𝐾)) ∈ ℝ ∧ 0 < (exp‘(θ‘𝐾)))) → (4 < (exp‘(θ‘𝑀)) ↔ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) < ((exp‘(θ‘𝐾)) / 4)))
255225, 253, 213, 215, 212, 214, 254syl222anc 1383 . . . . . . . 8 (𝜑 → (4 < (exp‘(θ‘𝑀)) ↔ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) < ((exp‘(θ‘𝐾)) / 4)))
256251, 255mpbid 235 . . . . . . 7 (𝜑 → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) < ((exp‘(θ‘𝐾)) / 4))
25726a1i 11 . . . . . . . . . . . . 13 (𝜑 → 2 ∈ ℝ)
258 2lt3 11859 . . . . . . . . . . . . . 14 2 < 3
259258a1i 11 . . . . . . . . . . . . 13 (𝜑 → 2 < 3)
260238, 103, 104, 240, 106letrd 10848 . . . . . . . . . . . . 13 (𝜑 → 3 ≤ 𝐾)
261257, 238, 104, 259, 260ltletrd 10851 . . . . . . . . . . . 12 (𝜑 → 2 < 𝐾)
262 chtub 25909 . . . . . . . . . . . 12 ((𝐾 ∈ ℝ ∧ 2 < 𝐾) → (θ‘𝐾) < ((log‘2) · ((2 · 𝐾) − 3)))
263104, 261, 262syl2anc 587 . . . . . . . . . . 11 (𝜑 → (θ‘𝐾) < ((log‘2) · ((2 · 𝐾) − 3)))
264 chtcl 25807 . . . . . . . . . . . . 13 (𝐾 ∈ ℝ → (θ‘𝐾) ∈ ℝ)
265104, 264syl 17 . . . . . . . . . . . 12 (𝜑 → (θ‘𝐾) ∈ ℝ)
266 relogcl 25280 . . . . . . . . . . . . . 14 (2 ∈ ℝ+ → (log‘2) ∈ ℝ)
26731, 266ax-mp 5 . . . . . . . . . . . . 13 (log‘2) ∈ ℝ
268 3z 12067 . . . . . . . . . . . . . . 15 3 ∈ ℤ
269 zsubcl 12076 . . . . . . . . . . . . . . 15 (((2 · 𝐾) ∈ ℤ ∧ 3 ∈ ℤ) → ((2 · 𝐾) − 3) ∈ ℤ)
27078, 268, 269sylancl 589 . . . . . . . . . . . . . 14 (𝜑 → ((2 · 𝐾) − 3) ∈ ℤ)
271270zred 12139 . . . . . . . . . . . . 13 (𝜑 → ((2 · 𝐾) − 3) ∈ ℝ)
272 remulcl 10673 . . . . . . . . . . . . 13 (((log‘2) ∈ ℝ ∧ ((2 · 𝐾) − 3) ∈ ℝ) → ((log‘2) · ((2 · 𝐾) − 3)) ∈ ℝ)
273267, 271, 272sylancr 590 . . . . . . . . . . . 12 (𝜑 → ((log‘2) · ((2 · 𝐾) − 3)) ∈ ℝ)
274 eflt 15531 . . . . . . . . . . . 12 (((θ‘𝐾) ∈ ℝ ∧ ((log‘2) · ((2 · 𝐾) − 3)) ∈ ℝ) → ((θ‘𝐾) < ((log‘2) · ((2 · 𝐾) − 3)) ↔ (exp‘(θ‘𝐾)) < (exp‘((log‘2) · ((2 · 𝐾) − 3)))))
275265, 273, 274syl2anc 587 . . . . . . . . . . 11 (𝜑 → ((θ‘𝐾) < ((log‘2) · ((2 · 𝐾) − 3)) ↔ (exp‘(θ‘𝐾)) < (exp‘((log‘2) · ((2 · 𝐾) − 3)))))
276263, 275mpbid 235 . . . . . . . . . 10 (𝜑 → (exp‘(θ‘𝐾)) < (exp‘((log‘2) · ((2 · 𝐾) − 3))))
277 reexplog 25299 . . . . . . . . . . . 12 ((2 ∈ ℝ+ ∧ ((2 · 𝐾) − 3) ∈ ℤ) → (2↑((2 · 𝐾) − 3)) = (exp‘(((2 · 𝐾) − 3) · (log‘2))))
27831, 270, 277sylancr 590 . . . . . . . . . . 11 (𝜑 → (2↑((2 · 𝐾) − 3)) = (exp‘(((2 · 𝐾) − 3) · (log‘2))))
279270zcnd 12140 . . . . . . . . . . . . 13 (𝜑 → ((2 · 𝐾) − 3) ∈ ℂ)
280267recni 10706 . . . . . . . . . . . . 13 (log‘2) ∈ ℂ
281 mulcom 10674 . . . . . . . . . . . . 13 ((((2 · 𝐾) − 3) ∈ ℂ ∧ (log‘2) ∈ ℂ) → (((2 · 𝐾) − 3) · (log‘2)) = ((log‘2) · ((2 · 𝐾) − 3)))
282279, 280, 281sylancl 589 . . . . . . . . . . . 12 (𝜑 → (((2 · 𝐾) − 3) · (log‘2)) = ((log‘2) · ((2 · 𝐾) − 3)))
283282fveq2d 6667 . . . . . . . . . . 11 (𝜑 → (exp‘(((2 · 𝐾) − 3) · (log‘2))) = (exp‘((log‘2) · ((2 · 𝐾) − 3))))
284278, 283eqtrd 2793 . . . . . . . . . 10 (𝜑 → (2↑((2 · 𝐾) − 3)) = (exp‘((log‘2) · ((2 · 𝐾) − 3))))
285276, 284breqtrrd 5064 . . . . . . . . 9 (𝜑 → (exp‘(θ‘𝐾)) < (2↑((2 · 𝐾) − 3)))
286 3p2e5 11838 . . . . . . . . . . . . . . . 16 (3 + 2) = 5
287286oveq1i 7166 . . . . . . . . . . . . . . 15 ((3 + 2) − 2) = (5 − 2)
288 3cn 11768 . . . . . . . . . . . . . . . 16 3 ∈ ℂ
289 2cn 11762 . . . . . . . . . . . . . . . 16 2 ∈ ℂ
290288, 289pncan3oi 10953 . . . . . . . . . . . . . . 15 ((3 + 2) − 2) = 3
291287, 290eqtr3i 2783 . . . . . . . . . . . . . 14 (5 − 2) = 3
292291oveq2i 7167 . . . . . . . . . . . . 13 ((2 · 𝐾) − (5 − 2)) = ((2 · 𝐾) − 3)
29378zcnd 12140 . . . . . . . . . . . . . 14 (𝜑 → (2 · 𝐾) ∈ ℂ)
294 5cn 11775 . . . . . . . . . . . . . . 15 5 ∈ ℂ
295 subsub 10967 . . . . . . . . . . . . . . 15 (((2 · 𝐾) ∈ ℂ ∧ 5 ∈ ℂ ∧ 2 ∈ ℂ) → ((2 · 𝐾) − (5 − 2)) = (((2 · 𝐾) − 5) + 2))
296294, 289, 295mp3an23 1450 . . . . . . . . . . . . . 14 ((2 · 𝐾) ∈ ℂ → ((2 · 𝐾) − (5 − 2)) = (((2 · 𝐾) − 5) + 2))
297293, 296syl 17 . . . . . . . . . . . . 13 (𝜑 → ((2 · 𝐾) − (5 − 2)) = (((2 · 𝐾) − 5) + 2))
298292, 297eqtr3id 2807 . . . . . . . . . . . 12 (𝜑 → ((2 · 𝐾) − 3) = (((2 · 𝐾) − 5) + 2))
299298oveq2d 7172 . . . . . . . . . . 11 (𝜑 → (2↑𝑐((2 · 𝐾) − 3)) = (2↑𝑐(((2 · 𝐾) − 5) + 2)))
300 2ne0 11791 . . . . . . . . . . . 12 2 ≠ 0
301 cxpexpz 25371 . . . . . . . . . . . 12 ((2 ∈ ℂ ∧ 2 ≠ 0 ∧ ((2 · 𝐾) − 3) ∈ ℤ) → (2↑𝑐((2 · 𝐾) − 3)) = (2↑((2 · 𝐾) − 3)))
302289, 300, 270, 301mp3an12i 1462 . . . . . . . . . . 11 (𝜑 → (2↑𝑐((2 · 𝐾) − 3)) = (2↑((2 · 𝐾) − 3)))
30381zcnd 12140 . . . . . . . . . . . 12 (𝜑 → ((2 · 𝐾) − 5) ∈ ℂ)
304 2cnne0 11897 . . . . . . . . . . . . 13 (2 ∈ ℂ ∧ 2 ≠ 0)
305 cxpadd 25383 . . . . . . . . . . . . 13 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ ((2 · 𝐾) − 5) ∈ ℂ ∧ 2 ∈ ℂ) → (2↑𝑐(((2 · 𝐾) − 5) + 2)) = ((2↑𝑐((2 · 𝐾) − 5)) · (2↑𝑐2)))
306304, 289, 305mp3an13 1449 . . . . . . . . . . . 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 2801 . . . . . . . . . 10 (𝜑 → (2↑((2 · 𝐾) − 3)) = ((2↑𝑐((2 · 𝐾) − 5)) · (2↑𝑐2)))
309 2nn0 11964 . . . . . . . . . . . . 13 2 ∈ ℕ0
310 cxpexp 25372 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ 2 ∈ ℕ0) → (2↑𝑐2) = (2↑2))
311289, 309, 310mp2an 691 . . . . . . . . . . . 12 (2↑𝑐2) = (2↑2)
312 sq2 13623 . . . . . . . . . . . 12 (2↑2) = 4
313311, 312eqtri 2781 . . . . . . . . . . 11 (2↑𝑐2) = 4
314313oveq2i 7167 . . . . . . . . . 10 ((2↑𝑐((2 · 𝐾) − 5)) · (2↑𝑐2)) = ((2↑𝑐((2 · 𝐾) − 5)) · 4)
315308, 314eqtrdi 2809 . . . . . . . . 9 (𝜑 → (2↑((2 · 𝐾) − 3)) = ((2↑𝑐((2 · 𝐾) − 5)) · 4))
316285, 315breqtrd 5062 . . . . . . . 8 (𝜑 → (exp‘(θ‘𝐾)) < ((2↑𝑐((2 · 𝐾) − 5)) · 4))
317224, 252pm3.2i 474 . . . . . . . . . 10 (4 ∈ ℝ ∧ 0 < 4)
318317a1i 11 . . . . . . . . 9 (𝜑 → (4 ∈ ℝ ∧ 0 < 4))
319 ltdivmul2 11568 . . . . . . . . 9 (((exp‘(θ‘𝐾)) ∈ ℝ ∧ (2↑𝑐((2 · 𝐾) − 5)) ∈ ℝ ∧ (4 ∈ ℝ ∧ 0 < 4)) → (((exp‘(θ‘𝐾)) / 4) < (2↑𝑐((2 · 𝐾) − 5)) ↔ (exp‘(θ‘𝐾)) < ((2↑𝑐((2 · 𝐾) − 5)) · 4)))
320212, 85, 318, 319syl3anc 1368 . . . . . . . 8 (𝜑 → (((exp‘(θ‘𝐾)) / 4) < (2↑𝑐((2 · 𝐾) − 5)) ↔ (exp‘(θ‘𝐾)) < ((2↑𝑐((2 · 𝐾) − 5)) · 4)))
321316, 320mpbird 260 . . . . . . 7 (𝜑 → ((exp‘(θ‘𝐾)) / 4) < (2↑𝑐((2 · 𝐾) − 5)))
322119, 223, 85, 256, 321lttrd 10852 . . . . . 6 (𝜑 → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) < (2↑𝑐((2 · 𝐾) − 5)))
323102, 119, 85, 221, 322lelttrd 10849 . . . . 5 (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) < (2↑𝑐((2 · 𝐾) − 5)))
32497nnred 11702 . . . . . 6 (𝜑 → (seq1( · , 𝐹)‘𝐾) ∈ ℝ)
325 nnre 11694 . . . . . . . 8 ((seq1( · , 𝐹)‘𝑀) ∈ ℕ → (seq1( · , 𝐹)‘𝑀) ∈ ℝ)
326 nngt0 11718 . . . . . . . 8 ((seq1( · , 𝐹)‘𝑀) ∈ ℕ → 0 < (seq1( · , 𝐹)‘𝑀))
327325, 326jca 515 . . . . . . 7 ((seq1( · , 𝐹)‘𝑀) ∈ ℕ → ((seq1( · , 𝐹)‘𝑀) ∈ ℝ ∧ 0 < (seq1( · , 𝐹)‘𝑀)))
32870, 327syl 17 . . . . . 6 (𝜑 → ((seq1( · , 𝐹)‘𝑀) ∈ ℝ ∧ 0 < (seq1( · , 𝐹)‘𝑀)))
329 ltdivmul 11566 . . . . . 6 (((seq1( · , 𝐹)‘𝐾) ∈ ℝ ∧ (2↑𝑐((2 · 𝐾) − 5)) ∈ ℝ ∧ ((seq1( · , 𝐹)‘𝑀) ∈ ℝ ∧ 0 < (seq1( · , 𝐹)‘𝑀))) → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) < (2↑𝑐((2 · 𝐾) − 5)) ↔ (seq1( · , 𝐹)‘𝐾) < ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2 · 𝐾) − 5)))))
330324, 85, 328, 329syl3anc 1368 . . . . 5 (𝜑 → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) < (2↑𝑐((2 · 𝐾) − 5)) ↔ (seq1( · , 𝐹)‘𝐾) < ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2 · 𝐾) − 5)))))
331323, 330mpbid 235 . . . 4 (𝜑 → (seq1( · , 𝐹)‘𝐾) < ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2 · 𝐾) − 5))))
33287, 331eqbrtrrd 5060 . . 3 (𝜑 → ((2 · 𝑁)C𝑁) < ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2 · 𝐾) − 5))))
33330, 85remulcld 10722 . . . 4 (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐((2 · 𝐾) − 5))) ∈ ℝ)
3343, 62, 55, 63, 64bposlem5 25985 . . . . 5 (𝜑 → (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)))
33571, 30, 84lemul1d 12528 . . . . 5 (𝜑 → ((seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) ↔ ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2 · 𝐾) − 5))) ≤ (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐((2 · 𝐾) − 5)))))
336334, 335mpbid 235 . . . 4 (𝜑 → ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2 · 𝐾) − 5))) ≤ (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐((2 · 𝐾) − 5))))
33778zred 12139 . . . . . . 7 (𝜑 → (2 · 𝐾) ∈ ℝ)
33837a1i 11 . . . . . . 7 (𝜑 → 5 ∈ ℝ)
339 flle 13231 . . . . . . . . . . 11 (((2 · 𝑁) / 3) ∈ ℝ → (⌊‘((2 · 𝑁) / 3)) ≤ ((2 · 𝑁) / 3))
34074, 339syl 17 . . . . . . . . . 10 (𝜑 → (⌊‘((2 · 𝑁) / 3)) ≤ ((2 · 𝑁) / 3))
34163, 340eqbrtrid 5071 . . . . . . . . 9 (𝜑𝐾 ≤ ((2 · 𝑁) / 3))
342 2pos 11790 . . . . . . . . . . . 12 0 < 2
34326, 342pm3.2i 474 . . . . . . . . . . 11 (2 ∈ ℝ ∧ 0 < 2)
344343a1i 11 . . . . . . . . . 10 (𝜑 → (2 ∈ ℝ ∧ 0 < 2))
345 lemul2 11544 . . . . . . . . . 10 ((𝐾 ∈ ℝ ∧ ((2 · 𝑁) / 3) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝐾 ≤ ((2 · 𝑁) / 3) ↔ (2 · 𝐾) ≤ (2 · ((2 · 𝑁) / 3))))
346104, 74, 344, 345syl3anc 1368 . . . . . . . . 9 (𝜑 → (𝐾 ≤ ((2 · 𝑁) / 3) ↔ (2 · 𝐾) ≤ (2 · ((2 · 𝑁) / 3))))
347341, 346mpbid 235 . . . . . . . 8 (𝜑 → (2 · 𝐾) ≤ (2 · ((2 · 𝑁) / 3)))
34818nncnd 11703 . . . . . . . . . 10 (𝜑 → (2 · 𝑁) ∈ ℂ)
349 3ne0 11793 . . . . . . . . . . . 12 3 ≠ 0
350288, 349pm3.2i 474 . . . . . . . . . . 11 (3 ∈ ℂ ∧ 3 ≠ 0)
351 divass 11367 . . . . . . . . . . 11 ((2 ∈ ℂ ∧ (2 · 𝑁) ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((2 · (2 · 𝑁)) / 3) = (2 · ((2 · 𝑁) / 3)))
352289, 350, 351mp3an13 1449 . . . . . . . . . 10 ((2 · 𝑁) ∈ ℂ → ((2 · (2 · 𝑁)) / 3) = (2 · ((2 · 𝑁) / 3)))
353348, 352syl 17 . . . . . . . . 9 (𝜑 → ((2 · (2 · 𝑁)) / 3) = (2 · ((2 · 𝑁) / 3)))
354 2t2e4 11851 . . . . . . . . . . . 12 (2 · 2) = 4
355354oveq1i 7166 . . . . . . . . . . 11 ((2 · 2) · 𝑁) = (4 · 𝑁)
3565nncnd 11703 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℂ)
357 mulass 10676 . . . . . . . . . . . 12 ((2 ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((2 · 2) · 𝑁) = (2 · (2 · 𝑁)))
358289, 289, 356, 357mp3an12i 1462 . . . . . . . . . . 11 (𝜑 → ((2 · 2) · 𝑁) = (2 · (2 · 𝑁)))
359355, 358syl5reqr 2808 . . . . . . . . . 10 (𝜑 → (2 · (2 · 𝑁)) = (4 · 𝑁))
360359oveq1d 7171 . . . . . . . . 9 (𝜑 → ((2 · (2 · 𝑁)) / 3) = ((4 · 𝑁) / 3))
361353, 360eqtr3d 2795 . . . . . . . 8 (𝜑 → (2 · ((2 · 𝑁) / 3)) = ((4 · 𝑁) / 3))
362347, 361breqtrd 5062 . . . . . . 7 (𝜑 → (2 · 𝐾) ≤ ((4 · 𝑁) / 3))
363337, 36, 338, 362lesub1dd 11307 . . . . . 6 (𝜑 → ((2 · 𝐾) − 5) ≤ (((4 · 𝑁) / 3) − 5))
364 1lt2 11858 . . . . . . . 8 1 < 2
365364a1i 11 . . . . . . 7 (𝜑 → 1 < 2)
366257, 365, 82, 39cxpled 25424 . . . . . 6 (𝜑 → (((2 · 𝐾) − 5) ≤ (((4 · 𝑁) / 3) − 5) ↔ (2↑𝑐((2 · 𝐾) − 5)) ≤ (2↑𝑐(((4 · 𝑁) / 3) − 5))))
367363, 366mpbid 235 . . . . 5 (𝜑 → (2↑𝑐((2 · 𝐾) − 5)) ≤ (2↑𝑐(((4 · 𝑁) / 3) − 5)))
36885, 42, 29lemul2d 12529 . . . . 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 235 . . . 4 (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐((2 · 𝐾) − 5))) ≤ (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))))
37086, 333, 43, 336, 369letrd 10848 . . 3 (𝜑 → ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2 · 𝐾) − 5))) ≤ (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))))
37115, 86, 43, 332, 370ltletrd 10851 . 2 (𝜑 → ((2 · 𝑁)C𝑁) < (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))))
37210, 15, 43, 54, 371lttrd 10852 1 (𝜑 → ((4↑𝑁) / 𝑁) < (((2 · 𝑁)↑𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑𝑐(((4 · 𝑁) / 3) − 5))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ≠ wne 2951  ∀wral 3070  ∃wrex 3071  ifcif 4423   class class class wbr 5036   ↦ cmpt 5116  ⟶wf 6336  ‘cfv 6340  (class class class)co 7156  ℂcc 10586  ℝcr 10587  0cc0 10588  1c1 10589   + caddc 10591   · cmul 10593   < clt 10726   ≤ cle 10727   − cmin 10921   / cdiv 11348  ℕcn 11687  2c2 11742  3c3 11743  4c4 11744  5c5 11745  6c6 11746  ℕ0cn0 11947  ℤcz 12033  ℤ≥cuz 12295  ℝ+crp 12443  ...cfz 12952  ⌊cfl 13222  seqcseq 13431  ↑cexp 13492  Ccbc 13725  √csqrt 14653  expce 15476   ∥ cdvds 15668  ℙcprime 16081   pCnt cpc 16242  logclog 25259  ↑𝑐ccxp 25260  θccht 25789 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5160  ax-sep 5173  ax-nul 5180  ax-pow 5238  ax-pr 5302  ax-un 7465  ax-inf2 9150  ax-cnex 10644  ax-resscn 10645  ax-1cn 10646  ax-icn 10647  ax-addcl 10648  ax-addrcl 10649  ax-mulcl 10650  ax-mulrcl 10651  ax-mulcom 10652  ax-addass 10653  ax-mulass 10654  ax-distr 10655  ax-i2m1 10656  ax-1ne0 10657  ax-1rid 10658  ax-rnegex 10659  ax-rrecex 10660  ax-cnre 10661  ax-pre-lttri 10662  ax-pre-lttrn 10663  ax-pre-ltadd 10664  ax-pre-mulgt0 10665  ax-pre-sup 10666  ax-addf 10667  ax-mulf 10668 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4842  df-iun 4888  df-iin 4889  df-br 5037  df-opab 5099  df-mpt 5117  df-tr 5143  df-id 5434  df-eprel 5439  df-po 5447  df-so 5448  df-fr 5487  df-se 5488  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6131  df-ord 6177  df-on 6178  df-lim 6179  df-suc 6180  df-iota 6299  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-isom 6349  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-of 7411  df-om 7586  df-1st 7699  df-2nd 7700  df-supp 7842  df-wrecs 7963  df-recs 8024  df-rdg 8062  df-1o 8118  df-2o 8119  df-oadd 8122  df-er 8305  df-map 8424  df-pm 8425  df-ixp 8493  df-en 8541  df-dom 8542  df-sdom 8543  df-fin 8544  df-fsupp 8880  df-fi 8921  df-sup 8952  df-inf 8953  df-oi 9020  df-dju 9376  df-card 9414  df-pnf 10728  df-mnf 10729  df-xr 10730  df-ltxr 10731  df-le 10732  df-sub 10923  df-neg 10924  df-div 11349  df-nn 11688  df-2 11750  df-3 11751  df-4 11752  df-5 11753  df-6 11754  df-7 11755  df-8 11756  df-9 11757  df-n0 11948  df-xnn0 12020  df-z 12034  df-dec 12151  df-uz 12296  df-q 12402  df-rp 12444  df-xneg 12561  df-xadd 12562  df-xmul 12563  df-ioo 12796  df-ioc 12797  df-ico 12798  df-icc 12799  df-fz 12953  df-fzo 13096  df-fl 13224  df-mod 13300  df-seq 13432  df-exp 13493  df-fac 13697  df-bc 13726  df-hash 13754  df-shft 14487  df-cj 14519  df-re 14520  df-im 14521  df-sqrt 14655  df-abs 14656  df-limsup 14889  df-clim 14906  df-rlim 14907  df-sum 15104  df-ef 15482  df-sin 15484  df-cos 15485  df-pi 15487  df-dvds 15669  df-gcd 15907  df-prm 16082  df-pc 16243  df-struct 16557  df-ndx 16558  df-slot 16559  df-base 16561  df-sets 16562  df-ress 16563  df-plusg 16650  df-mulr 16651  df-starv 16652  df-sca 16653  df-vsca 16654  df-ip 16655  df-tset 16656  df-ple 16657  df-ds 16659  df-unif 16660  df-hom 16661  df-cco 16662  df-rest 16768  df-topn 16769  df-0g 16787  df-gsum 16788  df-topgen 16789  df-pt 16790  df-prds 16793  df-xrs 16847  df-qtop 16852  df-imas 16853  df-xps 16855  df-mre 16929  df-mrc 16930  df-acs 16932  df-mgm 17932  df-sgrp 17981  df-mnd 17992  df-submnd 18037  df-mulg 18306  df-cntz 18528  df-cmn 18989  df-psmet 20172  df-xmet 20173  df-met 20174  df-bl 20175  df-mopn 20176  df-fbas 20177  df-fg 20178  df-cnfld 20181  df-top 21608  df-topon 21625  df-topsp 21647  df-bases 21660  df-cld 21733  df-ntr 21734  df-cls 21735  df-nei 21812  df-lp 21850  df-perf 21851  df-cn 21941  df-cnp 21942  df-haus 22029  df-tx 22276  df-hmeo 22469  df-fil 22560  df-fm 22652  df-flim 22653  df-flf 22654  df-xms 23036  df-ms 23037  df-tms 23038  df-cncf 23593  df-limc 24579  df-dv 24580  df-log 25261  df-cxp 25262  df-cht 25795  df-ppi 25798 This theorem is referenced by:  bposlem9  25989
 Copyright terms: Public domain W3C validator