Step | Hyp | Ref
| Expression |
1 | | oexpreposd.n |
. . . . 5
β’ (π β π β β) |
2 | 1 | adantr 480 |
. . . 4
β’ ((π β§ 0 < π) β π β β) |
3 | | oexpreposd.m |
. . . . . 6
β’ (π β π β β) |
4 | 3 | nnzd 12590 |
. . . . 5
β’ (π β π β β€) |
5 | 4 | adantr 480 |
. . . 4
β’ ((π β§ 0 < π) β π β β€) |
6 | | simpr 484 |
. . . 4
β’ ((π β§ 0 < π) β 0 < π) |
7 | | expgt0 14066 |
. . . 4
β’ ((π β β β§ π β β€ β§ 0 <
π) β 0 < (πβπ)) |
8 | 2, 5, 6, 7 | syl3anc 1370 |
. . 3
β’ ((π β§ 0 < π) β 0 < (πβπ)) |
9 | 8 | ex 412 |
. 2
β’ (π β (0 < π β 0 < (πβπ))) |
10 | | 0red 11222 |
. . . . 5
β’ (π β 0 β
β) |
11 | 10, 1 | lttrid 11357 |
. . . 4
β’ (π β (0 < π β Β¬ (0 = π β¨ π < 0))) |
12 | 11 | notbid 317 |
. . 3
β’ (π β (Β¬ 0 < π β Β¬ Β¬ (0 = π β¨ π < 0))) |
13 | | notnotr 130 |
. . . 4
β’ (Β¬
Β¬ (0 = π β¨ π < 0) β (0 = π β¨ π < 0)) |
14 | | 0re 11221 |
. . . . . . . . . 10
β’ 0 β
β |
15 | 14 | ltnri 11328 |
. . . . . . . . 9
β’ Β¬ 0
< 0 |
16 | 3 | 0expd 14109 |
. . . . . . . . . 10
β’ (π β (0βπ) = 0) |
17 | 16 | breq2d 5161 |
. . . . . . . . 9
β’ (π β (0 < (0βπ) β 0 <
0)) |
18 | 15, 17 | mtbiri 326 |
. . . . . . . 8
β’ (π β Β¬ 0 < (0βπ)) |
19 | 18 | adantr 480 |
. . . . . . 7
β’ ((π β§ 0 = π) β Β¬ 0 < (0βπ)) |
20 | | simpr 484 |
. . . . . . . . . 10
β’ ((π β§ 0 = π) β 0 = π) |
21 | 20 | eqcomd 2737 |
. . . . . . . . 9
β’ ((π β§ 0 = π) β π = 0) |
22 | 21 | oveq1d 7427 |
. . . . . . . 8
β’ ((π β§ 0 = π) β (πβπ) = (0βπ)) |
23 | 22 | breq2d 5161 |
. . . . . . 7
β’ ((π β§ 0 = π) β (0 < (πβπ) β 0 < (0βπ))) |
24 | 19, 23 | mtbird 324 |
. . . . . 6
β’ ((π β§ 0 = π) β Β¬ 0 < (πβπ)) |
25 | 24 | ex 412 |
. . . . 5
β’ (π β (0 = π β Β¬ 0 < (πβπ))) |
26 | 1 | renegcld 11646 |
. . . . . . . . . 10
β’ (π β -π β β) |
27 | 26 | adantr 480 |
. . . . . . . . 9
β’ ((π β§ 0 < -π) β -π β β) |
28 | 4 | adantr 480 |
. . . . . . . . 9
β’ ((π β§ 0 < -π) β π β β€) |
29 | | simpr 484 |
. . . . . . . . 9
β’ ((π β§ 0 < -π) β 0 < -π) |
30 | | expgt0 14066 |
. . . . . . . . 9
β’ ((-π β β β§ π β β€ β§ 0 <
-π) β 0 < (-πβπ)) |
31 | 27, 28, 29, 30 | syl3anc 1370 |
. . . . . . . 8
β’ ((π β§ 0 < -π) β 0 < (-πβπ)) |
32 | 31 | ex 412 |
. . . . . . 7
β’ (π β (0 < -π β 0 < (-πβπ))) |
33 | 1 | recnd 11247 |
. . . . . . . . . 10
β’ (π β π β β) |
34 | | oexpreposd.1 |
. . . . . . . . . . . 12
β’ (π β Β¬ (π / 2) β β) |
35 | | simpr 484 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π / 2) β β€) β (π / 2) β
β€) |
36 | | zq 12943 |
. . . . . . . . . . . . . . . . . 18
β’ ((π / 2) β β€ β
(π / 2) β
β) |
37 | 36 | adantl 481 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π / 2) β β€) β (π / 2) β
β) |
38 | | qden1elz 16698 |
. . . . . . . . . . . . . . . . 17
β’ ((π / 2) β β β
((denomβ(π / 2)) = 1
β (π / 2) β
β€)) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π / 2) β β€) β
((denomβ(π / 2)) = 1
β (π / 2) β
β€)) |
40 | 35, 39 | mpbird 256 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π / 2) β β€) β
(denomβ(π / 2)) =
1) |
41 | 40 | oveq2d 7428 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π / 2) β β€) β ((π / 2) Β·
(denomβ(π / 2))) =
((π / 2) Β·
1)) |
42 | | qmuldeneqnum 16688 |
. . . . . . . . . . . . . . 15
β’ ((π / 2) β β β
((π / 2) Β·
(denomβ(π / 2))) =
(numerβ(π /
2))) |
43 | 37, 42 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π / 2) β β€) β ((π / 2) Β·
(denomβ(π / 2))) =
(numerβ(π /
2))) |
44 | 35 | zcnd 12672 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π / 2) β β€) β (π / 2) β
β) |
45 | 44 | mulridd 11236 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π / 2) β β€) β ((π / 2) Β· 1) = (π / 2)) |
46 | 41, 43, 45 | 3eqtr3rd 2780 |
. . . . . . . . . . . . 13
β’ ((π β§ (π / 2) β β€) β (π / 2) = (numerβ(π / 2))) |
47 | 3 | nnred 12232 |
. . . . . . . . . . . . . . 15
β’ (π β π β β) |
48 | | 2re 12291 |
. . . . . . . . . . . . . . . 16
β’ 2 β
β |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β 2 β
β) |
50 | 3 | nngt0d 12266 |
. . . . . . . . . . . . . . 15
β’ (π β 0 < π) |
51 | | 2pos 12320 |
. . . . . . . . . . . . . . . 16
β’ 0 <
2 |
52 | 51 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β 0 < 2) |
53 | 47, 49, 50, 52 | divgt0d 12154 |
. . . . . . . . . . . . . 14
β’ (π β 0 < (π / 2)) |
54 | | qgt0numnn 16692 |
. . . . . . . . . . . . . 14
β’ (((π / 2) β β β§ 0
< (π / 2)) β
(numerβ(π / 2))
β β) |
55 | 36, 53, 54 | syl2anr 596 |
. . . . . . . . . . . . 13
β’ ((π β§ (π / 2) β β€) β
(numerβ(π / 2))
β β) |
56 | 46, 55 | eqeltrd 2832 |
. . . . . . . . . . . 12
β’ ((π β§ (π / 2) β β€) β (π / 2) β
β) |
57 | 34, 56 | mtand 813 |
. . . . . . . . . . 11
β’ (π β Β¬ (π / 2) β β€) |
58 | | evend2 16305 |
. . . . . . . . . . . 12
β’ (π β β€ β (2
β₯ π β (π / 2) β
β€)) |
59 | 4, 58 | syl 17 |
. . . . . . . . . . 11
β’ (π β (2 β₯ π β (π / 2) β β€)) |
60 | 57, 59 | mtbird 324 |
. . . . . . . . . 10
β’ (π β Β¬ 2 β₯ π) |
61 | | oexpneg 16293 |
. . . . . . . . . 10
β’ ((π β β β§ π β β β§ Β¬ 2
β₯ π) β (-πβπ) = -(πβπ)) |
62 | 33, 3, 60, 61 | syl3anc 1370 |
. . . . . . . . 9
β’ (π β (-πβπ) = -(πβπ)) |
63 | 62 | breq2d 5161 |
. . . . . . . 8
β’ (π β (0 < (-πβπ) β 0 < -(πβπ))) |
64 | 63 | biimpd 228 |
. . . . . . 7
β’ (π β (0 < (-πβπ) β 0 < -(πβπ))) |
65 | 3 | nnnn0d 12537 |
. . . . . . . . . . 11
β’ (π β π β
β0) |
66 | 1, 65 | reexpcld 14133 |
. . . . . . . . . 10
β’ (π β (πβπ) β β) |
67 | 66 | renegcld 11646 |
. . . . . . . . 9
β’ (π β -(πβπ) β β) |
68 | 10, 67 | lttrid 11357 |
. . . . . . . 8
β’ (π β (0 < -(πβπ) β Β¬ (0 = -(πβπ) β¨ -(πβπ) < 0))) |
69 | | pm2.46 880 |
. . . . . . . 8
β’ (Β¬ (0
= -(πβπ) β¨ -(πβπ) < 0) β Β¬ -(πβπ) < 0) |
70 | 68, 69 | syl6bi 252 |
. . . . . . 7
β’ (π β (0 < -(πβπ) β Β¬ -(πβπ) < 0)) |
71 | 32, 64, 70 | 3syld 60 |
. . . . . 6
β’ (π β (0 < -π β Β¬ -(πβπ) < 0)) |
72 | 1 | lt0neg1d 11788 |
. . . . . 6
β’ (π β (π < 0 β 0 < -π)) |
73 | 66 | lt0neg2d 11789 |
. . . . . . 7
β’ (π β (0 < (πβπ) β -(πβπ) < 0)) |
74 | 73 | notbid 317 |
. . . . . 6
β’ (π β (Β¬ 0 < (πβπ) β Β¬ -(πβπ) < 0)) |
75 | 71, 72, 74 | 3imtr4d 293 |
. . . . 5
β’ (π β (π < 0 β Β¬ 0 < (πβπ))) |
76 | 25, 75 | jaod 856 |
. . . 4
β’ (π β ((0 = π β¨ π < 0) β Β¬ 0 < (πβπ))) |
77 | 13, 76 | syl5 34 |
. . 3
β’ (π β (Β¬ Β¬ (0 = π β¨ π < 0) β Β¬ 0 < (πβπ))) |
78 | 12, 77 | sylbid 239 |
. 2
β’ (π β (Β¬ 0 < π β Β¬ 0 < (πβπ))) |
79 | 9, 78 | impcon4bid 226 |
1
β’ (π β (0 < π β 0 < (πβπ))) |