Proof of Theorem ang180lem1
Step | Hyp | Ref
| Expression |
1 | | picn 24211 |
. . . . . . 7
|
2 | | 2re 11090 |
. . . . . . . . . 10
|
3 | | pire 24210 |
. . . . . . . . . 10
|
4 | 2, 3 | remulcli 10054 |
. . . . . . . . 9
|
5 | 4 | recni 10052 |
. . . . . . . 8
|
6 | | 2pos 11112 |
. . . . . . . . . 10
|
7 | | pipos 24212 |
. . . . . . . . . 10
|
8 | 2, 3, 6, 7 | mulgt0ii 10170 |
. . . . . . . . 9
|
9 | 4, 8 | gt0ne0ii 10564 |
. . . . . . . 8
|
10 | 5, 9 | pm3.2i 471 |
. . . . . . 7
|
11 | | ax-icn 9995 |
. . . . . . . 8
|
12 | | ine0 10465 |
. . . . . . . 8
|
13 | 11, 12 | pm3.2i 471 |
. . . . . . 7
|
14 | | divcan5 10727 |
. . . . . . 7
|
15 | 1, 10, 13, 14 | mp3an 1424 |
. . . . . 6
|
16 | 3, 7 | gt0ne0ii 10564 |
. . . . . . 7
|
17 | | recdiv 10731 |
. . . . . . 7
|
18 | 5, 9, 1, 16, 17 | mp4an 709 |
. . . . . 6
|
19 | 2 | recni 10052 |
. . . . . . . 8
|
20 | 19, 1, 16 | divcan4i 10772 |
. . . . . . 7
|
21 | 20 | oveq2i 6661 |
. . . . . 6
|
22 | 15, 18, 21 | 3eqtr2i 2650 |
. . . . 5
|
23 | 22 | oveq2i 6661 |
. . . 4
|
24 | | ang180lem1.2 |
. . . . . 6
|
25 | | ax-1cn 9994 |
. . . . . . . . . . 11
|
26 | | simp1 1061 |
. . . . . . . . . . 11
|
27 | | subcl 10280 |
. . . . . . . . . . 11
|
28 | 25, 26, 27 | sylancr 695 |
. . . . . . . . . 10
|
29 | | simp3 1063 |
. . . . . . . . . . . 12
|
30 | 29 | necomd 2849 |
. . . . . . . . . . 11
|
31 | | subeq0 10307 |
. . . . . . . . . . . . 13
|
32 | 25, 26, 31 | sylancr 695 |
. . . . . . . . . . . 12
|
33 | 32 | necon3bid 2838 |
. . . . . . . . . . 11
|
34 | 30, 33 | mpbird 247 |
. . . . . . . . . 10
|
35 | 28, 34 | reccld 10794 |
. . . . . . . . 9
|
36 | 28, 34 | recne0d 10795 |
. . . . . . . . 9
|
37 | 35, 36 | logcld 24317 |
. . . . . . . 8
|
38 | | subcl 10280 |
. . . . . . . . . . 11
|
39 | 26, 25, 38 | sylancl 694 |
. . . . . . . . . 10
|
40 | | simp2 1062 |
. . . . . . . . . 10
|
41 | 39, 26, 40 | divcld 10801 |
. . . . . . . . 9
|
42 | | subeq0 10307 |
. . . . . . . . . . . . 13
|
43 | 26, 25, 42 | sylancl 694 |
. . . . . . . . . . . 12
|
44 | 43 | necon3bid 2838 |
. . . . . . . . . . 11
|
45 | 29, 44 | mpbird 247 |
. . . . . . . . . 10
|
46 | 39, 26, 45, 40 | divne0d 10817 |
. . . . . . . . 9
|
47 | 41, 46 | logcld 24317 |
. . . . . . . 8
|
48 | 37, 47 | addcld 10059 |
. . . . . . 7
|
49 | 26, 40 | logcld 24317 |
. . . . . . 7
|
50 | 48, 49 | addcld 10059 |
. . . . . 6
|
51 | 24, 50 | syl5eqel 2705 |
. . . . 5
|
52 | 11, 1 | mulcli 10045 |
. . . . . 6
|
53 | 52 | a1i 11 |
. . . . 5
|
54 | 11, 5 | mulcli 10045 |
. . . . . 6
|
55 | 54 | a1i 11 |
. . . . 5
|
56 | 11, 5, 12, 9 | mulne0i 10670 |
. . . . . 6
|
57 | 56 | a1i 11 |
. . . . 5
|
58 | 51, 53, 55, 57 | divsubdird 10840 |
. . . 4
|
59 | | ang180lem1.3 |
. . . . 5
|
60 | 13 | a1i 11 |
. . . . . . 7
|
61 | 10 | a1i 11 |
. . . . . . 7
|
62 | | divdiv1 10736 |
. . . . . . 7
|
63 | 51, 60, 61, 62 | syl3anc 1326 |
. . . . . 6
|
64 | 63 | oveq1d 6665 |
. . . . 5
|
65 | 59, 64 | syl5eq 2668 |
. . . 4
|
66 | 23, 58, 65 | 3eqtr4a 2682 |
. . 3
|
67 | | efsub 14830 |
. . . . . 6
|
68 | 51, 52, 67 | sylancl 694 |
. . . . 5
|
69 | | efipi 24225 |
. . . . . . 7
|
70 | 69 | oveq2i 6661 |
. . . . . 6
|
71 | 24 | fveq2i 6194 |
. . . . . . . . 9
|
72 | | efadd 14824 |
. . . . . . . . . . 11
|
73 | 48, 49, 72 | syl2anc 693 |
. . . . . . . . . 10
|
74 | | efadd 14824 |
. . . . . . . . . . . . 13
|
75 | 37, 47, 74 | syl2anc 693 |
. . . . . . . . . . . 12
|
76 | | eflog 24323 |
. . . . . . . . . . . . . 14
|
77 | 35, 36, 76 | syl2anc 693 |
. . . . . . . . . . . . 13
|
78 | | eflog 24323 |
. . . . . . . . . . . . . 14
|
79 | 41, 46, 78 | syl2anc 693 |
. . . . . . . . . . . . 13
|
80 | 77, 79 | oveq12d 6668 |
. . . . . . . . . . . 12
|
81 | 35, 41 | mulcomd 10061 |
. . . . . . . . . . . . 13
|
82 | 25 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
83 | 82, 28, 34 | div2negd 10816 |
. . . . . . . . . . . . . . 15
|
84 | | negsubdi2 10340 |
. . . . . . . . . . . . . . . . 17
|
85 | 25, 26, 84 | sylancr 695 |
. . . . . . . . . . . . . . . 16
|
86 | 85 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
87 | 83, 86 | eqtr3d 2658 |
. . . . . . . . . . . . . 14
|
88 | 87 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
89 | | neg1cn 11124 |
. . . . . . . . . . . . . . 15
|
90 | 89 | a1i 11 |
. . . . . . . . . . . . . 14
|
91 | 90, 39, 26, 45, 40 | dmdcand 10830 |
. . . . . . . . . . . . 13
|
92 | 81, 88, 91 | 3eqtrd 2660 |
. . . . . . . . . . . 12
|
93 | 75, 80, 92 | 3eqtrd 2660 |
. . . . . . . . . . 11
|
94 | | eflog 24323 |
. . . . . . . . . . . 12
|
95 | 26, 40, 94 | syl2anc 693 |
. . . . . . . . . . 11
|
96 | 93, 95 | oveq12d 6668 |
. . . . . . . . . 10
|
97 | 90, 26, 40 | divcan1d 10802 |
. . . . . . . . . 10
|
98 | 73, 96, 97 | 3eqtrd 2660 |
. . . . . . . . 9
|
99 | 71, 98 | syl5eq 2668 |
. . . . . . . 8
|
100 | 99 | oveq1d 6665 |
. . . . . . 7
|
101 | | neg1ne0 11126 |
. . . . . . . 8
|
102 | 89, 101 | dividi 10758 |
. . . . . . 7
|
103 | 100, 102 | syl6eq 2672 |
. . . . . 6
|
104 | 70, 103 | syl5eq 2668 |
. . . . 5
|
105 | 68, 104 | eqtrd 2656 |
. . . 4
|
106 | | subcl 10280 |
. . . . . 6
|
107 | 51, 52, 106 | sylancl 694 |
. . . . 5
|
108 | | efeq1 24275 |
. . . . 5
|
109 | 107, 108 | syl 17 |
. . . 4
|
110 | 105, 109 | mpbid 222 |
. . 3
|
111 | 66, 110 | eqeltrrd 2702 |
. 2
|
112 | 11 | a1i 11 |
. . . . 5
|
113 | 12 | a1i 11 |
. . . . 5
|
114 | 51, 112, 113 | divcld 10801 |
. . . 4
|
115 | 5 | a1i 11 |
. . . 4
|
116 | 9 | a1i 11 |
. . . 4
|
117 | 114, 115,
116 | divcan1d 10802 |
. . 3
|
118 | 59 | oveq1i 6660 |
. . . . . 6
|
119 | 114, 115,
116 | divcld 10801 |
. . . . . . 7
|
120 | | halfre 11246 |
. . . . . . . 8
|
121 | 120 | recni 10052 |
. . . . . . 7
|
122 | | npcan 10290 |
. . . . . . 7
|
123 | 119, 121,
122 | sylancl 694 |
. . . . . 6
|
124 | 118, 123 | syl5eq 2668 |
. . . . 5
|
125 | 111 | zred 11482 |
. . . . . 6
|
126 | | readdcl 10019 |
. . . . . 6
|
127 | 125, 120,
126 | sylancl 694 |
. . . . 5
|
128 | 124, 127 | eqeltrrd 2702 |
. . . 4
|
129 | | remulcl 10021 |
. . . 4
|
130 | 128, 4, 129 | sylancl 694 |
. . 3
|
131 | 117, 130 | eqeltrrd 2702 |
. 2
|
132 | 111, 131 | jca 554 |
1
|