Step | Hyp | Ref
| Expression |
1 | | fveq2 6846 |
. . . . . . 7
β’ (π = π β (πβπ) = (πβπ)) |
2 | 1 | fveq1d 6848 |
. . . . . 6
β’ (π = π β ((πβπ)βπ¦) = ((πβπ)βπ¦)) |
3 | | eqid 2733 |
. . . . . 6
β’ (π β β β¦ ((πβπ)βπ¦)) = (π β β β¦ ((πβπ)βπ¦)) |
4 | | fvex 6859 |
. . . . . 6
β’ ((πβπ)βπ¦) β V |
5 | 2, 3, 4 | fvmpt 6952 |
. . . . 5
β’ (π β β β ((π β β β¦ ((πβπ)βπ¦))βπ) = ((πβπ)βπ¦)) |
6 | 5 | ad2antlr 726 |
. . . 4
β’ (((π β§ π β β) β§ π¦ β β) β ((π β β β¦ ((πβπ)βπ¦))βπ) = ((πβπ)βπ¦)) |
7 | | nnuz 12814 |
. . . . 5
β’ β =
(β€β₯β1) |
8 | | simplr 768 |
. . . . 5
β’ (((π β§ π β β) β§ π¦ β β) β π β β) |
9 | | itg2i1fseq.5 |
. . . . . . 7
β’ (π β βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯)) |
10 | | fveq2 6846 |
. . . . . . . . . 10
β’ (π₯ = π¦ β ((πβπ)βπ₯) = ((πβπ)βπ¦)) |
11 | 10 | mpteq2dv 5211 |
. . . . . . . . 9
β’ (π₯ = π¦ β (π β β β¦ ((πβπ)βπ₯)) = (π β β β¦ ((πβπ)βπ¦))) |
12 | | fveq2 6846 |
. . . . . . . . 9
β’ (π₯ = π¦ β (πΉβπ₯) = (πΉβπ¦)) |
13 | 11, 12 | breq12d 5122 |
. . . . . . . 8
β’ (π₯ = π¦ β ((π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯) β (π β β β¦ ((πβπ)βπ¦)) β (πΉβπ¦))) |
14 | 13 | rspccva 3582 |
. . . . . . 7
β’
((βπ₯ β
β (π β β
β¦ ((πβπ)βπ₯)) β (πΉβπ₯) β§ π¦ β β) β (π β β β¦ ((πβπ)βπ¦)) β (πΉβπ¦)) |
15 | 9, 14 | sylan 581 |
. . . . . 6
β’ ((π β§ π¦ β β) β (π β β β¦ ((πβπ)βπ¦)) β (πΉβπ¦)) |
16 | 15 | adantlr 714 |
. . . . 5
β’ (((π β§ π β β) β§ π¦ β β) β (π β β β¦ ((πβπ)βπ¦)) β (πΉβπ¦)) |
17 | | fveq2 6846 |
. . . . . . . . . 10
β’ (π = π β (πβπ) = (πβπ)) |
18 | 17 | fveq1d 6848 |
. . . . . . . . 9
β’ (π = π β ((πβπ)βπ¦) = ((πβπ)βπ¦)) |
19 | | fvex 6859 |
. . . . . . . . 9
β’ ((πβπ)βπ¦) β V |
20 | 18, 3, 19 | fvmpt 6952 |
. . . . . . . 8
β’ (π β β β ((π β β β¦ ((πβπ)βπ¦))βπ) = ((πβπ)βπ¦)) |
21 | 20 | adantl 483 |
. . . . . . 7
β’ (((π β§ π¦ β β) β§ π β β) β ((π β β β¦ ((πβπ)βπ¦))βπ) = ((πβπ)βπ¦)) |
22 | | itg2i1fseq.3 |
. . . . . . . . . . 11
β’ (π β π:ββΆdom
β«1) |
23 | 22 | ffvelcdmda 7039 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πβπ) β dom
β«1) |
24 | | i1ff 25063 |
. . . . . . . . . 10
β’ ((πβπ) β dom β«1 β (πβπ):ββΆβ) |
25 | 23, 24 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πβπ):ββΆβ) |
26 | 25 | ffvelcdmda 7039 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π¦ β β) β ((πβπ)βπ¦) β β) |
27 | 26 | an32s 651 |
. . . . . . 7
β’ (((π β§ π¦ β β) β§ π β β) β ((πβπ)βπ¦) β β) |
28 | 21, 27 | eqeltrd 2834 |
. . . . . 6
β’ (((π β§ π¦ β β) β§ π β β) β ((π β β β¦ ((πβπ)βπ¦))βπ) β β) |
29 | 28 | adantllr 718 |
. . . . 5
β’ ((((π β§ π β β) β§ π¦ β β) β§ π β β) β ((π β β β¦ ((πβπ)βπ¦))βπ) β β) |
30 | | itg2i1fseq.4 |
. . . . . . . . . . . 12
β’ (π β βπ β β (0π
βr β€ (πβπ) β§ (πβπ) βr β€ (πβ(π + 1)))) |
31 | | simpr 486 |
. . . . . . . . . . . . 13
β’
((0π βr β€ (πβπ) β§ (πβπ) βr β€ (πβ(π + 1))) β (πβπ) βr β€ (πβ(π + 1))) |
32 | 31 | ralimi 3083 |
. . . . . . . . . . . 12
β’
(βπ β
β (0π βr β€ (πβπ) β§ (πβπ) βr β€ (πβ(π + 1))) β βπ β β (πβπ) βr β€ (πβ(π + 1))) |
33 | 30, 32 | syl 17 |
. . . . . . . . . . 11
β’ (π β βπ β β (πβπ) βr β€ (πβ(π + 1))) |
34 | | fvoveq1 7384 |
. . . . . . . . . . . . 13
β’ (π = π β (πβ(π + 1)) = (πβ(π + 1))) |
35 | 17, 34 | breq12d 5122 |
. . . . . . . . . . . 12
β’ (π = π β ((πβπ) βr β€ (πβ(π + 1)) β (πβπ) βr β€ (πβ(π + 1)))) |
36 | 35 | rspccva 3582 |
. . . . . . . . . . 11
β’
((βπ β
β (πβπ) βr β€
(πβ(π + 1)) β§ π β β) β (πβπ) βr β€ (πβ(π + 1))) |
37 | 33, 36 | sylan 581 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πβπ) βr β€ (πβ(π + 1))) |
38 | | ffn 6672 |
. . . . . . . . . . . 12
β’ ((πβπ):ββΆβ β (πβπ) Fn β) |
39 | 23, 24, 38 | 3syl 18 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (πβπ) Fn β) |
40 | | peano2nn 12173 |
. . . . . . . . . . . . 13
β’ (π β β β (π + 1) β
β) |
41 | | ffvelcdm 7036 |
. . . . . . . . . . . . 13
β’ ((π:ββΆdom
β«1 β§ (π
+ 1) β β) β (πβ(π + 1)) β dom
β«1) |
42 | 22, 40, 41 | syl2an 597 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (πβ(π + 1)) β dom
β«1) |
43 | | i1ff 25063 |
. . . . . . . . . . . 12
β’ ((πβ(π + 1)) β dom β«1 β
(πβ(π +
1)):ββΆβ) |
44 | | ffn 6672 |
. . . . . . . . . . . 12
β’ ((πβ(π + 1)):ββΆβ β (πβ(π + 1)) Fn β) |
45 | 42, 43, 44 | 3syl 18 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (πβ(π + 1)) Fn β) |
46 | | reex 11150 |
. . . . . . . . . . . 12
β’ β
β V |
47 | 46 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β β β
V) |
48 | | inidm 4182 |
. . . . . . . . . . 11
β’ (β
β© β) = β |
49 | | eqidd 2734 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π¦ β β) β ((πβπ)βπ¦) = ((πβπ)βπ¦)) |
50 | | eqidd 2734 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π¦ β β) β ((πβ(π + 1))βπ¦) = ((πβ(π + 1))βπ¦)) |
51 | 39, 45, 47, 47, 48, 49, 50 | ofrfval 7631 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((πβπ) βr β€ (πβ(π + 1)) β βπ¦ β β ((πβπ)βπ¦) β€ ((πβ(π + 1))βπ¦))) |
52 | 37, 51 | mpbid 231 |
. . . . . . . . 9
β’ ((π β§ π β β) β βπ¦ β β ((πβπ)βπ¦) β€ ((πβ(π + 1))βπ¦)) |
53 | 52 | r19.21bi 3233 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π¦ β β) β ((πβπ)βπ¦) β€ ((πβ(π + 1))βπ¦)) |
54 | 53 | an32s 651 |
. . . . . . 7
β’ (((π β§ π¦ β β) β§ π β β) β ((πβπ)βπ¦) β€ ((πβ(π + 1))βπ¦)) |
55 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π = (π + 1) β (πβπ) = (πβ(π + 1))) |
56 | 55 | fveq1d 6848 |
. . . . . . . . . 10
β’ (π = (π + 1) β ((πβπ)βπ¦) = ((πβ(π + 1))βπ¦)) |
57 | | fvex 6859 |
. . . . . . . . . 10
β’ ((πβ(π + 1))βπ¦) β V |
58 | 56, 3, 57 | fvmpt 6952 |
. . . . . . . . 9
β’ ((π + 1) β β β
((π β β β¦
((πβπ)βπ¦))β(π + 1)) = ((πβ(π + 1))βπ¦)) |
59 | 40, 58 | syl 17 |
. . . . . . . 8
β’ (π β β β ((π β β β¦ ((πβπ)βπ¦))β(π + 1)) = ((πβ(π + 1))βπ¦)) |
60 | 59 | adantl 483 |
. . . . . . 7
β’ (((π β§ π¦ β β) β§ π β β) β ((π β β β¦ ((πβπ)βπ¦))β(π + 1)) = ((πβ(π + 1))βπ¦)) |
61 | 54, 21, 60 | 3brtr4d 5141 |
. . . . . 6
β’ (((π β§ π¦ β β) β§ π β β) β ((π β β β¦ ((πβπ)βπ¦))βπ) β€ ((π β β β¦ ((πβπ)βπ¦))β(π + 1))) |
62 | 61 | adantllr 718 |
. . . . 5
β’ ((((π β§ π β β) β§ π¦ β β) β§ π β β) β ((π β β β¦ ((πβπ)βπ¦))βπ) β€ ((π β β β¦ ((πβπ)βπ¦))β(π + 1))) |
63 | 7, 8, 16, 29, 62 | climub 15555 |
. . . 4
β’ (((π β§ π β β) β§ π¦ β β) β ((π β β β¦ ((πβπ)βπ¦))βπ) β€ (πΉβπ¦)) |
64 | 6, 63 | eqbrtrrd 5133 |
. . 3
β’ (((π β§ π β β) β§ π¦ β β) β ((πβπ)βπ¦) β€ (πΉβπ¦)) |
65 | 64 | ralrimiva 3140 |
. 2
β’ ((π β§ π β β) β βπ¦ β β ((πβπ)βπ¦) β€ (πΉβπ¦)) |
66 | 22 | ffvelcdmda 7039 |
. . . 4
β’ ((π β§ π β β) β (πβπ) β dom
β«1) |
67 | | i1ff 25063 |
. . . 4
β’ ((πβπ) β dom β«1 β (πβπ):ββΆβ) |
68 | | ffn 6672 |
. . . 4
β’ ((πβπ):ββΆβ β (πβπ) Fn β) |
69 | 66, 67, 68 | 3syl 18 |
. . 3
β’ ((π β§ π β β) β (πβπ) Fn β) |
70 | | itg2i1fseq.2 |
. . . . 5
β’ (π β πΉ:ββΆ(0[,)+β)) |
71 | 70 | ffnd 6673 |
. . . 4
β’ (π β πΉ Fn β) |
72 | 71 | adantr 482 |
. . 3
β’ ((π β§ π β β) β πΉ Fn β) |
73 | 46 | a1i 11 |
. . 3
β’ ((π β§ π β β) β β β
V) |
74 | | eqidd 2734 |
. . 3
β’ (((π β§ π β β) β§ π¦ β β) β ((πβπ)βπ¦) = ((πβπ)βπ¦)) |
75 | | eqidd 2734 |
. . 3
β’ (((π β§ π β β) β§ π¦ β β) β (πΉβπ¦) = (πΉβπ¦)) |
76 | 69, 72, 73, 73, 48, 74, 75 | ofrfval 7631 |
. 2
β’ ((π β§ π β β) β ((πβπ) βr β€ πΉ β βπ¦ β β ((πβπ)βπ¦) β€ (πΉβπ¦))) |
77 | 65, 76 | mpbird 257 |
1
β’ ((π β§ π β β) β (πβπ) βr β€ πΉ) |