Metamath Proof Explorer

Theorem 2ap1caineq

Description: Inequality for Theorem 6.6 for AKS. (Contributed by metakunt, 8-Jun-2024)

Ref Expression
Hypotheses 2ap1caineq.1 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
2ap1caineq.2 ⊢ ( 𝜑 → 2 ≤ 𝑁 )
Assertion 2ap1caineq ( 𝜑 → ( 2 ↑ ( 𝑁 + 1 ) ) < ( ( ( 2 · 𝑁 ) + 1 ) C 𝑁 ) )

Proof

Step Hyp Ref Expression
1 2ap1caineq.1 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
2 2ap1caineq.2 ⊢ ( 𝜑 → 2 ≤ 𝑁 )
3 oveq1 ⊢ ( 𝑗 = 2 → ( 𝑗 + 1 ) = ( 2 + 1 ) )
4 3 oveq2d ⊢ ( 𝑗 = 2 → ( 2 ↑ ( 𝑗 + 1 ) ) = ( 2 ↑ ( 2 + 1 ) ) )
5 oveq2 ⊢ ( 𝑗 = 2 → ( 2 · 𝑗 ) = ( 2 · 2 ) )
6 5 oveq1d ⊢ ( 𝑗 = 2 → ( ( 2 · 𝑗 ) + 1 ) = ( ( 2 · 2 ) + 1 ) )
7 id ⊢ ( 𝑗 = 2 → 𝑗 = 2 )
8 6 7 oveq12d ⊢ ( 𝑗 = 2 → ( ( ( 2 · 𝑗 ) + 1 ) C 𝑗 ) = ( ( ( 2 · 2 ) + 1 ) C 2 ) )
9 4 8 breq12d ⊢ ( 𝑗 = 2 → ( ( 2 ↑ ( 𝑗 + 1 ) ) < ( ( ( 2 · 𝑗 ) + 1 ) C 𝑗 ) ↔ ( 2 ↑ ( 2 + 1 ) ) < ( ( ( 2 · 2 ) + 1 ) C 2 ) ) )
10 oveq1 ⊢ ( 𝑗 = 𝑘 → ( 𝑗 + 1 ) = ( 𝑘 + 1 ) )
11 10 oveq2d ⊢ ( 𝑗 = 𝑘 → ( 2 ↑ ( 𝑗 + 1 ) ) = ( 2 ↑ ( 𝑘 + 1 ) ) )
12 oveq2 ⊢ ( 𝑗 = 𝑘 → ( 2 · 𝑗 ) = ( 2 · 𝑘 ) )
13 12 oveq1d ⊢ ( 𝑗 = 𝑘 → ( ( 2 · 𝑗 ) + 1 ) = ( ( 2 · 𝑘 ) + 1 ) )
14 id ⊢ ( 𝑗 = 𝑘 → 𝑗 = 𝑘 )
15 13 14 oveq12d ⊢ ( 𝑗 = 𝑘 → ( ( ( 2 · 𝑗 ) + 1 ) C 𝑗 ) = ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) )
16 11 15 breq12d ⊢ ( 𝑗 = 𝑘 → ( ( 2 ↑ ( 𝑗 + 1 ) ) < ( ( ( 2 · 𝑗 ) + 1 ) C 𝑗 ) ↔ ( 2 ↑ ( 𝑘 + 1 ) ) < ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ) )
17 oveq1 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝑗 + 1 ) = ( ( 𝑘 + 1 ) + 1 ) )
18 17 oveq2d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 2 ↑ ( 𝑗 + 1 ) ) = ( 2 ↑ ( ( 𝑘 + 1 ) + 1 ) ) )
19 oveq2 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 2 · 𝑗 ) = ( 2 · ( 𝑘 + 1 ) ) )
20 19 oveq1d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 2 · 𝑗 ) + 1 ) = ( ( 2 · ( 𝑘 + 1 ) ) + 1 ) )
21 id ⊢ ( 𝑗 = ( 𝑘 + 1 ) → 𝑗 = ( 𝑘 + 1 ) )
22 20 21 oveq12d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( ( 2 · 𝑗 ) + 1 ) C 𝑗 ) = ( ( ( 2 · ( 𝑘 + 1 ) ) + 1 ) C ( 𝑘 + 1 ) ) )
23 18 22 breq12d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 2 ↑ ( 𝑗 + 1 ) ) < ( ( ( 2 · 𝑗 ) + 1 ) C 𝑗 ) ↔ ( 2 ↑ ( ( 𝑘 + 1 ) + 1 ) ) < ( ( ( 2 · ( 𝑘 + 1 ) ) + 1 ) C ( 𝑘 + 1 ) ) ) )
24 oveq1 ⊢ ( 𝑗 = 𝑁 → ( 𝑗 + 1 ) = ( 𝑁 + 1 ) )
25 24 oveq2d ⊢ ( 𝑗 = 𝑁 → ( 2 ↑ ( 𝑗 + 1 ) ) = ( 2 ↑ ( 𝑁 + 1 ) ) )
26 oveq2 ⊢ ( 𝑗 = 𝑁 → ( 2 · 𝑗 ) = ( 2 · 𝑁 ) )
27 26 oveq1d ⊢ ( 𝑗 = 𝑁 → ( ( 2 · 𝑗 ) + 1 ) = ( ( 2 · 𝑁 ) + 1 ) )
28 id ⊢ ( 𝑗 = 𝑁 → 𝑗 = 𝑁 )
29 27 28 oveq12d ⊢ ( 𝑗 = 𝑁 → ( ( ( 2 · 𝑗 ) + 1 ) C 𝑗 ) = ( ( ( 2 · 𝑁 ) + 1 ) C 𝑁 ) )
30 25 29 breq12d ⊢ ( 𝑗 = 𝑁 → ( ( 2 ↑ ( 𝑗 + 1 ) ) < ( ( ( 2 · 𝑗 ) + 1 ) C 𝑗 ) ↔ ( 2 ↑ ( 𝑁 + 1 ) ) < ( ( ( 2 · 𝑁 ) + 1 ) C 𝑁 ) ) )
31 8lt10 ⊢ 8 < 1 0
32 eqid ⊢ 8 = 8
33 cu2 ⊢ ( 2 ↑ 3 ) = 8
34 32 33 eqtr4i ⊢ 8 = ( 2 ↑ 3 )
35 5bc2eq10 ⊢ ( 5 C 2 ) = 1 0
36 35 eqcomi ⊢ 1 0 = ( 5 C 2 )
37 34 36 breq12i ⊢ ( 8 < 1 0 ↔ ( 2 ↑ 3 ) < ( 5 C 2 ) )
38 31 37 mpbi ⊢ ( 2 ↑ 3 ) < ( 5 C 2 )
39 df-3 ⊢ 3 = ( 2 + 1 )
40 39 oveq2i ⊢ ( 2 ↑ 3 ) = ( 2 ↑ ( 2 + 1 ) )
41 eqid ⊢ 5 = 5
42 2t2e4 ⊢ ( 2 · 2 ) = 4
43 42 oveq1i ⊢ ( ( 2 · 2 ) + 1 ) = ( 4 + 1 )
44 4p1e5 ⊢ ( 4 + 1 ) = 5
45 43 44 eqtri ⊢ ( ( 2 · 2 ) + 1 ) = 5
46 41 45 eqtr4i ⊢ 5 = ( ( 2 · 2 ) + 1 )
47 46 oveq1i ⊢ ( 5 C 2 ) = ( ( ( 2 · 2 ) + 1 ) C 2 )
48 40 47 breq12i ⊢ ( ( 2 ↑ 3 ) < ( 5 C 2 ) ↔ ( 2 ↑ ( 2 + 1 ) ) < ( ( ( 2 · 2 ) + 1 ) C 2 ) )
49 38 48 mpbi ⊢ ( 2 ↑ ( 2 + 1 ) ) < ( ( ( 2 · 2 ) + 1 ) C 2 )
50 49 a1i ⊢ ( 𝜑 → ( 2 ↑ ( 2 + 1 ) ) < ( ( ( 2 · 2 ) + 1 ) C 2 ) )
51 2re ⊢ 2 ∈ ℝ
52 51 a1i ⊢ ( ( 𝜑 ∧ ( 2 ↑ ( 𝑘 + 1 ) ) < ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ∧ ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) ) → 2 ∈ ℝ )
53 simpl ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 𝑘 ∈ ℤ )
54 0red ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 0 ∈ ℝ )
55 51 a1i ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 2 ∈ ℝ )
56 53 zred ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 𝑘 ∈ ℝ )
57 2pos ⊢ 0 < 2
58 57 a1i ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 0 < 2 )
59 simpr ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 2 ≤ 𝑘 )
60 54 55 56 58 59 ltletrd ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 0 < 𝑘 )
61 53 60 jca ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( 𝑘 ∈ ℤ ∧ 0 < 𝑘 ) )
62 elnnz ⊢ ( 𝑘 ∈ ℕ ↔ ( 𝑘 ∈ ℤ ∧ 0 < 𝑘 ) )
63 61 62 sylibr ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 𝑘 ∈ ℕ )
64 nnnn0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
65 63 64 syl ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 𝑘 ∈ ℕ0 )
66 65 nn0red ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 𝑘 ∈ ℝ )
67 54 55 66 58 59 ltletrd ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 0 < 𝑘 )
68 53 67 jca ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( 𝑘 ∈ ℤ ∧ 0 < 𝑘 ) )
69 68 62 sylibr ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 𝑘 ∈ ℕ )
70 69 nnred ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 𝑘 ∈ ℝ )
71 70 3ad2ant3 ⊢ ( ( 𝜑 ∧ ( 2 ↑ ( 𝑘 + 1 ) ) < ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ∧ ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) ) → 𝑘 ∈ ℝ )
72 52 71 remulcld ⊢ ( ( 𝜑 ∧ ( 2 ↑ ( 𝑘 + 1 ) ) < ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ∧ ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) ) → ( 2 · 𝑘 ) ∈ ℝ )
73 3re ⊢ 3 ∈ ℝ
74 73 a1i ⊢ ( ( 𝜑 ∧ ( 2 ↑ ( 𝑘 + 1 ) ) < ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ∧ ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) ) → 3 ∈ ℝ )
75 72 74 readdcld ⊢ ( ( 𝜑 ∧ ( 2 ↑ ( 𝑘 + 1 ) ) < ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ∧ ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) ) → ( ( 2 · 𝑘 ) + 3 ) ∈ ℝ )
76 71 52 readdcld ⊢ ( ( 𝜑 ∧ ( 2 ↑ ( 𝑘 + 1 ) ) < ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ∧ ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) ) → ( 𝑘 + 2 ) ∈ ℝ )
77 70 55 readdcld ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( 𝑘 + 2 ) ∈ ℝ )
78 69 nngt0d ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 0 < 𝑘 )
79 2rp ⊢ 2 ∈ ℝ+
80 79 a1i ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 2 ∈ ℝ+ )
81 70 80 ltaddrpd ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 𝑘 < ( 𝑘 + 2 ) )
82 54 70 77 78 81 lttrd ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 0 < ( 𝑘 + 2 ) )
83 54 82 ltned ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 0 ≠ ( 𝑘 + 2 ) )
84 83 necomd ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( 𝑘 + 2 ) ≠ 0 )
85 84 3ad2ant3 ⊢ ( ( 𝜑 ∧ ( 2 ↑ ( 𝑘 + 1 ) ) < ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ∧ ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) ) → ( 𝑘 + 2 ) ≠ 0 )
86 75 76 85 redivcld ⊢ ( ( 𝜑 ∧ ( 2 ↑ ( 𝑘 + 1 ) ) < ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ∧ ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) ) → ( ( ( 2 · 𝑘 ) + 3 ) / ( 𝑘 + 2 ) ) ∈ ℝ )
87 52 86 remulcld ⊢ ( ( 𝜑 ∧ ( 2 ↑ ( 𝑘 + 1 ) ) < ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ∧ ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) ) → ( 2 · ( ( ( 2 · 𝑘 ) + 3 ) / ( 𝑘 + 2 ) ) ) ∈ ℝ )
88 1nn0 ⊢ 1 ∈ ℕ0
89 88 a1i ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 1 ∈ ℕ0 )
90 65 89 nn0addcld ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( 𝑘 + 1 ) ∈ ℕ0 )
91 55 90 reexpcld ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℝ )
92 91 3ad2ant3 ⊢ ( ( 𝜑 ∧ ( 2 ↑ ( 𝑘 + 1 ) ) < ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ∧ ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) ) → ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℝ )
93 2nn0 ⊢ 2 ∈ ℕ0
94 93 a1i ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 2 ∈ ℕ0 )
95 94 65 nn0mulcld ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( 2 · 𝑘 ) ∈ ℕ0 )
96 95 89 nn0addcld ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( ( 2 · 𝑘 ) + 1 ) ∈ ℕ0 )
97 bccl ⊢ ( ( ( ( 2 · 𝑘 ) + 1 ) ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ∈ ℕ0 )
98 96 53 97 syl2anc ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ∈ ℕ0 )
99 98 nn0red ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ∈ ℝ )
100 99 3ad2ant3 ⊢ ( ( 𝜑 ∧ ( 2 ↑ ( 𝑘 + 1 ) ) < ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ∧ ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) ) → ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ∈ ℝ )
101 0le2 ⊢ 0 ≤ 2
102 101 a1i ⊢ ( ( 𝜑 ∧ ( 2 ↑ ( 𝑘 + 1 ) ) < ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ∧ ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) ) → 0 ≤ 2 )
103 eqid ⊢ 2 = 2
104 2t1e2 ⊢ ( 2 · 1 ) = 2
105 103 104 eqtr4i ⊢ 2 = ( 2 · 1 )
106 105 a1i ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 2 = ( 2 · 1 ) )
107 1red ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 1 ∈ ℝ )
108 55 70 remulcld ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( 2 · 𝑘 ) ∈ ℝ )
109 73 a1i ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 3 ∈ ℝ )
110 108 109 readdcld ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( ( 2 · 𝑘 ) + 3 ) ∈ ℝ )
111 110 77 84 redivcld ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( ( ( 2 · 𝑘 ) + 3 ) / ( 𝑘 + 2 ) ) ∈ ℝ )
112 nnrp ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ+ )
113 79 a1i ⊢ ( 𝑘 ∈ ℕ → 2 ∈ ℝ+ )
114 112 113 rpaddcld ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 + 2 ) ∈ ℝ+ )
115 114 rpcnd ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 + 2 ) ∈ ℂ )
116 115 mulridd ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑘 + 2 ) · 1 ) = ( 𝑘 + 2 ) )
117 nnre ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
118 51 a1i ⊢ ( 𝑘 ∈ ℕ → 2 ∈ ℝ )
119 118 117 remulcld ⊢ ( 𝑘 ∈ ℕ → ( 2 · 𝑘 ) ∈ ℝ )
120 73 a1i ⊢ ( 𝑘 ∈ ℕ → 3 ∈ ℝ )
121 112 rpge0d ⊢ ( 𝑘 ∈ ℕ → 0 ≤ 𝑘 )
122 1le2 ⊢ 1 ≤ 2
123 122 a1i ⊢ ( 𝑘 ∈ ℕ → 1 ≤ 2 )
124 117 118 121 123 lemulge12d ⊢ ( 𝑘 ∈ ℕ → 𝑘 ≤ ( 2 · 𝑘 ) )
125 2lt3 ⊢ 2 < 3
126 125 a1i ⊢ ( 𝑘 ∈ ℕ → 2 < 3 )
127 117 118 119 120 124 126 leltaddd ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 + 2 ) < ( ( 2 · 𝑘 ) + 3 ) )
128 116 127 eqbrtrd ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑘 + 2 ) · 1 ) < ( ( 2 · 𝑘 ) + 3 ) )
129 1red ⊢ ( 𝑘 ∈ ℕ → 1 ∈ ℝ )
130 119 120 readdcld ⊢ ( 𝑘 ∈ ℕ → ( ( 2 · 𝑘 ) + 3 ) ∈ ℝ )
131 129 130 114 ltmuldiv2d ⊢ ( 𝑘 ∈ ℕ → ( ( ( 𝑘 + 2 ) · 1 ) < ( ( 2 · 𝑘 ) + 3 ) ↔ 1 < ( ( ( 2 · 𝑘 ) + 3 ) / ( 𝑘 + 2 ) ) ) )
132 128 131 mpbid ⊢ ( 𝑘 ∈ ℕ → 1 < ( ( ( 2 · 𝑘 ) + 3 ) / ( 𝑘 + 2 ) ) )
133 69 132 syl ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 1 < ( ( ( 2 · 𝑘 ) + 3 ) / ( 𝑘 + 2 ) ) )
134 107 111 80 133 ltmul2dd ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( 2 · 1 ) < ( 2 · ( ( ( 2 · 𝑘 ) + 3 ) / ( 𝑘 + 2 ) ) ) )
135 106 134 eqbrtrd ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 2 < ( 2 · ( ( ( 2 · 𝑘 ) + 3 ) / ( 𝑘 + 2 ) ) ) )
136 135 3ad2ant3 ⊢ ( ( 𝜑 ∧ ( 2 ↑ ( 𝑘 + 1 ) ) < ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ∧ ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) ) → 2 < ( 2 · ( ( ( 2 · 𝑘 ) + 3 ) / ( 𝑘 + 2 ) ) ) )
137 101 a1i ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 0 ≤ 2 )
138 55 90 137 expge0d ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 0 ≤ ( 2 ↑ ( 𝑘 + 1 ) ) )
139 138 3ad2ant3 ⊢ ( ( 𝜑 ∧ ( 2 ↑ ( 𝑘 + 1 ) ) < ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ∧ ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) ) → 0 ≤ ( 2 ↑ ( 𝑘 + 1 ) ) )
140 simp2 ⊢ ( ( 𝜑 ∧ ( 2 ↑ ( 𝑘 + 1 ) ) < ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ∧ ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) ) → ( 2 ↑ ( 𝑘 + 1 ) ) < ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) )
141 52 87 92 100 102 136 139 140 ltmul12ad ⊢ ( ( 𝜑 ∧ ( 2 ↑ ( 𝑘 + 1 ) ) < ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ∧ ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) ) → ( 2 · ( 2 ↑ ( 𝑘 + 1 ) ) ) < ( ( 2 · ( ( ( 2 · 𝑘 ) + 3 ) / ( 𝑘 + 2 ) ) ) · ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ) )
142 2cnd ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 2 ∈ ℂ )
143 142 89 90 expaddd ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( 2 ↑ ( ( 𝑘 + 1 ) + 1 ) ) = ( ( 2 ↑ ( 𝑘 + 1 ) ) · ( 2 ↑ 1 ) ) )
144 142 90 expcld ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℂ )
145 142 89 expcld ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( 2 ↑ 1 ) ∈ ℂ )
146 144 145 mulcomd ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( ( 2 ↑ ( 𝑘 + 1 ) ) · ( 2 ↑ 1 ) ) = ( ( 2 ↑ 1 ) · ( 2 ↑ ( 𝑘 + 1 ) ) ) )
147 142 exp1d ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( 2 ↑ 1 ) = 2 )
148 147 oveq1d ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( ( 2 ↑ 1 ) · ( 2 ↑ ( 𝑘 + 1 ) ) ) = ( 2 · ( 2 ↑ ( 𝑘 + 1 ) ) ) )
149 eqidd ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( 2 · ( 2 ↑ ( 𝑘 + 1 ) ) ) = ( 2 · ( 2 ↑ ( 𝑘 + 1 ) ) ) )
150 146 148 149 3eqtrd ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( ( 2 ↑ ( 𝑘 + 1 ) ) · ( 2 ↑ 1 ) ) = ( 2 · ( 2 ↑ ( 𝑘 + 1 ) ) ) )
151 143 150 eqtrd ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( 2 ↑ ( ( 𝑘 + 1 ) + 1 ) ) = ( 2 · ( 2 ↑ ( 𝑘 + 1 ) ) ) )
152 151 eqcomd ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( 2 · ( 2 ↑ ( 𝑘 + 1 ) ) ) = ( 2 ↑ ( ( 𝑘 + 1 ) + 1 ) ) )
153 152 3ad2ant3 ⊢ ( ( 𝜑 ∧ ( 2 ↑ ( 𝑘 + 1 ) ) < ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ∧ ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) ) → ( 2 · ( 2 ↑ ( 𝑘 + 1 ) ) ) = ( 2 ↑ ( ( 𝑘 + 1 ) + 1 ) ) )
154 65 2np3bcnp1 ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( ( ( 2 · ( 𝑘 + 1 ) ) + 1 ) C ( 𝑘 + 1 ) ) = ( ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) · ( 2 · ( ( ( 2 · 𝑘 ) + 3 ) / ( 𝑘 + 2 ) ) ) ) )
155 98 nn0cnd ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ∈ ℂ )
156 69 nncnd ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 𝑘 ∈ ℂ )
157 142 156 mulcld ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( 2 · 𝑘 ) ∈ ℂ )
158 3cn ⊢ 3 ∈ ℂ
159 158 a1i ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → 3 ∈ ℂ )
160 157 159 addcld ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( ( 2 · 𝑘 ) + 3 ) ∈ ℂ )
161 156 142 addcld ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( 𝑘 + 2 ) ∈ ℂ )
162 160 161 84 divcld ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( ( ( 2 · 𝑘 ) + 3 ) / ( 𝑘 + 2 ) ) ∈ ℂ )
163 142 162 mulcld ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( 2 · ( ( ( 2 · 𝑘 ) + 3 ) / ( 𝑘 + 2 ) ) ) ∈ ℂ )
164 155 163 mulcomd ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) · ( 2 · ( ( ( 2 · 𝑘 ) + 3 ) / ( 𝑘 + 2 ) ) ) ) = ( ( 2 · ( ( ( 2 · 𝑘 ) + 3 ) / ( 𝑘 + 2 ) ) ) · ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ) )
165 154 164 eqtrd ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( ( ( 2 · ( 𝑘 + 1 ) ) + 1 ) C ( 𝑘 + 1 ) ) = ( ( 2 · ( ( ( 2 · 𝑘 ) + 3 ) / ( 𝑘 + 2 ) ) ) · ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ) )
166 165 eqcomd ⊢ ( ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) → ( ( 2 · ( ( ( 2 · 𝑘 ) + 3 ) / ( 𝑘 + 2 ) ) ) · ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ) = ( ( ( 2 · ( 𝑘 + 1 ) ) + 1 ) C ( 𝑘 + 1 ) ) )
167 166 3ad2ant3 ⊢ ( ( 𝜑 ∧ ( 2 ↑ ( 𝑘 + 1 ) ) < ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ∧ ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) ) → ( ( 2 · ( ( ( 2 · 𝑘 ) + 3 ) / ( 𝑘 + 2 ) ) ) · ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ) = ( ( ( 2 · ( 𝑘 + 1 ) ) + 1 ) C ( 𝑘 + 1 ) ) )
168 153 167 breq12d ⊢ ( ( 𝜑 ∧ ( 2 ↑ ( 𝑘 + 1 ) ) < ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ∧ ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) ) → ( ( 2 · ( 2 ↑ ( 𝑘 + 1 ) ) ) < ( ( 2 · ( ( ( 2 · 𝑘 ) + 3 ) / ( 𝑘 + 2 ) ) ) · ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ) ↔ ( 2 ↑ ( ( 𝑘 + 1 ) + 1 ) ) < ( ( ( 2 · ( 𝑘 + 1 ) ) + 1 ) C ( 𝑘 + 1 ) ) ) )
169 141 168 mpbid ⊢ ( ( 𝜑 ∧ ( 2 ↑ ( 𝑘 + 1 ) ) < ( ( ( 2 · 𝑘 ) + 1 ) C 𝑘 ) ∧ ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) ) → ( 2 ↑ ( ( 𝑘 + 1 ) + 1 ) ) < ( ( ( 2 · ( 𝑘 + 1 ) ) + 1 ) C ( 𝑘 + 1 ) ) )
170 2z ⊢ 2 ∈ ℤ
171 170 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
172 9 16 23 30 50 169 171 1 2 uzindd ⊢ ( 𝜑 → ( 2 ↑ ( 𝑁 + 1 ) ) < ( ( ( 2 · 𝑁 ) + 1 ) C 𝑁 ) )