Step | Hyp | Ref
| Expression |
1 | | wallispilem5.1 |
. . 3
β’ πΉ = (π β β β¦ (((2 Β· π) / ((2 Β· π) β 1)) Β· ((2
Β· π) / ((2 Β·
π) + 1)))) |
2 | | wallispilem5.2 |
. . 3
β’ πΌ = (π β β0 β¦
β«(0(,)Ο)((sinβπ₯)βπ) dπ₯) |
3 | | wallispilem5.3 |
. . 3
β’ πΊ = (π β β β¦ ((πΌβ(2 Β· π)) / (πΌβ((2 Β· π) + 1)))) |
4 | | wallispilem5.4 |
. . 3
β’ π» = (π β β β¦ ((Ο / 2) Β·
(1 / (seq1( Β· , πΉ)βπ)))) |
5 | 1, 2, 3, 4 | wallispilem4 44395 |
. 2
β’ πΊ = π» |
6 | | nnuz 12811 |
. . . 4
β’ β =
(β€β₯β1) |
7 | | 1zzd 12539 |
. . . 4
β’ (β€
β 1 β β€) |
8 | | wallispilem5.5 |
. . . . 5
β’ πΏ = (π β β β¦ (((2 Β· π) + 1) / (2 Β· π))) |
9 | | 2cnd 12236 |
. . . . 5
β’ (β€
β 2 β β) |
10 | | 2ne0 12262 |
. . . . . 6
β’ 2 β
0 |
11 | 10 | a1i 11 |
. . . . 5
β’ (β€
β 2 β 0) |
12 | | 1cnd 11155 |
. . . . 5
β’ (β€
β 1 β β) |
13 | 8, 9, 11, 12 | clim1fr1 43928 |
. . . 4
β’ (β€
β πΏ β
1) |
14 | | nnex 12164 |
. . . . . . 7
β’ β
β V |
15 | 14 | mptex 7174 |
. . . . . 6
β’ (π β β β¦ ((πΌβ(2 Β· π)) / (πΌβ((2 Β· π) + 1)))) β V |
16 | 3, 15 | eqeltri 2830 |
. . . . 5
β’ πΊ β V |
17 | 16 | a1i 11 |
. . . 4
β’ (β€
β πΊ β
V) |
18 | | 2nn0 12435 |
. . . . . . . . . . . 12
β’ 2 β
β0 |
19 | 18 | a1i 11 |
. . . . . . . . . . 11
β’ (π β β β 2 β
β0) |
20 | | nnnn0 12425 |
. . . . . . . . . . 11
β’ (π β β β π β
β0) |
21 | 19, 20 | nn0mulcld 12483 |
. . . . . . . . . 10
β’ (π β β β (2
Β· π) β
β0) |
22 | | 1nn0 12434 |
. . . . . . . . . . 11
β’ 1 β
β0 |
23 | 22 | a1i 11 |
. . . . . . . . . 10
β’ (π β β β 1 β
β0) |
24 | 21, 23 | nn0addcld 12482 |
. . . . . . . . 9
β’ (π β β β ((2
Β· π) + 1) β
β0) |
25 | 24 | nn0red 12479 |
. . . . . . . 8
β’ (π β β β ((2
Β· π) + 1) β
β) |
26 | 21 | nn0red 12479 |
. . . . . . . 8
β’ (π β β β (2
Β· π) β
β) |
27 | | 2cnd 12236 |
. . . . . . . . 9
β’ (π β β β 2 β
β) |
28 | | nncn 12166 |
. . . . . . . . 9
β’ (π β β β π β
β) |
29 | 10 | a1i 11 |
. . . . . . . . 9
β’ (π β β β 2 β
0) |
30 | | nnne0 12192 |
. . . . . . . . 9
β’ (π β β β π β 0) |
31 | 27, 28, 29, 30 | mulne0d 11812 |
. . . . . . . 8
β’ (π β β β (2
Β· π) β
0) |
32 | 25, 26, 31 | redivcld 11988 |
. . . . . . 7
β’ (π β β β (((2
Β· π) + 1) / (2
Β· π)) β
β) |
33 | 8, 32 | fmpti 7061 |
. . . . . 6
β’ πΏ:ββΆβ |
34 | 33 | a1i 11 |
. . . . 5
β’ (β€
β πΏ:ββΆβ) |
35 | 34 | ffvelcdmda 7036 |
. . . 4
β’
((β€ β§ π
β β) β (πΏβπ) β β) |
36 | 2 | wallispilem3 44394 |
. . . . . . . . . 10
β’ ((2
Β· π) β
β0 β (πΌβ(2 Β· π)) β
β+) |
37 | 21, 36 | syl 17 |
. . . . . . . . 9
β’ (π β β β (πΌβ(2 Β· π)) β
β+) |
38 | 37 | rpred 12962 |
. . . . . . . 8
β’ (π β β β (πΌβ(2 Β· π)) β
β) |
39 | 2 | wallispilem3 44394 |
. . . . . . . . 9
β’ (((2
Β· π) + 1) β
β0 β (πΌβ((2 Β· π) + 1)) β
β+) |
40 | 24, 39 | syl 17 |
. . . . . . . 8
β’ (π β β β (πΌβ((2 Β· π) + 1)) β
β+) |
41 | 38, 40 | rerpdivcld 12993 |
. . . . . . 7
β’ (π β β β ((πΌβ(2 Β· π)) / (πΌβ((2 Β· π) + 1))) β β) |
42 | 3, 41 | fmpti 7061 |
. . . . . 6
β’ πΊ:ββΆβ |
43 | 42 | a1i 11 |
. . . . 5
β’ (β€
β πΊ:ββΆβ) |
44 | 43 | ffvelcdmda 7036 |
. . . 4
β’
((β€ β§ π
β β) β (πΊβπ) β β) |
45 | 18 | a1i 11 |
. . . . . . . . . . 11
β’ (π β β β 2 β
β0) |
46 | | nnnn0 12425 |
. . . . . . . . . . 11
β’ (π β β β π β
β0) |
47 | 45, 46 | nn0mulcld 12483 |
. . . . . . . . . 10
β’ (π β β β (2
Β· π) β
β0) |
48 | 2 | wallispilem3 44394 |
. . . . . . . . . 10
β’ ((2
Β· π) β
β0 β (πΌβ(2 Β· π)) β
β+) |
49 | 47, 48 | syl 17 |
. . . . . . . . 9
β’ (π β β β (πΌβ(2 Β· π)) β
β+) |
50 | 49 | rpred 12962 |
. . . . . . . 8
β’ (π β β β (πΌβ(2 Β· π)) β
β) |
51 | | 2nn 12231 |
. . . . . . . . . . . . 13
β’ 2 β
β |
52 | 51 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β β β 2 β
β) |
53 | | id 22 |
. . . . . . . . . . . 12
β’ (π β β β π β
β) |
54 | 52, 53 | nnmulcld 12211 |
. . . . . . . . . . 11
β’ (π β β β (2
Β· π) β
β) |
55 | | nnm1nn0 12459 |
. . . . . . . . . . 11
β’ ((2
Β· π) β β
β ((2 Β· π)
β 1) β β0) |
56 | 54, 55 | syl 17 |
. . . . . . . . . 10
β’ (π β β β ((2
Β· π) β 1)
β β0) |
57 | 2 | wallispilem3 44394 |
. . . . . . . . . 10
β’ (((2
Β· π) β 1)
β β0 β (πΌβ((2 Β· π) β 1)) β
β+) |
58 | 56, 57 | syl 17 |
. . . . . . . . 9
β’ (π β β β (πΌβ((2 Β· π) β 1)) β
β+) |
59 | 58 | rpred 12962 |
. . . . . . . 8
β’ (π β β β (πΌβ((2 Β· π) β 1)) β
β) |
60 | 22 | a1i 11 |
. . . . . . . . . 10
β’ (π β β β 1 β
β0) |
61 | 47, 60 | nn0addcld 12482 |
. . . . . . . . 9
β’ (π β β β ((2
Β· π) + 1) β
β0) |
62 | 2 | wallispilem3 44394 |
. . . . . . . . 9
β’ (((2
Β· π) + 1) β
β0 β (πΌβ((2 Β· π) + 1)) β
β+) |
63 | 61, 62 | syl 17 |
. . . . . . . 8
β’ (π β β β (πΌβ((2 Β· π) + 1)) β
β+) |
64 | | 2cnd 12236 |
. . . . . . . . . . . 12
β’ (π β β β 2 β
β) |
65 | | nncn 12166 |
. . . . . . . . . . . 12
β’ (π β β β π β
β) |
66 | 64, 65 | mulcld 11180 |
. . . . . . . . . . 11
β’ (π β β β (2
Β· π) β
β) |
67 | | 1cnd 11155 |
. . . . . . . . . . 11
β’ (π β β β 1 β
β) |
68 | 66, 67 | npcand 11521 |
. . . . . . . . . 10
β’ (π β β β (((2
Β· π) β 1) + 1)
= (2 Β· π)) |
69 | 68 | fveq2d 6847 |
. . . . . . . . 9
β’ (π β β β (πΌβ(((2 Β· π) β 1) + 1)) = (πΌβ(2 Β· π))) |
70 | 2, 56 | wallispilem1 44392 |
. . . . . . . . 9
β’ (π β β β (πΌβ(((2 Β· π) β 1) + 1)) β€ (πΌβ((2 Β· π) β 1))) |
71 | 69, 70 | eqbrtrrd 5130 |
. . . . . . . 8
β’ (π β β β (πΌβ(2 Β· π)) β€ (πΌβ((2 Β· π) β 1))) |
72 | 50, 59, 63, 71 | lediv1dd 13020 |
. . . . . . 7
β’ (π β β β ((πΌβ(2 Β· π)) / (πΌβ((2 Β· π) + 1))) β€ ((πΌβ((2 Β· π) β 1)) / (πΌβ((2 Β· π) + 1)))) |
73 | 66, 67 | addcld 11179 |
. . . . . . . . . 10
β’ (π β β β ((2
Β· π) + 1) β
β) |
74 | 10 | a1i 11 |
. . . . . . . . . . 11
β’ (π β β β 2 β
0) |
75 | | nnne0 12192 |
. . . . . . . . . . 11
β’ (π β β β π β 0) |
76 | 64, 65, 74, 75 | mulne0d 11812 |
. . . . . . . . . 10
β’ (π β β β (2
Β· π) β
0) |
77 | 73, 66, 76 | divcld 11936 |
. . . . . . . . 9
β’ (π β β β (((2
Β· π) + 1) / (2
Β· π)) β
β) |
78 | 63 | rpcnd 12964 |
. . . . . . . . 9
β’ (π β β β (πΌβ((2 Β· π) + 1)) β
β) |
79 | 63 | rpne0d 12967 |
. . . . . . . . 9
β’ (π β β β (πΌβ((2 Β· π) + 1)) β 0) |
80 | 77, 78, 79 | divcan4d 11942 |
. . . . . . . 8
β’ (π β β β (((((2
Β· π) + 1) / (2
Β· π)) Β·
(πΌβ((2 Β· π) + 1))) / (πΌβ((2 Β· π) + 1))) = (((2 Β· π) + 1) / (2 Β· π))) |
81 | | 2re 12232 |
. . . . . . . . . . . . . . . 16
β’ 2 β
β |
82 | 81 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β β β 2 β
β) |
83 | | nnre 12165 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β π β
β) |
84 | 82, 83 | remulcld 11190 |
. . . . . . . . . . . . . . . 16
β’ (π β β β (2
Β· π) β
β) |
85 | | 1red 11161 |
. . . . . . . . . . . . . . . 16
β’ (π β β β 1 β
β) |
86 | 84, 85 | readdcld 11189 |
. . . . . . . . . . . . . . 15
β’ (π β β β ((2
Β· π) + 1) β
β) |
87 | 45 | nn0ge0d 12481 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β 0 β€
2) |
88 | | nnge1 12186 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β 1 β€
π) |
89 | 82, 83, 87, 88 | lemulge11d 12097 |
. . . . . . . . . . . . . . . 16
β’ (π β β β 2 β€ (2
Β· π)) |
90 | 84 | ltp1d 12090 |
. . . . . . . . . . . . . . . 16
β’ (π β β β (2
Β· π) < ((2
Β· π) +
1)) |
91 | 82, 84, 86, 89, 90 | lelttrd 11318 |
. . . . . . . . . . . . . . 15
β’ (π β β β 2 <
((2 Β· π) +
1)) |
92 | 82, 86, 91 | ltled 11308 |
. . . . . . . . . . . . . 14
β’ (π β β β 2 β€
((2 Β· π) +
1)) |
93 | 45 | nn0zd 12530 |
. . . . . . . . . . . . . . 15
β’ (π β β β 2 β
β€) |
94 | 61 | nn0zd 12530 |
. . . . . . . . . . . . . . 15
β’ (π β β β ((2
Β· π) + 1) β
β€) |
95 | | eluz 12782 |
. . . . . . . . . . . . . . 15
β’ ((2
β β€ β§ ((2 Β· π) + 1) β β€) β (((2 Β·
π) + 1) β
(β€β₯β2) β 2 β€ ((2 Β· π) + 1))) |
96 | 93, 94, 95 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β β β (((2
Β· π) + 1) β
(β€β₯β2) β 2 β€ ((2 Β· π) + 1))) |
97 | 92, 96 | mpbird 257 |
. . . . . . . . . . . . 13
β’ (π β β β ((2
Β· π) + 1) β
(β€β₯β2)) |
98 | 2, 97 | itgsinexp 44282 |
. . . . . . . . . . . 12
β’ (π β β β (πΌβ((2 Β· π) + 1)) = (((((2 Β· π) + 1) β 1) / ((2 Β·
π) + 1)) Β· (πΌβ(((2 Β· π) + 1) β
2)))) |
99 | 66, 67 | pncand 11518 |
. . . . . . . . . . . . . 14
β’ (π β β β (((2
Β· π) + 1) β 1)
= (2 Β· π)) |
100 | 99 | oveq1d 7373 |
. . . . . . . . . . . . 13
β’ (π β β β ((((2
Β· π) + 1) β 1)
/ ((2 Β· π) + 1)) =
((2 Β· π) / ((2
Β· π) +
1))) |
101 | | 1e2m1 12285 |
. . . . . . . . . . . . . . . . 17
β’ 1 = (2
β 1) |
102 | 101 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β β β 1 = (2
β 1)) |
103 | 102 | oveq2d 7374 |
. . . . . . . . . . . . . . 15
β’ (π β β β ((2
Β· π) β 1) =
((2 Β· π) β (2
β 1))) |
104 | 66, 64, 67 | subsub3d 11547 |
. . . . . . . . . . . . . . 15
β’ (π β β β ((2
Β· π) β (2
β 1)) = (((2 Β· π) + 1) β 2)) |
105 | 103, 104 | eqtr2d 2774 |
. . . . . . . . . . . . . 14
β’ (π β β β (((2
Β· π) + 1) β 2)
= ((2 Β· π) β
1)) |
106 | 105 | fveq2d 6847 |
. . . . . . . . . . . . 13
β’ (π β β β (πΌβ(((2 Β· π) + 1) β 2)) = (πΌβ((2 Β· π) β 1))) |
107 | 100, 106 | oveq12d 7376 |
. . . . . . . . . . . 12
β’ (π β β β (((((2
Β· π) + 1) β 1)
/ ((2 Β· π) + 1))
Β· (πΌβ(((2
Β· π) + 1) β
2))) = (((2 Β· π) /
((2 Β· π) + 1))
Β· (πΌβ((2
Β· π) β
1)))) |
108 | 98, 107 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (π β β β (πΌβ((2 Β· π) + 1)) = (((2 Β· π) / ((2 Β· π) + 1)) Β· (πΌβ((2 Β· π) β 1)))) |
109 | 108 | oveq2d 7374 |
. . . . . . . . . 10
β’ (π β β β ((((2
Β· π) + 1) / (2
Β· π)) Β·
(πΌβ((2 Β· π) + 1))) = ((((2 Β· π) + 1) / (2 Β· π)) Β· (((2 Β· π) / ((2 Β· π) + 1)) Β· (πΌβ((2 Β· π) β
1))))) |
110 | 54 | peano2nnd 12175 |
. . . . . . . . . . . . 13
β’ (π β β β ((2
Β· π) + 1) β
β) |
111 | 110 | nnne0d 12208 |
. . . . . . . . . . . 12
β’ (π β β β ((2
Β· π) + 1) β
0) |
112 | 66, 73, 111 | divcld 11936 |
. . . . . . . . . . 11
β’ (π β β β ((2
Β· π) / ((2 Β·
π) + 1)) β
β) |
113 | 58 | rpcnd 12964 |
. . . . . . . . . . 11
β’ (π β β β (πΌβ((2 Β· π) β 1)) β
β) |
114 | 77, 112, 113 | mulassd 11183 |
. . . . . . . . . 10
β’ (π β β β (((((2
Β· π) + 1) / (2
Β· π)) Β· ((2
Β· π) / ((2 Β·
π) + 1))) Β· (πΌβ((2 Β· π) β 1))) = ((((2 Β·
π) + 1) / (2 Β· π)) Β· (((2 Β· π) / ((2 Β· π) + 1)) Β· (πΌβ((2 Β· π) β
1))))) |
115 | 73, 66, 111, 76 | divcan6d 11955 |
. . . . . . . . . . . 12
β’ (π β β β ((((2
Β· π) + 1) / (2
Β· π)) Β· ((2
Β· π) / ((2 Β·
π) + 1))) =
1) |
116 | 115 | oveq1d 7373 |
. . . . . . . . . . 11
β’ (π β β β (((((2
Β· π) + 1) / (2
Β· π)) Β· ((2
Β· π) / ((2 Β·
π) + 1))) Β· (πΌβ((2 Β· π) β 1))) = (1 Β·
(πΌβ((2 Β· π) β 1)))) |
117 | 113 | mulid2d 11178 |
. . . . . . . . . . 11
β’ (π β β β (1
Β· (πΌβ((2
Β· π) β 1))) =
(πΌβ((2 Β· π) β 1))) |
118 | 116, 117 | eqtrd 2773 |
. . . . . . . . . 10
β’ (π β β β (((((2
Β· π) + 1) / (2
Β· π)) Β· ((2
Β· π) / ((2 Β·
π) + 1))) Β· (πΌβ((2 Β· π) β 1))) = (πΌβ((2 Β· π) β 1))) |
119 | 109, 114,
118 | 3eqtr2d 2779 |
. . . . . . . . 9
β’ (π β β β ((((2
Β· π) + 1) / (2
Β· π)) Β·
(πΌβ((2 Β· π) + 1))) = (πΌβ((2 Β· π) β 1))) |
120 | 119 | oveq1d 7373 |
. . . . . . . 8
β’ (π β β β (((((2
Β· π) + 1) / (2
Β· π)) Β·
(πΌβ((2 Β· π) + 1))) / (πΌβ((2 Β· π) + 1))) = ((πΌβ((2 Β· π) β 1)) / (πΌβ((2 Β· π) + 1)))) |
121 | 80, 120 | eqtr3d 2775 |
. . . . . . 7
β’ (π β β β (((2
Β· π) + 1) / (2
Β· π)) = ((πΌβ((2 Β· π) β 1)) / (πΌβ((2 Β· π) + 1)))) |
122 | 72, 121 | breqtrrd 5134 |
. . . . . 6
β’ (π β β β ((πΌβ(2 Β· π)) / (πΌβ((2 Β· π) + 1))) β€ (((2 Β· π) + 1) / (2 Β· π))) |
123 | 49, 63 | rpdivcld 12979 |
. . . . . . 7
β’ (π β β β ((πΌβ(2 Β· π)) / (πΌβ((2 Β· π) + 1))) β
β+) |
124 | | nfcv 2904 |
. . . . . . . 8
β’
β²ππ |
125 | | nfmpt1 5214 |
. . . . . . . . . . 11
β’
β²π(π β β0 β¦
β«(0(,)Ο)((sinβπ₯)βπ) dπ₯) |
126 | 2, 125 | nfcxfr 2902 |
. . . . . . . . . 10
β’
β²ππΌ |
127 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²π(2
Β· π) |
128 | 126, 127 | nffv 6853 |
. . . . . . . . 9
β’
β²π(πΌβ(2 Β· π)) |
129 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π
/ |
130 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²π((2
Β· π) +
1) |
131 | 126, 130 | nffv 6853 |
. . . . . . . . 9
β’
β²π(πΌβ((2 Β· π) + 1)) |
132 | 128, 129,
131 | nfov 7388 |
. . . . . . . 8
β’
β²π((πΌβ(2 Β· π)) / (πΌβ((2 Β· π) + 1))) |
133 | | oveq2 7366 |
. . . . . . . . . 10
β’ (π = π β (2 Β· π) = (2 Β· π)) |
134 | 133 | fveq2d 6847 |
. . . . . . . . 9
β’ (π = π β (πΌβ(2 Β· π)) = (πΌβ(2 Β· π))) |
135 | 133 | fvoveq1d 7380 |
. . . . . . . . 9
β’ (π = π β (πΌβ((2 Β· π) + 1)) = (πΌβ((2 Β· π) + 1))) |
136 | 134, 135 | oveq12d 7376 |
. . . . . . . 8
β’ (π = π β ((πΌβ(2 Β· π)) / (πΌβ((2 Β· π) + 1))) = ((πΌβ(2 Β· π)) / (πΌβ((2 Β· π) + 1)))) |
137 | 124, 132,
136, 3 | fvmptf 6970 |
. . . . . . 7
β’ ((π β β β§ ((πΌβ(2 Β· π)) / (πΌβ((2 Β· π) + 1))) β β+) β
(πΊβπ) = ((πΌβ(2 Β· π)) / (πΌβ((2 Β· π) + 1)))) |
138 | 123, 137 | mpdan 686 |
. . . . . 6
β’ (π β β β (πΊβπ) = ((πΌβ(2 Β· π)) / (πΌβ((2 Β· π) + 1)))) |
139 | 8 | a1i 11 |
. . . . . . 7
β’ (π β β β πΏ = (π β β β¦ (((2 Β· π) + 1) / (2 Β· π)))) |
140 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β β β§ π = π) β π = π) |
141 | 140 | oveq2d 7374 |
. . . . . . . . 9
β’ ((π β β β§ π = π) β (2 Β· π) = (2 Β· π)) |
142 | 141 | oveq1d 7373 |
. . . . . . . 8
β’ ((π β β β§ π = π) β ((2 Β· π) + 1) = ((2 Β· π) + 1)) |
143 | 142, 141 | oveq12d 7376 |
. . . . . . 7
β’ ((π β β β§ π = π) β (((2 Β· π) + 1) / (2 Β· π)) = (((2 Β· π) + 1) / (2 Β· π))) |
144 | 139, 143,
53, 77 | fvmptd 6956 |
. . . . . 6
β’ (π β β β (πΏβπ) = (((2 Β· π) + 1) / (2 Β· π))) |
145 | 122, 138,
144 | 3brtr4d 5138 |
. . . . 5
β’ (π β β β (πΊβπ) β€ (πΏβπ)) |
146 | 145 | adantl 483 |
. . . 4
β’
((β€ β§ π
β β) β (πΊβπ) β€ (πΏβπ)) |
147 | 78, 79 | dividd 11934 |
. . . . . . 7
β’ (π β β β ((πΌβ((2 Β· π) + 1)) / (πΌβ((2 Β· π) + 1))) = 1) |
148 | 63 | rpred 12962 |
. . . . . . . 8
β’ (π β β β (πΌβ((2 Β· π) + 1)) β
β) |
149 | 2, 47 | wallispilem1 44392 |
. . . . . . . 8
β’ (π β β β (πΌβ((2 Β· π) + 1)) β€ (πΌβ(2 Β· π))) |
150 | 148, 50, 63, 149 | lediv1dd 13020 |
. . . . . . 7
β’ (π β β β ((πΌβ((2 Β· π) + 1)) / (πΌβ((2 Β· π) + 1))) β€ ((πΌβ(2 Β· π)) / (πΌβ((2 Β· π) + 1)))) |
151 | 147, 150 | eqbrtrrd 5130 |
. . . . . 6
β’ (π β β β 1 β€
((πΌβ(2 Β· π)) / (πΌβ((2 Β· π) + 1)))) |
152 | 151, 138 | breqtrrd 5134 |
. . . . 5
β’ (π β β β 1 β€
(πΊβπ)) |
153 | 152 | adantl 483 |
. . . 4
β’
((β€ β§ π
β β) β 1 β€ (πΊβπ)) |
154 | 6, 7, 13, 17, 35, 44, 146, 153 | climsqz2 15530 |
. . 3
β’ (β€
β πΊ β
1) |
155 | 154 | mptru 1549 |
. 2
β’ πΊ β 1 |
156 | 5, 155 | eqbrtrri 5129 |
1
β’ π» β 1 |