Step | Hyp | Ref
| Expression |
1 | | 2sbcrex 42011 |
. . . 4
β’
([(π βΎ
(1...π)) / π’][(πβπ) / π£]βπ€ β β0 π β βπ€ β β0 [(π βΎ (1...π)) / π’][(πβπ) / π£]π) |
2 | 1 | rabbii 3430 |
. . 3
β’ {π β (β0
βm (1...π))
β£ [(π βΎ
(1...π)) / π’][(πβπ) / π£]βπ€ β β0 π} = {π β (β0
βm (1...π))
β£ βπ€ β
β0 [(π βΎ (1...π)) / π’][(πβπ) / π£]π} |
3 | | rexfrabdioph.1 |
. . . . . 6
β’ π = (π + 1) |
4 | | peano2nn0 12509 |
. . . . . 6
β’ (π β β0
β (π + 1) β
β0) |
5 | 3, 4 | eqeltrid 2829 |
. . . . 5
β’ (π β β0
β π β
β0) |
6 | 5 | adantr 480 |
. . . 4
β’ ((π β β0
β§ {π‘ β
(β0 βm (1...πΏ)) β£ [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€]π} β (DiophβπΏ)) β π β
β0) |
7 | | sbcrot3 42018 |
. . . . . . . . 9
β’
([(π‘βπΏ) / π€][(π βΎ (1...π)) / π’][(πβπ) / π£]π β [(π βΎ (1...π)) / π’][(πβπ) / π£][(π‘βπΏ) / π€]π) |
8 | 7 | sbcbii 3829 |
. . . . . . . 8
β’
([(π‘ βΎ
(1...π)) / π][(π‘βπΏ) / π€][(π βΎ (1...π)) / π’][(πβπ) / π£]π β [(π‘ βΎ (1...π)) / π][(π βΎ (1...π)) / π’][(πβπ) / π£][(π‘βπΏ) / π€]π) |
9 | | reseq1 5965 |
. . . . . . . . . 10
β’ (π = (π‘ βΎ (1...π)) β (π βΎ (1...π)) = ((π‘ βΎ (1...π)) βΎ (1...π))) |
10 | 9 | sbccomieg 42020 |
. . . . . . . . 9
β’
([(π‘ βΎ
(1...π)) / π][(π βΎ (1...π)) / π’][(πβπ) / π£][(π‘βπΏ) / π€]π β [((π‘ βΎ (1...π)) βΎ (1...π)) / π’][(π‘ βΎ (1...π)) / π][(πβπ) / π£][(π‘βπΏ) / π€]π) |
11 | | fzssp1 13541 |
. . . . . . . . . . . 12
β’
(1...π) β
(1...(π +
1)) |
12 | 3 | oveq2i 7412 |
. . . . . . . . . . . 12
β’
(1...π) =
(1...(π +
1)) |
13 | 11, 12 | sseqtrri 4011 |
. . . . . . . . . . 11
β’
(1...π) β
(1...π) |
14 | | resabs1 6001 |
. . . . . . . . . . 11
β’
((1...π) β
(1...π) β ((π‘ βΎ (1...π)) βΎ (1...π)) = (π‘ βΎ (1...π))) |
15 | | dfsbcq 3771 |
. . . . . . . . . . 11
β’ (((π‘ βΎ (1...π)) βΎ (1...π)) = (π‘ βΎ (1...π)) β ([((π‘ βΎ (1...π)) βΎ (1...π)) / π’][(π‘ βΎ (1...π)) / π][(πβπ) / π£][(π‘βπΏ) / π€]π β [(π‘ βΎ (1...π)) / π’][(π‘ βΎ (1...π)) / π][(πβπ) / π£][(π‘βπΏ) / π€]π)) |
16 | 13, 14, 15 | mp2b 10 |
. . . . . . . . . 10
β’
([((π‘ βΎ
(1...π)) βΎ (1...π)) / π’][(π‘ βΎ (1...π)) / π][(πβπ) / π£][(π‘βπΏ) / π€]π β [(π‘ βΎ (1...π)) / π’][(π‘ βΎ (1...π)) / π][(πβπ) / π£][(π‘βπΏ) / π€]π) |
17 | | vex 3470 |
. . . . . . . . . . . . . 14
β’ π‘ β V |
18 | 17 | resex 6019 |
. . . . . . . . . . . . 13
β’ (π‘ βΎ (1...π)) β V |
19 | | fveq1 6880 |
. . . . . . . . . . . . . 14
β’ (π = (π‘ βΎ (1...π)) β (πβπ) = ((π‘ βΎ (1...π))βπ)) |
20 | 19 | sbcco3gw 4414 |
. . . . . . . . . . . . 13
β’ ((π‘ βΎ (1...π)) β V β ([(π‘ βΎ (1...π)) / π][(πβπ) / π£][(π‘βπΏ) / π€]π β [((π‘ βΎ (1...π))βπ) / π£][(π‘βπΏ) / π€]π)) |
21 | 18, 20 | ax-mp 5 |
. . . . . . . . . . . 12
β’
([(π‘ βΎ
(1...π)) / π][(πβπ) / π£][(π‘βπΏ) / π€]π β [((π‘ βΎ (1...π))βπ) / π£][(π‘βπΏ) / π€]π) |
22 | | nn0p1nn 12508 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β (π + 1) β
β) |
23 | 3, 22 | eqeltrid 2829 |
. . . . . . . . . . . . . 14
β’ (π β β0
β π β
β) |
24 | | elfz1end 13528 |
. . . . . . . . . . . . . 14
β’ (π β β β π β (1...π)) |
25 | 23, 24 | sylib 217 |
. . . . . . . . . . . . 13
β’ (π β β0
β π β (1...π)) |
26 | | fvres 6900 |
. . . . . . . . . . . . 13
β’ (π β (1...π) β ((π‘ βΎ (1...π))βπ) = (π‘βπ)) |
27 | | dfsbcq 3771 |
. . . . . . . . . . . . 13
β’ (((π‘ βΎ (1...π))βπ) = (π‘βπ) β ([((π‘ βΎ (1...π))βπ) / π£][(π‘βπΏ) / π€]π β [(π‘βπ) / π£][(π‘βπΏ) / π€]π)) |
28 | 25, 26, 27 | 3syl 18 |
. . . . . . . . . . . 12
β’ (π β β0
β ([((π‘ βΎ
(1...π))βπ) / π£][(π‘βπΏ) / π€]π β [(π‘βπ) / π£][(π‘βπΏ) / π€]π)) |
29 | 21, 28 | bitrid 283 |
. . . . . . . . . . 11
β’ (π β β0
β ([(π‘ βΎ
(1...π)) / π][(πβπ) / π£][(π‘βπΏ) / π€]π β [(π‘βπ) / π£][(π‘βπΏ) / π€]π)) |
30 | 29 | sbcbidv 3828 |
. . . . . . . . . 10
β’ (π β β0
β ([(π‘ βΎ
(1...π)) / π’][(π‘ βΎ (1...π)) / π][(πβπ) / π£][(π‘βπΏ) / π€]π β [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€]π)) |
31 | 16, 30 | bitrid 283 |
. . . . . . . . 9
β’ (π β β0
β ([((π‘ βΎ
(1...π)) βΎ (1...π)) / π’][(π‘ βΎ (1...π)) / π][(πβπ) / π£][(π‘βπΏ) / π€]π β [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€]π)) |
32 | 10, 31 | bitrid 283 |
. . . . . . . 8
β’ (π β β0
β ([(π‘ βΎ
(1...π)) / π][(π βΎ (1...π)) / π’][(πβπ) / π£][(π‘βπΏ) / π€]π β [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€]π)) |
33 | 8, 32 | bitr2id 284 |
. . . . . . 7
β’ (π β β0
β ([(π‘ βΎ
(1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€]π β [(π‘ βΎ (1...π)) / π][(π‘βπΏ) / π€][(π βΎ (1...π)) / π’][(πβπ) / π£]π)) |
34 | 33 | rabbidv 3432 |
. . . . . 6
β’ (π β β0
β {π‘ β
(β0 βm (1...πΏ)) β£ [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€]π} = {π‘ β (β0
βm (1...πΏ))
β£ [(π‘ βΎ
(1...π)) / π][(π‘βπΏ) / π€][(π βΎ (1...π)) / π’][(πβπ) / π£]π}) |
35 | 34 | eleq1d 2810 |
. . . . 5
β’ (π β β0
β ({π‘ β
(β0 βm (1...πΏ)) β£ [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€]π} β (DiophβπΏ) β {π‘ β (β0
βm (1...πΏ))
β£ [(π‘ βΎ
(1...π)) / π][(π‘βπΏ) / π€][(π βΎ (1...π)) / π’][(πβπ) / π£]π} β (DiophβπΏ))) |
36 | 35 | biimpa 476 |
. . . 4
β’ ((π β β0
β§ {π‘ β
(β0 βm (1...πΏ)) β£ [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€]π} β (DiophβπΏ)) β {π‘ β (β0
βm (1...πΏ))
β£ [(π‘ βΎ
(1...π)) / π][(π‘βπΏ) / π€][(π βΎ (1...π)) / π’][(πβπ) / π£]π} β (DiophβπΏ)) |
37 | | rexfrabdioph.2 |
. . . . 5
β’ πΏ = (π + 1) |
38 | 37 | rexfrabdioph 42022 |
. . . 4
β’ ((π β β0
β§ {π‘ β
(β0 βm (1...πΏ)) β£ [(π‘ βΎ (1...π)) / π][(π‘βπΏ) / π€][(π βΎ (1...π)) / π’][(πβπ) / π£]π} β (DiophβπΏ)) β {π β (β0
βm (1...π))
β£ βπ€ β
β0 [(π βΎ (1...π)) / π’][(πβπ) / π£]π} β (Diophβπ)) |
39 | 6, 36, 38 | syl2anc 583 |
. . 3
β’ ((π β β0
β§ {π‘ β
(β0 βm (1...πΏ)) β£ [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€]π} β (DiophβπΏ)) β {π β (β0
βm (1...π))
β£ βπ€ β
β0 [(π βΎ (1...π)) / π’][(πβπ) / π£]π} β (Diophβπ)) |
40 | 2, 39 | eqeltrid 2829 |
. 2
β’ ((π β β0
β§ {π‘ β
(β0 βm (1...πΏ)) β£ [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€]π} β (DiophβπΏ)) β {π β (β0
βm (1...π))
β£ [(π βΎ
(1...π)) / π’][(πβπ) / π£]βπ€ β β0 π} β (Diophβπ)) |
41 | 3 | rexfrabdioph 42022 |
. 2
β’ ((π β β0
β§ {π β
(β0 βm (1...π)) β£ [(π βΎ (1...π)) / π’][(πβπ) / π£]βπ€ β β0 π} β (Diophβπ)) β {π’ β (β0
βm (1...π))
β£ βπ£ β
β0 βπ€ β β0 π} β (Diophβπ)) |
42 | 40, 41 | syldan 590 |
1
β’ ((π β β0
β§ {π‘ β
(β0 βm (1...πΏ)) β£ [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€]π} β (DiophβπΏ)) β {π’ β (β0
βm (1...π))
β£ βπ£ β
β0 βπ€ β β0 π} β (Diophβπ)) |