Step | Hyp | Ref
| Expression |
1 | | oveq1 6657 |
. . . . . . . . . . 11
|
2 | | oveq2 6658 |
. . . . . . . . . . 11
|
3 | 1, 2 | oveq12d 6668 |
. . . . . . . . . 10
|
4 | | fveq2 6191 |
. . . . . . . . . . 11
|
5 | 4 | oveq2d 6666 |
. . . . . . . . . 10
|
6 | 3, 5 | breq12d 4666 |
. . . . . . . . 9
|
7 | 6 | cbvralv 3171 |
. . . . . . . 8
|
8 | | nnre 11027 |
. . . . . . . . . . . . . 14
|
9 | | 1re 10039 |
. . . . . . . . . . . . . 14
|
10 | | lelttric 10144 |
. . . . . . . . . . . . . 14
|
11 | 8, 9, 10 | sylancl 694 |
. . . . . . . . . . . . 13
|
12 | 11 | ancli 574 |
. . . . . . . . . . . 12
|
13 | | andi 911 |
. . . . . . . . . . . 12
|
14 | 12, 13 | sylib 208 |
. . . . . . . . . . 11
|
15 | | nnge1 11046 |
. . . . . . . . . . . . . . . 16
|
16 | | letri3 10123 |
. . . . . . . . . . . . . . . . . . 19
|
17 | 8, 9, 16 | sylancl 694 |
. . . . . . . . . . . . . . . . . 18
|
18 | 17 | biimpar 502 |
. . . . . . . . . . . . . . . . 17
|
19 | 18 | anassrs 680 |
. . . . . . . . . . . . . . . 16
|
20 | 15, 19 | mpidan 704 |
. . . . . . . . . . . . . . 15
|
21 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
|
22 | | 1m1e0 11089 |
. . . . . . . . . . . . . . . 16
|
23 | 21, 22 | syl6eq 2672 |
. . . . . . . . . . . . . . 15
|
24 | 20, 23 | syl 17 |
. . . . . . . . . . . . . 14
|
25 | | faclbnd4lem3 13082 |
. . . . . . . . . . . . . 14
|
26 | 24, 25 | sylan2 491 |
. . . . . . . . . . . . 13
|
27 | 26 | a1d 25 |
. . . . . . . . . . . 12
|
28 | | 1nn 11031 |
. . . . . . . . . . . . . . . 16
|
29 | | nnsub 11059 |
. . . . . . . . . . . . . . . 16
|
30 | 28, 29 | mpan 706 |
. . . . . . . . . . . . . . 15
|
31 | 30 | biimpa 501 |
. . . . . . . . . . . . . 14
|
32 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
|
33 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
|
34 | 32, 33 | oveq12d 6668 |
. . . . . . . . . . . . . . . 16
|
35 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
36 | 35 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
|
37 | 34, 36 | breq12d 4666 |
. . . . . . . . . . . . . . 15
|
38 | 37 | rspcv 3305 |
. . . . . . . . . . . . . 14
|
39 | 31, 38 | syl 17 |
. . . . . . . . . . . . 13
|
40 | 39 | adantl 482 |
. . . . . . . . . . . 12
|
41 | 27, 40 | jaodan 826 |
. . . . . . . . . . 11
|
42 | 14, 41 | sylan2 491 |
. . . . . . . . . 10
|
43 | | faclbnd4lem2 13081 |
. . . . . . . . . . 11
|
44 | 43 | 3expa 1265 |
. . . . . . . . . 10
|
45 | 42, 44 | syld 47 |
. . . . . . . . 9
|
46 | 45 | ralrimdva 2969 |
. . . . . . . 8
|
47 | 7, 46 | syl5bi 232 |
. . . . . . 7
|
48 | 47 | expcom 451 |
. . . . . 6
|
49 | 48 | a2d 29 |
. . . . 5
|
50 | | nnnn0 11299 |
. . . . . . . 8
|
51 | | faclbnd3 13079 |
. . . . . . . 8
|
52 | 50, 51 | sylan2 491 |
. . . . . . 7
|
53 | | nncn 11028 |
. . . . . . . . . . 11
|
54 | 53 | exp0d 13002 |
. . . . . . . . . 10
|
55 | 54 | oveq1d 6665 |
. . . . . . . . 9
|
56 | 55 | adantl 482 |
. . . . . . . 8
|
57 | | nn0cn 11302 |
. . . . . . . . . 10
|
58 | | expcl 12878 |
. . . . . . . . . 10
|
59 | 57, 50, 58 | syl2an 494 |
. . . . . . . . 9
|
60 | 59 | mulid2d 10058 |
. . . . . . . 8
|
61 | 56, 60 | eqtrd 2656 |
. . . . . . 7
|
62 | | sq0 12955 |
. . . . . . . . . . . . . 14
|
63 | 62 | oveq2i 6661 |
. . . . . . . . . . . . 13
|
64 | | 2cn 11091 |
. . . . . . . . . . . . . 14
|
65 | | exp0 12864 |
. . . . . . . . . . . . . 14
|
66 | 64, 65 | ax-mp 5 |
. . . . . . . . . . . . 13
|
67 | 63, 66 | eqtri 2644 |
. . . . . . . . . . . 12
|
68 | 67 | a1i 11 |
. . . . . . . . . . 11
|
69 | 57 | addid1d 10236 |
. . . . . . . . . . . 12
|
70 | 69 | oveq2d 6666 |
. . . . . . . . . . 11
|
71 | 68, 70 | oveq12d 6668 |
. . . . . . . . . 10
|
72 | | expcl 12878 |
. . . . . . . . . . . 12
|
73 | 57, 72 | mpancom 703 |
. . . . . . . . . . 11
|
74 | 73 | mulid2d 10058 |
. . . . . . . . . 10
|
75 | 71, 74 | eqtrd 2656 |
. . . . . . . . 9
|
76 | 75 | oveq1d 6665 |
. . . . . . . 8
|
77 | 76 | adantr 481 |
. . . . . . 7
|
78 | 52, 61, 77 | 3brtr4d 4685 |
. . . . . 6
|
79 | 78 | ralrimiva 2966 |
. . . . 5
|
80 | | oveq2 6658 |
. . . . . . . . 9
|
81 | 80 | oveq1d 6665 |
. . . . . . . 8
|
82 | | oveq1 6657 |
. . . . . . . . . . 11
|
83 | 82 | oveq2d 6666 |
. . . . . . . . . 10
|
84 | | oveq2 6658 |
. . . . . . . . . . 11
|
85 | 84 | oveq2d 6666 |
. . . . . . . . . 10
|
86 | 83, 85 | oveq12d 6668 |
. . . . . . . . 9
|
87 | 86 | oveq1d 6665 |
. . . . . . . 8
|
88 | 81, 87 | breq12d 4666 |
. . . . . . 7
|
89 | 88 | ralbidv 2986 |
. . . . . 6
|
90 | 89 | imbi2d 330 |
. . . . 5
|
91 | | oveq2 6658 |
. . . . . . . . 9
|
92 | 91 | oveq1d 6665 |
. . . . . . . 8
|
93 | | oveq1 6657 |
. . . . . . . . . . 11
|
94 | 93 | oveq2d 6666 |
. . . . . . . . . 10
|
95 | | oveq2 6658 |
. . . . . . . . . . 11
|
96 | 95 | oveq2d 6666 |
. . . . . . . . . 10
|
97 | 94, 96 | oveq12d 6668 |
. . . . . . . . 9
|
98 | 97 | oveq1d 6665 |
. . . . . . . 8
|
99 | 92, 98 | breq12d 4666 |
. . . . . . 7
|
100 | 99 | ralbidv 2986 |
. . . . . 6
|
101 | 100 | imbi2d 330 |
. . . . 5
|
102 | | oveq2 6658 |
. . . . . . . . 9
|
103 | 102 | oveq1d 6665 |
. . . . . . . 8
|
104 | | oveq1 6657 |
. . . . . . . . . . 11
|
105 | 104 | oveq2d 6666 |
. . . . . . . . . 10
|
106 | | oveq2 6658 |
. . . . . . . . . . 11
|
107 | 106 | oveq2d 6666 |
. . . . . . . . . 10
|
108 | 105, 107 | oveq12d 6668 |
. . . . . . . . 9
|
109 | 108 | oveq1d 6665 |
. . . . . . . 8
|
110 | 103, 109 | breq12d 4666 |
. . . . . . 7
|
111 | 110 | ralbidv 2986 |
. . . . . 6
|
112 | 111 | imbi2d 330 |
. . . . 5
|
113 | | oveq2 6658 |
. . . . . . . . 9
|
114 | 113 | oveq1d 6665 |
. . . . . . . 8
|
115 | | oveq1 6657 |
. . . . . . . . . . 11
|
116 | 115 | oveq2d 6666 |
. . . . . . . . . 10
|
117 | | oveq2 6658 |
. . . . . . . . . . 11
|
118 | 117 | oveq2d 6666 |
. . . . . . . . . 10
|
119 | 116, 118 | oveq12d 6668 |
. . . . . . . . 9
|
120 | 119 | oveq1d 6665 |
. . . . . . . 8
|
121 | 114, 120 | breq12d 4666 |
. . . . . . 7
|
122 | 121 | ralbidv 2986 |
. . . . . 6
|
123 | 122 | imbi2d 330 |
. . . . 5
|
124 | 49, 79, 90, 101, 112, 123 | nn0indALT 11473 |
. . . 4
|
125 | 124 | imp 445 |
. . 3
|
126 | | oveq1 6657 |
. . . . . 6
|
127 | | oveq2 6658 |
. . . . . 6
|
128 | 126, 127 | oveq12d 6668 |
. . . . 5
|
129 | | fveq2 6191 |
. . . . . 6
|
130 | 129 | oveq2d 6666 |
. . . . 5
|
131 | 128, 130 | breq12d 4666 |
. . . 4
|
132 | 131 | rspcva 3307 |
. . 3
|
133 | 125, 132 | sylan2 491 |
. 2
|
134 | 133 | 3impb 1260 |
1
|