Metamath Proof Explorer

Theorem jm3.1lem2

Description: Lemma for jm3.1 . (Contributed by Stefan O'Rear, 16-Oct-2014)

Ref Expression
Hypotheses jm3.1.a ⊢ φ → A ∈ ℤ ≥ 2
jm3.1.b ⊢ φ → K ∈ ℤ ≥ 2
jm3.1.c ⊢ φ → N ∈ ℕ
jm3.1.d ⊢ φ → K Y rm N + 1 ≤ A
Assertion jm3.1lem2 ⊢ φ → K N < 2 ⁢ A ⁢ K - K 2 - 1

Proof

Step Hyp Ref Expression
1 jm3.1.a ⊢ φ → A ∈ ℤ ≥ 2
2 jm3.1.b ⊢ φ → K ∈ ℤ ≥ 2
3 jm3.1.c ⊢ φ → N ∈ ℕ
4 jm3.1.d ⊢ φ → K Y rm N + 1 ≤ A
5 eluzelre ⊢ K ∈ ℤ ≥ 2 → K ∈ ℝ
6 2 5 syl ⊢ φ → K ∈ ℝ
7 3 nnnn0d ⊢ φ → N ∈ ℕ 0
8 6 7 reexpcld ⊢ φ → K N ∈ ℝ
9 eluzelre ⊢ A ∈ ℤ ≥ 2 → A ∈ ℝ
10 1 9 syl ⊢ φ → A ∈ ℝ
11 2re ⊢ 2 ∈ ℝ
12 remulcl ⊢ 2 ∈ ℝ ∧ A ∈ ℝ → 2 ⁢ A ∈ ℝ
13 11 10 12 sylancr ⊢ φ → 2 ⁢ A ∈ ℝ
14 13 6 remulcld ⊢ φ → 2 ⁢ A ⁢ K ∈ ℝ
15 6 resqcld ⊢ φ → K 2 ∈ ℝ
16 14 15 resubcld ⊢ φ → 2 ⁢ A ⁢ K − K 2 ∈ ℝ
17 1re ⊢ 1 ∈ ℝ
18 resubcl ⊢ 2 ⁢ A ⁢ K − K 2 ∈ ℝ ∧ 1 ∈ ℝ → 2 ⁢ A ⁢ K - K 2 - 1 ∈ ℝ
19 16 17 18 sylancl ⊢ φ → 2 ⁢ A ⁢ K - K 2 - 1 ∈ ℝ
20 1 2 3 4 jm3.1lem1 ⊢ φ → K N < A
21 10 6 remulcld ⊢ φ → A ⁢ K ∈ ℝ
22 resubcl ⊢ K ∈ ℝ ∧ 1 ∈ ℝ → K − 1 ∈ ℝ
23 6 17 22 sylancl ⊢ φ → K − 1 ∈ ℝ
24 21 23 readdcld ⊢ φ → A ⁢ K + K - 1 ∈ ℝ
25 eluz2b1 ⊢ K ∈ ℤ ≥ 2 ↔ K ∈ ℤ ∧ 1 < K
26 25 simprbi ⊢ K ∈ ℤ ≥ 2 → 1 < K
27 2 26 syl ⊢ φ → 1 < K
28 eluz2nn ⊢ A ∈ ℤ ≥ 2 → A ∈ ℕ
29 1 28 syl ⊢ φ → A ∈ ℕ
30 29 nngt0d ⊢ φ → 0 < A
31 ltmulgt11 ⊢ A ∈ ℝ ∧ K ∈ ℝ ∧ 0 < A → 1 < K ↔ A < A ⁢ K
32 10 6 30 31 syl3anc ⊢ φ → 1 < K ↔ A < A ⁢ K
33 27 32 mpbid ⊢ φ → A < A ⁢ K
34 uz2m1nn ⊢ K ∈ ℤ ≥ 2 → K − 1 ∈ ℕ
35 2 34 syl ⊢ φ → K − 1 ∈ ℕ
36 35 nnrpd ⊢ φ → K − 1 ∈ ℝ +
37 21 36 ltaddrpd ⊢ φ → A ⁢ K < A ⁢ K + K - 1
38 10 21 24 33 37 lttrd ⊢ φ → A < A ⁢ K + K - 1
39 peano2re ⊢ K ∈ ℝ → K + 1 ∈ ℝ
40 6 39 syl ⊢ φ → K + 1 ∈ ℝ
41 40 6 remulcld ⊢ φ → K + 1 ⁢ K ∈ ℝ
42 resubcl ⊢ A ⁢ K ∈ ℝ ∧ 1 ∈ ℝ → A ⁢ K − 1 ∈ ℝ
43 21 17 42 sylancl ⊢ φ → A ⁢ K − 1 ∈ ℝ
44 43 15 resubcld ⊢ φ → A ⁢ K - 1 - K 2 ∈ ℝ
45 6 recnd ⊢ φ → K ∈ ℂ
46 45 exp1d ⊢ φ → K 1 = K
47 eluz2nn ⊢ K ∈ ℤ ≥ 2 → K ∈ ℕ
48 2 47 syl ⊢ φ → K ∈ ℕ
49 48 nnge1d ⊢ φ → 1 ≤ K
50 nnuz ⊢ ℕ = ℤ ≥ 1
51 3 50 eleqtrdi ⊢ φ → N ∈ ℤ ≥ 1
52 6 49 51 leexp2ad ⊢ φ → K 1 ≤ K N
53 46 52 eqbrtrrd ⊢ φ → K ≤ K N
54 6 8 10 53 20 lelttrd ⊢ φ → K < A
55 eluzelz ⊢ K ∈ ℤ ≥ 2 → K ∈ ℤ
56 2 55 syl ⊢ φ → K ∈ ℤ
57 eluzelz ⊢ A ∈ ℤ ≥ 2 → A ∈ ℤ
58 1 57 syl ⊢ φ → A ∈ ℤ
59 zltp1le ⊢ K ∈ ℤ ∧ A ∈ ℤ → K < A ↔ K + 1 ≤ A
60 56 58 59 syl2anc ⊢ φ → K < A ↔ K + 1 ≤ A
61 54 60 mpbid ⊢ φ → K + 1 ≤ A
62 48 nngt0d ⊢ φ → 0 < K
63 lemul1 ⊢ K + 1 ∈ ℝ ∧ A ∈ ℝ ∧ K ∈ ℝ ∧ 0 < K → K + 1 ≤ A ↔ K + 1 ⁢ K ≤ A ⁢ K
64 40 10 6 62 63 syl112anc ⊢ φ → K + 1 ≤ A ↔ K + 1 ⁢ K ≤ A ⁢ K
65 61 64 mpbid ⊢ φ → K + 1 ⁢ K ≤ A ⁢ K
66 41 21 44 65 leadd1dd ⊢ φ → K + 1 ⁢ K + A ⁢ K − 1 - K 2 ≤ A ⁢ K + A ⁢ K − 1 - K 2
67 21 recnd ⊢ φ → A ⁢ K ∈ ℂ
68 41 15 resubcld ⊢ φ → K + 1 ⁢ K − K 2 ∈ ℝ
69 68 recnd ⊢ φ → K + 1 ⁢ K − K 2 ∈ ℂ
70 1cnd ⊢ φ → 1 ∈ ℂ
71 67 69 70 addsub12d ⊢ φ → A ⁢ K + K + 1 ⁢ K − K 2 - 1 = K + 1 ⁢ K − K 2 + A ⁢ K - 1
72 45 70 45 adddird ⊢ φ → K + 1 ⁢ K = K ⁢ K + 1 ⁢ K
73 45 sqvald ⊢ φ → K 2 = K ⁢ K
74 72 73 oveq12d ⊢ φ → K + 1 ⁢ K − K 2 = K ⁢ K + 1 ⁢ K - K ⁢ K
75 45 45 mulcld ⊢ φ → K ⁢ K ∈ ℂ
76 ax-1cn ⊢ 1 ∈ ℂ
77 mulcl ⊢ 1 ∈ ℂ ∧ K ∈ ℂ → 1 ⁢ K ∈ ℂ
78 76 45 77 sylancr ⊢ φ → 1 ⁢ K ∈ ℂ
79 75 78 pncan2d ⊢ φ → K ⁢ K + 1 ⁢ K - K ⁢ K = 1 ⁢ K
80 45 mulid2d ⊢ φ → 1 ⁢ K = K
81 74 79 80 3eqtrd ⊢ φ → K + 1 ⁢ K − K 2 = K
82 81 oveq1d ⊢ φ → K + 1 ⁢ K - K 2 - 1 = K − 1
83 82 oveq2d ⊢ φ → A ⁢ K + K + 1 ⁢ K − K 2 - 1 = A ⁢ K + K - 1
84 41 recnd ⊢ φ → K + 1 ⁢ K ∈ ℂ
85 15 recnd ⊢ φ → K 2 ∈ ℂ
86 43 recnd ⊢ φ → A ⁢ K − 1 ∈ ℂ
87 84 85 86 subadd23d ⊢ φ → K + 1 ⁢ K − K 2 + A ⁢ K - 1 = K + 1 ⁢ K + A ⁢ K − 1 - K 2
88 71 83 87 3eqtr3d ⊢ φ → A ⁢ K + K - 1 = K + 1 ⁢ K + A ⁢ K − 1 - K 2
89 2cnd ⊢ φ → 2 ∈ ℂ
90 10 recnd ⊢ φ → A ∈ ℂ
91 89 90 45 mulassd ⊢ φ → 2 ⁢ A ⁢ K = 2 ⁢ A ⁢ K
92 67 2timesd ⊢ φ → 2 ⁢ A ⁢ K = A ⁢ K + A ⁢ K
93 91 92 eqtrd ⊢ φ → 2 ⁢ A ⁢ K = A ⁢ K + A ⁢ K
94 93 oveq1d ⊢ φ → 2 ⁢ A ⁢ K − K 2 = A ⁢ K + A ⁢ K - K 2
95 94 oveq1d ⊢ φ → 2 ⁢ A ⁢ K - K 2 - 1 = A ⁢ K + A ⁢ K - K 2 - 1
96 21 21 readdcld ⊢ φ → A ⁢ K + A ⁢ K ∈ ℝ
97 96 recnd ⊢ φ → A ⁢ K + A ⁢ K ∈ ℂ
98 97 85 70 sub32d ⊢ φ → A ⁢ K + A ⁢ K - K 2 - 1 = A ⁢ K + A ⁢ K - 1 - K 2
99 67 67 70 addsubassd ⊢ φ → A ⁢ K + A ⁢ K - 1 = A ⁢ K + A ⁢ K - 1
100 99 oveq1d ⊢ φ → A ⁢ K + A ⁢ K - 1 - K 2 = A ⁢ K + A ⁢ K − 1 - K 2
101 67 86 85 addsubassd ⊢ φ → A ⁢ K + A ⁢ K − 1 - K 2 = A ⁢ K + A ⁢ K − 1 - K 2
102 100 101 eqtrd ⊢ φ → A ⁢ K + A ⁢ K - 1 - K 2 = A ⁢ K + A ⁢ K − 1 - K 2
103 95 98 102 3eqtrd ⊢ φ → 2 ⁢ A ⁢ K - K 2 - 1 = A ⁢ K + A ⁢ K − 1 - K 2
104 66 88 103 3brtr4d ⊢ φ → A ⁢ K + K - 1 ≤ 2 ⁢ A ⁢ K - K 2 - 1
105 10 24 19 38 104 ltletrd ⊢ φ → A < 2 ⁢ A ⁢ K - K 2 - 1
106 8 10 19 20 105 lttrd ⊢ φ → K N < 2 ⁢ A ⁢ K - K 2 - 1