Step | Hyp | Ref
| Expression |
1 | | oveq1 7365 |
. . . . 5
โข (๐ = if(๐ โ โ0, ๐, 1) โ (๐โ(๐ โ 1)) = (if(๐ โ โ0, ๐, 1)โ(๐ โ 1))) |
2 | 1 | oveq2d 7374 |
. . . 4
โข (๐ = if(๐ โ โ0, ๐, 1) โ (((๐ โ 1)โ๐พ) ยท (๐โ(๐ โ 1))) = (((๐ โ 1)โ๐พ) ยท (if(๐ โ โ0, ๐, 1)โ(๐ โ 1)))) |
3 | | id 22 |
. . . . . . 7
โข (๐ = if(๐ โ โ0, ๐, 1) โ ๐ = if(๐ โ โ0, ๐, 1)) |
4 | | oveq1 7365 |
. . . . . . 7
โข (๐ = if(๐ โ โ0, ๐, 1) โ (๐ + ๐พ) = (if(๐ โ โ0, ๐, 1) + ๐พ)) |
5 | 3, 4 | oveq12d 7376 |
. . . . . 6
โข (๐ = if(๐ โ โ0, ๐, 1) โ (๐โ(๐ + ๐พ)) = (if(๐ โ โ0, ๐, 1)โ(if(๐ โ โ0, ๐, 1) + ๐พ))) |
6 | 5 | oveq2d 7374 |
. . . . 5
โข (๐ = if(๐ โ โ0, ๐, 1) โ ((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) = ((2โ(๐พโ2)) ยท (if(๐ โ โ0, ๐, 1)โ(if(๐ โ โ0, ๐, 1) + ๐พ)))) |
7 | 6 | oveq1d 7373 |
. . . 4
โข (๐ = if(๐ โ โ0, ๐, 1) โ (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ(๐ โ 1))) = (((2โ(๐พโ2)) ยท (if(๐ โ โ0, ๐, 1)โ(if(๐ โ โ0, ๐, 1) + ๐พ))) ยท (!โ(๐ โ 1)))) |
8 | 2, 7 | breq12d 5119 |
. . 3
โข (๐ = if(๐ โ โ0, ๐, 1) โ ((((๐ โ 1)โ๐พ) ยท (๐โ(๐ โ 1))) โค (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ(๐ โ 1))) โ (((๐ โ 1)โ๐พ) ยท (if(๐ โ โ0, ๐, 1)โ(๐ โ 1))) โค (((2โ(๐พโ2)) ยท (if(๐ โ โ0,
๐, 1)โ(if(๐ โ โ0,
๐, 1) + ๐พ))) ยท (!โ(๐ โ 1))))) |
9 | | oveq1 7365 |
. . . . 5
โข (๐ = if(๐ โ โ0, ๐, 1) โ (๐โ๐) = (if(๐ โ โ0, ๐, 1)โ๐)) |
10 | 9 | oveq2d 7374 |
. . . 4
โข (๐ = if(๐ โ โ0, ๐, 1) โ ((๐โ(๐พ + 1)) ยท (๐โ๐)) = ((๐โ(๐พ + 1)) ยท (if(๐ โ โ0, ๐, 1)โ๐))) |
11 | | oveq1 7365 |
. . . . . . 7
โข (๐ = if(๐ โ โ0, ๐, 1) โ (๐ + (๐พ + 1)) = (if(๐ โ โ0, ๐, 1) + (๐พ + 1))) |
12 | 3, 11 | oveq12d 7376 |
. . . . . 6
โข (๐ = if(๐ โ โ0, ๐, 1) โ (๐โ(๐ + (๐พ + 1))) = (if(๐ โ โ0, ๐, 1)โ(if(๐ โ โ0, ๐, 1) + (๐พ + 1)))) |
13 | 12 | oveq2d 7374 |
. . . . 5
โข (๐ = if(๐ โ โ0, ๐, 1) โ ((2โ((๐พ + 1)โ2)) ยท (๐โ(๐ + (๐พ + 1)))) = ((2โ((๐พ + 1)โ2)) ยท (if(๐ โ โ0,
๐, 1)โ(if(๐ โ โ0,
๐, 1) + (๐พ + 1))))) |
14 | 13 | oveq1d 7373 |
. . . 4
โข (๐ = if(๐ โ โ0, ๐, 1) โ (((2โ((๐พ + 1)โ2)) ยท (๐โ(๐ + (๐พ + 1)))) ยท (!โ๐)) = (((2โ((๐พ + 1)โ2)) ยท (if(๐ โ โ0,
๐, 1)โ(if(๐ โ โ0,
๐, 1) + (๐พ + 1)))) ยท (!โ๐))) |
15 | 10, 14 | breq12d 5119 |
. . 3
โข (๐ = if(๐ โ โ0, ๐, 1) โ (((๐โ(๐พ + 1)) ยท (๐โ๐)) โค (((2โ((๐พ + 1)โ2)) ยท (๐โ(๐ + (๐พ + 1)))) ยท (!โ๐)) โ ((๐โ(๐พ + 1)) ยท (if(๐ โ โ0, ๐, 1)โ๐)) โค (((2โ((๐พ + 1)โ2)) ยท (if(๐ โ โ0,
๐, 1)โ(if(๐ โ โ0,
๐, 1) + (๐พ + 1)))) ยท (!โ๐)))) |
16 | 8, 15 | imbi12d 345 |
. 2
โข (๐ = if(๐ โ โ0, ๐, 1) โ (((((๐ โ 1)โ๐พ) ยท (๐โ(๐ โ 1))) โค (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ(๐ โ 1))) โ ((๐โ(๐พ + 1)) ยท (๐โ๐)) โค (((2โ((๐พ + 1)โ2)) ยท (๐โ(๐ + (๐พ + 1)))) ยท (!โ๐))) โ ((((๐ โ 1)โ๐พ) ยท (if(๐ โ โ0, ๐, 1)โ(๐ โ 1))) โค (((2โ(๐พโ2)) ยท (if(๐ โ โ0,
๐, 1)โ(if(๐ โ โ0,
๐, 1) + ๐พ))) ยท (!โ(๐ โ 1))) โ ((๐โ(๐พ + 1)) ยท (if(๐ โ โ0, ๐, 1)โ๐)) โค (((2โ((๐พ + 1)โ2)) ยท (if(๐ โ โ0,
๐, 1)โ(if(๐ โ โ0,
๐, 1) + (๐พ + 1)))) ยท (!โ๐))))) |
17 | | oveq2 7366 |
. . . . 5
โข (๐พ = if(๐พ โ โ0, ๐พ, 1) โ ((๐ โ 1)โ๐พ) = ((๐ โ 1)โif(๐พ โ โ0, ๐พ, 1))) |
18 | 17 | oveq1d 7373 |
. . . 4
โข (๐พ = if(๐พ โ โ0, ๐พ, 1) โ (((๐ โ 1)โ๐พ) ยท (if(๐ โ โ0, ๐, 1)โ(๐ โ 1))) = (((๐ โ 1)โif(๐พ โ โ0, ๐พ, 1)) ยท (if(๐ โ โ0,
๐, 1)โ(๐ โ 1)))) |
19 | | oveq1 7365 |
. . . . . . 7
โข (๐พ = if(๐พ โ โ0, ๐พ, 1) โ (๐พโ2) = (if(๐พ โ โ0, ๐พ, 1)โ2)) |
20 | 19 | oveq2d 7374 |
. . . . . 6
โข (๐พ = if(๐พ โ โ0, ๐พ, 1) โ (2โ(๐พโ2)) = (2โ(if(๐พ โ โ0,
๐พ,
1)โ2))) |
21 | | oveq2 7366 |
. . . . . . 7
โข (๐พ = if(๐พ โ โ0, ๐พ, 1) โ (if(๐ โ โ0,
๐, 1) + ๐พ) = (if(๐ โ โ0, ๐, 1) + if(๐พ โ โ0, ๐พ, 1))) |
22 | 21 | oveq2d 7374 |
. . . . . 6
โข (๐พ = if(๐พ โ โ0, ๐พ, 1) โ (if(๐ โ โ0,
๐, 1)โ(if(๐ โ โ0,
๐, 1) + ๐พ)) = (if(๐ โ โ0, ๐, 1)โ(if(๐ โ โ0, ๐, 1) + if(๐พ โ โ0, ๐พ, 1)))) |
23 | 20, 22 | oveq12d 7376 |
. . . . 5
โข (๐พ = if(๐พ โ โ0, ๐พ, 1) โ ((2โ(๐พโ2)) ยท (if(๐ โ โ0,
๐, 1)โ(if(๐ โ โ0,
๐, 1) + ๐พ))) = ((2โ(if(๐พ โ โ0, ๐พ, 1)โ2)) ยท (if(๐ โ โ0,
๐, 1)โ(if(๐ โ โ0,
๐, 1) + if(๐พ โ โ0,
๐พ, 1))))) |
24 | 23 | oveq1d 7373 |
. . . 4
โข (๐พ = if(๐พ โ โ0, ๐พ, 1) โ (((2โ(๐พโ2)) ยท (if(๐ โ โ0,
๐, 1)โ(if(๐ โ โ0,
๐, 1) + ๐พ))) ยท (!โ(๐ โ 1))) = (((2โ(if(๐พ โ โ0,
๐พ, 1)โ2)) ยท
(if(๐ โ
โ0, ๐,
1)โ(if(๐ โ
โ0, ๐, 1)
+ if(๐พ โ
โ0, ๐พ,
1)))) ยท (!โ(๐
โ 1)))) |
25 | 18, 24 | breq12d 5119 |
. . 3
โข (๐พ = if(๐พ โ โ0, ๐พ, 1) โ ((((๐ โ 1)โ๐พ) ยท (if(๐ โ โ0, ๐, 1)โ(๐ โ 1))) โค (((2โ(๐พโ2)) ยท (if(๐ โ โ0,
๐, 1)โ(if(๐ โ โ0,
๐, 1) + ๐พ))) ยท (!โ(๐ โ 1))) โ (((๐ โ 1)โif(๐พ โ โ0, ๐พ, 1)) ยท (if(๐ โ โ0,
๐, 1)โ(๐ โ 1))) โค
(((2โ(if(๐พ โ
โ0, ๐พ,
1)โ2)) ยท (if(๐
โ โ0, ๐, 1)โ(if(๐ โ โ0, ๐, 1) + if(๐พ โ โ0, ๐พ, 1)))) ยท (!โ(๐ โ 1))))) |
26 | | oveq1 7365 |
. . . . . 6
โข (๐พ = if(๐พ โ โ0, ๐พ, 1) โ (๐พ + 1) = (if(๐พ โ โ0, ๐พ, 1) + 1)) |
27 | 26 | oveq2d 7374 |
. . . . 5
โข (๐พ = if(๐พ โ โ0, ๐พ, 1) โ (๐โ(๐พ + 1)) = (๐โ(if(๐พ โ โ0, ๐พ, 1) + 1))) |
28 | 27 | oveq1d 7373 |
. . . 4
โข (๐พ = if(๐พ โ โ0, ๐พ, 1) โ ((๐โ(๐พ + 1)) ยท (if(๐ โ โ0, ๐, 1)โ๐)) = ((๐โ(if(๐พ โ โ0, ๐พ, 1) + 1)) ยท (if(๐ โ โ0,
๐, 1)โ๐))) |
29 | 26 | oveq1d 7373 |
. . . . . . 7
โข (๐พ = if(๐พ โ โ0, ๐พ, 1) โ ((๐พ + 1)โ2) = ((if(๐พ โ โ0, ๐พ, 1) +
1)โ2)) |
30 | 29 | oveq2d 7374 |
. . . . . 6
โข (๐พ = if(๐พ โ โ0, ๐พ, 1) โ (2โ((๐พ + 1)โ2)) =
(2โ((if(๐พ โ
โ0, ๐พ, 1)
+ 1)โ2))) |
31 | 26 | oveq2d 7374 |
. . . . . . 7
โข (๐พ = if(๐พ โ โ0, ๐พ, 1) โ (if(๐ โ โ0,
๐, 1) + (๐พ + 1)) = (if(๐ โ โ0, ๐, 1) + (if(๐พ โ โ0, ๐พ, 1) + 1))) |
32 | 31 | oveq2d 7374 |
. . . . . 6
โข (๐พ = if(๐พ โ โ0, ๐พ, 1) โ (if(๐ โ โ0,
๐, 1)โ(if(๐ โ โ0,
๐, 1) + (๐พ + 1))) = (if(๐ โ โ0, ๐, 1)โ(if(๐ โ โ0, ๐, 1) + (if(๐พ โ โ0, ๐พ, 1) + 1)))) |
33 | 30, 32 | oveq12d 7376 |
. . . . 5
โข (๐พ = if(๐พ โ โ0, ๐พ, 1) โ ((2โ((๐พ + 1)โ2)) ยท
(if(๐ โ
โ0, ๐,
1)โ(if(๐ โ
โ0, ๐, 1)
+ (๐พ + 1)))) =
((2โ((if(๐พ โ
โ0, ๐พ, 1)
+ 1)โ2)) ยท (if(๐ โ โ0, ๐, 1)โ(if(๐ โ โ0, ๐, 1) + (if(๐พ โ โ0, ๐พ, 1) + 1))))) |
34 | 33 | oveq1d 7373 |
. . . 4
โข (๐พ = if(๐พ โ โ0, ๐พ, 1) โ (((2โ((๐พ + 1)โ2)) ยท
(if(๐ โ
โ0, ๐,
1)โ(if(๐ โ
โ0, ๐, 1)
+ (๐พ + 1)))) ยท
(!โ๐)) =
(((2โ((if(๐พ โ
โ0, ๐พ, 1)
+ 1)โ2)) ยท (if(๐ โ โ0, ๐, 1)โ(if(๐ โ โ0, ๐, 1) + (if(๐พ โ โ0, ๐พ, 1) + 1)))) ยท
(!โ๐))) |
35 | 28, 34 | breq12d 5119 |
. . 3
โข (๐พ = if(๐พ โ โ0, ๐พ, 1) โ (((๐โ(๐พ + 1)) ยท (if(๐ โ โ0, ๐, 1)โ๐)) โค (((2โ((๐พ + 1)โ2)) ยท (if(๐ โ โ0,
๐, 1)โ(if(๐ โ โ0,
๐, 1) + (๐พ + 1)))) ยท (!โ๐)) โ ((๐โ(if(๐พ โ โ0, ๐พ, 1) + 1)) ยท (if(๐ โ โ0,
๐, 1)โ๐)) โค (((2โ((if(๐พ โ โ0,
๐พ, 1) + 1)โ2))
ยท (if(๐ โ
โ0, ๐,
1)โ(if(๐ โ
โ0, ๐, 1)
+ (if(๐พ โ
โ0, ๐พ, 1)
+ 1)))) ยท (!โ๐)))) |
36 | 25, 35 | imbi12d 345 |
. 2
โข (๐พ = if(๐พ โ โ0, ๐พ, 1) โ (((((๐ โ 1)โ๐พ) ยท (if(๐ โ โ0, ๐, 1)โ(๐ โ 1))) โค (((2โ(๐พโ2)) ยท (if(๐ โ โ0,
๐, 1)โ(if(๐ โ โ0,
๐, 1) + ๐พ))) ยท (!โ(๐ โ 1))) โ ((๐โ(๐พ + 1)) ยท (if(๐ โ โ0, ๐, 1)โ๐)) โค (((2โ((๐พ + 1)โ2)) ยท (if(๐ โ โ0,
๐, 1)โ(if(๐ โ โ0,
๐, 1) + (๐พ + 1)))) ยท (!โ๐))) โ ((((๐ โ 1)โif(๐พ โ โ0, ๐พ, 1)) ยท (if(๐ โ โ0,
๐, 1)โ(๐ โ 1))) โค
(((2โ(if(๐พ โ
โ0, ๐พ,
1)โ2)) ยท (if(๐
โ โ0, ๐, 1)โ(if(๐ โ โ0, ๐, 1) + if(๐พ โ โ0, ๐พ, 1)))) ยท (!โ(๐ โ 1))) โ ((๐โ(if(๐พ โ โ0, ๐พ, 1) + 1)) ยท (if(๐ โ โ0,
๐, 1)โ๐)) โค (((2โ((if(๐พ โ โ0,
๐พ, 1) + 1)โ2))
ยท (if(๐ โ
โ0, ๐,
1)โ(if(๐ โ
โ0, ๐, 1)
+ (if(๐พ โ
โ0, ๐พ, 1)
+ 1)))) ยท (!โ๐))))) |
37 | | oveq1 7365 |
. . . . . 6
โข (๐ = if(๐ โ โ, ๐, 1) โ (๐ โ 1) = (if(๐ โ โ, ๐, 1) โ 1)) |
38 | 37 | oveq1d 7373 |
. . . . 5
โข (๐ = if(๐ โ โ, ๐, 1) โ ((๐ โ 1)โif(๐พ โ โ0, ๐พ, 1)) = ((if(๐ โ โ, ๐, 1) โ 1)โif(๐พ โ โ0, ๐พ, 1))) |
39 | 37 | oveq2d 7374 |
. . . . 5
โข (๐ = if(๐ โ โ, ๐, 1) โ (if(๐ โ โ0, ๐, 1)โ(๐ โ 1)) = (if(๐ โ โ0, ๐, 1)โ(if(๐ โ โ, ๐, 1) โ 1))) |
40 | 38, 39 | oveq12d 7376 |
. . . 4
โข (๐ = if(๐ โ โ, ๐, 1) โ (((๐ โ 1)โif(๐พ โ โ0, ๐พ, 1)) ยท (if(๐ โ โ0,
๐, 1)โ(๐ โ 1))) = (((if(๐ โ โ, ๐, 1) โ 1)โif(๐พ โ โ0,
๐พ, 1)) ยท (if(๐ โ โ0,
๐, 1)โ(if(๐ โ โ, ๐, 1) โ
1)))) |
41 | | fvoveq1 7381 |
. . . . 5
โข (๐ = if(๐ โ โ, ๐, 1) โ (!โ(๐ โ 1)) = (!โ(if(๐ โ โ, ๐, 1) โ
1))) |
42 | 41 | oveq2d 7374 |
. . . 4
โข (๐ = if(๐ โ โ, ๐, 1) โ (((2โ(if(๐พ โ โ0, ๐พ, 1)โ2)) ยท (if(๐ โ โ0,
๐, 1)โ(if(๐ โ โ0,
๐, 1) + if(๐พ โ โ0,
๐พ, 1)))) ยท
(!โ(๐ โ 1))) =
(((2โ(if(๐พ โ
โ0, ๐พ,
1)โ2)) ยท (if(๐
โ โ0, ๐, 1)โ(if(๐ โ โ0, ๐, 1) + if(๐พ โ โ0, ๐พ, 1)))) ยท
(!โ(if(๐ โ
โ, ๐, 1) โ
1)))) |
43 | 40, 42 | breq12d 5119 |
. . 3
โข (๐ = if(๐ โ โ, ๐, 1) โ ((((๐ โ 1)โif(๐พ โ โ0, ๐พ, 1)) ยท (if(๐ โ โ0,
๐, 1)โ(๐ โ 1))) โค
(((2โ(if(๐พ โ
โ0, ๐พ,
1)โ2)) ยท (if(๐
โ โ0, ๐, 1)โ(if(๐ โ โ0, ๐, 1) + if(๐พ โ โ0, ๐พ, 1)))) ยท (!โ(๐ โ 1))) โ (((if(๐ โ โ, ๐, 1) โ 1)โif(๐พ โ โ0,
๐พ, 1)) ยท (if(๐ โ โ0,
๐, 1)โ(if(๐ โ โ, ๐, 1) โ 1))) โค
(((2โ(if(๐พ โ
โ0, ๐พ,
1)โ2)) ยท (if(๐
โ โ0, ๐, 1)โ(if(๐ โ โ0, ๐, 1) + if(๐พ โ โ0, ๐พ, 1)))) ยท
(!โ(if(๐ โ
โ, ๐, 1) โ
1))))) |
44 | | oveq1 7365 |
. . . . 5
โข (๐ = if(๐ โ โ, ๐, 1) โ (๐โ(if(๐พ โ โ0, ๐พ, 1) + 1)) = (if(๐ โ โ, ๐, 1)โ(if(๐พ โ โ0, ๐พ, 1) + 1))) |
45 | | oveq2 7366 |
. . . . 5
โข (๐ = if(๐ โ โ, ๐, 1) โ (if(๐ โ โ0, ๐, 1)โ๐) = (if(๐ โ โ0, ๐, 1)โif(๐ โ โ, ๐, 1))) |
46 | 44, 45 | oveq12d 7376 |
. . . 4
โข (๐ = if(๐ โ โ, ๐, 1) โ ((๐โ(if(๐พ โ โ0, ๐พ, 1) + 1)) ยท (if(๐ โ โ0,
๐, 1)โ๐)) = ((if(๐ โ โ, ๐, 1)โ(if(๐พ โ โ0, ๐พ, 1) + 1)) ยท (if(๐ โ โ0,
๐, 1)โif(๐ โ โ, ๐, 1)))) |
47 | | fveq2 6843 |
. . . . 5
โข (๐ = if(๐ โ โ, ๐, 1) โ (!โ๐) = (!โif(๐ โ โ, ๐, 1))) |
48 | 47 | oveq2d 7374 |
. . . 4
โข (๐ = if(๐ โ โ, ๐, 1) โ (((2โ((if(๐พ โ โ0, ๐พ, 1) + 1)โ2)) ยท
(if(๐ โ
โ0, ๐,
1)โ(if(๐ โ
โ0, ๐, 1)
+ (if(๐พ โ
โ0, ๐พ, 1)
+ 1)))) ยท (!โ๐)) = (((2โ((if(๐พ โ โ0, ๐พ, 1) + 1)โ2)) ยท
(if(๐ โ
โ0, ๐,
1)โ(if(๐ โ
โ0, ๐, 1)
+ (if(๐พ โ
โ0, ๐พ, 1)
+ 1)))) ยท (!โif(๐ โ โ, ๐, 1)))) |
49 | 46, 48 | breq12d 5119 |
. . 3
โข (๐ = if(๐ โ โ, ๐, 1) โ (((๐โ(if(๐พ โ โ0, ๐พ, 1) + 1)) ยท (if(๐ โ โ0,
๐, 1)โ๐)) โค (((2โ((if(๐พ โ โ0,
๐พ, 1) + 1)โ2))
ยท (if(๐ โ
โ0, ๐,
1)โ(if(๐ โ
โ0, ๐, 1)
+ (if(๐พ โ
โ0, ๐พ, 1)
+ 1)))) ยท (!โ๐)) โ ((if(๐ โ โ, ๐, 1)โ(if(๐พ โ โ0, ๐พ, 1) + 1)) ยท (if(๐ โ โ0,
๐, 1)โif(๐ โ โ, ๐, 1))) โค (((2โ((if(๐พ โ โ0,
๐พ, 1) + 1)โ2))
ยท (if(๐ โ
โ0, ๐,
1)โ(if(๐ โ
โ0, ๐, 1)
+ (if(๐พ โ
โ0, ๐พ, 1)
+ 1)))) ยท (!โif(๐ โ โ, ๐, 1))))) |
50 | 43, 49 | imbi12d 345 |
. 2
โข (๐ = if(๐ โ โ, ๐, 1) โ (((((๐ โ 1)โif(๐พ โ โ0, ๐พ, 1)) ยท (if(๐ โ โ0,
๐, 1)โ(๐ โ 1))) โค
(((2โ(if(๐พ โ
โ0, ๐พ,
1)โ2)) ยท (if(๐
โ โ0, ๐, 1)โ(if(๐ โ โ0, ๐, 1) + if(๐พ โ โ0, ๐พ, 1)))) ยท (!โ(๐ โ 1))) โ ((๐โ(if(๐พ โ โ0, ๐พ, 1) + 1)) ยท (if(๐ โ โ0,
๐, 1)โ๐)) โค (((2โ((if(๐พ โ โ0,
๐พ, 1) + 1)โ2))
ยท (if(๐ โ
โ0, ๐,
1)โ(if(๐ โ
โ0, ๐, 1)
+ (if(๐พ โ
โ0, ๐พ, 1)
+ 1)))) ยท (!โ๐))) โ ((((if(๐ โ โ, ๐, 1) โ 1)โif(๐พ โ โ0, ๐พ, 1)) ยท (if(๐ โ โ0,
๐, 1)โ(if(๐ โ โ, ๐, 1) โ 1))) โค
(((2โ(if(๐พ โ
โ0, ๐พ,
1)โ2)) ยท (if(๐
โ โ0, ๐, 1)โ(if(๐ โ โ0, ๐, 1) + if(๐พ โ โ0, ๐พ, 1)))) ยท
(!โ(if(๐ โ
โ, ๐, 1) โ 1)))
โ ((if(๐ โ
โ, ๐,
1)โ(if(๐พ โ
โ0, ๐พ, 1)
+ 1)) ยท (if(๐ โ
โ0, ๐,
1)โif(๐ โ
โ, ๐, 1))) โค
(((2โ((if(๐พ โ
โ0, ๐พ, 1)
+ 1)โ2)) ยท (if(๐ โ โ0, ๐, 1)โ(if(๐ โ โ0, ๐, 1) + (if(๐พ โ โ0, ๐พ, 1) + 1)))) ยท
(!โif(๐ โ
โ, ๐,
1)))))) |
51 | | 1nn 12169 |
. . . 4
โข 1 โ
โ |
52 | 51 | elimel 4556 |
. . 3
โข if(๐ โ โ, ๐, 1) โ
โ |
53 | | 1nn0 12434 |
. . . 4
โข 1 โ
โ0 |
54 | 53 | elimel 4556 |
. . 3
โข if(๐พ โ โ0,
๐พ, 1) โ
โ0 |
55 | 53 | elimel 4556 |
. . 3
โข if(๐ โ โ0,
๐, 1) โ
โ0 |
56 | 52, 54, 55 | faclbnd4lem1 14199 |
. 2
โข
((((if(๐ โ
โ, ๐, 1) โ
1)โif(๐พ โ
โ0, ๐พ, 1))
ยท (if(๐ โ
โ0, ๐,
1)โ(if(๐ โ
โ, ๐, 1) โ 1)))
โค (((2โ(if(๐พ โ
โ0, ๐พ,
1)โ2)) ยท (if(๐
โ โ0, ๐, 1)โ(if(๐ โ โ0, ๐, 1) + if(๐พ โ โ0, ๐พ, 1)))) ยท
(!โ(if(๐ โ
โ, ๐, 1) โ 1)))
โ ((if(๐ โ
โ, ๐,
1)โ(if(๐พ โ
โ0, ๐พ, 1)
+ 1)) ยท (if(๐ โ
โ0, ๐,
1)โif(๐ โ
โ, ๐, 1))) โค
(((2โ((if(๐พ โ
โ0, ๐พ, 1)
+ 1)โ2)) ยท (if(๐ โ โ0, ๐, 1)โ(if(๐ โ โ0, ๐, 1) + (if(๐พ โ โ0, ๐พ, 1) + 1)))) ยท
(!โif(๐ โ
โ, ๐,
1)))) |
57 | 16, 36, 50, 56 | dedth3h 4547 |
1
โข ((๐ โ โ0
โง ๐พ โ
โ0 โง ๐
โ โ) โ ((((๐ โ 1)โ๐พ) ยท (๐โ(๐ โ 1))) โค (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ(๐ โ 1))) โ ((๐โ(๐พ + 1)) ยท (๐โ๐)) โค (((2โ((๐พ + 1)โ2)) ยท (๐โ(๐ + (๐พ + 1)))) ยท (!โ๐)))) |