Proof of Theorem 2lgsoddprmlem3d
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 6cn 12358 | . . 3
⊢ 6 ∈
ℂ | 
| 2 |  | 8cn 12364 | . . 3
⊢ 8 ∈
ℂ | 
| 3 |  | 0re 11264 | . . . 4
⊢ 0 ∈
ℝ | 
| 4 |  | 8pos 12379 | . . . 4
⊢ 0 <
8 | 
| 5 | 3, 4 | gtneii 11374 | . . 3
⊢ 8 ≠
0 | 
| 6 | 1, 2, 5 | divcan4i 12015 | . 2
⊢ ((6
· 8) / 8) = 6 | 
| 7 | 1, 2 | mulcli 11269 | . . . 4
⊢ (6
· 8) ∈ ℂ | 
| 8 |  | ax-1cn 11214 | . . . 4
⊢ 1 ∈
ℂ | 
| 9 |  | 4p3e7 12421 | . . . . . . 7
⊢ (4 + 3) =
7 | 
| 10 | 9 | eqcomi 2745 | . . . . . 6
⊢ 7 = (4 +
3) | 
| 11 | 10 | oveq1i 7442 | . . . . 5
⊢
(7↑2) = ((4 + 3)↑2) | 
| 12 |  | 4cn 12352 | . . . . . . 7
⊢ 4 ∈
ℂ | 
| 13 |  | 3cn 12348 | . . . . . . 7
⊢ 3 ∈
ℂ | 
| 14 | 12, 13 | binom2i 14252 | . . . . . 6
⊢ ((4 +
3)↑2) = (((4↑2) + (2 · (4 · 3))) +
(3↑2)) | 
| 15 |  | sq4e2t8 14239 | . . . . . . . . . 10
⊢
(4↑2) = (2 · 8) | 
| 16 |  | 2cn 12342 | . . . . . . . . . . . . 13
⊢ 2 ∈
ℂ | 
| 17 |  | 4t2e8 12435 | . . . . . . . . . . . . 13
⊢ (4
· 2) = 8 | 
| 18 | 12, 16, 17 | mulcomli 11271 | . . . . . . . . . . . 12
⊢ (2
· 4) = 8 | 
| 19 | 18 | oveq1i 7442 | . . . . . . . . . . 11
⊢ ((2
· 4) · 3) = (8 · 3) | 
| 20 | 16, 12, 13 | mulassi 11273 | . . . . . . . . . . 11
⊢ ((2
· 4) · 3) = (2 · (4 · 3)) | 
| 21 | 2, 13 | mulcomi 11270 | . . . . . . . . . . 11
⊢ (8
· 3) = (3 · 8) | 
| 22 | 19, 20, 21 | 3eqtr3i 2772 | . . . . . . . . . 10
⊢ (2
· (4 · 3)) = (3 · 8) | 
| 23 | 15, 22 | oveq12i 7444 | . . . . . . . . 9
⊢
((4↑2) + (2 · (4 · 3))) = ((2 · 8) + (3
· 8)) | 
| 24 | 16, 13, 2 | adddiri 11275 | . . . . . . . . 9
⊢ ((2 + 3)
· 8) = ((2 · 8) + (3 · 8)) | 
| 25 |  | 3p2e5 12418 | . . . . . . . . . . 11
⊢ (3 + 2) =
5 | 
| 26 | 13, 16, 25 | addcomli 11454 | . . . . . . . . . 10
⊢ (2 + 3) =
5 | 
| 27 | 26 | oveq1i 7442 | . . . . . . . . 9
⊢ ((2 + 3)
· 8) = (5 · 8) | 
| 28 | 23, 24, 27 | 3eqtr2i 2770 | . . . . . . . 8
⊢
((4↑2) + (2 · (4 · 3))) = (5 ·
8) | 
| 29 |  | sq3 14238 | . . . . . . . . 9
⊢
(3↑2) = 9 | 
| 30 |  | df-9 12337 | . . . . . . . . 9
⊢ 9 = (8 +
1) | 
| 31 | 29, 30 | eqtri 2764 | . . . . . . . 8
⊢
(3↑2) = (8 + 1) | 
| 32 | 28, 31 | oveq12i 7444 | . . . . . . 7
⊢
(((4↑2) + (2 · (4 · 3))) + (3↑2)) = ((5 ·
8) + (8 + 1)) | 
| 33 |  | 5cn 12355 | . . . . . . . . 9
⊢ 5 ∈
ℂ | 
| 34 | 33, 2 | mulcli 11269 | . . . . . . . 8
⊢ (5
· 8) ∈ ℂ | 
| 35 | 34, 2, 8 | addassi 11272 | . . . . . . 7
⊢ (((5
· 8) + 8) + 1) = ((5 · 8) + (8 + 1)) | 
| 36 |  | df-6 12334 | . . . . . . . . . . 11
⊢ 6 = (5 +
1) | 
| 37 | 36 | oveq1i 7442 | . . . . . . . . . 10
⊢ (6
· 8) = ((5 + 1) · 8) | 
| 38 | 33 | a1i 11 | . . . . . . . . . . . 12
⊢ (8 ∈
ℂ → 5 ∈ ℂ) | 
| 39 |  | id 22 | . . . . . . . . . . . 12
⊢ (8 ∈
ℂ → 8 ∈ ℂ) | 
| 40 | 38, 39 | adddirp1d 11288 | . . . . . . . . . . 11
⊢ (8 ∈
ℂ → ((5 + 1) · 8) = ((5 · 8) + 8)) | 
| 41 | 2, 40 | ax-mp 5 | . . . . . . . . . 10
⊢ ((5 + 1)
· 8) = ((5 · 8) + 8) | 
| 42 | 37, 41 | eqtri 2764 | . . . . . . . . 9
⊢ (6
· 8) = ((5 · 8) + 8) | 
| 43 | 42 | eqcomi 2745 | . . . . . . . 8
⊢ ((5
· 8) + 8) = (6 · 8) | 
| 44 | 43 | oveq1i 7442 | . . . . . . 7
⊢ (((5
· 8) + 8) + 1) = ((6 · 8) + 1) | 
| 45 | 32, 35, 44 | 3eqtr2i 2770 | . . . . . 6
⊢
(((4↑2) + (2 · (4 · 3))) + (3↑2)) = ((6 ·
8) + 1) | 
| 46 | 14, 45 | eqtri 2764 | . . . . 5
⊢ ((4 +
3)↑2) = ((6 · 8) + 1) | 
| 47 | 11, 46 | eqtri 2764 | . . . 4
⊢
(7↑2) = ((6 · 8) + 1) | 
| 48 | 7, 8, 47 | mvrraddi 11526 | . . 3
⊢
((7↑2) − 1) = (6 · 8) | 
| 49 | 48 | oveq1i 7442 | . 2
⊢
(((7↑2) − 1) / 8) = ((6 · 8) / 8) | 
| 50 |  | 3t2e6 12433 | . . 3
⊢ (3
· 2) = 6 | 
| 51 | 13, 16, 50 | mulcomli 11271 | . 2
⊢ (2
· 3) = 6 | 
| 52 | 6, 49, 51 | 3eqtr4i 2774 | 1
⊢
(((7↑2) − 1) / 8) = (2 · 3) |