Step | Hyp | Ref
| Expression |
1 | | nn0uz 12810 |
. 2
β’
β0 = (β€β₯β0) |
2 | | nnuz 12811 |
. 2
β’ β =
(β€β₯β1) |
3 | | 0zd 12516 |
. 2
β’ (π β 0 β
β€) |
4 | | 1zzd 12539 |
. 2
β’ (π β 1 β
β€) |
5 | | 2nn0 12435 |
. . . . . 6
β’ 2 β
β0 |
6 | 5 | a1i 11 |
. . . . 5
β’ (π β 2 β
β0) |
7 | | nn0mulcl 12454 |
. . . . 5
β’ ((2
β β0 β§ π β β0) β (2
Β· π) β
β0) |
8 | 6, 7 | sylan 581 |
. . . 4
β’ ((π β§ π β β0) β (2
Β· π) β
β0) |
9 | | nn0p1nn 12457 |
. . . 4
β’ ((2
Β· π) β
β0 β ((2 Β· π) + 1) β β) |
10 | 8, 9 | syl 17 |
. . 3
β’ ((π β§ π β β0) β ((2
Β· π) + 1) β
β) |
11 | 10 | fmpttd 7064 |
. 2
β’ (π β (π β β0 β¦ ((2
Β· π) +
1)):β0βΆβ) |
12 | | nn0mulcl 12454 |
. . . . . 6
β’ ((2
β β0 β§ π β β0) β (2
Β· π) β
β0) |
13 | 6, 12 | sylan 581 |
. . . . 5
β’ ((π β§ π β β0) β (2
Β· π) β
β0) |
14 | 13 | nn0red 12479 |
. . . 4
β’ ((π β§ π β β0) β (2
Β· π) β
β) |
15 | | peano2nn0 12458 |
. . . . . 6
β’ (π β β0
β (π + 1) β
β0) |
16 | | nn0mulcl 12454 |
. . . . . 6
β’ ((2
β β0 β§ (π + 1) β β0) β (2
Β· (π + 1)) β
β0) |
17 | 6, 15, 16 | syl2an 597 |
. . . . 5
β’ ((π β§ π β β0) β (2
Β· (π + 1)) β
β0) |
18 | 17 | nn0red 12479 |
. . . 4
β’ ((π β§ π β β0) β (2
Β· (π + 1)) β
β) |
19 | | 1red 11161 |
. . . 4
β’ ((π β§ π β β0) β 1 β
β) |
20 | | nn0re 12427 |
. . . . . . 7
β’ (π β β0
β π β
β) |
21 | 20 | adantl 483 |
. . . . . 6
β’ ((π β§ π β β0) β π β
β) |
22 | 21 | ltp1d 12090 |
. . . . 5
β’ ((π β§ π β β0) β π < (π + 1)) |
23 | | 1red 11161 |
. . . . . . . 8
β’ (π β β0
β 1 β β) |
24 | 20, 23 | readdcld 11189 |
. . . . . . 7
β’ (π β β0
β (π + 1) β
β) |
25 | | 2rp 12925 |
. . . . . . . 8
β’ 2 β
β+ |
26 | 25 | a1i 11 |
. . . . . . 7
β’ (π β β0
β 2 β β+) |
27 | 20, 24, 26 | ltmul2d 13004 |
. . . . . 6
β’ (π β β0
β (π < (π + 1) β (2 Β· π) < (2 Β· (π + 1)))) |
28 | 27 | adantl 483 |
. . . . 5
β’ ((π β§ π β β0) β (π < (π + 1) β (2 Β· π) < (2 Β· (π + 1)))) |
29 | 22, 28 | mpbid 231 |
. . . 4
β’ ((π β§ π β β0) β (2
Β· π) < (2
Β· (π +
1))) |
30 | 14, 18, 19, 29 | ltadd1dd 11771 |
. . 3
β’ ((π β§ π β β0) β ((2
Β· π) + 1) < ((2
Β· (π + 1)) +
1)) |
31 | | oveq2 7366 |
. . . . . 6
β’ (π = π β (2 Β· π) = (2 Β· π)) |
32 | 31 | oveq1d 7373 |
. . . . 5
β’ (π = π β ((2 Β· π) + 1) = ((2 Β· π) + 1)) |
33 | | eqid 2733 |
. . . . 5
β’ (π β β0
β¦ ((2 Β· π) +
1)) = (π β
β0 β¦ ((2 Β· π) + 1)) |
34 | | ovex 7391 |
. . . . 5
β’ ((2
Β· π) + 1) β
V |
35 | 32, 33, 34 | fvmpt 6949 |
. . . 4
β’ (π β β0
β ((π β
β0 β¦ ((2 Β· π) + 1))βπ) = ((2 Β· π) + 1)) |
36 | 35 | adantl 483 |
. . 3
β’ ((π β§ π β β0) β ((π β β0
β¦ ((2 Β· π) +
1))βπ) = ((2 Β·
π) + 1)) |
37 | 15 | adantl 483 |
. . . 4
β’ ((π β§ π β β0) β (π + 1) β
β0) |
38 | | oveq2 7366 |
. . . . . 6
β’ (π = (π + 1) β (2 Β· π) = (2 Β· (π + 1))) |
39 | 38 | oveq1d 7373 |
. . . . 5
β’ (π = (π + 1) β ((2 Β· π) + 1) = ((2 Β· (π + 1)) + 1)) |
40 | | ovex 7391 |
. . . . 5
β’ ((2
Β· (π + 1)) + 1)
β V |
41 | 39, 33, 40 | fvmpt 6949 |
. . . 4
β’ ((π + 1) β β0
β ((π β
β0 β¦ ((2 Β· π) + 1))β(π + 1)) = ((2 Β· (π + 1)) + 1)) |
42 | 37, 41 | syl 17 |
. . 3
β’ ((π β§ π β β0) β ((π β β0
β¦ ((2 Β· π) +
1))β(π + 1)) = ((2
Β· (π + 1)) +
1)) |
43 | 30, 36, 42 | 3brtr4d 5138 |
. 2
β’ ((π β§ π β β0) β ((π β β0
β¦ ((2 Β· π) +
1))βπ) < ((π β β0
β¦ ((2 Β· π) +
1))β(π +
1))) |
44 | | eldifi 4087 |
. . . . . . 7
β’ (π β (β β ran
(π β
β0 β¦ ((2 Β· π) + 1))) β π β β) |
45 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β β) β π β β) |
46 | | 0cnd 11153 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ 2 β₯ π) β 0 β
β) |
47 | | nnz 12525 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
β€) |
48 | 47 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β π β β€) |
49 | | odd2np1 16228 |
. . . . . . . . . . . . 13
β’ (π β β€ β (Β¬ 2
β₯ π β
βπ β β€ ((2
Β· π) + 1) = π)) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (Β¬ 2 β₯
π β βπ β β€ ((2 Β·
π) + 1) = π)) |
51 | | simprl 770 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ (π β β€ β§ ((2 Β· π) + 1) = π)) β π β β€) |
52 | | nnm1nn0 12459 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β (π β 1) β
β0) |
53 | 52 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ (π β β€ β§ ((2 Β· π) + 1) = π)) β (π β 1) β
β0) |
54 | 53 | nn0red 12479 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ (π β β€ β§ ((2 Β· π) + 1) = π)) β (π β 1) β β) |
55 | 25 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ (π β β€ β§ ((2 Β· π) + 1) = π)) β 2 β
β+) |
56 | 53 | nn0ge0d 12481 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ (π β β€ β§ ((2 Β· π) + 1) = π)) β 0 β€ (π β 1)) |
57 | 54, 55, 56 | divge0d 13002 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ (π β β€ β§ ((2 Β· π) + 1) = π)) β 0 β€ ((π β 1) / 2)) |
58 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β) β§ (π β β€ β§ ((2 Β· π) + 1) = π)) β ((2 Β· π) + 1) = π) |
59 | 58 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β) β§ (π β β€ β§ ((2 Β· π) + 1) = π)) β (((2 Β· π) + 1) β 1) = (π β 1)) |
60 | | 2cn 12233 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 2 β
β |
61 | | zcn 12509 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β€ β π β
β) |
62 | 61 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β β) β§ (π β β€ β§ ((2 Β· π) + 1) = π)) β π β β) |
63 | | mulcl 11140 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((2
β β β§ π
β β) β (2 Β· π) β β) |
64 | 60, 62, 63 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β) β§ (π β β€ β§ ((2 Β· π) + 1) = π)) β (2 Β· π) β β) |
65 | | ax-1cn 11114 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 1 β
β |
66 | | pncan 11412 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((2
Β· π) β β
β§ 1 β β) β (((2 Β· π) + 1) β 1) = (2 Β· π)) |
67 | 64, 65, 66 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β) β§ (π β β€ β§ ((2 Β· π) + 1) = π)) β (((2 Β· π) + 1) β 1) = (2 Β· π)) |
68 | 59, 67 | eqtr3d 2775 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ (π β β€ β§ ((2 Β· π) + 1) = π)) β (π β 1) = (2 Β· π)) |
69 | 68 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ (π β β€ β§ ((2 Β· π) + 1) = π)) β ((π β 1) / 2) = ((2 Β· π) / 2)) |
70 | | 2cnd 12236 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ (π β β€ β§ ((2 Β· π) + 1) = π)) β 2 β β) |
71 | | 2ne0 12262 |
. . . . . . . . . . . . . . . . . . . 20
β’ 2 β
0 |
72 | 71 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ (π β β€ β§ ((2 Β· π) + 1) = π)) β 2 β 0) |
73 | 62, 70, 72 | divcan3d 11941 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ (π β β€ β§ ((2 Β· π) + 1) = π)) β ((2 Β· π) / 2) = π) |
74 | 69, 73 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ (π β β€ β§ ((2 Β· π) + 1) = π)) β ((π β 1) / 2) = π) |
75 | 57, 74 | breqtrd 5132 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ (π β β€ β§ ((2 Β· π) + 1) = π)) β 0 β€ π) |
76 | | elnn0z 12517 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β (π β β€
β§ 0 β€ π)) |
77 | 51, 75, 76 | sylanbrc 584 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ (π β β€ β§ ((2 Β· π) + 1) = π)) β π β β0) |
78 | 77 | ex 414 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β ((π β β€ β§ ((2 Β· π) + 1) = π) β π β
β0)) |
79 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ ((π β β€ β§ ((2
Β· π) + 1) = π) β ((2 Β· π) + 1) = π) |
80 | 79 | eqcomd 2739 |
. . . . . . . . . . . . . 14
β’ ((π β β€ β§ ((2
Β· π) + 1) = π) β π = ((2 Β· π) + 1)) |
81 | 78, 80 | jca2 515 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β ((π β β€ β§ ((2 Β· π) + 1) = π) β (π β β0 β§ π = ((2 Β· π) + 1)))) |
82 | 81 | reximdv2 3158 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (βπ β β€ ((2 Β·
π) + 1) = π β βπ β β0
π = ((2 Β· π) + 1))) |
83 | 50, 82 | sylbid 239 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (Β¬ 2 β₯
π β βπ β β0
π = ((2 Β· π) + 1))) |
84 | | iserodd.f |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β0) β πΆ β
β) |
85 | | iserodd.h |
. . . . . . . . . . . . . . 15
β’ (π = ((2 Β· π) + 1) β π΅ = πΆ) |
86 | 85 | eleq1d 2819 |
. . . . . . . . . . . . . 14
β’ (π = ((2 Β· π) + 1) β (π΅ β β β πΆ β β)) |
87 | 84, 86 | syl5ibrcom 247 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β0) β (π = ((2 Β· π) + 1) β π΅ β β)) |
88 | 87 | rexlimdva 3149 |
. . . . . . . . . . . 12
β’ (π β (βπ β β0 π = ((2 Β· π) + 1) β π΅ β β)) |
89 | 88 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (βπ β β0
π = ((2 Β· π) + 1) β π΅ β β)) |
90 | 83, 89 | syld 47 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (Β¬ 2 β₯
π β π΅ β β)) |
91 | 90 | imp 408 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ Β¬ 2 β₯ π) β π΅ β β) |
92 | 46, 91 | ifclda 4522 |
. . . . . . . 8
β’ ((π β§ π β β) β if(2 β₯ π, 0, π΅) β β) |
93 | | eqid 2733 |
. . . . . . . . 9
β’ (π β β β¦ if(2
β₯ π, 0, π΅)) = (π β β β¦ if(2 β₯ π, 0, π΅)) |
94 | 93 | fvmpt2 6960 |
. . . . . . . 8
β’ ((π β β β§ if(2
β₯ π, 0, π΅) β β) β ((π β β β¦ if(2
β₯ π, 0, π΅))βπ) = if(2 β₯ π, 0, π΅)) |
95 | 45, 92, 94 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π β β) β ((π β β β¦ if(2 β₯ π, 0, π΅))βπ) = if(2 β₯ π, 0, π΅)) |
96 | 44, 95 | sylan2 594 |
. . . . . 6
β’ ((π β§ π β (β β ran (π β β0
β¦ ((2 Β· π) +
1)))) β ((π β
β β¦ if(2 β₯ π, 0, π΅))βπ) = if(2 β₯ π, 0, π΅)) |
97 | | eldif 3921 |
. . . . . . . 8
β’ (π β (β β ran
(π β
β0 β¦ ((2 Β· π) + 1))) β (π β β β§ Β¬ π β ran (π β β0 β¦ ((2
Β· π) +
1)))) |
98 | | oveq2 7366 |
. . . . . . . . . . . . . . 15
β’ (π = π β (2 Β· π) = (2 Β· π)) |
99 | 98 | oveq1d 7373 |
. . . . . . . . . . . . . 14
β’ (π = π β ((2 Β· π) + 1) = ((2 Β· π) + 1)) |
100 | 99 | cbvmptv 5219 |
. . . . . . . . . . . . 13
β’ (π β β0
β¦ ((2 Β· π) +
1)) = (π β
β0 β¦ ((2 Β· π) + 1)) |
101 | 100 | elrnmpt 5912 |
. . . . . . . . . . . 12
β’ (π β V β (π β ran (π β β0 β¦ ((2
Β· π) + 1)) β
βπ β
β0 π = ((2
Β· π) +
1))) |
102 | 101 | elv 3450 |
. . . . . . . . . . 11
β’ (π β ran (π β β0 β¦ ((2
Β· π) + 1)) β
βπ β
β0 π = ((2
Β· π) +
1)) |
103 | 83, 102 | syl6ibr 252 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (Β¬ 2 β₯
π β π β ran (π β β0 β¦ ((2
Β· π) +
1)))) |
104 | 103 | con1d 145 |
. . . . . . . . 9
β’ ((π β§ π β β) β (Β¬ π β ran (π β β0 β¦ ((2
Β· π) + 1)) β 2
β₯ π)) |
105 | 104 | impr 456 |
. . . . . . . 8
β’ ((π β§ (π β β β§ Β¬ π β ran (π β β0 β¦ ((2
Β· π) + 1)))) β
2 β₯ π) |
106 | 97, 105 | sylan2b 595 |
. . . . . . 7
β’ ((π β§ π β (β β ran (π β β0
β¦ ((2 Β· π) +
1)))) β 2 β₯ π) |
107 | 106 | iftrued 4495 |
. . . . . 6
β’ ((π β§ π β (β β ran (π β β0
β¦ ((2 Β· π) +
1)))) β if(2 β₯ π, 0, π΅) = 0) |
108 | 96, 107 | eqtrd 2773 |
. . . . 5
β’ ((π β§ π β (β β ran (π β β0
β¦ ((2 Β· π) +
1)))) β ((π β
β β¦ if(2 β₯ π, 0, π΅))βπ) = 0) |
109 | 108 | ralrimiva 3140 |
. . . 4
β’ (π β βπ β (β β ran (π β β0
β¦ ((2 Β· π) +
1)))((π β β
β¦ if(2 β₯ π, 0,
π΅))βπ) = 0) |
110 | | nfv 1918 |
. . . . 5
β’
β²π((π β β β¦ if(2
β₯ π, 0, π΅))βπ) = 0 |
111 | | nffvmpt1 6854 |
. . . . . 6
β’
β²π((π β β β¦ if(2 β₯ π, 0, π΅))βπ) |
112 | 111 | nfeq1 2919 |
. . . . 5
β’
β²π((π β β β¦ if(2
β₯ π, 0, π΅))βπ) = 0 |
113 | | fveqeq2 6852 |
. . . . 5
β’ (π = π β (((π β β β¦ if(2 β₯ π, 0, π΅))βπ) = 0 β ((π β β β¦ if(2 β₯ π, 0, π΅))βπ) = 0)) |
114 | 110, 112,
113 | cbvralw 3288 |
. . . 4
β’
(βπ β
(β β ran (π
β β0 β¦ ((2 Β· π) + 1)))((π β β β¦ if(2 β₯ π, 0, π΅))βπ) = 0 β βπ β (β β ran (π β β0
β¦ ((2 Β· π) +
1)))((π β β
β¦ if(2 β₯ π, 0,
π΅))βπ) = 0) |
115 | 109, 114 | sylib 217 |
. . 3
β’ (π β βπ β (β β ran (π β β0
β¦ ((2 Β· π) +
1)))((π β β
β¦ if(2 β₯ π, 0,
π΅))βπ) = 0) |
116 | 115 | r19.21bi 3233 |
. 2
β’ ((π β§ π β (β β ran (π β β0
β¦ ((2 Β· π) +
1)))) β ((π β
β β¦ if(2 β₯ π, 0, π΅))βπ) = 0) |
117 | 92 | fmpttd 7064 |
. . 3
β’ (π β (π β β β¦ if(2 β₯ π, 0, π΅)):ββΆβ) |
118 | 117 | ffvelcdmda 7036 |
. 2
β’ ((π β§ π β β) β ((π β β β¦ if(2 β₯ π, 0, π΅))βπ) β β) |
119 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π β β0) β π β
β0) |
120 | | eqid 2733 |
. . . . . . . 8
β’ (π β β0
β¦ πΆ) = (π β β0
β¦ πΆ) |
121 | 120 | fvmpt2 6960 |
. . . . . . 7
β’ ((π β β0
β§ πΆ β β)
β ((π β
β0 β¦ πΆ)βπ) = πΆ) |
122 | 119, 84, 121 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π β β0) β ((π β β0
β¦ πΆ)βπ) = πΆ) |
123 | | ovex 7391 |
. . . . . . . . . 10
β’ ((2
Β· π) + 1) β
V |
124 | 99, 33, 123 | fvmpt 6949 |
. . . . . . . . 9
β’ (π β β0
β ((π β
β0 β¦ ((2 Β· π) + 1))βπ) = ((2 Β· π) + 1)) |
125 | 124 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β β0) β ((π β β0
β¦ ((2 Β· π) +
1))βπ) = ((2 Β·
π) + 1)) |
126 | 125 | fveq2d 6847 |
. . . . . . 7
β’ ((π β§ π β β0) β ((π β β β¦ if(2
β₯ π, 0, π΅))β((π β β0 β¦ ((2
Β· π) +
1))βπ)) = ((π β β β¦ if(2
β₯ π, 0, π΅))β((2 Β· π) + 1))) |
127 | | breq2 5110 |
. . . . . . . . 9
β’ (π = ((2 Β· π) + 1) β (2 β₯ π β 2 β₯ ((2 Β·
π) + 1))) |
128 | 127, 85 | ifbieq2d 4513 |
. . . . . . . 8
β’ (π = ((2 Β· π) + 1) β if(2 β₯ π, 0, π΅) = if(2 β₯ ((2 Β· π) + 1), 0, πΆ)) |
129 | | nn0mulcl 12454 |
. . . . . . . . . 10
β’ ((2
β β0 β§ π β β0) β (2
Β· π) β
β0) |
130 | 6, 129 | sylan 581 |
. . . . . . . . 9
β’ ((π β§ π β β0) β (2
Β· π) β
β0) |
131 | | nn0p1nn 12457 |
. . . . . . . . 9
β’ ((2
Β· π) β
β0 β ((2 Β· π) + 1) β β) |
132 | 130, 131 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β β0) β ((2
Β· π) + 1) β
β) |
133 | | 2z 12540 |
. . . . . . . . . . . 12
β’ 2 β
β€ |
134 | | nn0z 12529 |
. . . . . . . . . . . . 13
β’ (π β β0
β π β
β€) |
135 | 134 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β β0) β π β
β€) |
136 | | dvdsmul1 16165 |
. . . . . . . . . . . 12
β’ ((2
β β€ β§ π
β β€) β 2 β₯ (2 Β· π)) |
137 | 133, 135,
136 | sylancr 588 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β 2 β₯
(2 Β· π)) |
138 | 130 | nn0zd 12530 |
. . . . . . . . . . . 12
β’ ((π β§ π β β0) β (2
Β· π) β
β€) |
139 | | 2nn 12231 |
. . . . . . . . . . . . 13
β’ 2 β
β |
140 | 139 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π β β0) β 2 β
β) |
141 | | 1lt2 12329 |
. . . . . . . . . . . . 13
β’ 1 <
2 |
142 | 141 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π β β0) β 1 <
2) |
143 | | ndvdsp1 16298 |
. . . . . . . . . . . 12
β’ (((2
Β· π) β β€
β§ 2 β β β§ 1 < 2) β (2 β₯ (2 Β· π) β Β¬ 2 β₯ ((2
Β· π) +
1))) |
144 | 138, 140,
142, 143 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β (2
β₯ (2 Β· π)
β Β¬ 2 β₯ ((2 Β· π) + 1))) |
145 | 137, 144 | mpd 15 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β Β¬ 2
β₯ ((2 Β· π) +
1)) |
146 | 145 | iffalsed 4498 |
. . . . . . . . 9
β’ ((π β§ π β β0) β if(2
β₯ ((2 Β· π) +
1), 0, πΆ) = πΆ) |
147 | 146, 84 | eqeltrd 2834 |
. . . . . . . 8
β’ ((π β§ π β β0) β if(2
β₯ ((2 Β· π) +
1), 0, πΆ) β
β) |
148 | 93, 128, 132, 147 | fvmptd3 6972 |
. . . . . . 7
β’ ((π β§ π β β0) β ((π β β β¦ if(2
β₯ π, 0, π΅))β((2 Β· π) + 1)) = if(2 β₯ ((2
Β· π) + 1), 0, πΆ)) |
149 | 126, 148,
146 | 3eqtrd 2777 |
. . . . . 6
β’ ((π β§ π β β0) β ((π β β β¦ if(2
β₯ π, 0, π΅))β((π β β0 β¦ ((2
Β· π) +
1))βπ)) = πΆ) |
150 | 122, 149 | eqtr4d 2776 |
. . . . 5
β’ ((π β§ π β β0) β ((π β β0
β¦ πΆ)βπ) = ((π β β β¦ if(2 β₯ π, 0, π΅))β((π β β0 β¦ ((2
Β· π) +
1))βπ))) |
151 | 150 | ralrimiva 3140 |
. . . 4
β’ (π β βπ β β0 ((π β β0
β¦ πΆ)βπ) = ((π β β β¦ if(2 β₯ π, 0, π΅))β((π β β0 β¦ ((2
Β· π) +
1))βπ))) |
152 | | nfv 1918 |
. . . . 5
β’
β²π((π β β0
β¦ πΆ)βπ) = ((π β β β¦ if(2 β₯ π, 0, π΅))β((π β β0 β¦ ((2
Β· π) +
1))βπ)) |
153 | | nffvmpt1 6854 |
. . . . . 6
β’
β²π((π β β0 β¦ πΆ)βπ) |
154 | 153 | nfeq1 2919 |
. . . . 5
β’
β²π((π β β0
β¦ πΆ)βπ) = ((π β β β¦ if(2 β₯ π, 0, π΅))β((π β β0 β¦ ((2
Β· π) +
1))βπ)) |
155 | | fveq2 6843 |
. . . . . 6
β’ (π = π β ((π β β0 β¦ πΆ)βπ) = ((π β β0 β¦ πΆ)βπ)) |
156 | | 2fveq3 6848 |
. . . . . 6
β’ (π = π β ((π β β β¦ if(2 β₯ π, 0, π΅))β((π β β0 β¦ ((2
Β· π) +
1))βπ)) = ((π β β β¦ if(2
β₯ π, 0, π΅))β((π β β0 β¦ ((2
Β· π) +
1))βπ))) |
157 | 155, 156 | eqeq12d 2749 |
. . . . 5
β’ (π = π β (((π β β0 β¦ πΆ)βπ) = ((π β β β¦ if(2 β₯ π, 0, π΅))β((π β β0 β¦ ((2
Β· π) +
1))βπ)) β
((π β
β0 β¦ πΆ)βπ) = ((π β β β¦ if(2 β₯ π, 0, π΅))β((π β β0 β¦ ((2
Β· π) +
1))βπ)))) |
158 | 152, 154,
157 | cbvralw 3288 |
. . . 4
β’
(βπ β
β0 ((π
β β0 β¦ πΆ)βπ) = ((π β β β¦ if(2 β₯ π, 0, π΅))β((π β β0 β¦ ((2
Β· π) +
1))βπ)) β
βπ β
β0 ((π
β β0 β¦ πΆ)βπ) = ((π β β β¦ if(2 β₯ π, 0, π΅))β((π β β0 β¦ ((2
Β· π) +
1))βπ))) |
159 | 151, 158 | sylib 217 |
. . 3
β’ (π β βπ β β0 ((π β β0
β¦ πΆ)βπ) = ((π β β β¦ if(2 β₯ π, 0, π΅))β((π β β0 β¦ ((2
Β· π) +
1))βπ))) |
160 | 159 | r19.21bi 3233 |
. 2
β’ ((π β§ π β β0) β ((π β β0
β¦ πΆ)βπ) = ((π β β β¦ if(2 β₯ π, 0, π΅))β((π β β0 β¦ ((2
Β· π) +
1))βπ))) |
161 | 1, 2, 3, 4, 11, 43, 116, 118, 160 | isercoll2 15559 |
1
β’ (π β (seq0( + , (π β β0
β¦ πΆ)) β π΄ β seq1( + , (π β β β¦ if(2
β₯ π, 0, π΅))) β π΄)) |