Step | Hyp | Ref
| Expression |
1 | | ax-1cn 7069 |
. . . . . 6
|
2 | | 1ap0 7690 |
. . . . . 6
# |
3 | 1, 2 | div0api 7834 |
. . . . 5
|
4 | | 0z 8362 |
. . . . . 6
|
5 | | 1nn 8050 |
. . . . . 6
|
6 | | znq 8709 |
. . . . . 6
|
7 | 4, 5, 6 | mp2an 416 |
. . . . 5
|
8 | 3, 7 | eqeltrri 2152 |
. . . 4
|
9 | | qapne 8724 |
. . . 4
# |
10 | 8, 9 | mpan2 415 |
. . 3
#
|
11 | 10 | biimpar 291 |
. 2
# |
12 | | elq 8707 |
. . . 4
|
13 | | nnne0 8067 |
. . . . . . . 8
|
14 | 13 | ancli 316 |
. . . . . . 7
|
15 | | nnz 8370 |
. . . . . . . . . . . . . . . 16
|
16 | | zapne 8422 |
. . . . . . . . . . . . . . . 16
# |
17 | 15, 4, 16 | sylancl 404 |
. . . . . . . . . . . . . . 15
#
|
18 | 17 | adantl 271 |
. . . . . . . . . . . . . 14
# |
19 | 18 | pm5.32i 441 |
. . . . . . . . . . . . 13
# |
20 | 19 | anbi1i 445 |
. . . . . . . . . . . 12
#
|
21 | | breq1 3788 |
. . . . . . . . . . . . 13
#
# |
22 | | zcn 8356 |
. . . . . . . . . . . . . . . 16
|
23 | | nncn 8047 |
. . . . . . . . . . . . . . . 16
|
24 | 22, 23 | anim12i 331 |
. . . . . . . . . . . . . . 15
|
25 | | divap0b 7771 |
. . . . . . . . . . . . . . . 16
# #
# |
26 | 25 | 3expa 1138 |
. . . . . . . . . . . . . . 15
# # # |
27 | 24, 26 | sylan 277 |
. . . . . . . . . . . . . 14
# # # |
28 | 27 | bicomd 139 |
. . . . . . . . . . . . 13
# # # |
29 | 21, 28 | sylan9bbr 450 |
. . . . . . . . . . . 12
# # # |
30 | 20, 29 | sylbir 133 |
. . . . . . . . . . 11
# # |
31 | | simplll 499 |
. . . . . . . . . . . 12
|
32 | | zapne 8422 |
. . . . . . . . . . . 12
# |
33 | 31, 4, 32 | sylancl 404 |
. . . . . . . . . . 11
# |
34 | 30, 33 | bitrd 186 |
. . . . . . . . . 10
# |
35 | | zmulcl 8404 |
. . . . . . . . . . . . . . . . 17
|
36 | 15, 35 | sylan2 280 |
. . . . . . . . . . . . . . . 16
|
37 | 36 | adantr 270 |
. . . . . . . . . . . . . . 15
|
38 | | msqznn 8447 |
. . . . . . . . . . . . . . . 16
|
39 | 38 | adantlr 460 |
. . . . . . . . . . . . . . 15
|
40 | 37, 39 | jca 300 |
. . . . . . . . . . . . . 14
|
41 | 40 | adantlr 460 |
. . . . . . . . . . . . 13
|
42 | 41 | adantlr 460 |
. . . . . . . . . . . 12
|
43 | 20 | anbi1i 445 |
. . . . . . . . . . . . . 14
# #
# |
44 | 33 | pm5.32i 441 |
. . . . . . . . . . . . . 14
#
|
45 | 43, 44 | bitri 182 |
. . . . . . . . . . . . 13
# #
|
46 | | oveq2 5540 |
. . . . . . . . . . . . . . 15
|
47 | | dividap 7789 |
. . . . . . . . . . . . . . . . . . . . 21
# |
48 | 47 | adantr 270 |
. . . . . . . . . . . . . . . . . . . 20
# # |
49 | 48 | oveq1d 5547 |
. . . . . . . . . . . . . . . . . . 19
# # |
50 | | simpll 495 |
. . . . . . . . . . . . . . . . . . . 20
# # |
51 | | simpl 107 |
. . . . . . . . . . . . . . . . . . . 20
# # # |
52 | | simpr 108 |
. . . . . . . . . . . . . . . . . . . 20
# # # |
53 | | divdivdivap 7801 |
. . . . . . . . . . . . . . . . . . . 20
# # # |
54 | 50, 51, 51, 52, 53 | syl22anc 1170 |
. . . . . . . . . . . . . . . . . . 19
# # |
55 | 49, 54 | eqtr3d 2115 |
. . . . . . . . . . . . . . . . . 18
# # |
56 | 55 | an4s 552 |
. . . . . . . . . . . . . . . . 17
# #
|
57 | 24, 56 | sylan 277 |
. . . . . . . . . . . . . . . 16
# #
|
58 | 57 | anass1rs 535 |
. . . . . . . . . . . . . . 15
# # |
59 | 46, 58 | sylan9eqr 2135 |
. . . . . . . . . . . . . 14
# # |
60 | 59 | an32s 532 |
. . . . . . . . . . . . 13
# # |
61 | 45, 60 | sylbir 133 |
. . . . . . . . . . . 12
|
62 | 42, 61 | jca 300 |
. . . . . . . . . . 11
|
63 | 62 | ex 113 |
. . . . . . . . . 10
|
64 | 34, 63 | sylbid 148 |
. . . . . . . . 9
# |
65 | 64 | ex 113 |
. . . . . . . 8
#
|
66 | 65 | anasss 391 |
. . . . . . 7
#
|
67 | 14, 66 | sylan2 280 |
. . . . . 6
# |
68 | | rspceov 5567 |
. . . . . . . 8
|
69 | 68 | 3expa 1138 |
. . . . . . 7
|
70 | | elq 8707 |
. . . . . . 7
|
71 | 69, 70 | sylibr 132 |
. . . . . 6
|
72 | 67, 71 | syl8 70 |
. . . . 5
# |
73 | 72 | rexlimivv 2482 |
. . . 4
#
|
74 | 12, 73 | sylbi 119 |
. . 3
#
|
75 | 74 | imp 122 |
. 2
# |
76 | 11, 75 | syldan 276 |
1
|