Step | Hyp | Ref
| Expression |
1 | | df-nqqs 7268 |
. 2
|
2 | | addpipqqs 7290 |
. 2
|
3 | | mulpipqqs 7293 |
. . 3
|
4 | | mulclpi 7248 |
. . . . . . 7
|
5 | | simpl 108 |
. . . . . . . 8
|
6 | | mulclpi 7248 |
. . . . . . . 8
|
7 | 5, 6 | jca 304 |
. . . . . . 7
|
8 | 4, 7 | anim12i 336 |
. . . . . 6
|
9 | | an12 551 |
. . . . . . 7
|
10 | | 3anass 967 |
. . . . . . 7
|
11 | 9, 10 | bitr4i 186 |
. . . . . 6
|
12 | 8, 11 | sylib 121 |
. . . . 5
|
13 | 12 | an4s 578 |
. . . 4
|
14 | | mulcanenqec 7306 |
. . . 4
|
15 | 13, 14 | syl 14 |
. . 3
|
16 | 3, 15 | eqtr4d 2193 |
. 2
|
17 | | mulpipqqs 7293 |
. 2
|
18 | | mulpipqqs 7293 |
. 2
|
19 | | addpipqqs 7290 |
. 2
|
20 | | mulclpi 7248 |
. . . . 5
|
21 | | mulclpi 7248 |
. . . . 5
|
22 | | addclpi 7247 |
. . . . 5
|
23 | 20, 21, 22 | syl2an 287 |
. . . 4
|
24 | 23 | an42s 579 |
. . 3
|
25 | | mulclpi 7248 |
. . . 4
|
26 | 25 | ad2ant2l 500 |
. . 3
|
27 | 24, 26 | jca 304 |
. 2
|
28 | | mulclpi 7248 |
. . . 4
|
29 | | mulclpi 7248 |
. . . 4
|
30 | 28, 29 | anim12i 336 |
. . 3
|
31 | 30 | an4s 578 |
. 2
|
32 | | mulclpi 7248 |
. . . 4
|
33 | | mulclpi 7248 |
. . . 4
|
34 | 32, 33 | anim12i 336 |
. . 3
|
35 | 34 | an4s 578 |
. 2
|
36 | | an42 577 |
. . . . 5
|
37 | 36 | anbi2i 453 |
. . . 4
|
38 | | 3anass 967 |
. . . 4
|
39 | | 3anass 967 |
. . . 4
|
40 | 37, 38, 39 | 3bitr4i 211 |
. . 3
|
41 | | mulclpi 7248 |
. . . . . 6
|
42 | 41 | ancoms 266 |
. . . . 5
|
43 | | distrpig 7253 |
. . . . 5
|
44 | 42, 20, 21, 43 | syl3an 1262 |
. . . 4
|
45 | | simp1r 1007 |
. . . . 5
|
46 | | simp1l 1006 |
. . . . 5
|
47 | 20 | 3ad2ant2 1004 |
. . . . . 6
|
48 | 21 | 3ad2ant3 1005 |
. . . . . 6
|
49 | 47, 48, 22 | syl2anc 409 |
. . . . 5
|
50 | | mulasspig 7252 |
. . . . 5
|
51 | 45, 46, 49, 50 | syl3anc 1220 |
. . . 4
|
52 | | mulcompig 7251 |
. . . . . . . . 9
|
53 | 52 | oveq1d 5839 |
. . . . . . . 8
|
54 | 53 | adantr 274 |
. . . . . . 7
|
55 | | simpll 519 |
. . . . . . . 8
|
56 | | simplr 520 |
. . . . . . . 8
|
57 | | simprl 521 |
. . . . . . . 8
|
58 | | mulcompig 7251 |
. . . . . . . . 9
|
59 | 58 | adantl 275 |
. . . . . . . 8
|
60 | | mulasspig 7252 |
. . . . . . . . 9
|
61 | 60 | adantl 275 |
. . . . . . . 8
|
62 | | simprr 522 |
. . . . . . . 8
|
63 | | mulclpi 7248 |
. . . . . . . . 9
|
64 | 63 | adantl 275 |
. . . . . . . 8
|
65 | 55, 56, 57, 59, 61, 62, 64 | caov4d 6005 |
. . . . . . 7
|
66 | 54, 65 | eqtr3d 2192 |
. . . . . 6
|
67 | 66 | 3adant3 1002 |
. . . . 5
|
68 | | simplr 520 |
. . . . . . 7
|
69 | | simpll 519 |
. . . . . . 7
|
70 | | simprl 521 |
. . . . . . 7
|
71 | 58 | adantl 275 |
. . . . . . 7
|
72 | 60 | adantl 275 |
. . . . . . 7
|
73 | | simprr 522 |
. . . . . . 7
|
74 | 63 | adantl 275 |
. . . . . . 7
|
75 | 68, 69, 70, 71, 72, 73, 74 | caov4d 6005 |
. . . . . 6
|
76 | 75 | 3adant2 1001 |
. . . . 5
|
77 | 67, 76 | oveq12d 5842 |
. . . 4
|
78 | 44, 51, 77 | 3eqtr3d 2198 |
. . 3
|
79 | 40, 78 | sylbir 134 |
. 2
|
80 | 70 | 3adant2 1001 |
. . . . . 6
|
81 | 62 | 3adant3 1002 |
. . . . . 6
|
82 | 80, 81, 25 | syl2anc 409 |
. . . . 5
|
83 | | mulasspig 7252 |
. . . . 5
|
84 | 45, 45, 82, 83 | syl3anc 1220 |
. . . 4
|
85 | 58 | adantl 275 |
. . . . 5
|
86 | 60 | adantl 275 |
. . . . 5
|
87 | 63 | adantl 275 |
. . . . 5
|
88 | 45, 45, 80, 85, 86, 81, 87 | caov4d 6005 |
. . . 4
|
89 | 84, 88 | eqtr3d 2192 |
. . 3
|
90 | 40, 89 | sylbir 134 |
. 2
|
91 | 1, 2, 16, 17, 18, 19, 27, 31, 35, 79, 90 | ecovidi 6592 |
1
|