Step | Hyp | Ref
| Expression |
1 | | sadcp1.n |
. 2
β’ (π β π β
β0) |
2 | | fveq2 6843 |
. . . . . 6
β’ (π₯ = 0 β (πΆβπ₯) = (πΆβ0)) |
3 | 2 | eleq2d 2820 |
. . . . 5
β’ (π₯ = 0 β (β
β
(πΆβπ₯) β β
β (πΆβ0))) |
4 | | oveq2 7366 |
. . . . . . 7
β’ (π₯ = 0 β (2βπ₯) = (2β0)) |
5 | | 2cn 12233 |
. . . . . . . 8
β’ 2 β
β |
6 | | exp0 13977 |
. . . . . . . 8
β’ (2 β
β β (2β0) = 1) |
7 | 5, 6 | ax-mp 5 |
. . . . . . 7
β’
(2β0) = 1 |
8 | 4, 7 | eqtrdi 2789 |
. . . . . 6
β’ (π₯ = 0 β (2βπ₯) = 1) |
9 | | oveq2 7366 |
. . . . . . . . . . . . 13
β’ (π₯ = 0 β (0..^π₯) = (0..^0)) |
10 | | fzo0 13602 |
. . . . . . . . . . . . 13
β’ (0..^0) =
β
|
11 | 9, 10 | eqtrdi 2789 |
. . . . . . . . . . . 12
β’ (π₯ = 0 β (0..^π₯) = β
) |
12 | 11 | ineq2d 4173 |
. . . . . . . . . . 11
β’ (π₯ = 0 β (π΄ β© (0..^π₯)) = (π΄ β© β
)) |
13 | | in0 4352 |
. . . . . . . . . . 11
β’ (π΄ β© β
) =
β
|
14 | 12, 13 | eqtrdi 2789 |
. . . . . . . . . 10
β’ (π₯ = 0 β (π΄ β© (0..^π₯)) = β
) |
15 | 14 | fveq2d 6847 |
. . . . . . . . 9
β’ (π₯ = 0 β (πΎβ(π΄ β© (0..^π₯))) = (πΎββ
)) |
16 | | sadcadd.k |
. . . . . . . . . . 11
β’ πΎ = β‘(bits βΎ
β0) |
17 | | 0nn0 12433 |
. . . . . . . . . . . . 13
β’ 0 β
β0 |
18 | | fvres 6862 |
. . . . . . . . . . . . 13
β’ (0 β
β0 β ((bits βΎ β0)β0) =
(bitsβ0)) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . . . . . 12
β’ ((bits
βΎ β0)β0) = (bitsβ0) |
20 | | 0bits 16324 |
. . . . . . . . . . . 12
β’
(bitsβ0) = β
|
21 | 19, 20 | eqtr2i 2762 |
. . . . . . . . . . 11
β’ β
=
((bits βΎ β0)β0) |
22 | 16, 21 | fveq12i 6849 |
. . . . . . . . . 10
β’ (πΎββ
) = (β‘(bits βΎ
β0)β((bits βΎ
β0)β0)) |
23 | | bitsf1o 16330 |
. . . . . . . . . . 11
β’ (bits
βΎ β0):β0β1-1-ontoβ(π« β0 β©
Fin) |
24 | | f1ocnvfv1 7223 |
. . . . . . . . . . 11
β’ (((bits
βΎ β0):β0β1-1-ontoβ(π« β0 β© Fin)
β§ 0 β β0) β (β‘(bits βΎ
β0)β((bits βΎ β0)β0)) =
0) |
25 | 23, 17, 24 | mp2an 691 |
. . . . . . . . . 10
β’ (β‘(bits βΎ
β0)β((bits βΎ β0)β0)) =
0 |
26 | 22, 25 | eqtri 2761 |
. . . . . . . . 9
β’ (πΎββ
) =
0 |
27 | 15, 26 | eqtrdi 2789 |
. . . . . . . 8
β’ (π₯ = 0 β (πΎβ(π΄ β© (0..^π₯))) = 0) |
28 | 11 | ineq2d 4173 |
. . . . . . . . . . 11
β’ (π₯ = 0 β (π΅ β© (0..^π₯)) = (π΅ β© β
)) |
29 | | in0 4352 |
. . . . . . . . . . 11
β’ (π΅ β© β
) =
β
|
30 | 28, 29 | eqtrdi 2789 |
. . . . . . . . . 10
β’ (π₯ = 0 β (π΅ β© (0..^π₯)) = β
) |
31 | 30 | fveq2d 6847 |
. . . . . . . . 9
β’ (π₯ = 0 β (πΎβ(π΅ β© (0..^π₯))) = (πΎββ
)) |
32 | 31, 26 | eqtrdi 2789 |
. . . . . . . 8
β’ (π₯ = 0 β (πΎβ(π΅ β© (0..^π₯))) = 0) |
33 | 27, 32 | oveq12d 7376 |
. . . . . . 7
β’ (π₯ = 0 β ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯)))) = (0 + 0)) |
34 | | 00id 11335 |
. . . . . . 7
β’ (0 + 0) =
0 |
35 | 33, 34 | eqtrdi 2789 |
. . . . . 6
β’ (π₯ = 0 β ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯)))) = 0) |
36 | 8, 35 | breq12d 5119 |
. . . . 5
β’ (π₯ = 0 β ((2βπ₯) β€ ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯)))) β 1 β€ 0)) |
37 | 3, 36 | bibi12d 346 |
. . . 4
β’ (π₯ = 0 β ((β
β
(πΆβπ₯) β (2βπ₯) β€ ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯))))) β (β
β (πΆβ0) β 1 β€
0))) |
38 | 37 | imbi2d 341 |
. . 3
β’ (π₯ = 0 β ((π β (β
β (πΆβπ₯) β (2βπ₯) β€ ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯)))))) β (π β (β
β (πΆβ0) β 1 β€
0)))) |
39 | | fveq2 6843 |
. . . . . 6
β’ (π₯ = π β (πΆβπ₯) = (πΆβπ)) |
40 | 39 | eleq2d 2820 |
. . . . 5
β’ (π₯ = π β (β
β (πΆβπ₯) β β
β (πΆβπ))) |
41 | | oveq2 7366 |
. . . . . 6
β’ (π₯ = π β (2βπ₯) = (2βπ)) |
42 | | oveq2 7366 |
. . . . . . . . 9
β’ (π₯ = π β (0..^π₯) = (0..^π)) |
43 | 42 | ineq2d 4173 |
. . . . . . . 8
β’ (π₯ = π β (π΄ β© (0..^π₯)) = (π΄ β© (0..^π))) |
44 | 43 | fveq2d 6847 |
. . . . . . 7
β’ (π₯ = π β (πΎβ(π΄ β© (0..^π₯))) = (πΎβ(π΄ β© (0..^π)))) |
45 | 42 | ineq2d 4173 |
. . . . . . . 8
β’ (π₯ = π β (π΅ β© (0..^π₯)) = (π΅ β© (0..^π))) |
46 | 45 | fveq2d 6847 |
. . . . . . 7
β’ (π₯ = π β (πΎβ(π΅ β© (0..^π₯))) = (πΎβ(π΅ β© (0..^π)))) |
47 | 44, 46 | oveq12d 7376 |
. . . . . 6
β’ (π₯ = π β ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯)))) = ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π))))) |
48 | 41, 47 | breq12d 5119 |
. . . . 5
β’ (π₯ = π β ((2βπ₯) β€ ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯)))) β (2βπ) β€ ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π)))))) |
49 | 40, 48 | bibi12d 346 |
. . . 4
β’ (π₯ = π β ((β
β (πΆβπ₯) β (2βπ₯) β€ ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯))))) β (β
β (πΆβπ) β (2βπ) β€ ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π))))))) |
50 | 49 | imbi2d 341 |
. . 3
β’ (π₯ = π β ((π β (β
β (πΆβπ₯) β (2βπ₯) β€ ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯)))))) β (π β (β
β (πΆβπ) β (2βπ) β€ ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π)))))))) |
51 | | fveq2 6843 |
. . . . . 6
β’ (π₯ = (π + 1) β (πΆβπ₯) = (πΆβ(π + 1))) |
52 | 51 | eleq2d 2820 |
. . . . 5
β’ (π₯ = (π + 1) β (β
β (πΆβπ₯) β β
β (πΆβ(π + 1)))) |
53 | | oveq2 7366 |
. . . . . 6
β’ (π₯ = (π + 1) β (2βπ₯) = (2β(π + 1))) |
54 | | oveq2 7366 |
. . . . . . . . 9
β’ (π₯ = (π + 1) β (0..^π₯) = (0..^(π + 1))) |
55 | 54 | ineq2d 4173 |
. . . . . . . 8
β’ (π₯ = (π + 1) β (π΄ β© (0..^π₯)) = (π΄ β© (0..^(π + 1)))) |
56 | 55 | fveq2d 6847 |
. . . . . . 7
β’ (π₯ = (π + 1) β (πΎβ(π΄ β© (0..^π₯))) = (πΎβ(π΄ β© (0..^(π + 1))))) |
57 | 54 | ineq2d 4173 |
. . . . . . . 8
β’ (π₯ = (π + 1) β (π΅ β© (0..^π₯)) = (π΅ β© (0..^(π + 1)))) |
58 | 57 | fveq2d 6847 |
. . . . . . 7
β’ (π₯ = (π + 1) β (πΎβ(π΅ β© (0..^π₯))) = (πΎβ(π΅ β© (0..^(π + 1))))) |
59 | 56, 58 | oveq12d 7376 |
. . . . . 6
β’ (π₯ = (π + 1) β ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯)))) = ((πΎβ(π΄ β© (0..^(π + 1)))) + (πΎβ(π΅ β© (0..^(π + 1)))))) |
60 | 53, 59 | breq12d 5119 |
. . . . 5
β’ (π₯ = (π + 1) β ((2βπ₯) β€ ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯)))) β (2β(π + 1)) β€ ((πΎβ(π΄ β© (0..^(π + 1)))) + (πΎβ(π΅ β© (0..^(π + 1))))))) |
61 | 52, 60 | bibi12d 346 |
. . . 4
β’ (π₯ = (π + 1) β ((β
β (πΆβπ₯) β (2βπ₯) β€ ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯))))) β (β
β (πΆβ(π + 1)) β (2β(π + 1)) β€ ((πΎβ(π΄ β© (0..^(π + 1)))) + (πΎβ(π΅ β© (0..^(π + 1)))))))) |
62 | 61 | imbi2d 341 |
. . 3
β’ (π₯ = (π + 1) β ((π β (β
β (πΆβπ₯) β (2βπ₯) β€ ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯)))))) β (π β (β
β (πΆβ(π + 1)) β (2β(π + 1)) β€ ((πΎβ(π΄ β© (0..^(π + 1)))) + (πΎβ(π΅ β© (0..^(π + 1))))))))) |
63 | | fveq2 6843 |
. . . . . 6
β’ (π₯ = π β (πΆβπ₯) = (πΆβπ)) |
64 | 63 | eleq2d 2820 |
. . . . 5
β’ (π₯ = π β (β
β (πΆβπ₯) β β
β (πΆβπ))) |
65 | | oveq2 7366 |
. . . . . 6
β’ (π₯ = π β (2βπ₯) = (2βπ)) |
66 | | oveq2 7366 |
. . . . . . . . 9
β’ (π₯ = π β (0..^π₯) = (0..^π)) |
67 | 66 | ineq2d 4173 |
. . . . . . . 8
β’ (π₯ = π β (π΄ β© (0..^π₯)) = (π΄ β© (0..^π))) |
68 | 67 | fveq2d 6847 |
. . . . . . 7
β’ (π₯ = π β (πΎβ(π΄ β© (0..^π₯))) = (πΎβ(π΄ β© (0..^π)))) |
69 | 66 | ineq2d 4173 |
. . . . . . . 8
β’ (π₯ = π β (π΅ β© (0..^π₯)) = (π΅ β© (0..^π))) |
70 | 69 | fveq2d 6847 |
. . . . . . 7
β’ (π₯ = π β (πΎβ(π΅ β© (0..^π₯))) = (πΎβ(π΅ β© (0..^π)))) |
71 | 68, 70 | oveq12d 7376 |
. . . . . 6
β’ (π₯ = π β ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯)))) = ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π))))) |
72 | 65, 71 | breq12d 5119 |
. . . . 5
β’ (π₯ = π β ((2βπ₯) β€ ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯)))) β (2βπ) β€ ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π)))))) |
73 | 64, 72 | bibi12d 346 |
. . . 4
β’ (π₯ = π β ((β
β (πΆβπ₯) β (2βπ₯) β€ ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯))))) β (β
β (πΆβπ) β (2βπ) β€ ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π))))))) |
74 | 73 | imbi2d 341 |
. . 3
β’ (π₯ = π β ((π β (β
β (πΆβπ₯) β (2βπ₯) β€ ((πΎβ(π΄ β© (0..^π₯))) + (πΎβ(π΅ β© (0..^π₯)))))) β (π β (β
β (πΆβπ) β (2βπ) β€ ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π)))))))) |
75 | | sadval.a |
. . . . 5
β’ (π β π΄ β
β0) |
76 | | sadval.b |
. . . . 5
β’ (π β π΅ β
β0) |
77 | | sadval.c |
. . . . 5
β’ πΆ = seq0((π β 2o, π β β0 β¦
if(cadd(π β π΄, π β π΅, β
β π), 1o, β
)), (π β β0
β¦ if(π = 0, β
,
(π β
1)))) |
78 | 75, 76, 77 | sadc0 16339 |
. . . 4
β’ (π β Β¬ β
β
(πΆβ0)) |
79 | | 0lt1 11682 |
. . . . . 6
β’ 0 <
1 |
80 | | 0re 11162 |
. . . . . . 7
β’ 0 β
β |
81 | | 1re 11160 |
. . . . . . 7
β’ 1 β
β |
82 | 80, 81 | ltnlei 11281 |
. . . . . 6
β’ (0 < 1
β Β¬ 1 β€ 0) |
83 | 79, 82 | mpbi 229 |
. . . . 5
β’ Β¬ 1
β€ 0 |
84 | 83 | a1i 11 |
. . . 4
β’ (π β Β¬ 1 β€
0) |
85 | 78, 84 | 2falsed 377 |
. . 3
β’ (π β (β
β (πΆβ0) β 1 β€
0)) |
86 | 75 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β β0) β§ (β
β (πΆβπ) β (2βπ) β€ ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π)))))) β π΄ β
β0) |
87 | 76 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β β0) β§ (β
β (πΆβπ) β (2βπ) β€ ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π)))))) β π΅ β
β0) |
88 | | simplr 768 |
. . . . . . 7
β’ (((π β§ π β β0) β§ (β
β (πΆβπ) β (2βπ) β€ ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π)))))) β π β β0) |
89 | | simpr 486 |
. . . . . . 7
β’ (((π β§ π β β0) β§ (β
β (πΆβπ) β (2βπ) β€ ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π)))))) β (β
β (πΆβπ) β (2βπ) β€ ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π)))))) |
90 | 86, 87, 77, 88, 16, 89 | sadcaddlem 16342 |
. . . . . 6
β’ (((π β§ π β β0) β§ (β
β (πΆβπ) β (2βπ) β€ ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π)))))) β (β
β (πΆβ(π + 1)) β (2β(π + 1)) β€ ((πΎβ(π΄ β© (0..^(π + 1)))) + (πΎβ(π΅ β© (0..^(π + 1))))))) |
91 | 90 | ex 414 |
. . . . 5
β’ ((π β§ π β β0) β ((β
β (πΆβπ) β (2βπ) β€ ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π))))) β (β
β (πΆβ(π + 1)) β (2β(π + 1)) β€ ((πΎβ(π΄ β© (0..^(π + 1)))) + (πΎβ(π΅ β© (0..^(π + 1)))))))) |
92 | 91 | expcom 415 |
. . . 4
β’ (π β β0
β (π β ((β
β (πΆβπ) β (2βπ) β€ ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π))))) β (β
β (πΆβ(π + 1)) β (2β(π + 1)) β€ ((πΎβ(π΄ β© (0..^(π + 1)))) + (πΎβ(π΅ β© (0..^(π + 1))))))))) |
93 | 92 | a2d 29 |
. . 3
β’ (π β β0
β ((π β (β
β (πΆβπ) β (2βπ) β€ ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π)))))) β (π β (β
β (πΆβ(π + 1)) β (2β(π + 1)) β€ ((πΎβ(π΄ β© (0..^(π + 1)))) + (πΎβ(π΅ β© (0..^(π + 1))))))))) |
94 | 38, 50, 62, 74, 85, 93 | nn0ind 12603 |
. 2
β’ (π β β0
β (π β (β
β (πΆβπ) β (2βπ) β€ ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π))))))) |
95 | 1, 94 | mpcom 38 |
1
β’ (π β (β
β (πΆβπ) β (2βπ) β€ ((πΎβ(π΄ β© (0..^π))) + (πΎβ(π΅ β© (0..^π)))))) |