Metamath Proof Explorer

Theorem 2lgslem3a

Description: Lemma for 2lgslem3a1 . (Contributed by AV, 14-Jul-2021)

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

Proof

Step Hyp Ref Expression
1 2lgslem2.n 
 |-  N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )
2 oveq1 
 |-  ( P = ( ( 8 x. K ) + 1 ) -> ( P - 1 ) = ( ( ( 8 x. K ) + 1 ) - 1 ) )
3 2 oveq1d 
 |-  ( P = ( ( 8 x. K ) + 1 ) -> ( ( P - 1 ) / 2 ) = ( ( ( ( 8 x. K ) + 1 ) - 1 ) / 2 ) )
4 fvoveq1 
 |-  ( P = ( ( 8 x. K ) + 1 ) -> ( |_ ` ( P / 4 ) ) = ( |_ ` ( ( ( 8 x. K ) + 1 ) / 4 ) ) )
5 3 4 oveq12d 
 |-  ( P = ( ( 8 x. K ) + 1 ) -> ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) = ( ( ( ( ( 8 x. K ) + 1 ) - 1 ) / 2 ) - ( |_ ` ( ( ( 8 x. K ) + 1 ) / 4 ) ) ) )
6 1 5 eqtrid 
 |-  ( P = ( ( 8 x. K ) + 1 ) -> N = ( ( ( ( ( 8 x. K ) + 1 ) - 1 ) / 2 ) - ( |_ ` ( ( ( 8 x. K ) + 1 ) / 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 pncan1 
 |-  ( ( 8 x. K ) e. CC -> ( ( ( 8 x. K ) + 1 ) - 1 ) = ( 8 x. K ) )
13 11 12 syl 
 |-  ( K e. NN0 -> ( ( ( 8 x. K ) + 1 ) - 1 ) = ( 8 x. K ) )
14 13 oveq1d 
 |-  ( K e. NN0 -> ( ( ( ( 8 x. K ) + 1 ) - 1 ) / 2 ) = ( ( 8 x. K ) / 2 ) )
15 4cn 
 |-  4 e. CC
16 2cn 
 |-  2 e. CC
17 4t2e8 
 |-  ( 4 x. 2 ) = 8
18 15 16 17 mulcomli 
 |-  ( 2 x. 4 ) = 8
19 18 eqcomi 
 |-  8 = ( 2 x. 4 )
20 19 a1i 
 |-  ( K e. NN0 -> 8 = ( 2 x. 4 ) )
21 20 oveq1d 
 |-  ( K e. NN0 -> ( 8 x. K ) = ( ( 2 x. 4 ) x. K ) )
22 16 a1i 
 |-  ( K e. NN0 -> 2 e. CC )
23 15 a1i 
 |-  ( K e. NN0 -> 4 e. CC )
24 nn0cn 
 |-  ( K e. NN0 -> K e. CC )
25 22 23 24 mulassd 
 |-  ( K e. NN0 -> ( ( 2 x. 4 ) x. K ) = ( 2 x. ( 4 x. K ) ) )
26 21 25 eqtrd 
 |-  ( K e. NN0 -> ( 8 x. K ) = ( 2 x. ( 4 x. K ) ) )
27 26 oveq1d 
 |-  ( K e. NN0 -> ( ( 8 x. K ) / 2 ) = ( ( 2 x. ( 4 x. K ) ) / 2 ) )
28 4nn0 
 |-  4 e. NN0
29 28 a1i 
 |-  ( K e. NN0 -> 4 e. NN0 )
30 29 9 nn0mulcld 
 |-  ( K e. NN0 -> ( 4 x. K ) e. NN0 )
31 30 nn0cnd 
 |-  ( K e. NN0 -> ( 4 x. K ) e. CC )
32 2ne0 
 |-  2 =/= 0
33 32 a1i 
 |-  ( K e. NN0 -> 2 =/= 0 )
34 31 22 33 divcan3d 
 |-  ( K e. NN0 -> ( ( 2 x. ( 4 x. K ) ) / 2 ) = ( 4 x. K ) )
35 14 27 34 3eqtrd 
 |-  ( K e. NN0 -> ( ( ( ( 8 x. K ) + 1 ) - 1 ) / 2 ) = ( 4 x. K ) )
36 1cnd 
 |-  ( K e. NN0 -> 1 e. CC )
37 4ne0 
 |-  4 =/= 0
38 15 37 pm3.2i 
 |-  ( 4 e. CC /\ 4 =/= 0 )
39 38 a1i 
 |-  ( K e. NN0 -> ( 4 e. CC /\ 4 =/= 0 ) )
40 divdir 
 |-  ( ( ( 8 x. K ) e. CC /\ 1 e. CC /\ ( 4 e. CC /\ 4 =/= 0 ) ) -> ( ( ( 8 x. K ) + 1 ) / 4 ) = ( ( ( 8 x. K ) / 4 ) + ( 1 / 4 ) ) )
41 11 36 39 40 syl3anc 
 |-  ( K e. NN0 -> ( ( ( 8 x. K ) + 1 ) / 4 ) = ( ( ( 8 x. K ) / 4 ) + ( 1 / 4 ) ) )
42 8cn 
 |-  8 e. CC
43 42 a1i 
 |-  ( K e. NN0 -> 8 e. CC )
44 div23 
 |-  ( ( 8 e. CC /\ K e. CC /\ ( 4 e. CC /\ 4 =/= 0 ) ) -> ( ( 8 x. K ) / 4 ) = ( ( 8 / 4 ) x. K ) )
45 43 24 39 44 syl3anc 
 |-  ( K e. NN0 -> ( ( 8 x. K ) / 4 ) = ( ( 8 / 4 ) x. K ) )
46 17 eqcomi 
 |-  8 = ( 4 x. 2 )
47 46 oveq1i 
 |-  ( 8 / 4 ) = ( ( 4 x. 2 ) / 4 )
48 16 15 37 divcan3i 
 |-  ( ( 4 x. 2 ) / 4 ) = 2
49 47 48 eqtri 
 |-  ( 8 / 4 ) = 2
50 49 a1i 
 |-  ( K e. NN0 -> ( 8 / 4 ) = 2 )
51 50 oveq1d 
 |-  ( K e. NN0 -> ( ( 8 / 4 ) x. K ) = ( 2 x. K ) )
52 45 51 eqtrd 
 |-  ( K e. NN0 -> ( ( 8 x. K ) / 4 ) = ( 2 x. K ) )
53 52 oveq1d 
 |-  ( K e. NN0 -> ( ( ( 8 x. K ) / 4 ) + ( 1 / 4 ) ) = ( ( 2 x. K ) + ( 1 / 4 ) ) )
54 41 53 eqtrd 
 |-  ( K e. NN0 -> ( ( ( 8 x. K ) + 1 ) / 4 ) = ( ( 2 x. K ) + ( 1 / 4 ) ) )
55 54 fveq2d 
 |-  ( K e. NN0 -> ( |_ ` ( ( ( 8 x. K ) + 1 ) / 4 ) ) = ( |_ ` ( ( 2 x. K ) + ( 1 / 4 ) ) ) )
56 1lt4 
 |-  1 < 4
57 2nn0 
 |-  2 e. NN0
58 57 a1i 
 |-  ( K e. NN0 -> 2 e. NN0 )
59 58 9 nn0mulcld 
 |-  ( K e. NN0 -> ( 2 x. K ) e. NN0 )
60 59 nn0zd 
 |-  ( K e. NN0 -> ( 2 x. K ) e. ZZ )
61 1nn0 
 |-  1 e. NN0
62 61 a1i 
 |-  ( K e. NN0 -> 1 e. NN0 )
63 4nn 
 |-  4 e. NN
64 63 a1i 
 |-  ( K e. NN0 -> 4 e. NN )
65 adddivflid 
 |-  ( ( ( 2 x. K ) e. ZZ /\ 1 e. NN0 /\ 4 e. NN ) -> ( 1 < 4 <-> ( |_ ` ( ( 2 x. K ) + ( 1 / 4 ) ) ) = ( 2 x. K ) ) )
66 60 62 64 65 syl3anc 
 |-  ( K e. NN0 -> ( 1 < 4 <-> ( |_ ` ( ( 2 x. K ) + ( 1 / 4 ) ) ) = ( 2 x. K ) ) )
67 56 66 mpbii 
 |-  ( K e. NN0 -> ( |_ ` ( ( 2 x. K ) + ( 1 / 4 ) ) ) = ( 2 x. K ) )
68 55 67 eqtrd 
 |-  ( K e. NN0 -> ( |_ ` ( ( ( 8 x. K ) + 1 ) / 4 ) ) = ( 2 x. K ) )
69 35 68 oveq12d 
 |-  ( K e. NN0 -> ( ( ( ( ( 8 x. K ) + 1 ) - 1 ) / 2 ) - ( |_ ` ( ( ( 8 x. K ) + 1 ) / 4 ) ) ) = ( ( 4 x. K ) - ( 2 x. K ) ) )
70 2t2e4 
 |-  ( 2 x. 2 ) = 4
71 70 eqcomi 
 |-  4 = ( 2 x. 2 )
72 71 a1i 
 |-  ( K e. NN0 -> 4 = ( 2 x. 2 ) )
73 72 oveq1d 
 |-  ( K e. NN0 -> ( 4 x. K ) = ( ( 2 x. 2 ) x. K ) )
74 22 22 24 mulassd 
 |-  ( K e. NN0 -> ( ( 2 x. 2 ) x. K ) = ( 2 x. ( 2 x. K ) ) )
75 73 74 eqtrd 
 |-  ( K e. NN0 -> ( 4 x. K ) = ( 2 x. ( 2 x. K ) ) )
76 75 oveq1d 
 |-  ( K e. NN0 -> ( ( 4 x. K ) - ( 2 x. K ) ) = ( ( 2 x. ( 2 x. K ) ) - ( 2 x. K ) ) )
77 59 nn0cnd 
 |-  ( K e. NN0 -> ( 2 x. K ) e. CC )
78 2txmxeqx 
 |-  ( ( 2 x. K ) e. CC -> ( ( 2 x. ( 2 x. K ) ) - ( 2 x. K ) ) = ( 2 x. K ) )
79 77 78 syl 
 |-  ( K e. NN0 -> ( ( 2 x. ( 2 x. K ) ) - ( 2 x. K ) ) = ( 2 x. K ) )
80 69 76 79 3eqtrd 
 |-  ( K e. NN0 -> ( ( ( ( ( 8 x. K ) + 1 ) - 1 ) / 2 ) - ( |_ ` ( ( ( 8 x. K ) + 1 ) / 4 ) ) ) = ( 2 x. K ) )
81 6 80 sylan9eqr 
 |-  ( ( K e. NN0 /\ P = ( ( 8 x. K ) + 1 ) ) -> N = ( 2 x. K ) )