Metamath Proof Explorer

Theorem stoweidlem1

Description: Lemma for stoweid . This lemma is used by Lemma 1 in BrosowskiDeutsh p. 90; the key step uses Bernoulli's inequality bernneq . (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem1.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
stoweidlem1.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
stoweidlem1.3 ⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
stoweidlem1.5 ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
stoweidlem1.6 ⊢ ( 𝜑 → 0 ≤ 𝐴 )
stoweidlem1.7 ⊢ ( 𝜑 → 𝐴 ≤ 1 )
stoweidlem1.8 ⊢ ( 𝜑 → 𝐷 ≤ 𝐴 )
Assertion stoweidlem1 ( 𝜑 → ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ≤ ( 1 / ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem1.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 stoweidlem1.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
3 stoweidlem1.3 ⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
4 stoweidlem1.5 ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
5 stoweidlem1.6 ⊢ ( 𝜑 → 0 ≤ 𝐴 )
6 stoweidlem1.7 ⊢ ( 𝜑 → 𝐴 ≤ 1 )
7 stoweidlem1.8 ⊢ ( 𝜑 → 𝐷 ≤ 𝐴 )
8 1re ⊢ 1 ∈ ℝ
9 8 a1i ⊢ ( 𝜑 → 1 ∈ ℝ )
10 4 rpred ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
11 1 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
12 10 11 reexpcld ⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ∈ ℝ )
13 9 12 resubcld ⊢ ( 𝜑 → ( 1 − ( 𝐴 ↑ 𝑁 ) ) ∈ ℝ )
14 2 nnnn0d ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
15 14 11 nn0expcld ⊢ ( 𝜑 → ( 𝐾 ↑ 𝑁 ) ∈ ℕ0 )
16 13 15 reexpcld ⊢ ( 𝜑 → ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ∈ ℝ )
17 2nn0 ⊢ 2 ∈ ℕ0
18 17 a1i ⊢ ( 𝜑 → 2 ∈ ℕ0 )
19 18 11 nn0mulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℕ0 )
20 10 19 reexpcld ⊢ ( 𝜑 → ( 𝐴 ↑ ( 2 · 𝑁 ) ) ∈ ℝ )
21 9 20 resubcld ⊢ ( 𝜑 → ( 1 − ( 𝐴 ↑ ( 2 · 𝑁 ) ) ) ∈ ℝ )
22 21 15 reexpcld ⊢ ( 𝜑 → ( ( 1 − ( 𝐴 ↑ ( 2 · 𝑁 ) ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ∈ ℝ )
23 2 nnred ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
24 23 10 remulcld ⊢ ( 𝜑 → ( 𝐾 · 𝐴 ) ∈ ℝ )
25 24 11 reexpcld ⊢ ( 𝜑 → ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ∈ ℝ )
26 2 nncnd ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
27 4 rpcnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
28 2 nnne0d ⊢ ( 𝜑 → 𝐾 ≠ 0 )
29 4 rpne0d ⊢ ( 𝜑 → 𝐴 ≠ 0 )
30 26 27 28 29 mulne0d ⊢ ( 𝜑 → ( 𝐾 · 𝐴 ) ≠ 0 )
31 26 27 mulcld ⊢ ( 𝜑 → ( 𝐾 · 𝐴 ) ∈ ℂ )
32 expne0 ⊢ ( ( ( 𝐾 · 𝐴 ) ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ≠ 0 ↔ ( 𝐾 · 𝐴 ) ≠ 0 ) )
33 31 1 32 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ≠ 0 ↔ ( 𝐾 · 𝐴 ) ≠ 0 ) )
34 30 33 mpbird ⊢ ( 𝜑 → ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ≠ 0 )
35 22 25 34 redivcld ⊢ ( 𝜑 → ( ( ( 1 − ( 𝐴 ↑ ( 2 · 𝑁 ) ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) ∈ ℝ )
36 3 rpred ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
37 23 36 remulcld ⊢ ( 𝜑 → ( 𝐾 · 𝐷 ) ∈ ℝ )
38 37 11 reexpcld ⊢ ( 𝜑 → ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ∈ ℝ )
39 3 rpcnd ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
40 3 rpne0d ⊢ ( 𝜑 → 𝐷 ≠ 0 )
41 26 39 28 40 mulne0d ⊢ ( 𝜑 → ( 𝐾 · 𝐷 ) ≠ 0 )
42 26 39 mulcld ⊢ ( 𝜑 → ( 𝐾 · 𝐷 ) ∈ ℂ )
43 expne0 ⊢ ( ( ( 𝐾 · 𝐷 ) ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ≠ 0 ↔ ( 𝐾 · 𝐷 ) ≠ 0 ) )
44 42 1 43 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ≠ 0 ↔ ( 𝐾 · 𝐷 ) ≠ 0 ) )
45 41 44 mpbird ⊢ ( 𝜑 → ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ≠ 0 )
46 9 38 45 redivcld ⊢ ( 𝜑 → ( 1 / ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ) ∈ ℝ )
47 23 11 reexpcld ⊢ ( 𝜑 → ( 𝐾 ↑ 𝑁 ) ∈ ℝ )
48 47 12 remulcld ⊢ ( 𝜑 → ( ( 𝐾 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) ∈ ℝ )
49 9 48 readdcld ⊢ ( 𝜑 → ( 1 + ( ( 𝐾 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) ) ∈ ℝ )
50 16 49 remulcld ⊢ ( 𝜑 → ( ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) · ( 1 + ( ( 𝐾 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) ) ) ∈ ℝ )
51 50 25 34 redivcld ⊢ ( 𝜑 → ( ( ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) · ( 1 + ( ( 𝐾 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) ) ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) ∈ ℝ )
52 9 12 readdcld ⊢ ( 𝜑 → ( 1 + ( 𝐴 ↑ 𝑁 ) ) ∈ ℝ )
53 52 15 reexpcld ⊢ ( 𝜑 → ( ( 1 + ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ∈ ℝ )
54 16 53 remulcld ⊢ ( 𝜑 → ( ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) · ( ( 1 + ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ) ∈ ℝ )
55 54 25 34 redivcld ⊢ ( 𝜑 → ( ( ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) · ( ( 1 + ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) ∈ ℝ )
56 49 25 34 redivcld ⊢ ( 𝜑 → ( ( 1 + ( ( 𝐾 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) ∈ ℝ )
57 exple1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ≤ 1 )
58 10 5 6 11 57 syl31anc ⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ≤ 1 )
59 9 12 subge0d ⊢ ( 𝜑 → ( 0 ≤ ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↔ ( 𝐴 ↑ 𝑁 ) ≤ 1 ) )
60 58 59 mpbird ⊢ ( 𝜑 → 0 ≤ ( 1 − ( 𝐴 ↑ 𝑁 ) ) )
61 13 15 60 expge0d ⊢ ( 𝜑 → 0 ≤ ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )
62 31 11 expcld ⊢ ( 𝜑 → ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ∈ ℂ )
63 62 34 dividd ⊢ ( 𝜑 → ( ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) = 1 )
64 62 addlidd ⊢ ( 𝜑 → ( 0 + ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) = ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) )
65 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
66 0le1 ⊢ 0 ≤ 1
67 66 a1i ⊢ ( 𝜑 → 0 ≤ 1 )
68 65 9 25 67 leadd1dd ⊢ ( 𝜑 → ( 0 + ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) ≤ ( 1 + ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) )
69 64 68 eqbrtrrd ⊢ ( 𝜑 → ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ≤ ( 1 + ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) )
70 9 25 readdcld ⊢ ( 𝜑 → ( 1 + ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) ∈ ℝ )
71 1 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
72 2 nngt0d ⊢ ( 𝜑 → 0 < 𝐾 )
73 4 rpgt0d ⊢ ( 𝜑 → 0 < 𝐴 )
74 23 10 72 73 mulgt0d ⊢ ( 𝜑 → 0 < ( 𝐾 · 𝐴 ) )
75 expgt0 ⊢ ( ( ( 𝐾 · 𝐴 ) ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 0 < ( 𝐾 · 𝐴 ) ) → 0 < ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) )
76 24 71 74 75 syl3anc ⊢ ( 𝜑 → 0 < ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) )
77 lediv1 ⊢ ( ( ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ∈ ℝ ∧ ( 1 + ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) ∈ ℝ ∧ ( ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ∈ ℝ ∧ 0 < ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) ) → ( ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ≤ ( 1 + ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) ↔ ( ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) ≤ ( ( 1 + ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) ) )
78 25 70 25 76 77 syl112anc ⊢ ( 𝜑 → ( ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ≤ ( 1 + ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) ↔ ( ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) ≤ ( ( 1 + ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) ) )
79 69 78 mpbid ⊢ ( 𝜑 → ( ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) ≤ ( ( 1 + ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) )
80 63 79 eqbrtrrd ⊢ ( 𝜑 → 1 ≤ ( ( 1 + ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) )
81 26 27 11 mulexpd ⊢ ( 𝜑 → ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) = ( ( 𝐾 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) )
82 81 oveq2d ⊢ ( 𝜑 → ( 1 + ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) = ( 1 + ( ( 𝐾 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) ) )
83 82 oveq1d ⊢ ( 𝜑 → ( ( 1 + ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) = ( ( 1 + ( ( 𝐾 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) )
84 80 83 breqtrd ⊢ ( 𝜑 → 1 ≤ ( ( 1 + ( ( 𝐾 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) )
85 16 56 61 84 lemulge11d ⊢ ( 𝜑 → ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ≤ ( ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) · ( ( 1 + ( ( 𝐾 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) ) )
86 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
87 27 11 expcld ⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ∈ ℂ )
88 86 87 subcld ⊢ ( 𝜑 → ( 1 − ( 𝐴 ↑ 𝑁 ) ) ∈ ℂ )
89 88 15 expcld ⊢ ( 𝜑 → ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ∈ ℂ )
90 26 11 expcld ⊢ ( 𝜑 → ( 𝐾 ↑ 𝑁 ) ∈ ℂ )
91 90 87 mulcld ⊢ ( 𝜑 → ( ( 𝐾 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) ∈ ℂ )
92 86 91 addcld ⊢ ( 𝜑 → ( 1 + ( ( 𝐾 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) ) ∈ ℂ )
93 89 92 62 34 divassd ⊢ ( 𝜑 → ( ( ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) · ( 1 + ( ( 𝐾 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) ) ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) = ( ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) · ( ( 1 + ( ( 𝐾 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) ) )
94 85 93 breqtrrd ⊢ ( 𝜑 → ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ≤ ( ( ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) · ( 1 + ( ( 𝐾 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) ) ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) )
95 90 87 mulcomd ⊢ ( 𝜑 → ( ( 𝐾 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) = ( ( 𝐴 ↑ 𝑁 ) · ( 𝐾 ↑ 𝑁 ) ) )
96 95 oveq2d ⊢ ( 𝜑 → ( 1 + ( ( 𝐾 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) ) = ( 1 + ( ( 𝐴 ↑ 𝑁 ) · ( 𝐾 ↑ 𝑁 ) ) ) )
97 9 renegcld ⊢ ( 𝜑 → - 1 ∈ ℝ )
98 le0neg2 ⊢ ( 1 ∈ ℝ → ( 0 ≤ 1 ↔ - 1 ≤ 0 ) )
99 8 98 ax-mp ⊢ ( 0 ≤ 1 ↔ - 1 ≤ 0 )
100 66 99 mpbi ⊢ - 1 ≤ 0
101 100 a1i ⊢ ( 𝜑 → - 1 ≤ 0 )
102 10 11 5 expge0d ⊢ ( 𝜑 → 0 ≤ ( 𝐴 ↑ 𝑁 ) )
103 97 65 12 101 102 letrd ⊢ ( 𝜑 → - 1 ≤ ( 𝐴 ↑ 𝑁 ) )
104 bernneq ⊢ ( ( ( 𝐴 ↑ 𝑁 ) ∈ ℝ ∧ ( 𝐾 ↑ 𝑁 ) ∈ ℕ0 ∧ - 1 ≤ ( 𝐴 ↑ 𝑁 ) ) → ( 1 + ( ( 𝐴 ↑ 𝑁 ) · ( 𝐾 ↑ 𝑁 ) ) ) ≤ ( ( 1 + ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )
105 12 15 103 104 syl3anc ⊢ ( 𝜑 → ( 1 + ( ( 𝐴 ↑ 𝑁 ) · ( 𝐾 ↑ 𝑁 ) ) ) ≤ ( ( 1 + ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )
106 96 105 eqbrtrd ⊢ ( 𝜑 → ( 1 + ( ( 𝐾 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) ) ≤ ( ( 1 + ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )
107 49 53 16 61 106 lemul2ad ⊢ ( 𝜑 → ( ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) · ( 1 + ( ( 𝐾 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) ) ) ≤ ( ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) · ( ( 1 + ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ) )
108 lediv1 ⊢ ( ( ( ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) · ( 1 + ( ( 𝐾 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) ) ) ∈ ℝ ∧ ( ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) · ( ( 1 + ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ) ∈ ℝ ∧ ( ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ∈ ℝ ∧ 0 < ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) ) → ( ( ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) · ( 1 + ( ( 𝐾 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) ) ) ≤ ( ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) · ( ( 1 + ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ) ↔ ( ( ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) · ( 1 + ( ( 𝐾 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) ) ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) ≤ ( ( ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) · ( ( 1 + ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) ) )
109 50 54 25 76 108 syl112anc ⊢ ( 𝜑 → ( ( ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) · ( 1 + ( ( 𝐾 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) ) ) ≤ ( ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) · ( ( 1 + ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ) ↔ ( ( ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) · ( 1 + ( ( 𝐾 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) ) ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) ≤ ( ( ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) · ( ( 1 + ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) ) )
110 107 109 mpbid ⊢ ( 𝜑 → ( ( ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) · ( 1 + ( ( 𝐾 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) ) ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) ≤ ( ( ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) · ( ( 1 + ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) )
111 16 51 55 94 110 letrd ⊢ ( 𝜑 → ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ≤ ( ( ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) · ( ( 1 + ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) )
112 86 87 addcld ⊢ ( 𝜑 → ( 1 + ( 𝐴 ↑ 𝑁 ) ) ∈ ℂ )
113 88 112 mulcomd ⊢ ( 𝜑 → ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) · ( 1 + ( 𝐴 ↑ 𝑁 ) ) ) = ( ( 1 + ( 𝐴 ↑ 𝑁 ) ) · ( 1 − ( 𝐴 ↑ 𝑁 ) ) ) )
114 113 oveq1d ⊢ ( 𝜑 → ( ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) · ( 1 + ( 𝐴 ↑ 𝑁 ) ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) = ( ( ( 1 + ( 𝐴 ↑ 𝑁 ) ) · ( 1 − ( 𝐴 ↑ 𝑁 ) ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )
115 88 112 15 mulexpd ⊢ ( 𝜑 → ( ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) · ( 1 + ( 𝐴 ↑ 𝑁 ) ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) = ( ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) · ( ( 1 + ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ) )
116 subsq ⊢ ( ( 1 ∈ ℂ ∧ ( 𝐴 ↑ 𝑁 ) ∈ ℂ ) → ( ( 1 ↑ 2 ) − ( ( 𝐴 ↑ 𝑁 ) ↑ 2 ) ) = ( ( 1 + ( 𝐴 ↑ 𝑁 ) ) · ( 1 − ( 𝐴 ↑ 𝑁 ) ) ) )
117 86 87 116 syl2anc ⊢ ( 𝜑 → ( ( 1 ↑ 2 ) − ( ( 𝐴 ↑ 𝑁 ) ↑ 2 ) ) = ( ( 1 + ( 𝐴 ↑ 𝑁 ) ) · ( 1 − ( 𝐴 ↑ 𝑁 ) ) ) )
118 sq1 ⊢ ( 1 ↑ 2 ) = 1
119 118 a1i ⊢ ( 𝜑 → ( 1 ↑ 2 ) = 1 )
120 27 18 11 expmuld ⊢ ( 𝜑 → ( 𝐴 ↑ ( 𝑁 · 2 ) ) = ( ( 𝐴 ↑ 𝑁 ) ↑ 2 ) )
121 1 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
122 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
123 121 122 mulcomd ⊢ ( 𝜑 → ( 𝑁 · 2 ) = ( 2 · 𝑁 ) )
124 123 oveq2d ⊢ ( 𝜑 → ( 𝐴 ↑ ( 𝑁 · 2 ) ) = ( 𝐴 ↑ ( 2 · 𝑁 ) ) )
125 120 124 eqtr3d ⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) ↑ 2 ) = ( 𝐴 ↑ ( 2 · 𝑁 ) ) )
126 119 125 oveq12d ⊢ ( 𝜑 → ( ( 1 ↑ 2 ) − ( ( 𝐴 ↑ 𝑁 ) ↑ 2 ) ) = ( 1 − ( 𝐴 ↑ ( 2 · 𝑁 ) ) ) )
127 117 126 eqtr3d ⊢ ( 𝜑 → ( ( 1 + ( 𝐴 ↑ 𝑁 ) ) · ( 1 − ( 𝐴 ↑ 𝑁 ) ) ) = ( 1 − ( 𝐴 ↑ ( 2 · 𝑁 ) ) ) )
128 127 oveq1d ⊢ ( 𝜑 → ( ( ( 1 + ( 𝐴 ↑ 𝑁 ) ) · ( 1 − ( 𝐴 ↑ 𝑁 ) ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) = ( ( 1 − ( 𝐴 ↑ ( 2 · 𝑁 ) ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )
129 114 115 128 3eqtr3d ⊢ ( 𝜑 → ( ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) · ( ( 1 + ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ) = ( ( 1 − ( 𝐴 ↑ ( 2 · 𝑁 ) ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )
130 129 oveq1d ⊢ ( 𝜑 → ( ( ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) · ( ( 1 + ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) = ( ( ( 1 − ( 𝐴 ↑ ( 2 · 𝑁 ) ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) )
131 111 130 breqtrd ⊢ ( 𝜑 → ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ≤ ( ( ( 1 − ( 𝐴 ↑ ( 2 · 𝑁 ) ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) )
132 22 9 jca ⊢ ( 𝜑 → ( ( ( 1 − ( 𝐴 ↑ ( 2 · 𝑁 ) ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ∈ ℝ ∧ 1 ∈ ℝ ) )
133 exple1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ∧ ( 2 · 𝑁 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( 2 · 𝑁 ) ) ≤ 1 )
134 10 5 6 19 133 syl31anc ⊢ ( 𝜑 → ( 𝐴 ↑ ( 2 · 𝑁 ) ) ≤ 1 )
135 9 20 subge0d ⊢ ( 𝜑 → ( 0 ≤ ( 1 − ( 𝐴 ↑ ( 2 · 𝑁 ) ) ) ↔ ( 𝐴 ↑ ( 2 · 𝑁 ) ) ≤ 1 ) )
136 134 135 mpbird ⊢ ( 𝜑 → 0 ≤ ( 1 − ( 𝐴 ↑ ( 2 · 𝑁 ) ) ) )
137 21 15 136 expge0d ⊢ ( 𝜑 → 0 ≤ ( ( 1 − ( 𝐴 ↑ ( 2 · 𝑁 ) ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )
138 1m1e0 ⊢ ( 1 − 1 ) = 0
139 10 19 5 expge0d ⊢ ( 𝜑 → 0 ≤ ( 𝐴 ↑ ( 2 · 𝑁 ) ) )
140 138 139 eqbrtrid ⊢ ( 𝜑 → ( 1 − 1 ) ≤ ( 𝐴 ↑ ( 2 · 𝑁 ) ) )
141 9 9 20 140 subled ⊢ ( 𝜑 → ( 1 − ( 𝐴 ↑ ( 2 · 𝑁 ) ) ) ≤ 1 )
142 exple1 ⊢ ( ( ( ( 1 − ( 𝐴 ↑ ( 2 · 𝑁 ) ) ) ∈ ℝ ∧ 0 ≤ ( 1 − ( 𝐴 ↑ ( 2 · 𝑁 ) ) ) ∧ ( 1 − ( 𝐴 ↑ ( 2 · 𝑁 ) ) ) ≤ 1 ) ∧ ( 𝐾 ↑ 𝑁 ) ∈ ℕ0 ) → ( ( 1 − ( 𝐴 ↑ ( 2 · 𝑁 ) ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ≤ 1 )
143 21 136 141 15 142 syl31anc ⊢ ( 𝜑 → ( ( 1 − ( 𝐴 ↑ ( 2 · 𝑁 ) ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ≤ 1 )
144 132 137 143 jca32 ⊢ ( 𝜑 → ( ( ( ( 1 − ( 𝐴 ↑ ( 2 · 𝑁 ) ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ∈ ℝ ∧ 1 ∈ ℝ ) ∧ ( 0 ≤ ( ( 1 − ( 𝐴 ↑ ( 2 · 𝑁 ) ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ∧ ( ( 1 − ( 𝐴 ↑ ( 2 · 𝑁 ) ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ≤ 1 ) ) )
145 38 25 jca ⊢ ( 𝜑 → ( ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ∈ ℝ ∧ ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ∈ ℝ ) )
146 3 rpgt0d ⊢ ( 𝜑 → 0 < 𝐷 )
147 23 36 72 146 mulgt0d ⊢ ( 𝜑 → 0 < ( 𝐾 · 𝐷 ) )
148 expgt0 ⊢ ( ( ( 𝐾 · 𝐷 ) ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 0 < ( 𝐾 · 𝐷 ) ) → 0 < ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) )
149 37 71 147 148 syl3anc ⊢ ( 𝜑 → 0 < ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) )
150 65 23 72 ltled ⊢ ( 𝜑 → 0 ≤ 𝐾 )
151 65 36 146 ltled ⊢ ( 𝜑 → 0 ≤ 𝐷 )
152 23 36 150 151 mulge0d ⊢ ( 𝜑 → 0 ≤ ( 𝐾 · 𝐷 ) )
153 36 10 23 150 7 lemul2ad ⊢ ( 𝜑 → ( 𝐾 · 𝐷 ) ≤ ( 𝐾 · 𝐴 ) )
154 leexp1a ⊢ ( ( ( ( 𝐾 · 𝐷 ) ∈ ℝ ∧ ( 𝐾 · 𝐴 ) ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 0 ≤ ( 𝐾 · 𝐷 ) ∧ ( 𝐾 · 𝐷 ) ≤ ( 𝐾 · 𝐴 ) ) ) → ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ≤ ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) )
155 37 24 11 152 153 154 syl32anc ⊢ ( 𝜑 → ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ≤ ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) )
156 149 155 jca ⊢ ( 𝜑 → ( 0 < ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ∧ ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ≤ ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) )
157 lediv12a ⊢ ( ( ( ( ( ( 1 − ( 𝐴 ↑ ( 2 · 𝑁 ) ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ∈ ℝ ∧ 1 ∈ ℝ ) ∧ ( 0 ≤ ( ( 1 − ( 𝐴 ↑ ( 2 · 𝑁 ) ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ∧ ( ( 1 − ( 𝐴 ↑ ( 2 · 𝑁 ) ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ≤ 1 ) ) ∧ ( ( ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ∈ ℝ ∧ ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ∈ ℝ ) ∧ ( 0 < ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ∧ ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ≤ ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) ) ) → ( ( ( 1 − ( 𝐴 ↑ ( 2 · 𝑁 ) ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) ≤ ( 1 / ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ) )
158 144 145 156 157 syl12anc ⊢ ( 𝜑 → ( ( ( 1 − ( 𝐴 ↑ ( 2 · 𝑁 ) ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) / ( ( 𝐾 · 𝐴 ) ↑ 𝑁 ) ) ≤ ( 1 / ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ) )
159 16 35 46 131 158 letrd ⊢ ( 𝜑 → ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ≤ ( 1 / ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ) )