Step | Hyp | Ref
| Expression |
1 | | nnnn0 9097 |
. . . . . . . 8
|
2 | | nnne0 8861 |
. . . . . . . 8
|
3 | 1, 2 | jca 304 |
. . . . . . 7
|
4 | | df-ne 2328 |
. . . . . . . . . . . 12
|
5 | 4 | anbi2i 453 |
. . . . . . . . . . 11
|
6 | | divalg2 11816 |
. . . . . . . . . . . . . . . . . . 19
|
7 | | breq1 3968 |
. . . . . . . . . . . . . . . . . . . . 21
|
8 | | oveq2 5832 |
. . . . . . . . . . . . . . . . . . . . . 22
|
9 | 8 | breq2d 3977 |
. . . . . . . . . . . . . . . . . . . . 21
|
10 | 7, 9 | anbi12d 465 |
. . . . . . . . . . . . . . . . . . . 20
|
11 | 10 | reu4 2906 |
. . . . . . . . . . . . . . . . . . 19
|
12 | 6, 11 | sylib 121 |
. . . . . . . . . . . . . . . . . 18
|
13 | | nngt0 8858 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
14 | 13 | 3ad2ant2 1004 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
15 | | zcn 9172 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
16 | 15 | subid1d 8175 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
17 | 16 | breq2d 3977 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
18 | 17 | biimpar 295 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
19 | 18 | 3adant2 1001 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
20 | 14, 19 | jca 304 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
21 | 20 | 3expa 1185 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
22 | 21 | anim2i 340 |
. . . . . . . . . . . . . . . . . . . . . 22
|
23 | 22 | ancoms 266 |
. . . . . . . . . . . . . . . . . . . . 21
|
24 | | 0nn0 9105 |
. . . . . . . . . . . . . . . . . . . . . 22
|
25 | | breq1 3968 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
26 | | oveq2 5832 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
27 | 26 | breq2d 3977 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
28 | 25, 27 | anbi12d 465 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
29 | 28 | anbi2d 460 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
30 | | eqeq2 2167 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
31 | 29, 30 | imbi12d 233 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
32 | 31 | rspcv 2812 |
. . . . . . . . . . . . . . . . . . . . . 22
|
33 | 24, 32 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
|
34 | 23, 33 | syl5 32 |
. . . . . . . . . . . . . . . . . . . 20
|
35 | 34 | expd 256 |
. . . . . . . . . . . . . . . . . . 19
|
36 | 35 | ralimi 2520 |
. . . . . . . . . . . . . . . . . 18
|
37 | 12, 36 | simpl2im 384 |
. . . . . . . . . . . . . . . . 17
|
38 | | r19.21v 2534 |
. . . . . . . . . . . . . . . . 17
|
39 | 37, 38 | sylib 121 |
. . . . . . . . . . . . . . . 16
|
40 | 39 | expd 256 |
. . . . . . . . . . . . . . 15
|
41 | 40 | pm2.43i 49 |
. . . . . . . . . . . . . 14
|
42 | 41 | 3impia 1182 |
. . . . . . . . . . . . 13
|
43 | | breq1 3968 |
. . . . . . . . . . . . . . . 16
|
44 | | oveq2 5832 |
. . . . . . . . . . . . . . . . 17
|
45 | 44 | breq2d 3977 |
. . . . . . . . . . . . . . . 16
|
46 | 43, 45 | anbi12d 465 |
. . . . . . . . . . . . . . 15
|
47 | | eqeq1 2164 |
. . . . . . . . . . . . . . 15
|
48 | 46, 47 | imbi12d 233 |
. . . . . . . . . . . . . 14
|
49 | 48 | rspcv 2812 |
. . . . . . . . . . . . 13
|
50 | 42, 49 | syl5com 29 |
. . . . . . . . . . . 12
|
51 | | pm3.37 679 |
. . . . . . . . . . . 12
|
52 | 50, 51 | syl6 33 |
. . . . . . . . . . 11
|
53 | 5, 52 | syl7bi 164 |
. . . . . . . . . 10
|
54 | 53 | exp4a 364 |
. . . . . . . . 9
|
55 | 54 | com23 78 |
. . . . . . . 8
|
56 | 55 | imp4a 347 |
. . . . . . 7
|
57 | 3, 56 | syl7 69 |
. . . . . 6
|
58 | 57 | com23 78 |
. . . . 5
|
59 | 58 | impd 252 |
. . . 4
|
60 | 59 | 3expia 1187 |
. . 3
|
61 | 60 | com23 78 |
. 2
|
62 | 61 | 3impia 1182 |
1
|