Step | Hyp | Ref
| Expression |
1 | | iinhoiicclem.f |
. . . 4
β’ (π β πΉ β β©
π β β Xπ β
π (π΄[,)(π΅ + (1 / π)))) |
2 | 1 | elexd 3464 |
. . 3
β’ (π β πΉ β V) |
3 | | 1nn 12169 |
. . . . . . . . 9
β’ 1 β
β |
4 | 3 | a1i 11 |
. . . . . . . 8
β’ (π β 1 β
β) |
5 | | iinhoiicclem.k |
. . . . . . . . 9
β’
β²ππ |
6 | | iinhoiicclem.a |
. . . . . . . . . 10
β’ ((π β§ π β π) β π΄ β β) |
7 | | iinhoiicclem.b |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β π΅ β β) |
8 | | peano2re 11333 |
. . . . . . . . . . . 12
β’ (π΅ β β β (π΅ + 1) β
β) |
9 | 7, 8 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (π΅ + 1) β β) |
10 | 9 | rexrd 11210 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (π΅ + 1) β
β*) |
11 | | icossre 13351 |
. . . . . . . . . 10
β’ ((π΄ β β β§ (π΅ + 1) β
β*) β (π΄[,)(π΅ + 1)) β β) |
12 | 6, 10, 11 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π β π) β (π΄[,)(π΅ + 1)) β β) |
13 | 5, 12 | ixpssixp 43390 |
. . . . . . . 8
β’ (π β Xπ β
π (π΄[,)(π΅ + 1)) β Xπ β π β) |
14 | | oveq2 7366 |
. . . . . . . . . . . . . 14
β’ (π = 1 β (1 / π) = (1 / 1)) |
15 | | 1div1e1 11850 |
. . . . . . . . . . . . . . 15
β’ (1 / 1) =
1 |
16 | 15 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π = 1 β (1 / 1) =
1) |
17 | 14, 16 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ (π = 1 β (1 / π) = 1) |
18 | 17 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ (π = 1 β (π΅ + (1 / π)) = (π΅ + 1)) |
19 | 18 | oveq2d 7374 |
. . . . . . . . . . 11
β’ (π = 1 β (π΄[,)(π΅ + (1 / π))) = (π΄[,)(π΅ + 1))) |
20 | 19 | ixpeq2dv 8854 |
. . . . . . . . . 10
β’ (π = 1 β Xπ β
π (π΄[,)(π΅ + (1 / π))) = Xπ β π (π΄[,)(π΅ + 1))) |
21 | 20 | sseq1d 3976 |
. . . . . . . . 9
β’ (π = 1 β (Xπ β
π (π΄[,)(π΅ + (1 / π))) β Xπ β π β β Xπ β
π (π΄[,)(π΅ + 1)) β Xπ β π β)) |
22 | 21 | rspcev 3580 |
. . . . . . . 8
β’ ((1
β β β§ Xπ β π (π΄[,)(π΅ + 1)) β Xπ β π β) β βπ β β Xπ β π (π΄[,)(π΅ + (1 / π))) β Xπ β π β) |
23 | 4, 13, 22 | syl2anc 585 |
. . . . . . 7
β’ (π β βπ β β Xπ β π (π΄[,)(π΅ + (1 / π))) β Xπ β π β) |
24 | | iinss 5017 |
. . . . . . 7
β’
(βπ β
β Xπ β π (π΄[,)(π΅ + (1 / π))) β Xπ β π β β β© π β β Xπ β π (π΄[,)(π΅ + (1 / π))) β Xπ β π β) |
25 | 23, 24 | syl 17 |
. . . . . 6
β’ (π β β© π β β Xπ β π (π΄[,)(π΅ + (1 / π))) β Xπ β π β) |
26 | 25, 1 | sseldd 3946 |
. . . . 5
β’ (π β πΉ β Xπ β π β) |
27 | | elixpconstg 43387 |
. . . . . 6
β’ (πΉ β β© π β β Xπ β π (π΄[,)(π΅ + (1 / π))) β (πΉ β Xπ β π β β πΉ:πβΆβ)) |
28 | 1, 27 | syl 17 |
. . . . 5
β’ (π β (πΉ β Xπ β π β β πΉ:πβΆβ)) |
29 | 26, 28 | mpbid 231 |
. . . 4
β’ (π β πΉ:πβΆβ) |
30 | 29 | ffnd 6670 |
. . 3
β’ (π β πΉ Fn π) |
31 | 29 | ffvelcdmda 7036 |
. . . . . 6
β’ ((π β§ π β π) β (πΉβπ) β β) |
32 | 6 | rexrd 11210 |
. . . . . . 7
β’ ((π β§ π β π) β π΄ β
β*) |
33 | | ssid 3967 |
. . . . . . . . . . . . 13
β’ Xπ β
π (π΄[,)(π΅ + 1)) β Xπ β π (π΄[,)(π΅ + 1)) |
34 | 33 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β Xπ β
π (π΄[,)(π΅ + 1)) β Xπ β π (π΄[,)(π΅ + 1))) |
35 | 20 | sseq1d 3976 |
. . . . . . . . . . . . 13
β’ (π = 1 β (Xπ β
π (π΄[,)(π΅ + (1 / π))) β Xπ β π (π΄[,)(π΅ + 1)) β Xπ β π (π΄[,)(π΅ + 1)) β Xπ β π (π΄[,)(π΅ + 1)))) |
36 | 35 | rspcev 3580 |
. . . . . . . . . . . 12
β’ ((1
β β β§ Xπ β π (π΄[,)(π΅ + 1)) β Xπ β π (π΄[,)(π΅ + 1))) β βπ β β Xπ β π (π΄[,)(π΅ + (1 / π))) β Xπ β π (π΄[,)(π΅ + 1))) |
37 | 4, 34, 36 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β βπ β β Xπ β π (π΄[,)(π΅ + (1 / π))) β Xπ β π (π΄[,)(π΅ + 1))) |
38 | | iinss 5017 |
. . . . . . . . . . 11
β’
(βπ β
β Xπ β π (π΄[,)(π΅ + (1 / π))) β Xπ β π (π΄[,)(π΅ + 1)) β β© π β β Xπ β π (π΄[,)(π΅ + (1 / π))) β Xπ β π (π΄[,)(π΅ + 1))) |
39 | 37, 38 | syl 17 |
. . . . . . . . . 10
β’ (π β β© π β β Xπ β π (π΄[,)(π΅ + (1 / π))) β Xπ β π (π΄[,)(π΅ + 1))) |
40 | 39, 1 | sseldd 3946 |
. . . . . . . . 9
β’ (π β πΉ β Xπ β π (π΄[,)(π΅ + 1))) |
41 | 40 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β π) β πΉ β Xπ β π (π΄[,)(π΅ + 1))) |
42 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β π) β π β π) |
43 | | fvixp2 43507 |
. . . . . . . 8
β’ ((πΉ β Xπ β
π (π΄[,)(π΅ + 1)) β§ π β π) β (πΉβπ) β (π΄[,)(π΅ + 1))) |
44 | 41, 42, 43 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π β π) β (πΉβπ) β (π΄[,)(π΅ + 1))) |
45 | | icogelb 13321 |
. . . . . . 7
β’ ((π΄ β β*
β§ (π΅ + 1) β
β* β§ (πΉβπ) β (π΄[,)(π΅ + 1))) β π΄ β€ (πΉβπ)) |
46 | 32, 10, 44, 45 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ π β π) β π΄ β€ (πΉβπ)) |
47 | 31 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β β) β (πΉβπ) β β) |
48 | 7 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π β β) β π΅ β β) |
49 | | nnrecre 12200 |
. . . . . . . . . . 11
β’ (π β β β (1 /
π) β
β) |
50 | 49 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π β β) β (1 / π) β
β) |
51 | 48, 50 | readdcld 11189 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β β) β (π΅ + (1 / π)) β β) |
52 | 32 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π β β) β π΄ β
β*) |
53 | | ressxr 11204 |
. . . . . . . . . . 11
β’ β
β β* |
54 | 53, 51 | sselid 3943 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π β β) β (π΅ + (1 / π)) β
β*) |
55 | | eliin 4960 |
. . . . . . . . . . . . . . . . 17
β’ (πΉ β V β (πΉ β β© π β β Xπ β π (π΄[,)(π΅ + (1 / π))) β βπ β β πΉ β Xπ β π (π΄[,)(π΅ + (1 / π))))) |
56 | 2, 55 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β (πΉ β β©
π β β Xπ β
π (π΄[,)(π΅ + (1 / π))) β βπ β β πΉ β Xπ β π (π΄[,)(π΅ + (1 / π))))) |
57 | 1, 56 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ (π β βπ β β πΉ β Xπ β π (π΄[,)(π΅ + (1 / π)))) |
58 | 57 | r19.21bi 3233 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β πΉ β Xπ β π (π΄[,)(π΅ + (1 / π)))) |
59 | | elixp2 8842 |
. . . . . . . . . . . . . 14
β’ (πΉ β Xπ β
π (π΄[,)(π΅ + (1 / π))) β (πΉ β V β§ πΉ Fn π β§ βπ β π (πΉβπ) β (π΄[,)(π΅ + (1 / π))))) |
60 | 58, 59 | sylib 217 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (πΉ β V β§ πΉ Fn π β§ βπ β π (πΉβπ) β (π΄[,)(π΅ + (1 / π))))) |
61 | 60 | simp3d 1145 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β βπ β π (πΉβπ) β (π΄[,)(π΅ + (1 / π)))) |
62 | 61 | r19.21bi 3233 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β π) β (πΉβπ) β (π΄[,)(π΅ + (1 / π)))) |
63 | 62 | an32s 651 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π β β) β (πΉβπ) β (π΄[,)(π΅ + (1 / π)))) |
64 | | icoltub 43832 |
. . . . . . . . . 10
β’ ((π΄ β β*
β§ (π΅ + (1 / π)) β β*
β§ (πΉβπ) β (π΄[,)(π΅ + (1 / π)))) β (πΉβπ) < (π΅ + (1 / π))) |
65 | 52, 54, 63, 64 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β β) β (πΉβπ) < (π΅ + (1 / π))) |
66 | 47, 51, 65 | ltled 11308 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π β β) β (πΉβπ) β€ (π΅ + (1 / π))) |
67 | 66 | ralrimiva 3140 |
. . . . . . 7
β’ ((π β§ π β π) β βπ β β (πΉβπ) β€ (π΅ + (1 / π))) |
68 | | nfv 1918 |
. . . . . . . 8
β’
β²π(π β§ π β π) |
69 | 53, 31 | sselid 3943 |
. . . . . . . 8
β’ ((π β§ π β π) β (πΉβπ) β
β*) |
70 | 68, 69, 7 | xrralrecnnle 43704 |
. . . . . . 7
β’ ((π β§ π β π) β ((πΉβπ) β€ π΅ β βπ β β (πΉβπ) β€ (π΅ + (1 / π)))) |
71 | 67, 70 | mpbird 257 |
. . . . . 6
β’ ((π β§ π β π) β (πΉβπ) β€ π΅) |
72 | 6, 7, 31, 46, 71 | eliccd 43828 |
. . . . 5
β’ ((π β§ π β π) β (πΉβπ) β (π΄[,]π΅)) |
73 | 72 | ex 414 |
. . . 4
β’ (π β (π β π β (πΉβπ) β (π΄[,]π΅))) |
74 | 5, 73 | ralrimi 3239 |
. . 3
β’ (π β βπ β π (πΉβπ) β (π΄[,]π΅)) |
75 | 2, 30, 74 | 3jca 1129 |
. 2
β’ (π β (πΉ β V β§ πΉ Fn π β§ βπ β π (πΉβπ) β (π΄[,]π΅))) |
76 | | elixp2 8842 |
. 2
β’ (πΉ β Xπ β
π (π΄[,]π΅) β (πΉ β V β§ πΉ Fn π β§ βπ β π (πΉβπ) β (π΄[,]π΅))) |
77 | 75, 76 | sylibr 233 |
1
β’ (π β πΉ β Xπ β π (π΄[,]π΅)) |