Metamath Proof Explorer


Theorem bposlem6

Description: Lemma for bpos . By using the various bounds at our disposal, arrive at an inequality that is false for N large enough. (Contributed by Mario Carneiro, 14-Mar-2014) (Revised by Wolf Lammen, 12-Sep-2020)

Ref Expression
Hypotheses bpos.1 ( 𝜑𝑁 ∈ ( ℤ ‘ 5 ) )
bpos.2 ( 𝜑 → ¬ ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝𝑝 ≤ ( 2 · 𝑁 ) ) )
bpos.3 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) )
bpos.4 𝐾 = ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) )
bpos.5 𝑀 = ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) )
Assertion bposlem6 ( 𝜑 → ( ( 4 ↑ 𝑁 ) / 𝑁 ) < ( ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) · ( 2 ↑𝑐 ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) ) ) )

Proof

Step Hyp Ref Expression
1 bpos.1 ( 𝜑𝑁 ∈ ( ℤ ‘ 5 ) )
2 bpos.2 ( 𝜑 → ¬ ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝𝑝 ≤ ( 2 · 𝑁 ) ) )
3 bpos.3 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) )
4 bpos.4 𝐾 = ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) )
5 bpos.5 𝑀 = ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) )
6 4nn 4 ∈ ℕ
7 5nn 5 ∈ ℕ
8 eluznn ( ( 5 ∈ ℕ ∧ 𝑁 ∈ ( ℤ ‘ 5 ) ) → 𝑁 ∈ ℕ )
9 7 1 8 sylancr ( 𝜑𝑁 ∈ ℕ )
10 9 nnnn0d ( 𝜑𝑁 ∈ ℕ0 )
11 nnexpcl ( ( 4 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 4 ↑ 𝑁 ) ∈ ℕ )
12 6 10 11 sylancr ( 𝜑 → ( 4 ↑ 𝑁 ) ∈ ℕ )
13 12 nnred ( 𝜑 → ( 4 ↑ 𝑁 ) ∈ ℝ )
14 13 9 nndivred ( 𝜑 → ( ( 4 ↑ 𝑁 ) / 𝑁 ) ∈ ℝ )
15 fzctr ( 𝑁 ∈ ℕ0𝑁 ∈ ( 0 ... ( 2 · 𝑁 ) ) )
16 10 15 syl ( 𝜑𝑁 ∈ ( 0 ... ( 2 · 𝑁 ) ) )
17 bccl2 ( 𝑁 ∈ ( 0 ... ( 2 · 𝑁 ) ) → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℕ )
18 16 17 syl ( 𝜑 → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℕ )
19 18 nnred ( 𝜑 → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℝ )
20 2nn 2 ∈ ℕ
21 nnmulcl ( ( 2 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 2 · 𝑁 ) ∈ ℕ )
22 20 9 21 sylancr ( 𝜑 → ( 2 · 𝑁 ) ∈ ℕ )
23 22 nnrpd ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ+ )
24 22 nnred ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ )
25 23 rpge0d ( 𝜑 → 0 ≤ ( 2 · 𝑁 ) )
26 24 25 resqrtcld ( 𝜑 → ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ )
27 3nn 3 ∈ ℕ
28 nndivre ( ( ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ ∧ 3 ∈ ℕ ) → ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) ∈ ℝ )
29 26 27 28 sylancl ( 𝜑 → ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) ∈ ℝ )
30 2re 2 ∈ ℝ
31 readdcl ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) ∈ ℝ ∧ 2 ∈ ℝ ) → ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ∈ ℝ )
32 29 30 31 sylancl ( 𝜑 → ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ∈ ℝ )
33 23 32 rpcxpcld ( 𝜑 → ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) ∈ ℝ+ )
34 33 rpred ( 𝜑 → ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) ∈ ℝ )
35 2rp 2 ∈ ℝ+
36 nnmulcl ( ( 4 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 4 · 𝑁 ) ∈ ℕ )
37 6 9 36 sylancr ( 𝜑 → ( 4 · 𝑁 ) ∈ ℕ )
38 37 nnred ( 𝜑 → ( 4 · 𝑁 ) ∈ ℝ )
39 nndivre ( ( ( 4 · 𝑁 ) ∈ ℝ ∧ 3 ∈ ℕ ) → ( ( 4 · 𝑁 ) / 3 ) ∈ ℝ )
40 38 27 39 sylancl ( 𝜑 → ( ( 4 · 𝑁 ) / 3 ) ∈ ℝ )
41 5re 5 ∈ ℝ
42 resubcl ( ( ( ( 4 · 𝑁 ) / 3 ) ∈ ℝ ∧ 5 ∈ ℝ ) → ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) ∈ ℝ )
43 40 41 42 sylancl ( 𝜑 → ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) ∈ ℝ )
44 rpcxpcl ( ( 2 ∈ ℝ+ ∧ ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) ∈ ℝ ) → ( 2 ↑𝑐 ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) ) ∈ ℝ+ )
45 35 43 44 sylancr ( 𝜑 → ( 2 ↑𝑐 ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) ) ∈ ℝ+ )
46 45 rpred ( 𝜑 → ( 2 ↑𝑐 ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) ) ∈ ℝ )
47 34 46 remulcld ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) · ( 2 ↑𝑐 ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) ) ) ∈ ℝ )
48 df-5 5 = ( 4 + 1 )
49 4z 4 ∈ ℤ
50 uzid ( 4 ∈ ℤ → 4 ∈ ( ℤ ‘ 4 ) )
51 peano2uz ( 4 ∈ ( ℤ ‘ 4 ) → ( 4 + 1 ) ∈ ( ℤ ‘ 4 ) )
52 49 50 51 mp2b ( 4 + 1 ) ∈ ( ℤ ‘ 4 )
53 48 52 eqeltri 5 ∈ ( ℤ ‘ 4 )
54 eqid ( ℤ ‘ 4 ) = ( ℤ ‘ 4 )
55 54 uztrn2 ( ( 5 ∈ ( ℤ ‘ 4 ) ∧ 𝑁 ∈ ( ℤ ‘ 5 ) ) → 𝑁 ∈ ( ℤ ‘ 4 ) )
56 53 1 55 sylancr ( 𝜑𝑁 ∈ ( ℤ ‘ 4 ) )
57 bclbnd ( 𝑁 ∈ ( ℤ ‘ 4 ) → ( ( 4 ↑ 𝑁 ) / 𝑁 ) < ( ( 2 · 𝑁 ) C 𝑁 ) )
58 56 57 syl ( 𝜑 → ( ( 4 ↑ 𝑁 ) / 𝑁 ) < ( ( 2 · 𝑁 ) C 𝑁 ) )
59 id ( 𝑛 ∈ ℙ → 𝑛 ∈ ℙ )
60 pccl ( ( 𝑛 ∈ ℙ ∧ ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℕ ) → ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ0 )
61 59 18 60 syl2anr ( ( 𝜑𝑛 ∈ ℙ ) → ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ0 )
62 61 ralrimiva ( 𝜑 → ∀ 𝑛 ∈ ℙ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ0 )
63 3 62 pcmptcl ( 𝜑 → ( 𝐹 : ℕ ⟶ ℕ ∧ seq 1 ( · , 𝐹 ) : ℕ ⟶ ℕ ) )
64 63 simprd ( 𝜑 → seq 1 ( · , 𝐹 ) : ℕ ⟶ ℕ )
65 1 2 3 4 5 bposlem4 ( 𝜑𝑀 ∈ ( 3 ... 𝐾 ) )
66 elfzuz ( 𝑀 ∈ ( 3 ... 𝐾 ) → 𝑀 ∈ ( ℤ ‘ 3 ) )
67 65 66 syl ( 𝜑𝑀 ∈ ( ℤ ‘ 3 ) )
68 eluznn ( ( 3 ∈ ℕ ∧ 𝑀 ∈ ( ℤ ‘ 3 ) ) → 𝑀 ∈ ℕ )
69 27 67 68 sylancr ( 𝜑𝑀 ∈ ℕ )
70 64 69 ffvelrnd ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ∈ ℕ )
71 70 nnred ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ∈ ℝ )
72 2z 2 ∈ ℤ
73 nndivre ( ( ( 2 · 𝑁 ) ∈ ℝ ∧ 3 ∈ ℕ ) → ( ( 2 · 𝑁 ) / 3 ) ∈ ℝ )
74 24 27 73 sylancl ( 𝜑 → ( ( 2 · 𝑁 ) / 3 ) ∈ ℝ )
75 74 flcld ( 𝜑 → ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) ) ∈ ℤ )
76 4 75 eqeltrid ( 𝜑𝐾 ∈ ℤ )
77 zmulcl ( ( 2 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 2 · 𝐾 ) ∈ ℤ )
78 72 76 77 sylancr ( 𝜑 → ( 2 · 𝐾 ) ∈ ℤ )
79 7 nnzi 5 ∈ ℤ
80 zsubcl ( ( ( 2 · 𝐾 ) ∈ ℤ ∧ 5 ∈ ℤ ) → ( ( 2 · 𝐾 ) − 5 ) ∈ ℤ )
81 78 79 80 sylancl ( 𝜑 → ( ( 2 · 𝐾 ) − 5 ) ∈ ℤ )
82 81 zred ( 𝜑 → ( ( 2 · 𝐾 ) − 5 ) ∈ ℝ )
83 rpcxpcl ( ( 2 ∈ ℝ+ ∧ ( ( 2 · 𝐾 ) − 5 ) ∈ ℝ ) → ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) ∈ ℝ+ )
84 35 82 83 sylancr ( 𝜑 → ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) ∈ ℝ+ )
85 84 rpred ( 𝜑 → ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) ∈ ℝ )
86 71 85 remulcld ( 𝜑 → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) · ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) ) ∈ ℝ )
87 1 2 3 4 bposlem3 ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) = ( ( 2 · 𝑁 ) C 𝑁 ) )
88 elfzuz3 ( 𝑀 ∈ ( 3 ... 𝐾 ) → 𝐾 ∈ ( ℤ𝑀 ) )
89 65 88 syl ( 𝜑𝐾 ∈ ( ℤ𝑀 ) )
90 3 62 69 89 pcmptdvds ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ∥ ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) )
91 70 nnzd ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ∈ ℤ )
92 70 nnne0d ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ≠ 0 )
93 uztrn ( ( 𝐾 ∈ ( ℤ𝑀 ) ∧ 𝑀 ∈ ( ℤ ‘ 3 ) ) → 𝐾 ∈ ( ℤ ‘ 3 ) )
94 89 67 93 syl2anc ( 𝜑𝐾 ∈ ( ℤ ‘ 3 ) )
95 eluznn ( ( 3 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ‘ 3 ) ) → 𝐾 ∈ ℕ )
96 27 94 95 sylancr ( 𝜑𝐾 ∈ ℕ )
97 64 96 ffvelrnd ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) ∈ ℕ )
98 97 nnzd ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) ∈ ℤ )
99 dvdsval2 ( ( ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ∈ ℤ ∧ ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ≠ 0 ∧ ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) ∈ ℤ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ∥ ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) ↔ ( ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) / ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) ∈ ℤ ) )
100 91 92 98 99 syl3anc ( 𝜑 → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ∥ ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) ↔ ( ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) / ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) ∈ ℤ ) )
101 90 100 mpbid ( 𝜑 → ( ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) / ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) ∈ ℤ )
102 101 zred ( 𝜑 → ( ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) / ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) ∈ ℝ )
103 69 nnred ( 𝜑𝑀 ∈ ℝ )
104 76 zred ( 𝜑𝐾 ∈ ℝ )
105 eluzle ( 𝐾 ∈ ( ℤ𝑀 ) → 𝑀𝐾 )
106 89 105 syl ( 𝜑𝑀𝐾 )
107 efchtdvds ( ( 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑀𝐾 ) → ( exp ‘ ( θ ‘ 𝑀 ) ) ∥ ( exp ‘ ( θ ‘ 𝐾 ) ) )
108 103 104 106 107 syl3anc ( 𝜑 → ( exp ‘ ( θ ‘ 𝑀 ) ) ∥ ( exp ‘ ( θ ‘ 𝐾 ) ) )
109 efchtcl ( 𝑀 ∈ ℝ → ( exp ‘ ( θ ‘ 𝑀 ) ) ∈ ℕ )
110 103 109 syl ( 𝜑 → ( exp ‘ ( θ ‘ 𝑀 ) ) ∈ ℕ )
111 110 nnzd ( 𝜑 → ( exp ‘ ( θ ‘ 𝑀 ) ) ∈ ℤ )
112 110 nnne0d ( 𝜑 → ( exp ‘ ( θ ‘ 𝑀 ) ) ≠ 0 )
113 efchtcl ( 𝐾 ∈ ℝ → ( exp ‘ ( θ ‘ 𝐾 ) ) ∈ ℕ )
114 104 113 syl ( 𝜑 → ( exp ‘ ( θ ‘ 𝐾 ) ) ∈ ℕ )
115 114 nnzd ( 𝜑 → ( exp ‘ ( θ ‘ 𝐾 ) ) ∈ ℤ )
116 dvdsval2 ( ( ( exp ‘ ( θ ‘ 𝑀 ) ) ∈ ℤ ∧ ( exp ‘ ( θ ‘ 𝑀 ) ) ≠ 0 ∧ ( exp ‘ ( θ ‘ 𝐾 ) ) ∈ ℤ ) → ( ( exp ‘ ( θ ‘ 𝑀 ) ) ∥ ( exp ‘ ( θ ‘ 𝐾 ) ) ↔ ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) ∈ ℤ ) )
117 111 112 115 116 syl3anc ( 𝜑 → ( ( exp ‘ ( θ ‘ 𝑀 ) ) ∥ ( exp ‘ ( θ ‘ 𝐾 ) ) ↔ ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) ∈ ℤ ) )
118 108 117 mpbid ( 𝜑 → ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) ∈ ℤ )
119 118 zred ( 𝜑 → ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) ∈ ℝ )
120 prmz ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
121 fllt ( ( ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ ∧ 𝑝 ∈ ℤ ) → ( ( √ ‘ ( 2 · 𝑁 ) ) < 𝑝 ↔ ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) < 𝑝 ) )
122 26 120 121 syl2an ( ( 𝜑𝑝 ∈ ℙ ) → ( ( √ ‘ ( 2 · 𝑁 ) ) < 𝑝 ↔ ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) < 𝑝 ) )
123 5 breq1i ( 𝑀 < 𝑝 ↔ ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) < 𝑝 )
124 122 123 bitr4di ( ( 𝜑𝑝 ∈ ℙ ) → ( ( √ ‘ ( 2 · 𝑁 ) ) < 𝑝𝑀 < 𝑝 ) )
125 120 zred ( 𝑝 ∈ ℙ → 𝑝 ∈ ℝ )
126 ltnle ( ( 𝑀 ∈ ℝ ∧ 𝑝 ∈ ℝ ) → ( 𝑀 < 𝑝 ↔ ¬ 𝑝𝑀 ) )
127 103 125 126 syl2an ( ( 𝜑𝑝 ∈ ℙ ) → ( 𝑀 < 𝑝 ↔ ¬ 𝑝𝑀 ) )
128 124 127 bitrd ( ( 𝜑𝑝 ∈ ℙ ) → ( ( √ ‘ ( 2 · 𝑁 ) ) < 𝑝 ↔ ¬ 𝑝𝑀 ) )
129 bposlem1 ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ↑ ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ≤ ( 2 · 𝑁 ) )
130 9 129 sylan ( ( 𝜑𝑝 ∈ ℙ ) → ( 𝑝 ↑ ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ≤ ( 2 · 𝑁 ) )
131 125 adantl ( ( 𝜑𝑝 ∈ ℙ ) → 𝑝 ∈ ℝ )
132 id ( 𝑝 ∈ ℙ → 𝑝 ∈ ℙ )
133 pccl ( ( 𝑝 ∈ ℙ ∧ ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℕ ) → ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ0 )
134 132 18 133 syl2anr ( ( 𝜑𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ0 )
135 131 134 reexpcld ( ( 𝜑𝑝 ∈ ℙ ) → ( 𝑝 ↑ ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ∈ ℝ )
136 24 adantr ( ( 𝜑𝑝 ∈ ℙ ) → ( 2 · 𝑁 ) ∈ ℝ )
137 131 resqcld ( ( 𝜑𝑝 ∈ ℙ ) → ( 𝑝 ↑ 2 ) ∈ ℝ )
138 lelttr ( ( ( 𝑝 ↑ ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ∈ ℝ ∧ ( 2 · 𝑁 ) ∈ ℝ ∧ ( 𝑝 ↑ 2 ) ∈ ℝ ) → ( ( ( 𝑝 ↑ ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ≤ ( 2 · 𝑁 ) ∧ ( 2 · 𝑁 ) < ( 𝑝 ↑ 2 ) ) → ( 𝑝 ↑ ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) < ( 𝑝 ↑ 2 ) ) )
139 135 136 137 138 syl3anc ( ( 𝜑𝑝 ∈ ℙ ) → ( ( ( 𝑝 ↑ ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ≤ ( 2 · 𝑁 ) ∧ ( 2 · 𝑁 ) < ( 𝑝 ↑ 2 ) ) → ( 𝑝 ↑ ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) < ( 𝑝 ↑ 2 ) ) )
140 130 139 mpand ( ( 𝜑𝑝 ∈ ℙ ) → ( ( 2 · 𝑁 ) < ( 𝑝 ↑ 2 ) → ( 𝑝 ↑ ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) < ( 𝑝 ↑ 2 ) ) )
141 resqrtth ( ( ( 2 · 𝑁 ) ∈ ℝ ∧ 0 ≤ ( 2 · 𝑁 ) ) → ( ( √ ‘ ( 2 · 𝑁 ) ) ↑ 2 ) = ( 2 · 𝑁 ) )
142 24 25 141 syl2anc ( 𝜑 → ( ( √ ‘ ( 2 · 𝑁 ) ) ↑ 2 ) = ( 2 · 𝑁 ) )
143 142 breq1d ( 𝜑 → ( ( ( √ ‘ ( 2 · 𝑁 ) ) ↑ 2 ) < ( 𝑝 ↑ 2 ) ↔ ( 2 · 𝑁 ) < ( 𝑝 ↑ 2 ) ) )
144 143 adantr ( ( 𝜑𝑝 ∈ ℙ ) → ( ( ( √ ‘ ( 2 · 𝑁 ) ) ↑ 2 ) < ( 𝑝 ↑ 2 ) ↔ ( 2 · 𝑁 ) < ( 𝑝 ↑ 2 ) ) )
145 134 nn0zd ( ( 𝜑𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℤ )
146 72 a1i ( ( 𝜑𝑝 ∈ ℙ ) → 2 ∈ ℤ )
147 prmgt1 ( 𝑝 ∈ ℙ → 1 < 𝑝 )
148 147 adantl ( ( 𝜑𝑝 ∈ ℙ ) → 1 < 𝑝 )
149 131 145 146 148 ltexp2d ( ( 𝜑𝑝 ∈ ℙ ) → ( ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) < 2 ↔ ( 𝑝 ↑ ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) < ( 𝑝 ↑ 2 ) ) )
150 140 144 149 3imtr4d ( ( 𝜑𝑝 ∈ ℙ ) → ( ( ( √ ‘ ( 2 · 𝑁 ) ) ↑ 2 ) < ( 𝑝 ↑ 2 ) → ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) < 2 ) )
151 df-2 2 = ( 1 + 1 )
152 151 breq2i ( ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) < 2 ↔ ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) < ( 1 + 1 ) )
153 150 152 syl6ib ( ( 𝜑𝑝 ∈ ℙ ) → ( ( ( √ ‘ ( 2 · 𝑁 ) ) ↑ 2 ) < ( 𝑝 ↑ 2 ) → ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) < ( 1 + 1 ) ) )
154 26 adantr ( ( 𝜑𝑝 ∈ ℙ ) → ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ )
155 24 25 sqrtge0d ( 𝜑 → 0 ≤ ( √ ‘ ( 2 · 𝑁 ) ) )
156 155 adantr ( ( 𝜑𝑝 ∈ ℙ ) → 0 ≤ ( √ ‘ ( 2 · 𝑁 ) ) )
157 prmnn ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
158 157 nnrpd ( 𝑝 ∈ ℙ → 𝑝 ∈ ℝ+ )
159 158 rpge0d ( 𝑝 ∈ ℙ → 0 ≤ 𝑝 )
160 159 adantl ( ( 𝜑𝑝 ∈ ℙ ) → 0 ≤ 𝑝 )
161 154 131 156 160 lt2sqd ( ( 𝜑𝑝 ∈ ℙ ) → ( ( √ ‘ ( 2 · 𝑁 ) ) < 𝑝 ↔ ( ( √ ‘ ( 2 · 𝑁 ) ) ↑ 2 ) < ( 𝑝 ↑ 2 ) ) )
162 1z 1 ∈ ℤ
163 zleltp1 ( ( ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℤ ∧ 1 ∈ ℤ ) → ( ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ≤ 1 ↔ ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) < ( 1 + 1 ) ) )
164 145 162 163 sylancl ( ( 𝜑𝑝 ∈ ℙ ) → ( ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ≤ 1 ↔ ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) < ( 1 + 1 ) ) )
165 153 161 164 3imtr4d ( ( 𝜑𝑝 ∈ ℙ ) → ( ( √ ‘ ( 2 · 𝑁 ) ) < 𝑝 → ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ≤ 1 ) )
166 128 165 sylbird ( ( 𝜑𝑝 ∈ ℙ ) → ( ¬ 𝑝𝑀 → ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ≤ 1 ) )
167 166 imp ( ( ( 𝜑𝑝 ∈ ℙ ) ∧ ¬ 𝑝𝑀 ) → ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ≤ 1 )
168 167 adantrl ( ( ( 𝜑𝑝 ∈ ℙ ) ∧ ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) ) → ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ≤ 1 )
169 iftrue ( ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) → if ( ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) , ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) , 0 ) = ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) )
170 169 adantl ( ( ( 𝜑𝑝 ∈ ℙ ) ∧ ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) ) → if ( ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) , ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) , 0 ) = ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) )
171 iftrue ( ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) → if ( ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) , 1 , 0 ) = 1 )
172 171 adantl ( ( ( 𝜑𝑝 ∈ ℙ ) ∧ ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) ) → if ( ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) , 1 , 0 ) = 1 )
173 168 170 172 3brtr4d ( ( ( 𝜑𝑝 ∈ ℙ ) ∧ ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) ) → if ( ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) , ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) , 0 ) ≤ if ( ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) , 1 , 0 ) )
174 0le0 0 ≤ 0
175 iffalse ( ¬ ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) → if ( ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) , ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) , 0 ) = 0 )
176 iffalse ( ¬ ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) → if ( ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) , 1 , 0 ) = 0 )
177 175 176 breq12d ( ¬ ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) → ( if ( ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) , ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) , 0 ) ≤ if ( ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) , 1 , 0 ) ↔ 0 ≤ 0 ) )
178 174 177 mpbiri ( ¬ ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) → if ( ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) , ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) , 0 ) ≤ if ( ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) , 1 , 0 ) )
179 178 adantl ( ( ( 𝜑𝑝 ∈ ℙ ) ∧ ¬ ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) ) → if ( ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) , ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) , 0 ) ≤ if ( ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) , 1 , 0 ) )
180 173 179 pm2.61dan ( ( 𝜑𝑝 ∈ ℙ ) → if ( ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) , ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) , 0 ) ≤ if ( ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) , 1 , 0 ) )
181 62 adantr ( ( 𝜑𝑝 ∈ ℙ ) → ∀ 𝑛 ∈ ℙ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ0 )
182 69 adantr ( ( 𝜑𝑝 ∈ ℙ ) → 𝑀 ∈ ℕ )
183 simpr ( ( 𝜑𝑝 ∈ ℙ ) → 𝑝 ∈ ℙ )
184 oveq1 ( 𝑛 = 𝑝 → ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) = ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) )
185 89 adantr ( ( 𝜑𝑝 ∈ ℙ ) → 𝐾 ∈ ( ℤ𝑀 ) )
186 3 181 182 183 184 185 pcmpt2 ( ( 𝜑𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) / ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) ) = if ( ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) , ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) , 0 ) )
187 eqid ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) )
188 187 prmorcht ( 𝐾 ∈ ℕ → ( exp ‘ ( θ ‘ 𝐾 ) ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) ) ) ‘ 𝐾 ) )
189 96 188 syl ( 𝜑 → ( exp ‘ ( θ ‘ 𝐾 ) ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) ) ) ‘ 𝐾 ) )
190 187 prmorcht ( 𝑀 ∈ ℕ → ( exp ‘ ( θ ‘ 𝑀 ) ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) ) ) ‘ 𝑀 ) )
191 69 190 syl ( 𝜑 → ( exp ‘ ( θ ‘ 𝑀 ) ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) ) ) ‘ 𝑀 ) )
192 189 191 oveq12d ( 𝜑 → ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) = ( ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) ) ) ‘ 𝐾 ) / ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) ) ) ‘ 𝑀 ) ) )
193 192 adantr ( ( 𝜑𝑝 ∈ ℙ ) → ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) = ( ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) ) ) ‘ 𝐾 ) / ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) ) ) ‘ 𝑀 ) ) )
194 193 oveq2d ( ( 𝜑𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) ) = ( 𝑝 pCnt ( ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) ) ) ‘ 𝐾 ) / ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) ) ) ‘ 𝑀 ) ) ) )
195 nncn ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
196 195 exp1d ( 𝑛 ∈ ℕ → ( 𝑛 ↑ 1 ) = 𝑛 )
197 196 ifeq1d ( 𝑛 ∈ ℕ → if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ 1 ) , 1 ) = if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) )
198 197 mpteq2ia ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ 1 ) , 1 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) )
199 198 eqcomi ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ 1 ) , 1 ) )
200 1nn0 1 ∈ ℕ0
201 200 a1i ( ( 𝜑𝑛 ∈ ℙ ) → 1 ∈ ℕ0 )
202 201 ralrimiva ( 𝜑 → ∀ 𝑛 ∈ ℙ 1 ∈ ℕ0 )
203 202 adantr ( ( 𝜑𝑝 ∈ ℙ ) → ∀ 𝑛 ∈ ℙ 1 ∈ ℕ0 )
204 eqidd ( 𝑛 = 𝑝 → 1 = 1 )
205 199 203 182 183 204 185 pcmpt2 ( ( 𝜑𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) ) ) ‘ 𝐾 ) / ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) ) ) ‘ 𝑀 ) ) ) = if ( ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) , 1 , 0 ) )
206 194 205 eqtrd ( ( 𝜑𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) ) = if ( ( 𝑝𝐾 ∧ ¬ 𝑝𝑀 ) , 1 , 0 ) )
207 180 186 206 3brtr4d ( ( 𝜑𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) / ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) ) ≤ ( 𝑝 pCnt ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) ) )
208 207 ralrimiva ( 𝜑 → ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt ( ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) / ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) ) ≤ ( 𝑝 pCnt ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) ) )
209 pc2dvds ( ( ( ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) / ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) ∈ ℤ ∧ ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) ∈ ℤ ) → ( ( ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) / ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) ∥ ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt ( ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) / ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) ) ≤ ( 𝑝 pCnt ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) ) ) )
210 101 118 209 syl2anc ( 𝜑 → ( ( ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) / ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) ∥ ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt ( ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) / ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) ) ≤ ( 𝑝 pCnt ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) ) ) )
211 208 210 mpbird ( 𝜑 → ( ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) / ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) ∥ ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) )
212 114 nnred ( 𝜑 → ( exp ‘ ( θ ‘ 𝐾 ) ) ∈ ℝ )
213 110 nnred ( 𝜑 → ( exp ‘ ( θ ‘ 𝑀 ) ) ∈ ℝ )
214 114 nngt0d ( 𝜑 → 0 < ( exp ‘ ( θ ‘ 𝐾 ) ) )
215 110 nngt0d ( 𝜑 → 0 < ( exp ‘ ( θ ‘ 𝑀 ) ) )
216 212 213 214 215 divgt0d ( 𝜑 → 0 < ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) )
217 elnnz ( ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) ∈ ℕ ↔ ( ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) ∈ ℤ ∧ 0 < ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) ) )
218 118 216 217 sylanbrc ( 𝜑 → ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) ∈ ℕ )
219 dvdsle ( ( ( ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) / ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) ∈ ℤ ∧ ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) ∈ ℕ ) → ( ( ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) / ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) ∥ ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) / ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) ≤ ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) ) )
220 101 218 219 syl2anc ( 𝜑 → ( ( ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) / ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) ∥ ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) / ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) ≤ ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) ) )
221 211 220 mpd ( 𝜑 → ( ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) / ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) ≤ ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) )
222 nndivre ( ( ( exp ‘ ( θ ‘ 𝐾 ) ) ∈ ℝ ∧ 4 ∈ ℕ ) → ( ( exp ‘ ( θ ‘ 𝐾 ) ) / 4 ) ∈ ℝ )
223 212 6 222 sylancl ( 𝜑 → ( ( exp ‘ ( θ ‘ 𝐾 ) ) / 4 ) ∈ ℝ )
224 4re 4 ∈ ℝ
225 224 a1i ( 𝜑 → 4 ∈ ℝ )
226 6re 6 ∈ ℝ
227 226 a1i ( 𝜑 → 6 ∈ ℝ )
228 4lt6 4 < 6
229 228 a1i ( 𝜑 → 4 < 6 )
230 cht3 ( θ ‘ 3 ) = ( log ‘ 6 )
231 230 fveq2i ( exp ‘ ( θ ‘ 3 ) ) = ( exp ‘ ( log ‘ 6 ) )
232 6pos 0 < 6
233 226 232 elrpii 6 ∈ ℝ+
234 reeflog ( 6 ∈ ℝ+ → ( exp ‘ ( log ‘ 6 ) ) = 6 )
235 233 234 ax-mp ( exp ‘ ( log ‘ 6 ) ) = 6
236 231 235 eqtri ( exp ‘ ( θ ‘ 3 ) ) = 6
237 3re 3 ∈ ℝ
238 237 a1i ( 𝜑 → 3 ∈ ℝ )
239 eluzle ( 𝑀 ∈ ( ℤ ‘ 3 ) → 3 ≤ 𝑀 )
240 67 239 syl ( 𝜑 → 3 ≤ 𝑀 )
241 chtwordi ( ( 3 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 3 ≤ 𝑀 ) → ( θ ‘ 3 ) ≤ ( θ ‘ 𝑀 ) )
242 238 103 240 241 syl3anc ( 𝜑 → ( θ ‘ 3 ) ≤ ( θ ‘ 𝑀 ) )
243 chtcl ( 3 ∈ ℝ → ( θ ‘ 3 ) ∈ ℝ )
244 237 243 ax-mp ( θ ‘ 3 ) ∈ ℝ
245 chtcl ( 𝑀 ∈ ℝ → ( θ ‘ 𝑀 ) ∈ ℝ )
246 103 245 syl ( 𝜑 → ( θ ‘ 𝑀 ) ∈ ℝ )
247 efle ( ( ( θ ‘ 3 ) ∈ ℝ ∧ ( θ ‘ 𝑀 ) ∈ ℝ ) → ( ( θ ‘ 3 ) ≤ ( θ ‘ 𝑀 ) ↔ ( exp ‘ ( θ ‘ 3 ) ) ≤ ( exp ‘ ( θ ‘ 𝑀 ) ) ) )
248 244 246 247 sylancr ( 𝜑 → ( ( θ ‘ 3 ) ≤ ( θ ‘ 𝑀 ) ↔ ( exp ‘ ( θ ‘ 3 ) ) ≤ ( exp ‘ ( θ ‘ 𝑀 ) ) ) )
249 242 248 mpbid ( 𝜑 → ( exp ‘ ( θ ‘ 3 ) ) ≤ ( exp ‘ ( θ ‘ 𝑀 ) ) )
250 236 249 eqbrtrrid ( 𝜑 → 6 ≤ ( exp ‘ ( θ ‘ 𝑀 ) ) )
251 225 227 213 229 250 ltletrd ( 𝜑 → 4 < ( exp ‘ ( θ ‘ 𝑀 ) ) )
252 4pos 0 < 4
253 252 a1i ( 𝜑 → 0 < 4 )
254 ltdiv2 ( ( ( 4 ∈ ℝ ∧ 0 < 4 ) ∧ ( ( exp ‘ ( θ ‘ 𝑀 ) ) ∈ ℝ ∧ 0 < ( exp ‘ ( θ ‘ 𝑀 ) ) ) ∧ ( ( exp ‘ ( θ ‘ 𝐾 ) ) ∈ ℝ ∧ 0 < ( exp ‘ ( θ ‘ 𝐾 ) ) ) ) → ( 4 < ( exp ‘ ( θ ‘ 𝑀 ) ) ↔ ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) < ( ( exp ‘ ( θ ‘ 𝐾 ) ) / 4 ) ) )
255 225 253 213 215 212 214 254 syl222anc ( 𝜑 → ( 4 < ( exp ‘ ( θ ‘ 𝑀 ) ) ↔ ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) < ( ( exp ‘ ( θ ‘ 𝐾 ) ) / 4 ) ) )
256 251 255 mpbid ( 𝜑 → ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) < ( ( exp ‘ ( θ ‘ 𝐾 ) ) / 4 ) )
257 30 a1i ( 𝜑 → 2 ∈ ℝ )
258 2lt3 2 < 3
259 258 a1i ( 𝜑 → 2 < 3 )
260 238 103 104 240 106 letrd ( 𝜑 → 3 ≤ 𝐾 )
261 257 238 104 259 260 ltletrd ( 𝜑 → 2 < 𝐾 )
262 chtub ( ( 𝐾 ∈ ℝ ∧ 2 < 𝐾 ) → ( θ ‘ 𝐾 ) < ( ( log ‘ 2 ) · ( ( 2 · 𝐾 ) − 3 ) ) )
263 104 261 262 syl2anc ( 𝜑 → ( θ ‘ 𝐾 ) < ( ( log ‘ 2 ) · ( ( 2 · 𝐾 ) − 3 ) ) )
264 chtcl ( 𝐾 ∈ ℝ → ( θ ‘ 𝐾 ) ∈ ℝ )
265 104 264 syl ( 𝜑 → ( θ ‘ 𝐾 ) ∈ ℝ )
266 relogcl ( 2 ∈ ℝ+ → ( log ‘ 2 ) ∈ ℝ )
267 35 266 ax-mp ( log ‘ 2 ) ∈ ℝ
268 3z 3 ∈ ℤ
269 zsubcl ( ( ( 2 · 𝐾 ) ∈ ℤ ∧ 3 ∈ ℤ ) → ( ( 2 · 𝐾 ) − 3 ) ∈ ℤ )
270 78 268 269 sylancl ( 𝜑 → ( ( 2 · 𝐾 ) − 3 ) ∈ ℤ )
271 270 zred ( 𝜑 → ( ( 2 · 𝐾 ) − 3 ) ∈ ℝ )
272 remulcl ( ( ( log ‘ 2 ) ∈ ℝ ∧ ( ( 2 · 𝐾 ) − 3 ) ∈ ℝ ) → ( ( log ‘ 2 ) · ( ( 2 · 𝐾 ) − 3 ) ) ∈ ℝ )
273 267 271 272 sylancr ( 𝜑 → ( ( log ‘ 2 ) · ( ( 2 · 𝐾 ) − 3 ) ) ∈ ℝ )
274 eflt ( ( ( θ ‘ 𝐾 ) ∈ ℝ ∧ ( ( log ‘ 2 ) · ( ( 2 · 𝐾 ) − 3 ) ) ∈ ℝ ) → ( ( θ ‘ 𝐾 ) < ( ( log ‘ 2 ) · ( ( 2 · 𝐾 ) − 3 ) ) ↔ ( exp ‘ ( θ ‘ 𝐾 ) ) < ( exp ‘ ( ( log ‘ 2 ) · ( ( 2 · 𝐾 ) − 3 ) ) ) ) )
275 265 273 274 syl2anc ( 𝜑 → ( ( θ ‘ 𝐾 ) < ( ( log ‘ 2 ) · ( ( 2 · 𝐾 ) − 3 ) ) ↔ ( exp ‘ ( θ ‘ 𝐾 ) ) < ( exp ‘ ( ( log ‘ 2 ) · ( ( 2 · 𝐾 ) − 3 ) ) ) ) )
276 263 275 mpbid ( 𝜑 → ( exp ‘ ( θ ‘ 𝐾 ) ) < ( exp ‘ ( ( log ‘ 2 ) · ( ( 2 · 𝐾 ) − 3 ) ) ) )
277 reexplog ( ( 2 ∈ ℝ+ ∧ ( ( 2 · 𝐾 ) − 3 ) ∈ ℤ ) → ( 2 ↑ ( ( 2 · 𝐾 ) − 3 ) ) = ( exp ‘ ( ( ( 2 · 𝐾 ) − 3 ) · ( log ‘ 2 ) ) ) )
278 35 270 277 sylancr ( 𝜑 → ( 2 ↑ ( ( 2 · 𝐾 ) − 3 ) ) = ( exp ‘ ( ( ( 2 · 𝐾 ) − 3 ) · ( log ‘ 2 ) ) ) )
279 270 zcnd ( 𝜑 → ( ( 2 · 𝐾 ) − 3 ) ∈ ℂ )
280 267 recni ( log ‘ 2 ) ∈ ℂ
281 mulcom ( ( ( ( 2 · 𝐾 ) − 3 ) ∈ ℂ ∧ ( log ‘ 2 ) ∈ ℂ ) → ( ( ( 2 · 𝐾 ) − 3 ) · ( log ‘ 2 ) ) = ( ( log ‘ 2 ) · ( ( 2 · 𝐾 ) − 3 ) ) )
282 279 280 281 sylancl ( 𝜑 → ( ( ( 2 · 𝐾 ) − 3 ) · ( log ‘ 2 ) ) = ( ( log ‘ 2 ) · ( ( 2 · 𝐾 ) − 3 ) ) )
283 282 fveq2d ( 𝜑 → ( exp ‘ ( ( ( 2 · 𝐾 ) − 3 ) · ( log ‘ 2 ) ) ) = ( exp ‘ ( ( log ‘ 2 ) · ( ( 2 · 𝐾 ) − 3 ) ) ) )
284 278 283 eqtrd ( 𝜑 → ( 2 ↑ ( ( 2 · 𝐾 ) − 3 ) ) = ( exp ‘ ( ( log ‘ 2 ) · ( ( 2 · 𝐾 ) − 3 ) ) ) )
285 276 284 breqtrrd ( 𝜑 → ( exp ‘ ( θ ‘ 𝐾 ) ) < ( 2 ↑ ( ( 2 · 𝐾 ) − 3 ) ) )
286 3p2e5 ( 3 + 2 ) = 5
287 286 oveq1i ( ( 3 + 2 ) − 2 ) = ( 5 − 2 )
288 3cn 3 ∈ ℂ
289 2cn 2 ∈ ℂ
290 288 289 pncan3oi ( ( 3 + 2 ) − 2 ) = 3
291 287 290 eqtr3i ( 5 − 2 ) = 3
292 291 oveq2i ( ( 2 · 𝐾 ) − ( 5 − 2 ) ) = ( ( 2 · 𝐾 ) − 3 )
293 78 zcnd ( 𝜑 → ( 2 · 𝐾 ) ∈ ℂ )
294 5cn 5 ∈ ℂ
295 subsub ( ( ( 2 · 𝐾 ) ∈ ℂ ∧ 5 ∈ ℂ ∧ 2 ∈ ℂ ) → ( ( 2 · 𝐾 ) − ( 5 − 2 ) ) = ( ( ( 2 · 𝐾 ) − 5 ) + 2 ) )
296 294 289 295 mp3an23 ( ( 2 · 𝐾 ) ∈ ℂ → ( ( 2 · 𝐾 ) − ( 5 − 2 ) ) = ( ( ( 2 · 𝐾 ) − 5 ) + 2 ) )
297 293 296 syl ( 𝜑 → ( ( 2 · 𝐾 ) − ( 5 − 2 ) ) = ( ( ( 2 · 𝐾 ) − 5 ) + 2 ) )
298 292 297 eqtr3id ( 𝜑 → ( ( 2 · 𝐾 ) − 3 ) = ( ( ( 2 · 𝐾 ) − 5 ) + 2 ) )
299 298 oveq2d ( 𝜑 → ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 3 ) ) = ( 2 ↑𝑐 ( ( ( 2 · 𝐾 ) − 5 ) + 2 ) ) )
300 2ne0 2 ≠ 0
301 cxpexpz ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ ( ( 2 · 𝐾 ) − 3 ) ∈ ℤ ) → ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 3 ) ) = ( 2 ↑ ( ( 2 · 𝐾 ) − 3 ) ) )
302 289 300 270 301 mp3an12i ( 𝜑 → ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 3 ) ) = ( 2 ↑ ( ( 2 · 𝐾 ) − 3 ) ) )
303 81 zcnd ( 𝜑 → ( ( 2 · 𝐾 ) − 5 ) ∈ ℂ )
304 2cnne0 ( 2 ∈ ℂ ∧ 2 ≠ 0 )
305 cxpadd ( ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( ( 2 · 𝐾 ) − 5 ) ∈ ℂ ∧ 2 ∈ ℂ ) → ( 2 ↑𝑐 ( ( ( 2 · 𝐾 ) − 5 ) + 2 ) ) = ( ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) · ( 2 ↑𝑐 2 ) ) )
306 304 289 305 mp3an13 ( ( ( 2 · 𝐾 ) − 5 ) ∈ ℂ → ( 2 ↑𝑐 ( ( ( 2 · 𝐾 ) − 5 ) + 2 ) ) = ( ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) · ( 2 ↑𝑐 2 ) ) )
307 303 306 syl ( 𝜑 → ( 2 ↑𝑐 ( ( ( 2 · 𝐾 ) − 5 ) + 2 ) ) = ( ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) · ( 2 ↑𝑐 2 ) ) )
308 299 302 307 3eqtr3d ( 𝜑 → ( 2 ↑ ( ( 2 · 𝐾 ) − 3 ) ) = ( ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) · ( 2 ↑𝑐 2 ) ) )
309 2nn0 2 ∈ ℕ0
310 cxpexp ( ( 2 ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( 2 ↑𝑐 2 ) = ( 2 ↑ 2 ) )
311 289 309 310 mp2an ( 2 ↑𝑐 2 ) = ( 2 ↑ 2 )
312 sq2 ( 2 ↑ 2 ) = 4
313 311 312 eqtri ( 2 ↑𝑐 2 ) = 4
314 313 oveq2i ( ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) · ( 2 ↑𝑐 2 ) ) = ( ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) · 4 )
315 308 314 eqtrdi ( 𝜑 → ( 2 ↑ ( ( 2 · 𝐾 ) − 3 ) ) = ( ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) · 4 ) )
316 285 315 breqtrd ( 𝜑 → ( exp ‘ ( θ ‘ 𝐾 ) ) < ( ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) · 4 ) )
317 224 252 pm3.2i ( 4 ∈ ℝ ∧ 0 < 4 )
318 317 a1i ( 𝜑 → ( 4 ∈ ℝ ∧ 0 < 4 ) )
319 ltdivmul2 ( ( ( exp ‘ ( θ ‘ 𝐾 ) ) ∈ ℝ ∧ ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) ∈ ℝ ∧ ( 4 ∈ ℝ ∧ 0 < 4 ) ) → ( ( ( exp ‘ ( θ ‘ 𝐾 ) ) / 4 ) < ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) ↔ ( exp ‘ ( θ ‘ 𝐾 ) ) < ( ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) · 4 ) ) )
320 212 85 318 319 syl3anc ( 𝜑 → ( ( ( exp ‘ ( θ ‘ 𝐾 ) ) / 4 ) < ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) ↔ ( exp ‘ ( θ ‘ 𝐾 ) ) < ( ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) · 4 ) ) )
321 316 320 mpbird ( 𝜑 → ( ( exp ‘ ( θ ‘ 𝐾 ) ) / 4 ) < ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) )
322 119 223 85 256 321 lttrd ( 𝜑 → ( ( exp ‘ ( θ ‘ 𝐾 ) ) / ( exp ‘ ( θ ‘ 𝑀 ) ) ) < ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) )
323 102 119 85 221 322 lelttrd ( 𝜑 → ( ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) / ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) < ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) )
324 97 nnred ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) ∈ ℝ )
325 nnre ( ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ∈ ℕ → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ∈ ℝ )
326 nngt0 ( ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ∈ ℕ → 0 < ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) )
327 325 326 jca ( ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ∈ ℕ → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ∈ ℝ ∧ 0 < ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) )
328 70 327 syl ( 𝜑 → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ∈ ℝ ∧ 0 < ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) )
329 ltdivmul ( ( ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) ∈ ℝ ∧ ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) ∈ ℝ ∧ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ∈ ℝ ∧ 0 < ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) ) → ( ( ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) / ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) < ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) ↔ ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) < ( ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) · ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) ) ) )
330 324 85 328 329 syl3anc ( 𝜑 → ( ( ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) / ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) < ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) ↔ ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) < ( ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) · ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) ) ) )
331 323 330 mpbid ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) < ( ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) · ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) ) )
332 87 331 eqbrtrrd ( 𝜑 → ( ( 2 · 𝑁 ) C 𝑁 ) < ( ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) · ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) ) )
333 34 85 remulcld ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) · ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) ) ∈ ℝ )
334 1 2 3 4 5 bposlem5 ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ≤ ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) )
335 71 34 84 lemul1d ( 𝜑 → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ≤ ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) ↔ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) · ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) ) ≤ ( ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) · ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) ) ) )
336 334 335 mpbid ( 𝜑 → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) · ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) ) ≤ ( ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) · ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) ) )
337 78 zred ( 𝜑 → ( 2 · 𝐾 ) ∈ ℝ )
338 41 a1i ( 𝜑 → 5 ∈ ℝ )
339 flle ( ( ( 2 · 𝑁 ) / 3 ) ∈ ℝ → ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) ) ≤ ( ( 2 · 𝑁 ) / 3 ) )
340 74 339 syl ( 𝜑 → ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) ) ≤ ( ( 2 · 𝑁 ) / 3 ) )
341 4 340 eqbrtrid ( 𝜑𝐾 ≤ ( ( 2 · 𝑁 ) / 3 ) )
342 2pos 0 < 2
343 30 342 pm3.2i ( 2 ∈ ℝ ∧ 0 < 2 )
344 343 a1i ( 𝜑 → ( 2 ∈ ℝ ∧ 0 < 2 ) )
345 lemul2 ( ( 𝐾 ∈ ℝ ∧ ( ( 2 · 𝑁 ) / 3 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( 𝐾 ≤ ( ( 2 · 𝑁 ) / 3 ) ↔ ( 2 · 𝐾 ) ≤ ( 2 · ( ( 2 · 𝑁 ) / 3 ) ) ) )
346 104 74 344 345 syl3anc ( 𝜑 → ( 𝐾 ≤ ( ( 2 · 𝑁 ) / 3 ) ↔ ( 2 · 𝐾 ) ≤ ( 2 · ( ( 2 · 𝑁 ) / 3 ) ) ) )
347 341 346 mpbid ( 𝜑 → ( 2 · 𝐾 ) ≤ ( 2 · ( ( 2 · 𝑁 ) / 3 ) ) )
348 22 nncnd ( 𝜑 → ( 2 · 𝑁 ) ∈ ℂ )
349 3ne0 3 ≠ 0
350 288 349 pm3.2i ( 3 ∈ ℂ ∧ 3 ≠ 0 )
351 divass ( ( 2 ∈ ℂ ∧ ( 2 · 𝑁 ) ∈ ℂ ∧ ( 3 ∈ ℂ ∧ 3 ≠ 0 ) ) → ( ( 2 · ( 2 · 𝑁 ) ) / 3 ) = ( 2 · ( ( 2 · 𝑁 ) / 3 ) ) )
352 289 350 351 mp3an13 ( ( 2 · 𝑁 ) ∈ ℂ → ( ( 2 · ( 2 · 𝑁 ) ) / 3 ) = ( 2 · ( ( 2 · 𝑁 ) / 3 ) ) )
353 348 352 syl ( 𝜑 → ( ( 2 · ( 2 · 𝑁 ) ) / 3 ) = ( 2 · ( ( 2 · 𝑁 ) / 3 ) ) )
354 9 nncnd ( 𝜑𝑁 ∈ ℂ )
355 mulass ( ( 2 ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 2 · 2 ) · 𝑁 ) = ( 2 · ( 2 · 𝑁 ) ) )
356 289 289 354 355 mp3an12i ( 𝜑 → ( ( 2 · 2 ) · 𝑁 ) = ( 2 · ( 2 · 𝑁 ) ) )
357 2t2e4 ( 2 · 2 ) = 4
358 357 oveq1i ( ( 2 · 2 ) · 𝑁 ) = ( 4 · 𝑁 )
359 356 358 eqtr3di ( 𝜑 → ( 2 · ( 2 · 𝑁 ) ) = ( 4 · 𝑁 ) )
360 359 oveq1d ( 𝜑 → ( ( 2 · ( 2 · 𝑁 ) ) / 3 ) = ( ( 4 · 𝑁 ) / 3 ) )
361 353 360 eqtr3d ( 𝜑 → ( 2 · ( ( 2 · 𝑁 ) / 3 ) ) = ( ( 4 · 𝑁 ) / 3 ) )
362 347 361 breqtrd ( 𝜑 → ( 2 · 𝐾 ) ≤ ( ( 4 · 𝑁 ) / 3 ) )
363 337 40 338 362 lesub1dd ( 𝜑 → ( ( 2 · 𝐾 ) − 5 ) ≤ ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) )
364 1lt2 1 < 2
365 364 a1i ( 𝜑 → 1 < 2 )
366 257 365 82 43 cxpled ( 𝜑 → ( ( ( 2 · 𝐾 ) − 5 ) ≤ ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) ↔ ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) ≤ ( 2 ↑𝑐 ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) ) ) )
367 363 366 mpbid ( 𝜑 → ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) ≤ ( 2 ↑𝑐 ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) ) )
368 85 46 33 lemul2d ( 𝜑 → ( ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) ≤ ( 2 ↑𝑐 ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) ) ↔ ( ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) · ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) ) ≤ ( ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) · ( 2 ↑𝑐 ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) ) ) ) )
369 367 368 mpbid ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) · ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) ) ≤ ( ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) · ( 2 ↑𝑐 ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) ) ) )
370 86 333 47 336 369 letrd ( 𝜑 → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) · ( 2 ↑𝑐 ( ( 2 · 𝐾 ) − 5 ) ) ) ≤ ( ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) · ( 2 ↑𝑐 ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) ) ) )
371 19 86 47 332 370 ltletrd ( 𝜑 → ( ( 2 · 𝑁 ) C 𝑁 ) < ( ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) · ( 2 ↑𝑐 ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) ) ) )
372 14 19 47 58 371 lttrd ( 𝜑 → ( ( 4 ↑ 𝑁 ) / 𝑁 ) < ( ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) · ( 2 ↑𝑐 ( ( ( 4 · 𝑁 ) / 3 ) − 5 ) ) ) )