Step | Hyp | Ref
| Expression |
1 | | ax-1cn 7846 |
. . . . . 6
|
2 | | 1ap0 8488 |
. . . . . 6
# |
3 | 1, 2 | div0api 8642 |
. . . . 5
|
4 | | 0z 9202 |
. . . . . 6
|
5 | | 1nn 8868 |
. . . . . 6
|
6 | | znq 9562 |
. . . . . 6
|
7 | 4, 5, 6 | mp2an 423 |
. . . . 5
|
8 | 3, 7 | eqeltrri 2240 |
. . . 4
|
9 | | qapne 9577 |
. . . 4
# |
10 | 8, 9 | mpan2 422 |
. . 3
#
|
11 | 10 | biimpar 295 |
. 2
# |
12 | | elq 9560 |
. . . 4
|
13 | | nnne0 8885 |
. . . . . . . 8
|
14 | 13 | ancli 321 |
. . . . . . 7
|
15 | | nnz 9210 |
. . . . . . . . . . . . . . . 16
|
16 | | zapne 9265 |
. . . . . . . . . . . . . . . 16
# |
17 | 15, 4, 16 | sylancl 410 |
. . . . . . . . . . . . . . 15
#
|
18 | 17 | adantl 275 |
. . . . . . . . . . . . . 14
# |
19 | 18 | pm5.32i 450 |
. . . . . . . . . . . . 13
# |
20 | 19 | anbi1i 454 |
. . . . . . . . . . . 12
#
|
21 | | breq1 3985 |
. . . . . . . . . . . . 13
#
# |
22 | | zcn 9196 |
. . . . . . . . . . . . . . . 16
|
23 | | nncn 8865 |
. . . . . . . . . . . . . . . 16
|
24 | 22, 23 | anim12i 336 |
. . . . . . . . . . . . . . 15
|
25 | | divap0b 8579 |
. . . . . . . . . . . . . . . 16
# #
# |
26 | 25 | 3expa 1193 |
. . . . . . . . . . . . . . 15
# # # |
27 | 24, 26 | sylan 281 |
. . . . . . . . . . . . . 14
# # # |
28 | 27 | bicomd 140 |
. . . . . . . . . . . . 13
# # # |
29 | 21, 28 | sylan9bbr 459 |
. . . . . . . . . . . 12
# # # |
30 | 20, 29 | sylbir 134 |
. . . . . . . . . . 11
# # |
31 | | simplll 523 |
. . . . . . . . . . . 12
|
32 | | zapne 9265 |
. . . . . . . . . . . 12
# |
33 | 31, 4, 32 | sylancl 410 |
. . . . . . . . . . 11
# |
34 | 30, 33 | bitrd 187 |
. . . . . . . . . 10
# |
35 | | zmulcl 9244 |
. . . . . . . . . . . . . . . . 17
|
36 | 15, 35 | sylan2 284 |
. . . . . . . . . . . . . . . 16
|
37 | 36 | adantr 274 |
. . . . . . . . . . . . . . 15
|
38 | | msqznn 9291 |
. . . . . . . . . . . . . . . 16
|
39 | 38 | adantlr 469 |
. . . . . . . . . . . . . . 15
|
40 | 37, 39 | jca 304 |
. . . . . . . . . . . . . 14
|
41 | 40 | adantlr 469 |
. . . . . . . . . . . . 13
|
42 | 41 | adantlr 469 |
. . . . . . . . . . . 12
|
43 | 20 | anbi1i 454 |
. . . . . . . . . . . . . 14
# #
# |
44 | 33 | pm5.32i 450 |
. . . . . . . . . . . . . 14
#
|
45 | 43, 44 | bitri 183 |
. . . . . . . . . . . . 13
# #
|
46 | | oveq2 5850 |
. . . . . . . . . . . . . . 15
|
47 | | dividap 8597 |
. . . . . . . . . . . . . . . . . . . . 21
# |
48 | 47 | adantr 274 |
. . . . . . . . . . . . . . . . . . . 20
# # |
49 | 48 | oveq1d 5857 |
. . . . . . . . . . . . . . . . . . 19
# # |
50 | | simpll 519 |
. . . . . . . . . . . . . . . . . . . 20
# # |
51 | | simpl 108 |
. . . . . . . . . . . . . . . . . . . 20
# # # |
52 | | simpr 109 |
. . . . . . . . . . . . . . . . . . . 20
# # # |
53 | | divdivdivap 8609 |
. . . . . . . . . . . . . . . . . . . 20
# # # |
54 | 50, 51, 51, 52, 53 | syl22anc 1229 |
. . . . . . . . . . . . . . . . . . 19
# # |
55 | 49, 54 | eqtr3d 2200 |
. . . . . . . . . . . . . . . . . 18
# # |
56 | 55 | an4s 578 |
. . . . . . . . . . . . . . . . 17
# #
|
57 | 24, 56 | sylan 281 |
. . . . . . . . . . . . . . . 16
# #
|
58 | 57 | anass1rs 561 |
. . . . . . . . . . . . . . 15
# # |
59 | 46, 58 | sylan9eqr 2221 |
. . . . . . . . . . . . . 14
# # |
60 | 59 | an32s 558 |
. . . . . . . . . . . . 13
# # |
61 | 45, 60 | sylbir 134 |
. . . . . . . . . . . 12
|
62 | 42, 61 | jca 304 |
. . . . . . . . . . 11
|
63 | 62 | ex 114 |
. . . . . . . . . 10
|
64 | 34, 63 | sylbid 149 |
. . . . . . . . 9
# |
65 | 64 | ex 114 |
. . . . . . . 8
#
|
66 | 65 | anasss 397 |
. . . . . . 7
#
|
67 | 14, 66 | sylan2 284 |
. . . . . 6
# |
68 | | rspceov 5884 |
. . . . . . . 8
|
69 | 68 | 3expa 1193 |
. . . . . . 7
|
70 | | elq 9560 |
. . . . . . 7
|
71 | 69, 70 | sylibr 133 |
. . . . . 6
|
72 | 67, 71 | syl8 71 |
. . . . 5
# |
73 | 72 | rexlimivv 2589 |
. . . 4
#
|
74 | 12, 73 | sylbi 120 |
. . 3
#
|
75 | 74 | imp 123 |
. 2
# |
76 | 11, 75 | syldan 280 |
1
|