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 2t2e4 ⊢ ( 2 · 2 ) = 4
355 354 oveq1i ⊢ ( ( 2 · 2 ) · 𝑁 ) = ( 4 · 𝑁 )
356 9 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
357 mulass ⊢ ( ( 2 ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 2 · 2 ) · 𝑁 ) = ( 2 · ( 2 · 𝑁 ) ) )
358 289 289 356 357 mp3an12i ⊢ ( 𝜑 → ( ( 2 · 2 ) · 𝑁 ) = ( 2 · ( 2 · 𝑁 ) ) )
359 355 358 syl5reqr ⊢ ( 𝜑 → ( 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 ) ) ) )