Metamath Proof Explorer

Theorem 2lgslem3d

Description: Lemma for 2lgslem3d1 . (Contributed by AV, 16-Jul-2021)

Ref Expression
Hypothesis 2lgslem2.n 
|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )
Assertion 2lgslem3d 
|- ( ( K e. NN0 /\ P = ( ( 8 x. K ) + 7 ) ) -> N = ( ( 2 x. K ) + 2 ) )

Proof

Step Hyp Ref Expression
1 2lgslem2.n 
 |-  N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )
2 oveq1 
 |-  ( P = ( ( 8 x. K ) + 7 ) -> ( P - 1 ) = ( ( ( 8 x. K ) + 7 ) - 1 ) )
3 2 oveq1d 
 |-  ( P = ( ( 8 x. K ) + 7 ) -> ( ( P - 1 ) / 2 ) = ( ( ( ( 8 x. K ) + 7 ) - 1 ) / 2 ) )
4 fvoveq1 
 |-  ( P = ( ( 8 x. K ) + 7 ) -> ( |_ ` ( P / 4 ) ) = ( |_ ` ( ( ( 8 x. K ) + 7 ) / 4 ) ) )
5 3 4 oveq12d 
 |-  ( P = ( ( 8 x. K ) + 7 ) -> ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) = ( ( ( ( ( 8 x. K ) + 7 ) - 1 ) / 2 ) - ( |_ ` ( ( ( 8 x. K ) + 7 ) / 4 ) ) ) )
6 1 5 eqtrid 
 |-  ( P = ( ( 8 x. K ) + 7 ) -> N = ( ( ( ( ( 8 x. K ) + 7 ) - 1 ) / 2 ) - ( |_ ` ( ( ( 8 x. K ) + 7 ) / 4 ) ) ) )
7 8nn0 
 |-  8 e. NN0
8 7 a1i 
 |-  ( K e. NN0 -> 8 e. NN0 )
9 id 
 |-  ( K e. NN0 -> K e. NN0 )
10 8 9 nn0mulcld 
 |-  ( K e. NN0 -> ( 8 x. K ) e. NN0 )
11 10 nn0cnd 
 |-  ( K e. NN0 -> ( 8 x. K ) e. CC )
12 7cn 
 |-  7 e. CC
13 12 a1i 
 |-  ( K e. NN0 -> 7 e. CC )
14 1cnd 
 |-  ( K e. NN0 -> 1 e. CC )
15 11 13 14 addsubassd 
 |-  ( K e. NN0 -> ( ( ( 8 x. K ) + 7 ) - 1 ) = ( ( 8 x. K ) + ( 7 - 1 ) ) )
16 4t2e8 
 |-  ( 4 x. 2 ) = 8
17 16 eqcomi 
 |-  8 = ( 4 x. 2 )
18 17 a1i 
 |-  ( K e. NN0 -> 8 = ( 4 x. 2 ) )
19 18 oveq1d 
 |-  ( K e. NN0 -> ( 8 x. K ) = ( ( 4 x. 2 ) x. K ) )
20 4cn 
 |-  4 e. CC
21 20 a1i 
 |-  ( K e. NN0 -> 4 e. CC )
22 2cn 
 |-  2 e. CC
23 22 a1i 
 |-  ( K e. NN0 -> 2 e. CC )
24 nn0cn 
 |-  ( K e. NN0 -> K e. CC )
25 21 23 24 mul32d 
 |-  ( K e. NN0 -> ( ( 4 x. 2 ) x. K ) = ( ( 4 x. K ) x. 2 ) )
26 19 25 eqtrd 
 |-  ( K e. NN0 -> ( 8 x. K ) = ( ( 4 x. K ) x. 2 ) )
27 7m1e6 
 |-  ( 7 - 1 ) = 6
28 27 a1i 
 |-  ( K e. NN0 -> ( 7 - 1 ) = 6 )
29 26 28 oveq12d 
 |-  ( K e. NN0 -> ( ( 8 x. K ) + ( 7 - 1 ) ) = ( ( ( 4 x. K ) x. 2 ) + 6 ) )
30 15 29 eqtrd 
 |-  ( K e. NN0 -> ( ( ( 8 x. K ) + 7 ) - 1 ) = ( ( ( 4 x. K ) x. 2 ) + 6 ) )
31 30 oveq1d 
 |-  ( K e. NN0 -> ( ( ( ( 8 x. K ) + 7 ) - 1 ) / 2 ) = ( ( ( ( 4 x. K ) x. 2 ) + 6 ) / 2 ) )
