Step | Hyp | Ref
| Expression |
1 | | sbc4rex 41141 |
. . . . . . . 8
β’
([(πβπΏ) / π€]βπ₯ β β0 βπ¦ β β0
βπ§ β
β0 βπ β β0 π β βπ₯ β β0 βπ¦ β β0
βπ§ β
β0 βπ β β0 [(πβπΏ) / π€]π) |
2 | 1 | sbcbii 3804 |
. . . . . . 7
β’
([(πβπ) / π£][(πβπΏ) / π€]βπ₯ β β0 βπ¦ β β0
βπ§ β
β0 βπ β β0 π β [(πβπ) / π£]βπ₯ β β0 βπ¦ β β0
βπ§ β
β0 βπ β β0 [(πβπΏ) / π€]π) |
3 | | sbc4rex 41141 |
. . . . . . 7
β’
([(πβπ) / π£]βπ₯ β β0 βπ¦ β β0
βπ§ β
β0 βπ β β0 [(πβπΏ) / π€]π β βπ₯ β β0 βπ¦ β β0
βπ§ β
β0 βπ β β0 [(πβπ) / π£][(πβπΏ) / π€]π) |
4 | 2, 3 | bitri 275 |
. . . . . 6
β’
([(πβπ) / π£][(πβπΏ) / π€]βπ₯ β β0 βπ¦ β β0
βπ§ β
β0 βπ β β0 π β βπ₯ β β0 βπ¦ β β0
βπ§ β
β0 βπ β β0 [(πβπ) / π£][(πβπΏ) / π€]π) |
5 | 4 | sbcbii 3804 |
. . . . 5
β’
([(π βΎ
(1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]βπ₯ β β0 βπ¦ β β0
βπ§ β
β0 βπ β β0 π β [(π βΎ (1...π)) / π’]βπ₯ β β0 βπ¦ β β0
βπ§ β
β0 βπ β β0 [(πβπ) / π£][(πβπΏ) / π€]π) |
6 | | sbc4rex 41141 |
. . . . 5
β’
([(π βΎ
(1...π)) / π’]βπ₯ β β0
βπ¦ β
β0 βπ§ β β0 βπ β β0
[(πβπ) / π£][(πβπΏ) / π€]π β βπ₯ β β0 βπ¦ β β0
βπ§ β
β0 βπ β β0 [(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]π) |
7 | 5, 6 | bitri 275 |
. . . 4
β’
([(π βΎ
(1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]βπ₯ β β0 βπ¦ β β0
βπ§ β
β0 βπ β β0 π β βπ₯ β β0 βπ¦ β β0
βπ§ β
β0 βπ β β0 [(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]π) |
8 | 7 | rabbii 3416 |
. . 3
β’ {π β (β0
βm (1...πΏ))
β£ [(π βΎ
(1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]βπ₯ β β0 βπ¦ β β0
βπ§ β
β0 βπ β β0 π} = {π β (β0
βm (1...πΏ))
β£ βπ₯ β
β0 βπ¦ β β0 βπ§ β β0
βπ β
β0 [(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]π} |
9 | | rexfrabdioph.2 |
. . . . . . 7
β’ πΏ = (π + 1) |
10 | | rexfrabdioph.1 |
. . . . . . . . 9
β’ π = (π + 1) |
11 | | nn0p1nn 12459 |
. . . . . . . . 9
β’ (π β β0
β (π + 1) β
β) |
12 | 10, 11 | eqeltrid 2842 |
. . . . . . . 8
β’ (π β β0
β π β
β) |
13 | 12 | peano2nnd 12177 |
. . . . . . 7
β’ (π β β0
β (π + 1) β
β) |
14 | 9, 13 | eqeltrid 2842 |
. . . . . 6
β’ (π β β0
β πΏ β
β) |
15 | 14 | nnnn0d 12480 |
. . . . 5
β’ (π β β0
β πΏ β
β0) |
16 | 15 | adantr 482 |
. . . 4
β’ ((π β β0
β§ {π‘ β
(β0 βm (1...π»)) β£ [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π} β (Diophβπ»)) β πΏ β
β0) |
17 | | sbcrot5 41144 |
. . . . . . . . . . . . 13
β’
([(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π β [(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π][(πβπΏ) / π€]π) |
18 | 17 | sbcbii 3804 |
. . . . . . . . . . . 12
β’
([(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π β [(πβπ) / π£][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π][(πβπΏ) / π€]π) |
19 | | sbcrot5 41144 |
. . . . . . . . . . . 12
β’
([(πβπ) / π£][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π][(πβπΏ) / π€]π β [(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π][(πβπ) / π£][(πβπΏ) / π€]π) |
20 | 18, 19 | bitri 275 |
. . . . . . . . . . 11
β’
([(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π β [(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π][(πβπ) / π£][(πβπΏ) / π€]π) |
21 | 20 | sbcbii 3804 |
. . . . . . . . . 10
β’
([(π βΎ
(1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π β [(π βΎ (1...π)) / π’][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π][(πβπ) / π£][(πβπΏ) / π€]π) |
22 | | sbcrot5 41144 |
. . . . . . . . . 10
β’
([(π βΎ
(1...π)) / π’][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π][(πβπ) / π£][(πβπΏ) / π€]π β [(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π][(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]π) |
23 | 21, 22 | bitri 275 |
. . . . . . . . 9
β’
([(π βΎ
(1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π β [(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π][(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]π) |
24 | 23 | sbcbii 3804 |
. . . . . . . 8
β’
([(π‘ βΎ
(1...πΏ)) / π][(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π β [(π‘ βΎ (1...πΏ)) / π][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π][(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]π) |
25 | | reseq1 5936 |
. . . . . . . . . 10
β’ (π = (π‘ βΎ (1...πΏ)) β (π βΎ (1...π)) = ((π‘ βΎ (1...πΏ)) βΎ (1...π))) |
26 | 25 | sbccomieg 41145 |
. . . . . . . . 9
β’
([(π‘ βΎ
(1...πΏ)) / π][(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π β [((π‘ βΎ (1...πΏ)) βΎ (1...π)) / π’][(π‘ βΎ (1...πΏ)) / π][(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π) |
27 | | fzssp1 13491 |
. . . . . . . . . . . . 13
β’
(1...π) β
(1...(π +
1)) |
28 | 10 | oveq2i 7373 |
. . . . . . . . . . . . 13
β’
(1...π) =
(1...(π +
1)) |
29 | 27, 28 | sseqtrri 3986 |
. . . . . . . . . . . 12
β’
(1...π) β
(1...π) |
30 | | fzssp1 13491 |
. . . . . . . . . . . . 13
β’
(1...π) β
(1...(π +
1)) |
31 | 9 | oveq2i 7373 |
. . . . . . . . . . . . 13
β’
(1...πΏ) =
(1...(π +
1)) |
32 | 30, 31 | sseqtrri 3986 |
. . . . . . . . . . . 12
β’
(1...π) β
(1...πΏ) |
33 | 29, 32 | sstri 3958 |
. . . . . . . . . . 11
β’
(1...π) β
(1...πΏ) |
34 | | resabs1 5972 |
. . . . . . . . . . 11
β’
((1...π) β
(1...πΏ) β ((π‘ βΎ (1...πΏ)) βΎ (1...π)) = (π‘ βΎ (1...π))) |
35 | | dfsbcq 3746 |
. . . . . . . . . . 11
β’ (((π‘ βΎ (1...πΏ)) βΎ (1...π)) = (π‘ βΎ (1...π)) β ([((π‘ βΎ (1...πΏ)) βΎ (1...π)) / π’][(π‘ βΎ (1...πΏ)) / π][(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π β [(π‘ βΎ (1...π)) / π’][(π‘ βΎ (1...πΏ)) / π][(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π)) |
36 | 33, 34, 35 | mp2b 10 |
. . . . . . . . . 10
β’
([((π‘ βΎ
(1...πΏ)) βΎ (1...π)) / π’][(π‘ βΎ (1...πΏ)) / π][(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π β [(π‘ βΎ (1...π)) / π’][(π‘ βΎ (1...πΏ)) / π][(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π) |
37 | | fveq1 6846 |
. . . . . . . . . . . . 13
β’ (π = (π‘ βΎ (1...πΏ)) β (πβπ) = ((π‘ βΎ (1...πΏ))βπ)) |
38 | 37 | sbccomieg 41145 |
. . . . . . . . . . . 12
β’
([(π‘ βΎ
(1...πΏ)) / π][(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π β [((π‘ βΎ (1...πΏ))βπ) / π£][(π‘ βΎ (1...πΏ)) / π][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π) |
39 | | elfz1end 13478 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β (1...π)) |
40 | 12, 39 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β π β (1...π)) |
41 | 32, 40 | sselid 3947 |
. . . . . . . . . . . . . 14
β’ (π β β0
β π β (1...πΏ)) |
42 | | fvres 6866 |
. . . . . . . . . . . . . 14
β’ (π β (1...πΏ) β ((π‘ βΎ (1...πΏ))βπ) = (π‘βπ)) |
43 | | dfsbcq 3746 |
. . . . . . . . . . . . . 14
β’ (((π‘ βΎ (1...πΏ))βπ) = (π‘βπ) β ([((π‘ βΎ (1...πΏ))βπ) / π£][(π‘ βΎ (1...πΏ)) / π][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π β [(π‘βπ) / π£][(π‘ βΎ (1...πΏ)) / π][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π)) |
44 | 41, 42, 43 | 3syl 18 |
. . . . . . . . . . . . 13
β’ (π β β0
β ([((π‘ βΎ
(1...πΏ))βπ) / π£][(π‘ βΎ (1...πΏ)) / π][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π β [(π‘βπ) / π£][(π‘ βΎ (1...πΏ)) / π][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π)) |
45 | | vex 3452 |
. . . . . . . . . . . . . . . . 17
β’ π‘ β V |
46 | 45 | resex 5990 |
. . . . . . . . . . . . . . . 16
β’ (π‘ βΎ (1...πΏ)) β V |
47 | | fveq1 6846 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π‘ βΎ (1...πΏ)) β (πβπΏ) = ((π‘ βΎ (1...πΏ))βπΏ)) |
48 | 47 | sbcco3gw 4387 |
. . . . . . . . . . . . . . . 16
β’ ((π‘ βΎ (1...πΏ)) β V β ([(π‘ βΎ (1...πΏ)) / π][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π β [((π‘ βΎ (1...πΏ))βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π)) |
49 | 46, 48 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’
([(π‘ βΎ
(1...πΏ)) / π][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π β [((π‘ βΎ (1...πΏ))βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π) |
50 | | elfz1end 13478 |
. . . . . . . . . . . . . . . . 17
β’ (πΏ β β β πΏ β (1...πΏ)) |
51 | 14, 50 | sylib 217 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β πΏ β (1...πΏ)) |
52 | | fvres 6866 |
. . . . . . . . . . . . . . . 16
β’ (πΏ β (1...πΏ) β ((π‘ βΎ (1...πΏ))βπΏ) = (π‘βπΏ)) |
53 | | dfsbcq 3746 |
. . . . . . . . . . . . . . . 16
β’ (((π‘ βΎ (1...πΏ))βπΏ) = (π‘βπΏ) β ([((π‘ βΎ (1...πΏ))βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π β [(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π)) |
54 | 51, 52, 53 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β ([((π‘ βΎ
(1...πΏ))βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π β [(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π)) |
55 | 49, 54 | bitrid 283 |
. . . . . . . . . . . . . 14
β’ (π β β0
β ([(π‘ βΎ
(1...πΏ)) / π][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π β [(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π)) |
56 | 55 | sbcbidv 3803 |
. . . . . . . . . . . . 13
β’ (π β β0
β ([(π‘βπ) / π£][(π‘ βΎ (1...πΏ)) / π][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π β [(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π)) |
57 | 44, 56 | bitrd 279 |
. . . . . . . . . . . 12
β’ (π β β0
β ([((π‘ βΎ
(1...πΏ))βπ) / π£][(π‘ βΎ (1...πΏ)) / π][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π β [(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π)) |
58 | 38, 57 | bitrid 283 |
. . . . . . . . . . 11
β’ (π β β0
β ([(π‘ βΎ
(1...πΏ)) / π][(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π β [(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π)) |
59 | 58 | sbcbidv 3803 |
. . . . . . . . . 10
β’ (π β β0
β ([(π‘ βΎ
(1...π)) / π’][(π‘ βΎ (1...πΏ)) / π][(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π β [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π)) |
60 | 36, 59 | bitrid 283 |
. . . . . . . . 9
β’ (π β β0
β ([((π‘ βΎ
(1...πΏ)) βΎ (1...π)) / π’][(π‘ βΎ (1...πΏ)) / π][(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π β [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π)) |
61 | 26, 60 | bitrid 283 |
. . . . . . . 8
β’ (π β β0
β ([(π‘ βΎ
(1...πΏ)) / π][(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π β [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π)) |
62 | 24, 61 | bitr3id 285 |
. . . . . . 7
β’ (π β β0
β ([(π‘ βΎ
(1...πΏ)) / π][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π][(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]π β [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π)) |
63 | 62 | rabbidv 3418 |
. . . . . 6
β’ (π β β0
β {π‘ β
(β0 βm (1...π»)) β£ [(π‘ βΎ (1...πΏ)) / π][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π][(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]π} = {π‘ β (β0
βm (1...π»))
β£ [(π‘ βΎ
(1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π}) |
64 | 63 | eleq1d 2823 |
. . . . 5
β’ (π β β0
β ({π‘ β
(β0 βm (1...π»)) β£ [(π‘ βΎ (1...πΏ)) / π][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π][(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]π} β (Diophβπ») β {π‘ β (β0
βm (1...π»))
β£ [(π‘ βΎ
(1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π} β (Diophβπ»))) |
65 | 64 | biimpar 479 |
. . . 4
β’ ((π β β0
β§ {π‘ β
(β0 βm (1...π»)) β£ [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π} β (Diophβπ»)) β {π‘ β (β0
βm (1...π»))
β£ [(π‘ βΎ
(1...πΏ)) / π][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π][(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]π} β (Diophβπ»)) |
66 | | rexfrabdioph.3 |
. . . . 5
β’ πΎ = (πΏ + 1) |
67 | | rexfrabdioph.4 |
. . . . 5
β’ π½ = (πΎ + 1) |
68 | | rexfrabdioph.5 |
. . . . 5
β’ πΌ = (π½ + 1) |
69 | | rexfrabdioph.6 |
. . . . 5
β’ π» = (πΌ + 1) |
70 | 66, 67, 68, 69 | 4rexfrabdioph 41150 |
. . . 4
β’ ((πΏ β β0
β§ {π‘ β
(β0 βm (1...π»)) β£ [(π‘ βΎ (1...πΏ)) / π][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π][(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]π} β (Diophβπ»)) β {π β (β0
βm (1...πΏ))
β£ βπ₯ β
β0 βπ¦ β β0 βπ§ β β0
βπ β
β0 [(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]π} β (DiophβπΏ)) |
71 | 16, 65, 70 | syl2anc 585 |
. . 3
β’ ((π β β0
β§ {π‘ β
(β0 βm (1...π»)) β£ [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π} β (Diophβπ»)) β {π β (β0
βm (1...πΏ))
β£ βπ₯ β
β0 βπ¦ β β0 βπ§ β β0
βπ β
β0 [(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]π} β (DiophβπΏ)) |
72 | 8, 71 | eqeltrid 2842 |
. 2
β’ ((π β β0
β§ {π‘ β
(β0 βm (1...π»)) β£ [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π} β (Diophβπ»)) β {π β (β0
βm (1...πΏ))
β£ [(π βΎ
(1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]βπ₯ β β0 βπ¦ β β0
βπ§ β
β0 βπ β β0 π} β (DiophβπΏ)) |
73 | 10, 9 | 2rexfrabdioph 41148 |
. 2
β’ ((π β β0
β§ {π β
(β0 βm (1...πΏ)) β£ [(π βΎ (1...π)) / π’][(πβπ) / π£][(πβπΏ) / π€]βπ₯ β β0 βπ¦ β β0
βπ§ β
β0 βπ β β0 π} β (DiophβπΏ)) β {π’ β (β0
βm (1...π))
β£ βπ£ β
β0 βπ€ β β0 βπ₯ β β0
βπ¦ β
β0 βπ§ β β0 βπ β β0
π} β (Diophβπ)) |
74 | 72, 73 | syldan 592 |
1
β’ ((π β β0
β§ {π‘ β
(β0 βm (1...π»)) β£ [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π} β (Diophβπ»)) β {π’ β (β0
βm (1...π))
β£ βπ£ β
β0 βπ€ β β0 βπ₯ β β0
βπ¦ β
β0 βπ§ β β0 βπ β β0
π} β (Diophβπ)) |