Metamath Proof Explorer

Theorem 2lgslem3c

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

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

Proof

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