32 4nn0 
 |-  4 e. NN0
33 32 a1i 
 |-  ( K e. NN0 -> 4 e. NN0 )
34 33 9 nn0mulcld 
 |-  ( K e. NN0 -> ( 4 x. K ) e. NN0 )
35 34 nn0cnd 
 |-  ( K e. NN0 -> ( 4 x. K ) e. CC )
36 35 23 mulcld 
 |-  ( K e. NN0 -> ( ( 4 x. K ) x. 2 ) e. CC )
37 6cn 
 |-  6 e. CC
38 37 a1i 
 |-  ( K e. NN0 -> 6 e. CC )
39 2rp 
 |-  2 e. RR+
40 39 a1i 
 |-  ( K e. NN0 -> 2 e. RR+ )
41 40 rpcnne0d 
 |-  ( K e. NN0 -> ( 2 e. CC /\ 2 =/= 0 ) )
42 divdir 
 |-  ( ( ( ( 4 x. K ) x. 2 ) e. CC /\ 6 e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( ( ( 4 x. K ) x. 2 ) + 6 ) / 2 ) = ( ( ( ( 4 x. K ) x. 2 ) / 2 ) + ( 6 / 2 ) ) )
43 36 38 41 42 syl3anc 
 |-  ( K e. NN0 -> ( ( ( ( 4 x. K ) x. 2 ) + 6 ) / 2 ) = ( ( ( ( 4 x. K ) x. 2 ) / 2 ) + ( 6 / 2 ) ) )
44 2ne0 
 |-  2 =/= 0
45 44 a1i 
 |-  ( K e. NN0 -> 2 =/= 0 )
46 35 23 45 divcan4d 
 |-  ( K e. NN0 -> ( ( ( 4 x. K ) x. 2 ) / 2 ) = ( 4 x. K ) )
47 3t2e6 
 |-  ( 3 x. 2 ) = 6
48 47 eqcomi 
 |-  6 = ( 3 x. 2 )
49 48 oveq1i 
 |-  ( 6 / 2 ) = ( ( 3 x. 2 ) / 2 )
50 3cn 
 |-  3 e. CC
51 50 22 44 divcan4i 
 |-  ( ( 3 x. 2 ) / 2 ) = 3
52 49 51 eqtri 
 |-  ( 6 / 2 ) = 3
53 52 a1i 
 |-  ( K e. NN0 -> ( 6 / 2 ) = 3 )
54 46 53 oveq12d 
 |-  ( K e. NN0 -> ( ( ( ( 4 x. K ) x. 2 ) / 2 ) + ( 6 / 2 ) ) = ( ( 4 x. K ) + 3 ) )
55 31 43 54 3eqtrd 
 |-  ( K e. NN0 -> ( ( ( ( 8 x. K ) + 7 ) - 1 ) / 2 ) = ( ( 4 x. K ) + 3 ) )
56 4ne0 
 |-  4 =/= 0
57 20 56 pm3.2i 
 |-  ( 4 e. CC /\ 4 =/= 0 )
58 57 a1i 
 |-  ( K e. NN0 -> ( 4 e. CC /\ 4 =/= 0 ) )
59 divdir 
 |-  ( ( ( 8 x. K ) e. CC /\ 7 e. CC /\ ( 4 e. CC /\ 4 =/= 0 ) ) -> ( ( ( 8 x. K ) + 7 ) / 4 ) = ( ( ( 8 x. K ) / 4 ) + ( 7 / 4 ) ) )
60 11 13 58 59 syl3anc 
 |-  ( K e. NN0 -> ( ( ( 8 x. K ) + 7 ) / 4 ) = ( ( ( 8 x. K ) / 4 ) + ( 7 / 4 ) ) )
61 8cn 
 |-  8 e. CC
62 61 a1i 
 |-  ( K e. NN0 -> 8 e. CC )
63 div23 
 |-  ( ( 8 e. CC /\ K e. CC /\ ( 4 e. CC /\ 4 =/= 0 ) ) -> ( ( 8 x. K ) / 4 ) = ( ( 8 / 4 ) x. K ) )
64 62 24 58 63 syl3anc 
 |-  ( K e. NN0 -> ( ( 8 x. K ) / 4 ) = ( ( 8 / 4 ) x. K ) )
65 17 oveq1i 
 |-  ( 8 / 4 ) = ( ( 4 x. 2 ) / 4 )
66 22 20 56 divcan3i 
 |-  ( ( 4 x. 2 ) / 4 ) = 2
