Step | Hyp | Ref
| Expression |
1 | | elq 8557 |
. . . 4
|
2 | 1 | biimpi 113 |
. . 3
|
3 | 2 | adantl 262 |
. 2
|
4 | | simplll 485 |
. . . . . 6
|
5 | | elq 8557 |
. . . . . 6
|
6 | 4, 5 | sylib 127 |
. . . . 5
|
7 | | simplrl 487 |
. . . . . . . . . . . . 13
|
8 | 7 | zcnd 8361 |
. . . . . . . . . . . 12
|
9 | | simprl 483 |
. . . . . . . . . . . . . . . 16
|
10 | 9 | ad3antrrr 461 |
. . . . . . . . . . . . . . 15
|
11 | 10 | zcnd 8361 |
. . . . . . . . . . . . . 14
|
12 | | simprr 484 |
. . . . . . . . . . . . . . . 16
|
13 | 12 | ad3antrrr 461 |
. . . . . . . . . . . . . . 15
|
14 | 13 | nncnd 7928 |
. . . . . . . . . . . . . 14
|
15 | | nnap0 7943 |
. . . . . . . . . . . . . . 15
# |
16 | 13, 15 | syl 14 |
. . . . . . . . . . . . . 14
# |
17 | 11, 14, 16 | divclapd 7765 |
. . . . . . . . . . . . 13
|
18 | | simplrr 488 |
. . . . . . . . . . . . . 14
|
19 | 18 | nncnd 7928 |
. . . . . . . . . . . . 13
|
20 | 17, 19 | mulcld 7047 |
. . . . . . . . . . . 12
|
21 | | nnap0 7943 |
. . . . . . . . . . . . . 14
# |
22 | 18, 21 | syl 14 |
. . . . . . . . . . . . 13
# |
23 | 19, 22 | recclapd 7757 |
. . . . . . . . . . . 12
|
24 | 19, 22 | recap0d 7758 |
. . . . . . . . . . . 12
# |
25 | | apmul1 7764 |
. . . . . . . . . . . 12
# # # |
26 | 8, 20, 23, 24, 25 | syl112anc 1139 |
. . . . . . . . . . 11
#
# |
27 | 8, 19, 22 | divrecapd 7768 |
. . . . . . . . . . . . 13
|
28 | 27 | eqcomd 2045 |
. . . . . . . . . . . 12
|
29 | 17, 19, 23 | mulassd 7050 |
. . . . . . . . . . . . 13
|
30 | 19, 22 | recidapd 7759 |
. . . . . . . . . . . . . 14
|
31 | 30 | oveq2d 5528 |
. . . . . . . . . . . . 13
|
32 | 17 | mulid1d 7044 |
. . . . . . . . . . . . 13
|
33 | 29, 31, 32 | 3eqtrd 2076 |
. . . . . . . . . . . 12
|
34 | 28, 33 | breq12d 3777 |
. . . . . . . . . . 11
#
# |
35 | 26, 34 | bitrd 177 |
. . . . . . . . . 10
#
# |
36 | 13 | nnzd 8359 |
. . . . . . . . . . . . . . 15
|
37 | 7, 36 | zmulcld 8366 |
. . . . . . . . . . . . . 14
|
38 | 37 | zcnd 8361 |
. . . . . . . . . . . . 13
|
39 | 18 | nnzd 8359 |
. . . . . . . . . . . . . . 15
|
40 | 39, 10 | zmulcld 8366 |
. . . . . . . . . . . . . 14
|
41 | 40 | zcnd 8361 |
. . . . . . . . . . . . 13
|
42 | 14, 16 | recclapd 7757 |
. . . . . . . . . . . . 13
|
43 | 14, 16 | recap0d 7758 |
. . . . . . . . . . . . 13
# |
44 | | apmul1 7764 |
. . . . . . . . . . . . 13
# # # |
45 | 38, 41, 42, 43, 44 | syl112anc 1139 |
. . . . . . . . . . . 12
#
# |
46 | 8, 14, 42 | mulassd 7050 |
. . . . . . . . . . . . . 14
|
47 | 14, 16 | recidapd 7759 |
. . . . . . . . . . . . . . 15
|
48 | 47 | oveq2d 5528 |
. . . . . . . . . . . . . 14
|
49 | 8 | mulid1d 7044 |
. . . . . . . . . . . . . 14
|
50 | 46, 48, 49 | 3eqtrd 2076 |
. . . . . . . . . . . . 13
|
51 | 50 | breq1d 3774 |
. . . . . . . . . . . 12
#
# |
52 | 45, 51 | bitrd 177 |
. . . . . . . . . . 11
#
# |
53 | 19, 11, 42 | mulassd 7050 |
. . . . . . . . . . . . 13
|
54 | 11, 14, 16 | divrecapd 7768 |
. . . . . . . . . . . . . 14
|
55 | 54 | oveq2d 5528 |
. . . . . . . . . . . . 13
|
56 | 19, 17 | mulcomd 7048 |
. . . . . . . . . . . . 13
|
57 | 53, 55, 56 | 3eqtr2d 2078 |
. . . . . . . . . . . 12
|
58 | 57 | breq2d 3776 |
. . . . . . . . . . 11
#
# |
59 | 52, 58 | bitrd 177 |
. . . . . . . . . 10
#
# |
60 | | simpr 103 |
. . . . . . . . . . 11
|
61 | | simpllr 486 |
. . . . . . . . . . 11
|
62 | 60, 61 | breq12d 3777 |
. . . . . . . . . 10
#
# |
63 | 35, 59, 62 | 3bitr4d 209 |
. . . . . . . . 9
#
# |
64 | | zapne 8315 |
. . . . . . . . . 10
# |
65 | 37, 40, 64 | syl2anc 391 |
. . . . . . . . 9
#
|
66 | 63, 65 | bitr3d 179 |
. . . . . . . 8
#
|
67 | 63 | notbid 592 |
. . . . . . . . . 10
#
# |
68 | | apti 7613 |
. . . . . . . . . . 11
# |
69 | 38, 41, 68 | syl2anc 391 |
. . . . . . . . . 10
# |
70 | | qcn 8569 |
. . . . . . . . . . . . 13
|
71 | 70 | ad2antrr 457 |
. . . . . . . . . . . 12
|
72 | 71 | ad3antrrr 461 |
. . . . . . . . . . 11
|
73 | 61, 17 | eqeltrd 2114 |
. . . . . . . . . . 11
|
74 | | apti 7613 |
. . . . . . . . . . 11
# |
75 | 72, 73, 74 | syl2anc 391 |
. . . . . . . . . 10
# |
76 | 67, 69, 75 | 3bitr4d 209 |
. . . . . . . . 9
|
77 | 76 | necon3bid 2246 |
. . . . . . . 8
|
78 | 66, 77 | bitrd 177 |
. . . . . . 7
#
|
79 | 78 | ex 108 |
. . . . . 6
#
|
80 | 79 | rexlimdvva 2440 |
. . . . 5
#
|
81 | 6, 80 | mpd 13 |
. . . 4
#
|
82 | 81 | ex 108 |
. . 3
# |
83 | 82 | rexlimdvva 2440 |
. 2
# |
84 | 3, 83 | mpd 13 |
1
#
|