67 65 66 eqtri 
 |-  ( 8 / 4 ) = 2
68 67 a1i 
 |-  ( K e. NN0 -> ( 8 / 4 ) = 2 )
69 68 oveq1d 
 |-  ( K e. NN0 -> ( ( 8 / 4 ) x. K ) = ( 2 x. K ) )
70 64 69 eqtrd 
 |-  ( K e. NN0 -> ( ( 8 x. K ) / 4 ) = ( 2 x. K ) )
71 70 oveq1d 
 |-  ( K e. NN0 -> ( ( ( 8 x. K ) / 4 ) + ( 7 / 4 ) ) = ( ( 2 x. K ) + ( 7 / 4 ) ) )
72 60 71 eqtrd 
 |-  ( K e. NN0 -> ( ( ( 8 x. K ) + 7 ) / 4 ) = ( ( 2 x. K ) + ( 7 / 4 ) ) )
73 72 fveq2d 
 |-  ( K e. NN0 -> ( |_ ` ( ( ( 8 x. K ) + 7 ) / 4 ) ) = ( |_ ` ( ( 2 x. K ) + ( 7 / 4 ) ) ) )
74 3lt4 
 |-  3 < 4
75 2nn0 
 |-  2 e. NN0
76 75 a1i 
 |-  ( K e. NN0 -> 2 e. NN0 )
77 76 9 nn0mulcld 
 |-  ( K e. NN0 -> ( 2 x. K ) e. NN0 )
78 77 nn0zd 
 |-  ( K e. NN0 -> ( 2 x. K ) e. ZZ )
79 78 peano2zd 
 |-  ( K e. NN0 -> ( ( 2 x. K ) + 1 ) e. ZZ )
80 3nn0 
 |-  3 e. NN0
81 80 a1i 
 |-  ( K e. NN0 -> 3 e. NN0 )
82 4nn 
 |-  4 e. NN
83 82 a1i 
 |-  ( K e. NN0 -> 4 e. NN )
84 adddivflid 
 |-  ( ( ( ( 2 x. K ) + 1 ) e. ZZ /\ 3 e. NN0 /\ 4 e. NN ) -> ( 3 < 4 <-> ( |_ ` ( ( ( 2 x. K ) + 1 ) + ( 3 / 4 ) ) ) = ( ( 2 x. K ) + 1 ) ) )
85 79 81 83 84 syl3anc 
 |-  ( K e. NN0 -> ( 3 < 4 <-> ( |_ ` ( ( ( 2 x. K ) + 1 ) + ( 3 / 4 ) ) ) = ( ( 2 x. K ) + 1 ) ) )
86 23 24 mulcld 
 |-  ( K e. NN0 -> ( 2 x. K ) e. CC )
87 50 a1i 
 |-  ( K e. NN0 -> 3 e. CC )
88 56 a1i 
 |-  ( K e. NN0 -> 4 =/= 0 )
89 87 21 88 divcld 
 |-  ( K e. NN0 -> ( 3 / 4 ) e. CC )
90 86 14 89 addassd 
 |-  ( K e. NN0 -> ( ( ( 2 x. K ) + 1 ) + ( 3 / 4 ) ) = ( ( 2 x. K ) + ( 1 + ( 3 / 4 ) ) ) )
91 4p3e7 
 |-  ( 4 + 3 ) = 7
92 91 eqcomi 
 |-  7 = ( 4 + 3 )
93 92 oveq1i 
 |-  ( 7 / 4 ) = ( ( 4 + 3 ) / 4 )
94 20 50 20 56 divdiri 
 |-  ( ( 4 + 3 ) / 4 ) = ( ( 4 / 4 ) + ( 3 / 4 ) )
95 20 56 dividi 
 |-  ( 4 / 4 ) = 1
96 95 oveq1i 
 |-  ( ( 4 / 4 ) + ( 3 / 4 ) ) = ( 1 + ( 3 / 4 ) )
97 93 94 96 3eqtri 
 |-  ( 7 / 4 ) = ( 1 + ( 3 / 4 ) )
98 97 a1i 
 |-  ( K e. NN0 -> ( 7 / 4 ) = ( 1 + ( 3 / 4 ) ) )
99 98 eqcomd 
 |-  ( K e. NN0 -> ( 1 + ( 3 / 4 ) ) = ( 7 / 4 ) )
100 99 oveq2d 
 |-  ( K e. NN0 -> ( ( 2 x. K ) + ( 1 + ( 3 / 4 ) ) ) = ( ( 2 x. K ) + ( 7 / 4 ) ) )
101 90 100 eqtrd 
 |-  ( K e. NN0 -> ( ( ( 2 x. K ) + 1 ) + ( 3 / 4 ) ) = ( ( 2 x. K ) + ( 7 / 4 ) ) )
102 101 fveqeq2d 
 |-  ( K e. NN0 -> ( ( |_ ` ( ( ( 2 x. K ) + 1 ) + ( 3 / 4 ) ) ) = ( ( 2 x. K ) + 1 ) <-> ( |_ ` ( ( 2 x. K ) + ( 7 / 4 ) ) ) = ( ( 2 x. K ) + 1 ) ) )
103 85 102 bitrd 
 |-  ( K e. NN0 -> ( 3 < 4 <-> ( |_ ` ( ( 2 x. K ) + ( 7 / 4 ) ) ) = ( ( 2 x. K ) + 1 ) ) )
104 74 103 mpbii 
 |-  ( K e. NN0 -> ( |_ ` ( ( 2 x. K ) + ( 7 / 4 ) ) ) = ( ( 2 x. K ) + 1 ) )
105 73 104 eqtrd 
 |-  ( K e. NN0 -> ( |_ ` ( ( ( 8 x. K ) + 7 ) / 4 ) ) = ( ( 2 x. K ) + 1 ) )
106 55 105 oveq12d 
 |-  ( K e. NN0 -> ( ( ( ( ( 8 x. K ) + 7 ) - 1 ) / 2 ) - ( |_ ` ( ( ( 8 x. K ) + 7 ) / 4 ) ) ) = ( ( ( 4 x. K ) + 3 ) - ( ( 2 x. K ) + 1 ) ) )
107 77 nn0cnd 
 |-  ( K e. NN0 -> ( 2 x. K ) e. CC )
108 35 87 107 14 addsub4d 
 |-  ( K e. NN0 -> ( ( ( 4 x. K ) + 3 ) - ( ( 2 x. K ) + 1 ) ) = ( ( ( 4 x. K ) - ( 2 x. K ) ) + ( 3 - 1 ) ) )
109 2t2e4 
 |-  ( 2 x. 2 ) = 4
110 109 eqcomi 
 |-  4 = ( 2 x. 2 )
111 110 a1i 
 |-  ( K e. NN0 -> 4 = ( 2 x. 2 ) )
112 111 oveq1d 
 |-  ( K e. NN0 -> ( 4 x. K ) = ( ( 2 x. 2 ) x. K ) )
113 23 23 24 mulassd 
 |-  ( K e. NN0 -> ( ( 2 x. 2 ) x. K ) = ( 2 x. ( 2 x. K ) ) )
114 112 113 eqtrd 
 |-  ( K e. NN0 -> ( 4 x. K ) = ( 2 x. ( 2 x. K ) ) )
115 114 oveq1d 
 |-  ( K e. NN0 -> ( ( 4 x. K ) - ( 2 x. K ) ) = ( ( 2 x. ( 2 x. K ) ) - ( 2 x. K ) ) )
116 2txmxeqx 
 |-  ( ( 2 x. K ) e. CC -> ( ( 2 x. ( 2 x. K ) ) - ( 2 x. K ) ) = ( 2 x. K ) )
117 107 116 syl 
 |-  ( K e. NN0 -> ( ( 2 x. ( 2 x. K ) ) - ( 2 x. K ) ) = ( 2 x. K ) )
118 115 117 eqtrd 
 |-  ( K e. NN0 -> ( ( 4 x. K ) - ( 2 x. K ) ) = ( 2 x. K ) )
119 3m1e2 
 |-  ( 3 - 1 ) = 2
120 119 a1i 
 |-  ( K e. NN0 -> ( 3 - 1 ) = 2 )
121 118 120 oveq12d 
 |-  ( K e. NN0 -> ( ( ( 4 x. K ) - ( 2 x. K ) ) + ( 3 - 1 ) ) = ( ( 2 x. K ) + 2 ) )
122 106 108 121 3eqtrd 
 |-  ( K e. NN0 -> ( ( ( ( ( 8 x. K ) + 7 ) - 1 ) / 2 ) - ( |_ ` ( ( ( 8 x. K ) + 7 ) / 4 ) ) ) = ( ( 2 x. K ) + 2 ) )
123 6 122 sylan9eqr 
 |-  ( ( K e. NN0 /\ P = ( ( 8 x. K ) + 7 ) ) -> N = ( ( 2 x. K ) + 2 ) )